Let x0 of type ι be given.
Let x1 of type ι be given.
Apply mul_SNo_nonzero_cancel with
exp_SNo_nat 2 (add_SNo x0 x1),
mul_SNo (eps_ x0) (eps_ x1),
eps_ (add_SNo x0 x1) leaving 5 subgoals.
Apply SNo_exp_SNo_nat with
2,
add_SNo x0 x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L2.
Apply SNoLt_irref with
0.
Apply H6 with
λ x2 x3 . SNoLt 0 x2.
Apply exp_SNo_nat_pos with
2,
add_SNo x0 x1 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying SNoLt_0_2.
The subproof is completed by applying L2.
Apply SNo_mul_SNo with
eps_ x0,
eps_ x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply SNo_eps_ with
add_SNo x0 x1.
Apply add_SNo_In_omega with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
set y2 to be ...
Let x3 of type ι → ο be given.
set y4 to be ...
set y5 to be ...
Apply L7 with
λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.
Assume H8: y5 y4 y4.
The subproof is completed by applying H8.
Apply mul_SNo_assoc with
exp_SNo_nat 2 x3,
exp_SNo_nat 2 y4,
mul_SNo (eps_ x3) (eps_ y4),
λ x6 x7 . (λ x8 . y5) x7 x6 leaving 4 subgoals.
Apply SNo_exp_SNo_nat with
2,
x3 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_nat_p with
x3.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
Apply SNo_mul_SNo with
eps_ x3,
eps_ y4 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
set y6 to be ...
Let x7 of type ι → ο be given.
set y8 to be ...
Let x9 of type ι → ο be given.
Apply mul_SNo_com with
eps_ y5,
eps_ y6,
λ x10 x11 . mul_SNo (exp_SNo_nat 2 y6) x11 = mul_SNo (mul_SNo (exp_SNo_nat 2 y6) (eps_ y6)) (eps_ y5),
λ x10 . x9 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply mul_SNo_assoc with
exp_SNo_nat 2 y6,
eps_ y6,
eps_ y5 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L5.
The subproof is completed by applying L4.
set y10 to be ...
set y11 to be ...
Apply L9 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Apply L8 with
λ x10 . y9 x10 y8 ⟶ y9 y8 x10.
Assume H9: y9 y8 y8.
The subproof is completed by applying H9.
set y7 to be λ x7 . y6
Apply L8 with
λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.
Assume H9: y7 y6 y6.
The subproof is completed by applying H9.
Apply mul_SNo_eps_power_2' with
y5,
λ x8 . y7 leaving 2 subgoals.
Apply omega_nat_p with
y5.
The subproof is completed by applying L2.
Apply mul_SNo_eps_power_2' with
add_SNo y5 y6,
λ x8 x9 . (λ x10 . y7) x9 x8 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L8.
Let x3 of type ι → ι → ο be given.
Apply L6 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H7: x3 y2 y2.
The subproof is completed by applying H7.