Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Apply nat_inv with x0, add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H2: x0 = 0.
Apply H2 with λ x2 x3 . add_nat x3 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).
Apply add_nat_0L with x1, λ x2 x3 . x3 = 0 ⟶ and (x0 = 0) (x1 = 0) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: x1 = 0.
Apply andI with x0 = 0, x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H2: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).
Apply H2 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).
Let x2 of type ι be given.
Assume H3: (λ x3 . and (nat_p x3) (x0 = ordsucc x3)) x2.
Apply H3 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).
Assume H4: nat_p x2.
Assume H5: x0 = ordsucc x2.
Apply H5 with λ x3 x4 . add_nat x4 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).
Apply add_nat_SL with x2, x1, λ x3 x4 . x4 = 0 ⟶ and (x0 = 0) (x1 = 0) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Assume H6: ordsucc (add_nat x2 x1) = 0.
Apply FalseE with and (x0 = 0) (x1 = 0).
Apply neq_ordsucc_0 with add_nat x2 x1.
The subproof is completed by applying H6.
■