Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1 ∈ SNoR_omega x0 ⟶ ∃ x2 . and (x2 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x2)))).
Apply unknownprop_690598e6fd4ea25bb12e3b584dc4b13fe6c60343f666f02f1641e57297d2d891 with SNoR_omega x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H2: x1 ∈ {x2 ∈ SNoS_ omega|SNoLt x0 x2}.
Apply SepE1 with SNoS_ omega, λ x2 . SNoLt x0 x2, x1.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H2: x1 ∈ SNoR_omega x0.
Apply SNoS_E2 with omega, x1, ∃ x2 . and (x2 ∈ omega) (∀ x3 . x3 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x3 ⟶ SNoLt x3 (add_SNo x1 (eps_ x2)) ⟶ x3 ∈ SNoR_omega x0) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply SepE1 with SNoS_ omega, λ x2 . SNoLt x0 x2, x1.
The subproof is completed by applying H2.
Assume H3: SNoLev x1 ∈ omega.
Assume H4: ordinal (SNoLev x1).
Assume H5: SNo x1.
Assume H6: SNo_ (SNoLev x1) x1.
Apply H1 with x1, ∃ x2 . and (x2 ∈ omega) (∀ x3 . x3 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x3 ⟶ SNoLt x3 (add_SNo x1 (eps_ x2)) ⟶ x3 ∈ SNoR_omega x0) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H7: (λ x3 . and (x3 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x3))))) x2.
Apply H7 with ∃ x3 . and (x3 ∈ omega) (∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x3))) x4 ⟶ SNoLt x4 (add_SNo x1 (eps_ x3)) ⟶ x4 ∈ SNoR_omega x0).
Assume H8: x2 ∈ omega.
Assume H9: SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x2))).
Let x3 of type ο be given.
Assume H10: ∀ x4 . and (x4 ∈ omega) (∀ x5 . x5 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x4))) x5 ⟶ SNoLt x5 (add_SNo x1 (eps_ x4)) ⟶ x5 ∈ SNoR_omega x0) ⟶ x3.
Apply H10 with x2.
Apply andI with x2 ∈ omega, ∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x4 ⟶ SNoLt x4 (add_SNo x1 (eps_ x2)) ⟶ x4 ∈ SNoR_omega x0 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x4 of type ι be given.
Assume H11: x4 ∈ SNoS_ omega.
Assume H12: SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x4.
Assume H13: SNoLt x4 (add_SNo x1 (eps_ x2)).
Apply SNoS_E2 with omega, x4, x4 ∈ SNoR_omega x0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H11.
Assume H14: SNoLev x4 ∈ omega.
Assume H15: ordinal (SNoLev x4).
Assume H16: SNo ....
...
■