Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Apply xm with SNoR x0 = 0, or (SNoR x0 = 0) (∃ x1 . SNo_min_of (SNoR x0) x1) leaving 2 subgoals.
The subproof is completed by applying orIL with SNoR x0 = 0, ∃ x1 . SNo_min_of (SNoR x0) x1.
Assume H1: SNoR x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply orIR with SNoR x0 = 0, ∃ x1 . SNo_min_of (SNoR x0) x1.
Apply finite_min_exists with SNoR x0 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H2: x1 ∈ SNoR 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 SNoR_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 x0 x1.
The subproof is completed by applying H7.
Apply SNoS_omega_SNoR_finite with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■