Search for blocks/addresses/...

Proofgold Proof

pf
Apply ordinal_ind with λ x0 . ∀ x1 . x1SNoS_ x0SNoLev (minus_SNo x1)SNoLev x1.
Let x0 of type ι be given.
Assume H0: ordinal x0.
Apply H0 with (∀ x1 . x1x0∀ x2 . x2SNoS_ x1SNoLev (minus_SNo x2)SNoLev x2)∀ x1 . x1SNoS_ x0SNoLev (minus_SNo x1)SNoLev x1.
Assume H1: TransSet x0.
Assume H2: ∀ x1 . x1x0TransSet x1.
Assume H3: ∀ x1 . x1x0∀ x2 . x2SNoS_ x1SNoLev (minus_SNo x2)SNoLev x2.
Let x1 of type ι be given.
Assume H4: x1SNoS_ x0.
Apply SNoS_E2 with x0, x1, SNoLev (minus_SNo x1)SNoLev x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H5: SNoLev x1x0.
Assume H6: ordinal (SNoLev x1).
Assume H7: SNo x1.
Assume H8: SNo_ (SNoLev x1) x1.
Claim L9: ...
...
Apply minus_SNo_eq with x1, λ x2 x3 . SNoLev x3SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply SNoCutP_SNoCut_impred with {minus_SNo x2|x2 ∈ SNoR x1}, {minus_SNo x2|x2 ∈ SNoL x1}, SNoLev (SNoCut {minus_SNo x2|x2 ∈ SNoR x1} {minus_SNo x2|x2 ∈ SNoL x1})SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying L9.
Assume H10: SNo (SNoCut {minus_SNo x2|x2 ∈ SNoR x1} {minus_SNo x2|x2 ∈ SNoL x1}).
Assume H11: SNoLev (SNoCut {minus_SNo x2|x2 ∈ SNoR x1} {minus_SNo x2|x2 ∈ SNoL x1})ordsucc (binunion (famunion {minus_SNo x2|x2 ∈ SNoR x1} (λ x2 . ordsucc (SNoLev x2))) (famunion {minus_SNo x2|x2 ∈ SNoL x1} (λ x2 . ordsucc (SNoLev x2)))).
Assume H12: ∀ x2 . x2prim5 (SNoR x1) minus_SNoSNoLt x2 (SNoCut (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo)).
Assume H13: ∀ x2 . x2prim5 (SNoL x1) minus_SNoSNoLt (SNoCut (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo)) x2.
Assume H14: ∀ x2 . ...(∀ x3 . x3prim5 (SNoR x1) minus_SNoSNoLt x3 x2)(∀ x3 . x3prim5 (SNoL x1) minus_SNoSNoLt x2 x3)and (SNoLev (SNoCut (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo))SNoLev x2) (SNoEq_ (SNoLev (SNoCut (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo))) (SNoCut (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo)) x2).
...