[STATEMENT]
lemma num_params_approx_tm:
  assumes "approx_tm prec ord I a f env = Some t"
  assumes "\<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I"
  shows "num_params (tm_poly t) \<le> length I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
approx_tm prec ord I a f env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
proof (induction f arbitrary: t)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Add f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Minus f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 18 subgoals...
[PROOF STEP]
case (Add f1 f2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Add f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (18 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Add f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Minus f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Add f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Add f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits intro!: num_params_tm_add_le)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (17 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Minus f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Minus f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 17 subgoals...
[PROOF STEP]
case (Minus f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Minus f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (17 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Minus f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Minus f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Minus f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (16 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 16 subgoals...
[PROOF STEP]
case (Mult f1 f2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Mult f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (16 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Mult f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 16 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Mult f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Mult f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits intro!: num_params_tm_mul_le)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (15 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 15 subgoals...
[PROOF STEP]
case (Inverse f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Inverse f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (15 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Inverse f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 15 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Inverse f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Inverse f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (14 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 14 subgoals...
[PROOF STEP]
case (Cos f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Cos f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (14 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Cos f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Cos f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Cos f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (13 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 13 subgoals...
[PROOF STEP]
case (Arctan f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Arctan f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (13 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Arctan f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 13 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Arctan f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Arctan f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (12 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 12 subgoals...
[PROOF STEP]
case (Abs f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Abs f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (12 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Abs f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Abs f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Abs f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto simp: tm_abs.simps Let_def intro!: num_params_tm_union_le)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (11 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 11 subgoals...
[PROOF STEP]
case (Max f1 f2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Max f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (11 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Max f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Max f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Max f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto simp: tm_max.simps Let_def intro!: num_params_tm_union_le split: option.splits)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (10 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Min f1 f2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Min f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (10 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Min f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 10. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Min f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Min f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto simp: tm_min.simps Let_def intro!: num_params_tm_union_le split: option.splits)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (9 subgoals):
 1. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case Pi
[PROOF STATE]
proof (state)
this:
approx_tm prec ord I a Pi env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (9 subgoals):
 1. \<And>t. \<lbrakk>approx_tm prec ord I a Pi env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 9. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
approx_tm prec ord I a Pi env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
approx_tm prec ord I a Pi env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto )
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (8 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Sqrt f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Sqrt f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (8 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Sqrt f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 8. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Sqrt f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Sqrt f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (7 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Exp f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Exp f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (7 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Exp f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 7. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Exp f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Exp f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (6 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Powr f1 f2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Powr f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (6 subgoals):
 1. \<And>f1 f2 t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f1 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; \<And>t. \<lbrakk>approx_tm prec ord I a f2 env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Powr f1 f2) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 6. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Powr f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f1 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
\<lbrakk>approx_tm prec ord I a f2 env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Powr f1 f2) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (5 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Ln f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Ln f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (5 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Ln f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 5. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Ln f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Ln f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (4 subgoals):
 1. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Power f x2a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Power f x2a) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (4 subgoals):
 1. \<And>f x2a t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Power f x2a) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 4. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Power f x2a) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Power f x2a) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_pow_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (3 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Floor f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Floor f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (3 subgoals):
 1. \<And>f t. \<lbrakk>\<And>t. \<lbrakk>approx_tm prec ord I a f env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I; approx_tm prec ord I a (Floor f) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 3. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Floor f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>approx_tm prec ord I a f env = Some ?t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly ?t) \<le> length I
approx_tm prec ord I a (Floor f) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: option.splits simp: Let_def compute_tm_by_comp_eq_Some_iff
        intro!: num_params_tm_comp_le dest!: tm_floatarith_eq_Some_num_params)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (2 subgoals):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:
approx_tm prec ord I a (Var x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (2 subgoals):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Var x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
 2. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
approx_tm prec ord I a (Var x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
approx_tm prec ord I a (Var x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal (1 subgoal):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
case (Num x)
[PROOF STATE]
proof (state)
this:
approx_tm prec ord I a (Num x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. \<And>x t. \<lbrakk>approx_tm prec ord I a (Num x) env = Some t; \<And>tm. tm \<in> set env \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> num_params (tm_poly t) \<le> length I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
approx_tm prec ord I a (Num x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
approx_tm prec ord I a (Num x) env = Some t
?tm \<in> set env \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> length I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
num_params (tm_poly t) \<le> length I

goal:
No subgoals!
[PROOF STEP]
qed