Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0SNoS_ (ordsucc omega).
Assume H1: SNoLt x0 omega.
Apply SNoS_E2 with ordsucc omega, x0, ∃ x1 . and (x1omega) (SNoLt x0 x1) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Assume H2: SNoLev x0ordsucc omega.
Assume H3: ordinal (SNoLev x0).
Assume H4: SNo x0.
Assume H5: SNo_ (SNoLev x0) x0.
Apply SNoLtE with x0, omega, ∃ x1 . and (x1omega) (SNoLt x0 x1) leaving 6 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H6: SNo x1.
Assume H7: SNoLev x1binintersect (SNoLev x0) (SNoLev omega).
Assume H8: SNoEq_ (SNoLev x1) x1 x0.
Assume H9: SNoEq_ (SNoLev x1) x1 omega.
Assume H10: SNoLt x0 x1.
Assume H11: SNoLt x1 omega.
Assume H12: nIn (SNoLev x1) x0.
Assume H13: SNoLev x1omega.
Let x2 of type ο be given.
Assume H14: ∀ x3 . and (x3omega) (SNoLt x0 x3)x2.
Apply H14 with SNoLev x1.
Apply andI with SNoLev x1omega, SNoLt x0 (SNoLev x1) leaving 2 subgoals.
The subproof is completed by applying H13.
Apply SNoLtLe_tra with x0, x1, SNoLev x1 leaving 5 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Apply ordinal_SNo with SNoLev x1.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply ordinal_SNoLev_max_2 with SNoLev x1, x1 leaving 3 subgoals.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H6.
The subproof is completed by applying H6.
The subproof is completed by applying ordsuccI2 with SNoLev x1.
Assume H6: SNoLev x0SNoLev omega.
Assume H7: SNoEq_ (SNoLev x0) x0 omega.
Assume H8: SNoLev x0omega.
Let x1 of type ο be given.
Assume H9: ∀ x2 . and (x2omega) (SNoLt x0 x2)x1.
Apply H9 with ordsucc (SNoLev x0).
Apply andI with ordsucc (SNoLev x0)omega, SNoLt x0 (ordsucc (SNoLev x0)) leaving 2 subgoals.
Apply omega_ordsucc with SNoLev x0.
The subproof is completed by applying H8.
Apply ordinal_SNoLev_max with ordsucc (SNoLev x0), x0 leaving 3 subgoals.
Apply ordinal_ordsucc with SNoLev x0.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
The subproof is completed by applying ordsuccI2 with SNoLev x0.
Apply ordinal_SNoLev with omega, λ x1 x2 . x2SNoLev x0SNoEq_ x2 x0 omeganIn x2 x0∃ x3 . and (x3omega) (SNoLt x0 x3) leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Assume H6: omegaSNoLev x0.
Apply FalseE with SNoEq_ omega x0 omeganIn omega x0∃ x1 . and (x1omega) (SNoLt x0 x1).
Apply ordsuccE with omega, SNoLev x0, False leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H7: SNoLev x0omega.
Apply In_no2cycle with SNoLev x0, omega leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
Assume H7: SNoLev x0 = omega.
Apply In_irref with omega.
Apply H7 with λ x1 x2 . omegax1.
The subproof is completed by applying H6.