Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 .
ordinal
x1
⟶
SNo
x1
⟶
add_SNo
x0
(
ordsucc
x1
)
=
ordsucc
(
add_SNo
x0
x1
)
.
Claim L1:
ordinal
0
The subproof is completed by applying ordinal_Empty.
Claim L2:
not
(
SNo
0
⟶
add_SNo
(
minus_SNo
1
)
1
=
ordsucc
(
add_SNo
(
minus_SNo
1
)
0
)
)
Apply add_SNo_minus_SNo_linv with
1
,
λ x0 x1 .
not
(
SNo
0
⟶
x1
=
ordsucc
(
add_SNo
(
minus_SNo
1
)
0
)
)
leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply add_SNo_0R with
minus_SNo
1
,
λ x0 x1 .
not
(
SNo
0
⟶
0
=
ordsucc
x1
)
leaving 2 subgoals.
Apply SNo_minus_SNo with
1
.
The subproof is completed by applying SNo_1.
Assume H2:
SNo
0
⟶
0
=
ordsucc
(
minus_SNo
1
)
.
Claim L3:
0
=
ordsucc
(
minus_SNo
1
)
⟶
∀ x0 : ο .
x0
Assume H3:
0
=
ordsucc
(
minus_SNo
1
)
.
Apply EmptyE with
minus_SNo
1
.
Apply H3 with
λ x0 x1 .
minus_SNo
1
∈
x1
.
The subproof is completed by applying ordsuccI2 with
minus_SNo
1
.
Apply L3.
Apply H2.
The subproof is completed by applying SNo_0.
Apply L2.
Apply H0 with
minus_SNo
1
,
0
.
The subproof is completed by applying L1.
■