Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Apply ordinal_ind with λ x1 . add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1).
Let x1 of type ι be given.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . x2x1add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Apply SNoCutP_SNoCut with binunion {add_SNo x2 x1|x2 ∈ SNoS_ (ordsucc x0)} {add_SNo (ordsucc x0) x2|x2 ∈ SNoS_ x1}, 0, add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1) leaving 2 subgoals.
Apply add_SNo_ordinal_SNoCutP with ordsucc x0, x1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H1.
Assume H9: and (and (and (SNo (SNoCut (binunion {add_SNo x2 x1|x2 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0)) (SNoLev (SNoCut (binunion {add_SNo x2 x1|x2 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0)ordsucc (binunion (famunion (binunion {add_SNo x2 x1|x2 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) (λ x2 . ordsucc (SNoLev x2))) (famunion 0 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))SNoLt x2 (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0))) (∀ x2 . x20SNoLt (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0) x2).
Apply H9 with (∀ x2 . ...(∀ x3 . x3binunion {...|x4 ∈ SNoS_ (ordsucc ...)} ...SNoLt x3 x2)(∀ x3 . x30SNoLt x2 x3)and (SNoLev (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0)SNoLev x2) (SNoEq_ (SNoLev (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0)) (SNoCut (binunion {add_SNo x3 x1|x3 ∈ SNoS_ (ordsucc x0)} (prim5 (SNoS_ x1) (add_SNo (ordsucc x0)))) 0) x2))add_SNo (ordsucc x0) x1 = ordsucc (add_SNo x0 x1).
...