Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Apply nat_ind with λ x1 . add_SNo (minus_SNo x0) x1 ∈ int_alt1 leaving 2 subgoals.
Apply add_SNo_0R with minus_SNo x0, λ x1 x2 . x2 ∈ int_alt1 leaving 2 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying L3.
Apply unknownprop_a66fb27a7b2af57722c6537d3983b55a12cc28475f1d8b8d9bdb1d857010e7af with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H4: nat_p x1.
Assume H5: add_SNo (minus_SNo x0) x1 ∈ int_alt1.
Claim L6: ...
...
Claim L7: ...
...
Apply ordinal_ordsucc_SNo_eq with x1, λ x2 x3 . add_SNo (minus_SNo x0) x3 ∈ int_alt1 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply add_SNo_com_3_0_1 with minus_SNo x0, 1, x1, λ x2 x3 . x3 ∈ int_alt1 leaving 4 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L7.
Claim L8: ∀ x2 . x2 ∈ omega ⟶ add_SNo (minus_SNo x0) x1 = x2 ⟶ add_SNo 1 (add_SNo (minus_SNo x0) x1) ∈ int_alt1
Let x2 of type ι be given.
Assume H8: x2 ∈ omega.
Assume H9: add_SNo (minus_SNo x0) x1 = x2.
Apply H9 with λ x3 x4 . add_SNo 1 x4 ∈ int_alt1.
Apply ordinal_ordsucc_SNo_eq with x2, λ x3 x4 . x3 ∈ int_alt1 leaving 2 subgoals.
Apply nat_p_ordinal with ....
...
...
Claim L9: ∀ x2 . x2 ∈ omega ⟶ add_SNo (minus_SNo x0) x1 = minus_SNo x2 ⟶ add_SNo 1 (add_SNo (minus_SNo x0) x1) ∈ int_alt1
Let x2 of type ι be given.
Assume H9: x2 ∈ omega.
Assume H10: add_SNo (minus_SNo x0) x1 = minus_SNo x2.
Apply H10 with λ x3 x4 . add_SNo 1 x4 ∈ int_alt1.
Apply nat_inv with x2, add_SNo 1 (minus_SNo x2) ∈ int_alt1 leaving 3 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H9.
Assume H11: x2 = 0.
Apply H11 with λ x3 x4 . add_SNo 1 (minus_SNo x4) ∈ int_alt1.
Apply minus_SNo_0 with λ x3 x4 . add_SNo 1 x4 ∈ int_alt1.
Apply add_SNo_0R with 1, λ x3 x4 . x4 ∈ int_alt1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with 1.
Apply nat_p_omega with 1.
The subproof is completed by applying nat_1.
Assume H11: ∃ x3 . and (nat_p x3) (x2 = ordsucc x3).
Apply H11 with add_SNo 1 (minus_SNo x2) ∈ int_alt1.
Let x3 of type ι be given.
Assume H12: (λ x4 . and (nat_p x4) (x2 = ordsucc x4)) x3.
Apply H12 with add_SNo 1 (minus_SNo x2) ∈ int_alt1.
Assume H13: nat_p x3.
Assume H14: x2 = ordsucc x3.
Apply H14 with λ x4 x5 . add_SNo 1 (minus_SNo x5) ∈ int_alt1.
Apply ordinal_ordsucc_SNo_eq with x3, λ x4 x5 . add_SNo 1 (minus_SNo x5) ∈ int_alt1 leaving 2 subgoals.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H13.
Apply minus_add_SNo_distr with 1, x3, λ x4 x5 . add_SNo 1 x5 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply ordinal_SNo with x3.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H13.
Apply add_SNo_minus_SNo_prop2 with 1, minus_SNo x3, λ x4 x5 . x5 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply SNo_minus_SNo with x3.
Apply ordinal_SNo with x3.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H13.
Apply unknownprop_a66fb27a7b2af57722c6537d3983b55a12cc28475f1d8b8d9bdb1d857010e7af with x3.
Apply nat_p_omega with x3.
The subproof is completed by applying H13.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with λ x2 . add_SNo (minus_SNo x0) x1 = x2 ⟶ add_SNo 1 (add_SNo (minus_SNo x0) x1) ∈ int_alt1, add_SNo (minus_SNo x0) x1 leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying H5.
Let x2 of type ι → ι → ο be given.
Assume H10: x2 (add_SNo (minus_SNo x0) x1) (add_SNo (minus_SNo x0) x1).
The subproof is completed by applying H10.
■