[STATEMENT]
lemma isDERIV_FDERIV_floatarith:
  assumes "isDERIV x fa vs" "\<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs"
  assumes [simp]: "length xs = length ds"
  shows "isDERIV x (FDERIV_floatarith fa xs ds) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (FDERIV_floatarith fa xs ds) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x fa vs
?i < length ds \<Longrightarrow> isDERIV x (ds ! ?i) vs
length xs = length ds

goal (1 subgoal):
 1. isDERIV x (FDERIV_floatarith fa xs ds) vs
[PROOF STEP]
apply (induction fa)
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Add fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Add fa1 fa2) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Minus fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Minus fa) xs ds) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Mult fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Mult fa1 fa2) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Inverse fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Inverse fa) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Cos fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa) xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 9. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 10. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
A total of 18 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa1_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1_ xs ds) vs; \<lbrakk>isDERIV x fa2_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2_ xs ds) vs; isDERIV x (Add fa1_ fa2_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Add fa1_ fa2_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Minus fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Minus fa) xs ds) vs
 2. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Mult fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Mult fa1 fa2) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Inverse fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Inverse fa) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Cos fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 7. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 9. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 10. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
A total of 17 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Minus fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Minus fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Mult fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Mult fa1 fa2) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Inverse fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Inverse fa) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Cos fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 6. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 7. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 8. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 9. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 10. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
A total of 16 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa1_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1_ xs ds) vs; \<lbrakk>isDERIV x fa2_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2_ xs ds) vs; isDERIV x (Mult fa1_ fa2_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Mult fa1_ fa2_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Inverse fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Inverse fa) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Cos fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 5. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 6. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 7. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 8. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 9. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 10. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
A total of 15 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Inverse fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Inverse fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Cos fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 4. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 5. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 6. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 8. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 9. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 10. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
A total of 14 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Cos fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Cos fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Arctan fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 4. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 5. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 9. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 10. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
A total of 13 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Arctan fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Arctan fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Abs fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa) xs ds) vs
 2. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 4. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 7. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 8. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 9. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 10. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
A total of 12 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Abs fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Abs fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Max fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1 fa2) xs ds) vs
 2. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 3. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 6. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 8. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 9. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 10. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
A total of 11 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa1_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1_ xs ds) vs; \<lbrakk>isDERIV x fa2_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2_ xs ds) vs; isDERIV x (Max fa1_ fa2_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Max fa1_ fa2_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Min fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1 fa2) xs ds) vs
 2. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 5. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 7. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 8. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 9. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 10. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa1_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1_ xs ds) vs; \<lbrakk>isDERIV x fa2_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2_ xs ds) vs; isDERIV x (Min fa1_ fa2_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Min fa1_ fa2_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 4. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 6. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 8. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 9. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x Pi vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith Pi xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Sqrt fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 5. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 7. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 8. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Sqrt fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Sqrt fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Exp fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa) xs ds) vs
 2. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 4. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 6. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 7. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Exp fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Exp fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>isDERIV x fa1 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1 xs ds) vs; \<lbrakk>isDERIV x fa2 vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2 xs ds) vs; isDERIV x (Powr fa1 fa2) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1 fa2) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 3. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 5. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 6. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa1_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa1_ xs ds) vs; \<lbrakk>isDERIV x fa2_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa2_ xs ds) vs; isDERIV x (Powr fa1_ fa2_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Powr fa1_ fa2_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Ln fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa) xs ds) vs
 2. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 3. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 4. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 5. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Ln fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Ln fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>fa x2a. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e x2a) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e x2a) xs ds) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 3. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 4. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal for fa n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (fa ^\<^sub>e n) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (fa ^\<^sub>e n) xs ds) vs
