Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: SNo x1.
Assume H2: SNoLev x1x0.
Claim L3: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying H0.
Claim L4: SNoLev x0 = x0
Apply ordinal_SNoLev with x0.
The subproof is completed by applying H0.
Apply SNoLt_trichotomy_or with x1, x0, SNoLt x1 x0 leaving 4 subgoals.
The subproof is completed by applying H1.
Apply ordinal_SNo with x0.
The subproof is completed by applying H0.
Assume H5: or (SNoLt x1 x0) (x1 = x0).
Apply H5 with SNoLt x1 x0 leaving 2 subgoals.
Assume H6: SNoLt x1 x0.
The subproof is completed by applying H6.
Assume H6: x1 = x0.
Apply FalseE with SNoLt x1 x0.
Apply In_irref with x0.
Apply L4 with λ x2 x3 . x2x0.
Apply H6 with λ x2 x3 . SNoLev x2x0.
The subproof is completed by applying H2.
Assume H5: SNoLt x0 x1.
Apply FalseE with SNoLt x1 x0.
Apply SNoLtE with x0, x1, False leaving 6 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Apply L4 with λ x3 x4 . SNo x2SNoLev x2binintersect x4 (SNoLev x1)SNoEq_ (SNoLev x2) x2 x0SNoEq_ (SNoLev x2) x2 x1SNoLt x0 x2SNoLt x2 x1nIn (SNoLev x2) x0SNoLev x2x1False.
Assume H6: SNo x2.
Assume H7: SNoLev x2binintersect x0 (SNoLev x1).
Assume H8: SNoEq_ (SNoLev x2) x2 x0.
Assume H9: SNoEq_ (SNoLev x2) x2 x1.
Assume H10: SNoLt x0 x2.
Assume H11: SNoLt x2 x1.
Assume H12: nIn (SNoLev x2) x0.
Apply FalseE with SNoLev x2x1False.
Apply H12.
Apply binintersectE1 with x0, SNoLev x1, SNoLev x2.
The subproof is completed by applying H7.
Apply L4 with λ x2 x3 . x3SNoLev x1SNoEq_ x3 x0 x1x3x1False.
Assume H6: x0SNoLev x1.
Apply FalseE with SNoEq_ x0 x0 x1x0x1False.
Apply In_no2cycle with x0, SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Apply L4 with λ x2 x3 . SNoLev x1x3SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0False.
Assume H6: SNoLev x1x0.
Assume H7: SNoEq_ (SNoLev x1) x0 x1.
Assume H8: nIn (SNoLev x1) x0.
Apply H8.
The subproof is completed by applying H6.