Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Assume H0: x0 0.
Assume H1: ∀ x1 . nat_p x1x0 x1x0 (ordsucc x1).
Claim L2: and (nat_p 0) (x0 0)
Apply andI with nat_p 0, x0 0 leaving 2 subgoals.
The subproof is completed by applying nat_0.
The subproof is completed by applying H0.
Claim L3: ∀ x1 . and (nat_p x1) (x0 x1)and (nat_p (ordsucc x1)) (x0 (ordsucc x1))
Let x1 of type ι be given.
Assume H3: and (nat_p x1) (x0 x1).
Apply H3 with and (nat_p (ordsucc x1)) (x0 (ordsucc x1)).
Assume H4: nat_p x1.
Assume H5: x0 x1.
Apply andI with nat_p (ordsucc x1), x0 (ordsucc x1) leaving 2 subgoals.
Apply nat_ordsucc with x1.
The subproof is completed by applying H4.
Apply H1 with x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Assume H4: nat_p x1.
Claim L5: and (nat_p x1) (x0 x1)
Apply H4 with λ x2 . and (nat_p x2) (x0 x2) leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply andER with nat_p x1, x0 x1.
The subproof is completed by applying L5.