Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Apply nat_ind with λ x1 . ∀ x2 . nat_p x2 ⟶ add_nat x0 x1 = ordsucc x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ add_nat x3 x4 ∈ x2 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: add_nat x0 0 = ordsucc x1.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Let x3 of type ι be given.
Assume H4: x3 ∈ 0.
Apply FalseE with add_nat x2 x3 ∈ x1.
Apply EmptyE with x3.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: ∀ x2 . nat_p x2 ⟶ add_nat x0 x1 = ordsucc x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ add_nat x3 x4 ∈ x2.
Apply nat_inv_impred with λ x2 . add_nat x0 (ordsucc x1) = ordsucc x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ ordsucc x1 ⟶ add_nat x3 x4 ∈ x2 leaving 2 subgoals.
Apply add_nat_SR with x0, x1, λ x2 x3 . x3 = 1 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ ordsucc x1 ⟶ add_nat x4 x5 ∈ 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: ordsucc (add_nat x0 x1) = 1.
Apply nat_inv_impred with λ x2 . add_nat x2 x1 = 0 ⟶ x2 = 0, x0, λ x2 x3 . ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ ordsucc x1 ⟶ add_nat x4 x5 ∈ 0 leaving 5 subgoals.
Assume H4: add_nat 0 x1 = 0.
Let x2 of type ι → ι → ο be given.
Assume H5: x2 0 0.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Assume H4: nat_p x2.
Apply add_nat_SL with x2, x1, λ x3 x4 . x4 = 0 ⟶ ordsucc x2 = 0 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Assume H5: ordsucc (add_nat x2 x1) = 0.
Apply FalseE with ordsucc x2 = 0.
Apply neq_ordsucc_0 with add_nat x2 x1.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
Apply ordsucc_inj with add_nat x0 x1, 0.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2 ∈ 0.
Apply FalseE with ∀ x3 . x3 ∈ ordsucc x1 ⟶ add_nat x2 x3 ∈ 0.
Apply EmptyE with x2.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H3: nat_p x2.
Apply add_nat_SR with x0, x1, λ x3 x4 . x4 = ordsucc (ordsucc x2) ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ ordsucc x1 ⟶ add_nat x5 x6 ∈ ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H4: ordsucc (add_nat x0 x1) = ordsucc (ordsucc x2).
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Let x4 of type ι be given.
Assume H6: x4 ∈ ordsucc x1.
Claim L7: ...
...
Apply ordsuccE with x1, x4, add_nat x3 x4 ∈ ordsucc x2 leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H8: x4 ∈ x1.
Apply ordsuccI1 with x2, add_nat x3 x4.
Apply H2 with x2, x3, ... leaving 4 subgoals.
...
...
...
...
...
■