Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind with λ x0 . ∀ x1 x2 . SNoCutP x1 x2 ⟶ x0 = SNoCut x1 x2 ⟶ minus_SNo x0 = SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1}.
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x2 x3 . SNoCutP x2 x3 ⟶ x1 = SNoCut x2 x3 ⟶ minus_SNo x1 = SNoCut {minus_SNo x4|x4 ∈ x3} {minus_SNo x4|x4 ∈ x2}.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: SNoCutP x1 x2.
Apply H2 with x0 = SNoCut x1 x2 ⟶ minus_SNo x0 = SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1}.
Assume H3: and (∀ x3 . x3 ∈ x1 ⟶ SNo x3) (∀ x3 . x3 ∈ x2 ⟶ SNo x3).
Apply H3 with (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x2 ⟶ SNoLt x3 x4) ⟶ x0 = SNoCut x1 x2 ⟶ minus_SNo x0 = SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1}.
Assume H4: ∀ x3 . x3 ∈ x1 ⟶ SNo x3.
Assume H5: ∀ x3 . x3 ∈ x2 ⟶ SNo x3.
Assume H6: ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x2 ⟶ SNoLt x3 x4.
Assume H7: x0 = SNoCut x1 x2.
Claim L8: ...
...
Claim L9: ...
...
Apply SNoCutP_SNoCut_impred with {minus_SNo x3|x3 ∈ x2}, {minus_SNo x3|x3 ∈ x1}, minus_SNo x0 = SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1} leaving 2 subgoals.
The subproof is completed by applying L9.
Assume H10: SNo (SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1}).
Assume H11: SNoLev (SNoCut {minus_SNo x3|x3 ∈ x2} {minus_SNo x3|x3 ∈ x1}) ∈ ordsucc (binunion (famunion {minus_SNo x3|x3 ∈ x2} (λ x3 . ordsucc (SNoLev x3))) (famunion {minus_SNo x3|x3 ∈ x1} (λ x3 . ordsucc (SNoLev x3)))).
Assume H12: ∀ x3 . x3 ∈ {minus_SNo x4|x4 ∈ x2} ⟶ SNoLt x3 (SNoCut {minus_SNo x4|x4 ∈ x2} {minus_SNo x4|x4 ∈ x1}).
Assume H13: ∀ x3 . x3 ∈ {minus_SNo x4|x4 ∈ x1} ⟶ SNoLt (SNoCut {minus_SNo x4|x4 ∈ x2} {minus_SNo x4|x4 ∈ x1}) x3.
Assume H14: ∀ x3 . ... ⟶ ... ⟶ ... ⟶ and (SNoLev (SNoCut {minus_SNo x4|x4 ∈ x2} {minus_SNo x4|x4 ∈ x1}) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut {minus_SNo x4|x4 ∈ x2} {minus_SNo x4|x4 ∈ x1})) (SNoCut {minus_SNo x4|x4 ∈ x2} {...|x4 ∈ x1}) ...).
...
■