| pf |
|---|
Apply nat_ind with λ x0 . SNoLt x0 (exp_SNo_nat 2 x0) leaving 2 subgoals.
Apply exp_SNo_nat_0 with 2, λ x0 x1 . SNoLt 0 x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying SNoLt_0_1.
Let x0 of type ι be given.
Apply SNo_exp_SNo_nat with 2, x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
Apply exp_SNo_nat_S with 2, x0, λ x1 x2 . SNoLt (ordsucc x0) x2 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
Apply add_SNo_1_ordsucc with x0, λ x1 x2 . SNoLt x1 (mul_SNo 2 (exp_SNo_nat 2 x0)) leaving 2 subgoals.
Apply nat_p_omega with x0.
The subproof is completed by applying H0.
Apply add_SNo_1_1_2 with λ x1 x2 . SNoLt (add_SNo x0 1) (mul_SNo x1 (exp_SNo_nat 2 x0)).
Apply mul_SNo_distrR with 1, 1, exp_SNo_nat 2 x0, λ x1 x2 . SNoLt (add_SNo x0 1) x2 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L2.
Apply mul_SNo_oneL with exp_SNo_nat 2 x0, λ x1 x2 . SNoLt (add_SNo x0 1) (add_SNo x2 x2) leaving 2 subgoals.
The subproof is completed by applying L2.
Apply SNoLtLe_tra with add_SNo x0 1, add_SNo (exp_SNo_nat 2 x0) 1, add_SNo (exp_SNo_nat 2 x0) (exp_SNo_nat 2 x0) leaving 5 subgoals.
Apply SNo_add_SNo with x0, 1 leaving 2 subgoals.
Apply nat_p_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply SNo_add_SNo with exp_SNo_nat 2 x0, 1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_1.
Apply SNo_add_SNo with exp_SNo_nat 2 x0, exp_SNo_nat 2 x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
Apply add_SNo_Lt1 with x0, 1, exp_SNo_nat 2 x0 leaving 4 subgoals.
Apply nat_p_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
Apply add_SNo_Le2 with exp_SNo_nat 2 x0, 1, exp_SNo_nat 2 x0 leaving 4 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L2.
Apply exp_SNo_1_bd with 2, x0 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
Apply SNoLtLe with 1, 2.
The subproof is completed by applying SNoLt_1_2.
The subproof is completed by applying H0.
■ |
|