Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Claim L1: ...
...
Claim L2: ...
...
Apply SNoCutP_SNoCut with SNoL x0, SNoR x0, x0 = SNoCut (SNoL x0) (SNoR x0) leaving 2 subgoals.
The subproof is completed by applying L2.
Assume H3: and (and (and (SNo (SNoCut (SNoL x0) (SNoR x0))) (SNoLev (SNoCut (SNoL x0) (SNoR x0))ordsucc (binunion (famunion (SNoL x0) (λ x1 . ordsucc (SNoLev x1))) (famunion (SNoR x0) (λ x1 . ordsucc (SNoLev x1)))))) (∀ x1 . x1SNoL x0SNoLt x1 (SNoCut (SNoL x0) (SNoR x0)))) (∀ x1 . x1SNoR x0SNoLt (SNoCut (SNoL x0) (SNoR x0)) x1).
Apply H3 with (∀ x1 . SNo x1(∀ x2 . x2SNoL x0SNoLt x2 x1)(∀ x2 . x2SNoR x0SNoLt x1 x2)and (SNoLev (SNoCut (SNoL x0) (SNoR x0))SNoLev x1) (SNoEq_ (SNoLev (SNoCut (SNoL x0) (SNoR x0))) (SNoCut (SNoL x0) (SNoR x0)) x1))x0 = SNoCut (SNoL x0) (SNoR x0).
Assume H4: and (and (SNo (SNoCut (SNoL x0) (SNoR x0))) (SNoLev (SNoCut (SNoL x0) (SNoR x0))ordsucc (binunion (famunion (SNoL x0) (λ x1 . ordsucc (SNoLev x1))) (famunion (SNoR x0) (λ x1 . ordsucc (SNoLev x1)))))) (∀ x1 . x1SNoL x0SNoLt x1 (SNoCut (SNoL x0) (SNoR x0))).
Apply H4 with (∀ x1 . x1SNoR x0SNoLt (SNoCut (SNoL x0) (SNoR x0)) x1)(∀ x1 . SNo x1(∀ x2 . x2SNoL x0SNoLt x2 x1)(∀ x2 . x2SNoR x0SNoLt x1 x2)and (SNoLev (SNoCut (SNoL x0) (SNoR x0))SNoLev x1) (SNoEq_ (SNoLev (SNoCut (SNoL x0) (SNoR x0))) (SNoCut (SNoL x0) (SNoR x0)) x1))x0 = SNoCut (SNoL x0) (SNoR x0).
Assume H5: and (SNo (SNoCut (SNoL x0) (SNoR x0))) (SNoLev (SNoCut (SNoL x0) (SNoR x0))ordsucc (binunion (famunion (SNoL x0) (λ x1 . ordsucc (SNoLev x1))) (famunion (SNoR x0) (λ x1 . ordsucc (SNoLev x1))))).
Apply H5 with .........x0 = SNoCut (SNoL ...) ....
...