Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNoLt x0 x1.
Let x2 of type ο be given.
Assume H3: ∀ x3 . x3 ∈ SNoL x1 ⟶ x3 ∈ SNoR x0 ⟶ x2.
Assume H4: x0 ∈ SNoL x1 ⟶ x2.
Assume H5: x1 ∈ SNoR x0 ⟶ x2.
Apply SNoLtE with x0, x1, x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H6: SNo x3.
Assume H7: SNoLev x3 ∈ binintersect (SNoLev x0) (SNoLev x1).
Assume H8: SNoEq_ (SNoLev x3) x3 x0.
Assume H9: SNoEq_ (SNoLev x3) x3 x1.
Assume H10: SNoLt x0 x3.
Assume H11: SNoLt x3 x1.
Assume H12: nIn (SNoLev x3) x0.
Assume H13: SNoLev x3 ∈ x1.
Apply binintersectE with SNoLev x0, SNoLev x1, SNoLev x3, x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H14: SNoLev x3 ∈ SNoLev x0.
Assume H15: SNoLev x3 ∈ SNoLev x1.
Apply H3 with x3 leaving 2 subgoals.
Apply SNoL_I with x1, x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H15.
The subproof is completed by applying H11.
Apply SNoR_I with x0, x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H14.
The subproof is completed by applying H10.
Assume H6: SNoLev x0 ∈ SNoLev x1.
Assume H7: SNoEq_ (SNoLev x0) x0 x1.
Assume H8: SNoLev x0 ∈ x1.
Apply H4.
Apply SNoL_I with x1, x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Assume H6: SNoLev x1 ∈ SNoLev x0.
Assume H7: SNoEq_ (SNoLev x1) x0 x1.
Assume H8: nIn (SNoLev x1) x0.
Apply H5.
Apply SNoR_I with x0, x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
■