Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_ind with λ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x1 x3)) ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x2 x3)) ⟶ x1 (ordsucc x0) = x1 0 ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNoLe (add_SNo (x1 (ordsucc x3)) (minus_SNo (x1 x3))) (x2 x3)) ⟶ SNoLe 0 (finite_add_SNo (ordsucc x0) x2) leaving 2 subgoals.
Let x0 of type ι → ι be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ 1 ⟶ SNo (x0 x2).
Assume H1: ∀ x2 . x2 ∈ 1 ⟶ SNo (x1 x2).
Assume H2: x0 1 = x0 0.
Assume H3: ∀ x2 . x2 ∈ 1 ⟶ SNoLe (add_SNo (x0 (ordsucc x2)) (minus_SNo (x0 x2))) (x1 x2).
Claim L4: add_SNo (x0 1) (minus_SNo (x0 0)) = 0
Apply H2 with λ x2 x3 . add_SNo x3 (minus_SNo (x0 0)) = 0.
Apply add_SNo_minus_SNo_rinv with x0 0.
Apply H0 with 0.
The subproof is completed by applying In_0_1.
Apply unknownprop_69faeba9a75f2f8d58865148c9f0f7e35d3ac66d15111e3cc3404d6a2eed4dcd with x1, 0, λ x2 x3 . SNoLe 0 x3 leaving 2 subgoals.
The subproof is completed by applying nat_0.
Apply unknownprop_4376a6c44e07ee63cfd63de35739aa1967e60551544bcab6d1b8284e5b2ad2ba with x1, λ x2 x3 . SNoLe 0 (add_SNo x3 (x1 0)).
Apply add_SNo_0L with x1 0, λ x2 x3 . SNoLe 0 x3 leaving 2 subgoals.
Apply H1 with 0.
The subproof is completed by applying In_0_1.
Apply L4 with λ x2 x3 . SNoLe x2 (x1 0).
Apply H3 with 0.
The subproof is completed by applying In_0_1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x1 x3)) ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x2 x3)) ⟶ x1 (ordsucc x0) = x1 0 ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNoLe (add_SNo (x1 (ordsucc x3)) (minus_SNo (x1 x3))) (x2 x3)) ⟶ SNoLe 0 (finite_add_SNo (ordsucc x0) x2).
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H2: ∀ x3 . x3 ∈ ordsucc (ordsucc x0) ⟶ SNo (x1 x3).
Assume H3: ∀ x3 . x3 ∈ ordsucc (ordsucc x0) ⟶ SNo (x2 x3).
Assume H4: x1 (ordsucc (ordsucc x0)) = x1 0.
Assume H5: ∀ x3 . x3 ∈ ordsucc (ordsucc x0) ⟶ SNoLe (add_SNo (x1 (ordsucc x3)) (minus_SNo (x1 x3))) (x2 x3).
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply unknownprop_69faeba9a75f2f8d58865148c9f0f7e35d3ac66d15111e3cc3404d6a2eed4dcd with x2, ordsucc x0, λ x3 x4 . SNoLe 0 x4 leaving 2 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply unknownprop_69faeba9a75f2f8d58865148c9f0f7e35d3ac66d15111e3cc3404d6a2eed4dcd with x2, x0, λ x3 x4 . SNoLe 0 (add_SNo x4 (x2 (ordsucc x0))) leaving 2 subgoals.
The subproof is completed by applying H0.
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Apply add_SNo_assoc with finite_add_SNo x0 x2, x2 x0, x2 (ordsucc x0), λ x3 x4 . SNoLe 0 x3 leaving 4 subgoals.
Apply unknownprop_814c004451946f1c9f980b657692a7768a826c8b8434cb9bb69b9f9613c2c671 with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Apply L20 with λ x3 x4 . SNoLe 0 (add_SNo (finite_add_SNo x0 ...) ...).
...
■