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: SNoLev x1 ∈ ordsucc (SNoLev x0).
Assume H3: SNoLt x1 (SNo_extend1 x0).
Apply SNoLtLe_or with x0, x1, SNoLe x1 x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H4: SNoLt x0 x1.
Apply FalseE with SNoLe x1 x0.
Apply SNoLtE with x0, x1, False leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H5: SNo x2.
Assume H6: SNoLev x2 ∈ binintersect (SNoLev x0) (SNoLev x1).
Assume H7: SNoEq_ (SNoLev x2) x2 x0.
Assume H8: SNoEq_ (SNoLev x2) x2 x1.
Assume H9: SNoLt x0 x2.
Assume H10: SNoLt x2 x1.
Assume H11: nIn (SNoLev x2) x0.
Assume H12: SNoLev x2 ∈ x1.
Apply SNoLt_irref with x2.
Apply SNoLt_tra with x2, x1, x2 leaving 5 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
The subproof is completed by applying H10.
Apply SNoLt_tra with x1, SNo_extend1 x0, x2 leaving 5 subgoals.
The subproof is completed by applying H1.
Apply SNo_extend1_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
Claim L13: SNoLev x2 ∈ SNoLev x0
Apply binintersectE1 with SNoLev x0, SNoLev x1, SNoLev x2.
The subproof is completed by applying H6.
Apply SNoLtI3 with SNo_extend1 x0, x2 leaving 3 subgoals.
Apply SNo_extend1_SNoLev with x0, λ x3 x4 . SNoLev x2 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccI1 with SNoLev x0, SNoLev x2.
The subproof is completed by applying L13.
Apply SNoEq_tra_ with SNoLev x2, SNo_extend1 x0, x0, x2 leaving 2 subgoals.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x2, SNo_extend1 x0, x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L13.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
Apply SNoEq_sym_ with SNoLev x2, x2, x0.
The subproof is completed by applying H7.
Assume H14: SNoLev x2 ∈ SNo_extend1 x0.
Apply H11.
Apply SNoEq_E1 with SNoLev x0, SNo_extend1 x0, x0, SNoLev x2 leaving 3 subgoals.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying L13.
The subproof is completed by applying H14.
Assume H5: SNoLev x0 ∈ SNoLev x1.
Apply FalseE with SNoEq_ (SNoLev x0) x0 x1 ⟶ SNoLev x0 ∈ x1 ⟶ False.
Apply ordsuccE with SNoLev x0, SNoLev x1, False leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H6: SNoLev x1 ∈ SNoLev x0.
Apply In_no2cycle with SNoLev x1, SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Assume H6: SNoLev x1 = SNoLev x0.
Apply In_irref with SNoLev x1.
Apply H6 with λ x2 x3 . x3 ∈ SNoLev x1.
The subproof is completed by applying H5.
Assume H5: SNoLev x1 ∈ SNoLev x0.
Assume H6: SNoEq_ (SNoLev x1) x0 x1.
Assume H7: nIn (SNoLev x1) x0.
Apply SNoLt_irref with x1.
Apply SNoLt_tra with x1, SNo_extend1 x0, x1 leaving 5 subgoals.
The subproof is completed by applying H1.
Apply SNo_extend1_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply SNoLtI3 with SNo_extend1 x0, x1 leaving 3 subgoals.
Apply SNo_extend1_SNoLev with x0, λ x2 x3 . SNoLev x1 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccI1 with SNoLev x0, SNoLev x1.
The subproof is completed by applying H5.
Apply SNoEq_tra_ with SNoLev x1, SNo_extend1 x0, x0, x1 leaving 2 subgoals.
Apply SNoEq_antimon_ with SNoLev x0, SNoLev x1, SNo_extend1 x0, x0 leaving 3 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
Assume H8: SNoLev x1 ∈ SNo_extend1 x0.
Apply H7.
Apply SNoEq_E1 with SNoLev x0, SNo_extend1 x0, x0, SNoLev x1 leaving 3 subgoals.
Apply SNo_extend1_SNoEq with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Assume H4: SNoLe x1 x0.
The subproof is completed by applying H4.
■