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_ae47a38e201daae59edf8724f290c3473f31a249345a4fe6f394ae507b501f4b with
x0
,
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x1
)
)
)
,
λ x2 x3 .
x3
=
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
leaving 2 subgoals.
Apply unknownprop_5e2628df9f5f85e18b5435fd3c0ad09162064b9312de3fdc10d248bc12486c0b with
x1
.
The subproof is completed by applying H0.
Apply unknownprop_ae47a38e201daae59edf8724f290c3473f31a249345a4fe6f394ae507b501f4b with
x0
,
x1
,
λ x2 x3 .
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
x3
)
)
)
=
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
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
ordsucc
(
add_nat
x0
x1
)
)
)
)
)
)
)
)
)
.
The subproof is completed by applying H1.
■