[PROOF STEP]
by (cases n) (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa. \<lbrakk>\<lbrakk>isDERIV x fa vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa xs ds) vs; isDERIV x (Floor fa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa) xs ds) vs
 2. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 3. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>isDERIV x fa_ vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith fa_ xs ds) vs; isDERIV x (Floor fa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Floor fa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>isDERIV x (Var xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa) xs ds) vs
 2. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x (Var xa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Var xa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>isDERIV x (Num xa) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa) xs ds) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x (Num xa_) vs; \<And>i. i < length ds \<Longrightarrow> isDERIV x (ds ! i) vs; length xs = length ds\<rbrakk> \<Longrightarrow> isDERIV x (FDERIV_floatarith (Num xa_) xs ds) vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isDERIV_FDERIV_floatariths:
  assumes "isFDERIV N xs fas vs" "isFDERIV N xs ds vs" and [simp]: "length fas = length ds"
  shows "isFDERIV N xs (FDERIV_floatariths fas xs ds) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV N xs (FDERIV_floatariths fas xs ds) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isFDERIV N xs fas vs
isFDERIV N xs ds vs
length fas = length ds

goal (1 subgoal):
 1. isFDERIV N xs (FDERIV_floatariths fas xs ds) vs
[PROOF STEP]
by (auto simp: isFDERIV_def FDERIV_floatariths_def intro!: isDERIV_FDERIV_floatarith)


[STATEMENT]
lemma isFDERIV_map_Var:
  assumes [simp]: "length ds = N" "length xs = N"
  shows "isFDERIV N xs (map Var ds) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV N xs (map Var ds) vs
[PROOF STEP]
by (auto simp: isFDERIV_def)


[STATEMENT]
theorem isFDERIV_imp_isnFDERIV:
  assumes "isFDERIV N xs fas vs" and [simp]: "length fas = N" "length xs = N" "length ds = N"
  shows "isnFDERIV N fas xs ds vs n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isnFDERIV N fas xs ds vs n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isFDERIV N xs fas vs
length fas = N
length xs = N
length ds = N

goal (1 subgoal):
 1. isnFDERIV N fas xs ds vs n
[PROOF STEP]
by (induction n) (auto intro!: isFDERIV_imp_isFDERIV_FDERIV_n isFDERIV_map_Var)


[STATEMENT]
lemma eventually_isnFDERIV:
  assumes iD: "isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2*DIM('a)] (list_of_eucl x @ list_of_eucl (d::'a)) n"
  assumes m: "max_Var_floatariths fas \<le> 2 * DIM('a::executable_euclidean_space)"
  shows "\<forall>\<^sub>F (x::'a) in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2*DIM('a)] (list_of_eucl x @ list_of_eucl d) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
[PROOF STEP]
using iD
[PROOF STATE]
proof (prove)
using this:
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0 \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0
 2. \<And>n. \<lbrakk>isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n; isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)

goal (2 subgoals):
 1. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0 \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0
 2. \<And>n. \<lbrakk>isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n; isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
have 1: "\<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n"
    and 2: "isFDERIV DIM('a) [0..<DIM('a)] (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n)
      (list_of_eucl x @ list_of_eucl d)"
[PROOF STATE]
proof (prove)
using this:
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n &&& isFDERIV DIM('a) [0..<DIM('a)] (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) (list_of_eucl x @ list_of_eucl d)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
isFDERIV DIM('a) [0..<DIM('a)] (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) (list_of_eucl x @ list_of_eucl d)

goal (2 subgoals):
 1. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0 \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0
 2. \<And>n. \<lbrakk>isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n; isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
have "max_Var_floatariths (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) \<le>
      DIM('a) + length (list_of_eucl d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) \<le> DIM('a) + length (list_of_eucl d)
[PROOF STEP]
by (auto intro!: max_Var_floatarith_FDERIV_n_floatariths[THEN order_trans] m[THEN order_trans])
[PROOF STATE]
proof (state)
this:
max_Var_floatariths (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) \<le> DIM('a) + length (list_of_eucl d)

goal (2 subgoals):
 1. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0 \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0
 2. \<And>n. \<lbrakk>isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n; isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
from eventually_isFDERIV[OF 2 this] 1
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) (list_of_eucl x @ list_of_eucl d)
\<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] (FDERIV_n_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]) n) (list_of_eucl x @ list_of_eucl d)
\<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) n

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)
[PROOF STEP]
by eventually_elim simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) (Suc n)

