Let x0 of type ι be given.
Apply SNoS_E2 with
ordsucc omega,
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (mul_SNo (eps_ x1) x0) 1) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Apply SNoS_ordsucc_omega_bdd_above with
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (mul_SNo (eps_ x1) x0) 1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Apply H7 with
∃ x2 . and (x2 ∈ omega) (SNoLt (mul_SNo (eps_ x2) x0) 1).
Let x2 of type ο be given.
Apply H11 with
x1.
Apply andI with
x1 ∈ omega,
SNoLt (mul_SNo (eps_ x1) x0) 1 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply SNoLt_tra with
mul_SNo (eps_ x1) x0,
mul_SNo (eps_ x1) x1,
1 leaving 5 subgoals.
Apply SNo_mul_SNo with
eps_ x1,
x0 leaving 2 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying H5.
Apply SNo_mul_SNo with
eps_ x1,
x1 leaving 2 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_1.
Apply pos_mul_SNo_Lt with
eps_ x1,
x0,
x1 leaving 5 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H8.
Apply SNo_eps_pos with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
The subproof is completed by applying H9.
Apply SNoLtLe_or with
mul_SNo (eps_ x1) x1,
1,
SNoLt (mul_SNo (eps_ x1) x1) 1 leaving 4 subgoals.
Apply SNo_mul_SNo with
eps_ x1,
x1 leaving 2 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_1.
The subproof is completed by applying H12.
Apply FalseE with
SNoLt (mul_SNo (eps_ x1) x1) 1.
Apply mul_SNo_oneR with
exp_SNo_nat 2 x1,
λ x3 x4 . SNoLe x3 (mul_SNo (exp_SNo_nat 2 x1) (mul_SNo (eps_ x1) x1)) leaving 2 subgoals.
The subproof is completed by applying L13.
Apply nonneg_mul_SNo_Le with
exp_SNo_nat 2 x1,
1,
mul_SNo (eps_ x1) x1 leaving 5 subgoals.
The subproof is completed by applying L13.
Apply SNoLtLe with
0,
exp_SNo_nat 2 x1.
Apply exp_SNo_nat_pos with
2,
x1 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying SNoLt_0_2.
Apply omega_nat_p with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying SNo_1.
Apply SNo_mul_SNo with
eps_ x1,
x1 leaving 2 subgoals.
Apply SNoLt_irref with
exp_SNo_nat 2 x1.
Apply SNoLeLt_tra with
exp_SNo_nat 2 x1,
x1,
exp_SNo_nat 2 x1 leaving 5 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L10.
The subproof is completed by applying L13.
Apply mul_SNo_oneL with
x1,
λ x3 x4 . SNoLe (exp_SNo_nat 2 x1) x3 leaving 2 subgoals.
The subproof is completed by applying L10.
Apply mul_SNo_eps_power_2' with
x1,
λ x3 x4 . SNoLe (exp_SNo_nat 2 x1) (mul_SNo x3 x1) leaving 2 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H8.
Apply mul_SNo_assoc with
exp_SNo_nat 2 x1,
eps_ x1,
x1,
λ x3 x4 . SNoLe (exp_SNo_nat 2 x1) x3 leaving 4 subgoals.
The subproof is completed by applying L13.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H8.
The subproof is completed by applying L10.
The subproof is completed by applying L14.
Apply exp_SNo_2_bd with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H8.