Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Apply xm with SNoL x0 = 0, or (SNoL x0 = 0) (∃ x1 . SNo_max_of (SNoL x0) x1) leaving 2 subgoals.
The subproof is completed by applying orIL with SNoL x0 = 0, ∃ x1 . SNo_max_of (SNoL x0) x1.
Assume H1: SNoL x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply orIR with SNoL x0 = 0, ∃ x1 . SNo_max_of (SNoL x0) x1.
Apply finite_max_exists with SNoL x0 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H2: x1 ∈ SNoL x0.
Apply SNoS_E2 with omega, x0, SNo x1 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H3: SNoLev x0 ∈ omega.
Assume H4: ordinal (SNoLev x0).
Assume H5: SNo x0.
Assume H6: SNo_ (SNoLev x0) x0.
Apply SNoL_E with x0, x1, SNo x1 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
Assume H7: SNo x1.
Assume H8: SNoLev x1 ∈ SNoLev x0.
Assume H9: SNoLt x1 x0.
The subproof is completed by applying H7.
Apply SNoS_omega_SNoL_finite with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■