Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Apply SNoS_E2 with omega, x0, ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H1: SNoLev x0 ∈ omega.
Assume H2: ordinal (SNoLev x0).
Assume H3: SNo x0.
Assume H4: SNo_ (SNoLev x0) x0.
Let x1 of type ι be given.
Assume H5: x1 ∈ omega.
Claim L6: SNo (eps_ (ordsucc x1))
Apply SNo_eps_ with ordsucc x1.
Apply omega_ordsucc with x1.
The subproof is completed by applying H5.
Let x2 of type ο be given.
Assume H7: ∀ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1)))) ⟶ x2.
Apply H7 with add_SNo x0 (minus_SNo (eps_ (ordsucc x1))).
Apply andI with add_SNo x0 (minus_SNo (eps_ (ordsucc x1))) ∈ SNoS_ omega, and (SNoLt (add_SNo x0 (minus_SNo (eps_ (ordsucc x1)))) x0) (SNoLt x0 (add_SNo (add_SNo x0 (minus_SNo (eps_ (ordsucc x1)))) (eps_ x1))) leaving 2 subgoals.
Apply add_SNo_SNoS_omega with x0, minus_SNo (eps_ (ordsucc x1)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply minus_SNo_SNoS_omega with eps_ (ordsucc x1).
Apply SNo_eps_SNoS_omega with ordsucc x1.
Apply omega_ordsucc with x1.
The subproof is completed by applying H5.
Apply andI with SNoLt (add_SNo x0 (minus_SNo (eps_ (ordsucc x1)))) x0, SNoLt x0 (add_SNo (add_SNo x0 (minus_SNo (eps_ (ordsucc x1)))) (eps_ x1)) leaving 2 subgoals.
Apply add_SNo_minus_Lt1b with x0, eps_ (ordsucc x1), x0 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L6.
The subproof is completed by applying H3.
Apply add_SNo_eps_Lt with x0, ordsucc x1 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply omega_ordsucc with x1.
The subproof is completed by applying H5.
Apply eps_ordsucc_half_add with x1, λ x3 x4 . SNoLt x0 (add_SNo (add_SNo x0 (minus_SNo (eps_ (ordsucc x1)))) x3) leaving 2 subgoals.
Apply omega_nat_p with x1.
The subproof is completed by applying H5.
Apply add_SNo_com_4_inner_mid with x0, minus_SNo (eps_ (ordsucc x1)), eps_ (ordsucc x1), eps_ (ordsucc x1), λ x3 x4 . SNoLt x0 x4 leaving 5 subgoals.
The subproof is completed by applying H3.
Apply SNo_minus_SNo with eps_ (ordsucc x1).
The subproof is completed by applying L6.
The subproof is completed by applying L6.
The subproof is completed by applying L6.
Apply add_SNo_minus_SNo_linv with eps_ (ordsucc x1), λ x3 x4 . SNoLt x0 (add_SNo (add_SNo x0 (eps_ (ordsucc x1))) x4) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply add_SNo_0R with add_SNo x0 (eps_ (ordsucc x1)), λ x3 x4 . SNoLt x0 x4 leaving 2 subgoals.
Apply SNo_add_SNo with x0, eps_ (ordsucc x1) leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L6.
Apply add_SNo_eps_Lt with x0, ordsucc x1 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply omega_ordsucc with x1.
The subproof is completed by applying H5.
■