Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Assume H0:
nat_p
x1
.
Apply unknownprop_cb22f23c255b11e2fef1f0187745d1c6297e541a75b408830b470617abac132a with
x0
,
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x1
)
)
)
)
)
)
)
,
λ x2 x3 .
x3
=
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
leaving 2 subgoals.
Apply unknownprop_1a52e19bf4045e8e446a298da7dba8c076ee67253cdcf7b15e893847906b7879 with
x1
.
The subproof is completed by applying H0.
Apply unknownprop_cb22f23c255b11e2fef1f0187745d1c6297e541a75b408830b470617abac132a with
x0
,
x1
,
λ x2 x3 .
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x3
)
)
)
)
)
)
)
=
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type
ι
→
ι
→
ο
be given.
Assume H1:
x2
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
.
The subproof is completed by applying H1.
■