goal (1 subgoal):
 1. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0 \<Longrightarrow> \<forall>\<^sub>F x in at x. isnFDERIV DIM('a) fas [0..<DIM('a)] [DIM('a)..<2 * DIM('a)] (list_of_eucl x @ list_of_eucl d) 0
[PROOF STEP]
qed simp


[STATEMENT]
lemma isFDERIV_open:
  assumes "max_Var_floatariths fas \<le> DIM('a)"
  shows "open {x::'a. isFDERIV DIM('a::executable_euclidean_space)  [0..<DIM('a)] fas (list_of_eucl x)}"
    (is "open (Collect ?s)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
proof (safe intro!: topological_space_class.openI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
fix x::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
assume x: "?s x"
[PROOF STATE]
proof (state)
this:
isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)

goal (1 subgoal):
 1. \<And>x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
with eventually_isFDERIV[where 'a='a, of fas x Nil]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ []); max_Var_floatariths fas \<le> DIM('a) + length []\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ [])
isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)
[PROOF STEP]
have "\<forall>\<^sub>F x in at x. x \<in> Collect ?s"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ []); max_Var_floatariths fas \<le> DIM('a) + length []\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ [])
isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. x \<in> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
by (auto simp: assms)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x. x \<in> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}

goal (1 subgoal):
 1. \<And>x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at x. x \<in> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
obtain S where "open S" "x \<in> S"
    "(\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> ?s xa)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at x. x \<in> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>open S; x \<in> S; \<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl xa)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_at_topological
[PROOF STATE]
proof (prove)
using this:
\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> UNIV \<longrightarrow> xa \<in> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)})

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>open S; x \<in> S; \<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl xa)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open S
x \<in> S
\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl xa)

goal (1 subgoal):
 1. \<And>x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)
open S
x \<in> S
\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl xa)
[PROOF STEP]
show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> Collect ?s"
[PROOF STATE]
proof (prove)
using this:
isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)
open S
x \<in> S
\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl xa)

goal (1 subgoal):
 1. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}
[PROOF STEP]
by (auto intro!: exI[where x=S])
[PROOF STATE]
proof (state)
this:
\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatarith_eq:
  assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" "length ds = DIM('a)"
  shows "interpret_floatarith (FDERIV_floatarith fa xs ds) vs =
    einterpret (map (\<lambda>x. DERIV_floatarith x fa) xs) vs \<bullet> (einterpret ds vs::'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (FDERIV_floatarith fa xs ds) vs = einterpret (map (\<lambda>x. DERIV_floatarith x fa) xs) vs \<bullet> einterpret ds vs
[PROOF STEP]
by (auto simp: FDERIV_floatarith_def interpret_floatarith_inner_floatariths)


[STATEMENT]
lemma subst_floatarith_Var_DERIV_floatarith:
  assumes "\<And>x. x = n \<longleftrightarrow> s x = n"
  shows "subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) =
  DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(?x = n) = (s ?x = n)

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)
[PROOF STEP]
proof (induction fa)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Add fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2))
 2. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Minus fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa))
 3. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Mult fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2))
 4. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Inverse fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa))
 5. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Cos fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa))
 6. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Arctan fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa))
 7. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Abs fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa))
 8. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Max fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2))
 9. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Min fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2))
 10. (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n Pi) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) Pi)
A total of 18 subgoals...
[PROOF STEP]
case (Power fa n)
[PROOF STATE]
proof (state)
this:
(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)
(?x = n) = (s ?x = n)

goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Add fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2))
 2. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Minus fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa))
 3. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Mult fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2))
 4. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Inverse fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa))
 5. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Cos fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa))
 6. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Arctan fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa))
 7. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Abs fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa))
 8. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Max fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2))
 9. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Min fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2))
 10. (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n Pi) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) Pi)
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)
(?x = n) = (s ?x = n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa)
(?x = n) = (s ?x = n)

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (fa ^\<^sub>e n)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (fa ^\<^sub>e n))
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (fa ^\<^sub>e n)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (fa ^\<^sub>e n))

goal (17 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Add fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Add fa1 fa2))
 2. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Minus fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Minus fa))
 3. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Mult fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Mult fa1 fa2))
 4. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Inverse fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Inverse fa))
 5. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Cos fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Cos fa))
 6. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Arctan fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Arctan fa))
 7. \<And>fa. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Abs fa)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Abs fa))
 8. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Max fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Max fa1 fa2))
 9. \<And>fa1 fa2. \<lbrakk>(\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa1) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa1); (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n fa2) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) fa2); \<And>x. (x = n) = (s x = n)\<rbrakk> \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n (Min fa1 fa2)) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) (Min fa1 fa2))
 10. (\<And>x. (x = n) = (s x = n)) \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith n Pi) = DERIV_floatarith n (subst_floatarith (\<lambda>x. Var (s x)) Pi)
A total of 17 subgoals...
[PROOF STEP]
qed force+


[STATEMENT]
lemma subst_floatarith_inner_floatariths[simp]:
  assumes "length fs = length gs"
  shows "subst_floatarith s (inner_floatariths fs gs) =
      inner_floatariths (map (subst_floatarith s) fs) (map (subst_floatarith s) gs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith s (inner_floatariths fs gs) = inner_floatariths (map (subst_floatarith s) fs) (map (subst_floatarith s) gs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length fs = length gs

goal (1 subgoal):
 1. subst_floatarith s (inner_floatariths fs gs) = inner_floatariths (map (subst_floatarith s) fs) (map (subst_floatarith s) gs)
[PROOF STEP]
by (induction rule: list_induct2) auto


[STATEMENT]
lemma Num_eq_subst_Var[simp]: "Num x = subst_floatarith (\<lambda>x. Var (s x)) fa \<longleftrightarrow> fa = Num x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Num x = subst_floatarith (\<lambda>x. Var (s x)) fa) = (fa = Num x)
[PROOF STEP]
by (cases fa) auto


[STATEMENT]
lemma Add_eq_subst_VarE:
  assumes "Add fa1 fa2 = subst_floatarith (\<lambda>x. Var (s x)) fa"
  obtains a1 a2 where "fa = Add a1 a2" "fa1 = subst_floatarith (\<lambda>x. Var (s x)) a1"
      "fa2 = subst_floatarith (\<lambda>x. Var (s x)) a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>fa = Add a1 a2; fa1 = subst_floatarith (\<lambda>x. Var (s x)) a1; fa2 = subst_floatarith (\<lambda>x. Var (s x)) a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Add fa1 fa2 = subst_floatarith (\<lambda>x. Var (s x)) fa

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>fa = Add a1 a2; fa1 = subst_floatarith (\<lambda>x. Var (s x)) a1; fa2 = subst_floatarith (\<lambda>x. Var (s x)) a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases fa) auto


[STATEMENT]
lemma subst_floatarith_eq_self[simp]: "subst_floatarith s f = f" if "max_Var_floatarith f = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith s f = f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith f = 0

goal (1 subgoal):
 1. subst_floatarith s f = f
[PROOF STEP]
by (induction f) auto


[STATEMENT]
lemma fold_const_fa_unique: "False" if "(\<And>x. f = Num x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that[of 0] that[of 1]
[PROOF STATE]
proof (prove)
using this:
f = Num 0
f = Num 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_unique: False if "(\<And>x::float. x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that[of 0] that[of 1]
[PROOF STATE]
proof (prove)
using this:
0 = 0
1 = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto