Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 x2 .
SNoLt
x1
x0
⟶
SNo_
x2
x1
⟶
ordinal
x2
⟶
SNo
x1
⟶
SNoLev
x1
=
x2
⟶
and
(
and
(
SNo
x1
)
(
SNoLev
x1
∈
SNoLev
x0
)
)
(
SNoLt
x1
x0
)
.
Claim L1:
SNoLt
(
minus_SNo
1
)
0
Apply minus_SNo_Lt_contra1 with
0
,
1
leaving 3 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
Apply minus_SNo_0 with
λ x0 x1 .
SNoLt
x1
1
.
The subproof is completed by applying SNoLt_0_1.
Claim L2:
ordinal
1
Apply nat_p_ordinal with
1
.
The subproof is completed by applying nat_1.
Claim L3:
SNo_
1
(
minus_SNo
1
)
Apply minus_SNo_SNo_ with
1
,
1
leaving 2 subgoals.
The subproof is completed by applying L2.
Apply ordinal_SNo_ with
1
.
The subproof is completed by applying L2.
Claim L4:
SNo
(
minus_SNo
1
)
Apply SNo_minus_SNo with
1
.
The subproof is completed by applying SNo_1.
Claim L5:
not
(
SNoLev
(
minus_SNo
1
)
=
1
⟶
and
(
and
(
SNo
(
minus_SNo
1
)
)
(
SNoLev
(
minus_SNo
1
)
∈
SNoLev
0
)
)
(
SNoLt
(
minus_SNo
1
)
0
)
)
Apply minus_SNo_Lev with
1
,
λ x0 x1 .
not
(
x1
=
1
⟶
and
(
and
(
SNo
(
minus_SNo
1
)
)
(
x1
∈
SNoLev
0
)
)
(
SNoLt
(
minus_SNo
1
)
0
)
)
leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply SNoLev_0 with
λ x0 x1 .
not
(
SNoLev
1
=
1
⟶
and
(
and
(
SNo
(
minus_SNo
1
)
)
(
SNoLev
1
∈
x1
)
)
(
SNoLt
(
minus_SNo
1
)
0
)
)
.
Apply ordinal_SNoLev with
1
,
λ x0 x1 .
not
(
x1
=
1
⟶
and
(
and
(
SNo
(
minus_SNo
1
)
)
(
x1
∈
0
)
)
(
SNoLt
(
minus_SNo
1
)
0
)
)
leaving 2 subgoals.
The subproof is completed by applying L2.
Assume H5:
1
=
1
⟶
and
(
and
(
SNo
(
minus_SNo
1
)
)
(
1
∈
0
)
)
(
SNoLt
(
minus_SNo
1
)
0
)
.
Apply H5 with
False
leaving 2 subgoals.
Let x0 of type
ι
→
ι
→
ο
be given.
Assume H6:
x0
1
1
.
The subproof is completed by applying H6.
Assume H6:
and
(
SNo
(
minus_SNo
1
)
)
(
1
∈
0
)
.
Assume H7:
SNoLt
(
minus_SNo
1
)
0
.
Apply H6 with
False
.
Assume H8:
SNo
(
minus_SNo
1
)
.
Assume H9:
1
∈
0
.
Apply EmptyE with
1
.
The subproof is completed by applying H9.
Apply L5.
Apply H0 with
0
,
minus_SNo
1
,
1
leaving 4 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
The subproof is completed by applying L2.
The subproof is completed by applying L4.
■