Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 .
ordinal
x0
⟶
SNo
x0
⟶
SNo
x1
⟶
ordinal
(
add_SNo
x0
x1
)
.
Claim L1:
ordinal
0
The subproof is completed by applying ordinal_Empty.
Claim L2:
SNo
0
The subproof is completed by applying SNo_0.
Claim L3:
not
(
SNo
(
minus_SNo
1
)
⟶
ordinal
(
add_SNo
0
(
minus_SNo
1
)
)
)
Apply add_SNo_0L with
minus_SNo
1
,
λ x0 x1 .
not
(
SNo
(
minus_SNo
1
)
⟶
ordinal
x1
)
leaving 2 subgoals.
Apply SNo_minus_SNo with
1
.
The subproof is completed by applying SNo_1.
Assume H3:
SNo
(
minus_SNo
1
)
⟶
ordinal
(
minus_SNo
1
)
.
Claim L4:
SNo
(
minus_SNo
1
)
Apply SNo_minus_SNo with
1
.
The subproof is completed by applying SNo_1.
Claim L5:
not
(
ordinal
(
minus_SNo
1
)
)
Assume H5:
ordinal
(
minus_SNo
1
)
.
Apply EmptyE with
minus_SNo
1
.
Apply ordinal_SNoLt_In with
minus_SNo
1
,
0
leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying ordinal_Empty.
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.
Apply L5.
Apply H3.
The subproof is completed by applying L4.
Apply L3.
Apply H0 with
0
,
minus_SNo
1
leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
■