Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
(
minus_SNo
x0
)
⟶
add_SNo
(
minus_SNo
x0
)
(
add_SNo
x0
x1
)
=
x1
⟶
x1
=
x2
.
Claim L1:
SNo
0
The subproof is completed by applying SNo_0.
Claim L2:
SNo
0
The subproof is completed by applying SNo_0.
Claim L3:
SNo
1
The subproof is completed by applying SNo_1.
Claim L4:
SNo
(
minus_SNo
0
)
Apply minus_SNo_0 with
λ x0 x1 .
SNo
x1
.
The subproof is completed by applying L1.
Claim L5:
not
(
add_SNo
(
minus_SNo
0
)
(
add_SNo
0
0
)
=
0
⟶
0
=
1
)
Assume H5:
add_SNo
(
minus_SNo
0
)
(
add_SNo
0
0
)
=
0
⟶
0
=
1
.
Apply neq_0_1.
Apply H5.
Apply add_SNo_minus_L2 with
0
,
0
leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply L5.
Apply H0 with
0
,
0
,
1
leaving 4 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■