Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNoCutP x0 x1.
Apply H0 with and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2x0SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2x1SNoLt (SNoCut x0 x1) x2)) (∀ x2 . SNo x2(∀ x3 . x3x0SNoLt x3 x2)(∀ x3 . x3x1SNoLt x2 x3)and (SNoLev (SNoCut x0 x1)SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2)).
Assume H1: and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2).
Apply H1 with (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2x0SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2x1SNoLt (SNoCut x0 x1) x2)) (∀ x2 . SNo x2(∀ x3 . x3x0SNoLt x3 x2)(∀ x3 . x3x1SNoLt x2 x3)and (SNoLev (SNoCut x0 x1)SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2)).
Assume H2: ∀ x2 . x2x0SNo x2.
Assume H3: ∀ x2 . x2x1SNo x2.
Assume H4: ∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3.
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Apply PNo_bd_pred with λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3x0), λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3x1), binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2))), and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x2 . ordsucc ...)) ...))) ...) ...) ... leaving 5 subgoals.
...
...
...
...
...