Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNoCutP x0 x1.
Assume H1: ∀ x2 . x2 ∈ x0 ⟶ minus_SNo (minus_SNo x2) = x2.
Assume H2: ∀ x2 . x2 ∈ x1 ⟶ minus_SNo (minus_SNo x2) = x2.
Assume H3: ∀ x2 . x2 ∈ x0 ⟶ SNo x2.
Assume H4: ∀ x2 . x2 ∈ x1 ⟶ SNo x2.
Assume H5: SNo (SNoCut x0 x1).
Assume H6: SNo (minus_SNo (minus_SNo (SNoCut x0 x1))).
Assume H7: and (SNoLev (SNoCut x0 x1) ⊆ SNoLev (minus_SNo (minus_SNo (SNoCut x0 x1)))) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) (minus_SNo (minus_SNo (SNoCut x0 x1)))).
Apply H7 with minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1.
Assume H8: SNoLev (SNoCut x0 x1) ⊆ SNoLev (minus_SNo (minus_SNo (SNoCut x0 x1))).
Assume H9: SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) (minus_SNo (minus_SNo (SNoCut x0 x1))).
Apply minus_SNo_invol with SNoCut x0 x1.
Apply SNoCutP_SNo_SNoCut with x0, x1.
The subproof is completed by applying H0.
■