Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ and (and (and (SNo (minus_SNo x1)) (∀ x2 . x2 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2))) (∀ x2 . x2 ∈ SNoR x1 ⟶ SNoLt (minus_SNo x2) (minus_SNo x1))) (SNoCutP (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo)).
Assume H2: ∀ x1 . x1 ∈ SNoL x0 ⟶ and (and (SNo (minus_SNo x1)) (∀ x2 . x2 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2))) (∀ x2 . x2 ∈ SNoR x1 ⟶ SNoLt (minus_SNo x2) (minus_SNo x1)).
Assume H3: SNoCutP (prim5 (SNoR x0) minus_SNo) (prim5 (SNoL x0) minus_SNo).
Apply and4I with SNo (minus_SNo x0), ∀ x1 . x1 ∈ SNoL x0 ⟶ SNoLt (minus_SNo x0) (minus_SNo x1), ∀ x1 . x1 ∈ SNoR x0 ⟶ SNoLt (minus_SNo x1) (minus_SNo x0), SNoCutP (prim5 (SNoR x0) minus_SNo) (prim5 (SNoL x0) minus_SNo) leaving 4 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H4: x1 ∈ SNoL x0.
Apply SNoL_E with x0, x1, SNoLt (minus_SNo x0) (minus_SNo x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H5: SNo x1.
Assume H6: SNoLev x1 ∈ SNoLev x0.
Assume H7: SNoLt x1 x0.
Apply minus_SNo_Lt_contra with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
Let x1 of type ι be given.
Assume H4: x1 ∈ SNoR x0.
Apply SNoR_E with x0, x1, SNoLt (minus_SNo x1) (minus_SNo x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H5: SNo x1.
Assume H6: SNoLev x1 ∈ SNoLev x0.
Assume H7: SNoLt x0 x1.
Apply minus_SNo_Lt_contra with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
■