[STATEMENT]
lemma extendf_deriv:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "\<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (extendf_deriv I i_f f' \<nu> x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i_f f' \<nu> x) (at x)
[PROOF STEP]
using free
[PROOF STATE]
proof (prove)
using this:
dfree f'

goal (1 subgoal):
 1. \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i_f f' \<nu> x) (at x)
[PROOF STEP]
apply (induction rule: dfree.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>i. \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) (Var i) \<nu>) has_derivative extendf_deriv I i_f (Var i) \<nu> x) (at x)
 2. \<And>r. \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) (Const r) \<nu>) has_derivative extendf_deriv I i_f (Const r) \<nu> x) (at x)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x)\<rbrakk> \<Longrightarrow> \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) ($f i args) \<nu>) has_derivative extendf_deriv I i_f ($f i args) \<nu> x) (at x)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) has_derivative extendf_deriv I i_f (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x) (at x)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> \<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) has_derivative extendf_deriv I i_f (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x) (at x)
[PROOF STEP]
apply(auto)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>args i x. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2 x. \<lbrakk>dfree \<theta>\<^sub>1; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative (\<lambda>a. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x a * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)) (at x)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2 x. \<lbrakk>dfree \<theta>\<^sub>1; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative (\<lambda>a. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x a * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)) (at x)
 2. \<And>args i x. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
[PROOF STEP]
subgoal for \<theta>\<^sub>1 \<theta>\<^sub>2 x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative (\<lambda>a. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x a * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)) (at x)
[PROOF STEP]
apply(rule has_derivative_mult)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dfree \<theta>\<^sub>1; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x)
 2. \<lbrakk>dfree \<theta>\<^sub>1; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>1 \<nu> x) (at x); dfree \<theta>\<^sub>2; \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>) has_derivative extendf_deriv I i_f \<theta>\<^sub>2 \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>args i x. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
[PROOF STEP]
subgoal for args i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x)\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
[PROOF STEP]
apply(cases "i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
 2. \<And>b. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inr b\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inr b\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
 2. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. (case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. R $ f') (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (case i of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)) (at x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inr b\<rbrakk> \<Longrightarrow> ((\<lambda>R. R $ b) has_derivative (\<lambda>\<nu>'. \<nu>' $ b)) (at x)
 2. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
subgoal for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inr b\<rbrakk> \<Longrightarrow> ((\<lambda>R. R $ b) has_derivative (\<lambda>\<nu>'. \<nu>' $ b)) (at x)
[PROOF STEP]
using has_derivative_proj'
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>x. x $ ?i) has_derivative (\<lambda>x. x $ ?i)) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inr b\<rbrakk> \<Longrightarrow> ((\<lambda>R. R $ b) has_derivative (\<lambda>\<nu>'. \<nu>' $ b)) (at x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
assume dfrees:"(\<And>i. dfree (args i))"
[PROOF STATE]
proof (state)
this:
dfree (args ?i7)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
assume IH1:"(\<And>ia. \<forall>x. ((\<lambda>R. dterm_sem
                      \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                         ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                      (args ia) \<nu>) has_derivative
                extendf_deriv I i_f (args ia) \<nu> x)
                (at x))"
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args ?ia7) \<nu>) has_derivative extendf_deriv I i_f (args ?ia7) \<nu> x) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args ?ia7) \<nu>) has_derivative extendf_deriv I i_f (args ?ia7) \<nu> x) (at x)
[PROOF STEP]
have IH1':"(\<And>ia. \<And>x. ((\<lambda>R. dterm_sem
                      \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                         ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                      (args ia) \<nu>) has_derivative
                extendf_deriv I i_f (args ia) \<nu> x)
                (at x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args ?ia7) \<nu>) has_derivative extendf_deriv I i_f (args ?ia7) \<nu> x) (at x)

goal (1 subgoal):
 1. \<And>ia x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args ia) \<nu>) has_derivative extendf_deriv I i_f (args ia) \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args ?ia7) \<nu>) has_derivative extendf_deriv I i_f (args ?ia7) \<nu> ?x7) (at ?x7)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
assume a:"i = Inl a"
[PROOF STATE]
proof (state)
this:
i = Inl a

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
have chain:"\<And>f f' x s g g'. (f has_derivative f') (at x within s) \<Longrightarrow>
      (g has_derivative g') (at (f x) within f ` s) \<Longrightarrow> (g \<circ> f has_derivative g' \<circ> f') (at x within s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f' x s g g'. \<lbrakk>(f has_derivative f') (at x within s); (g has_derivative g') (at (f x) within f ` s)\<rbrakk> \<Longrightarrow> (g \<circ> f has_derivative g' \<circ> f') (at x within s)
[PROOF STEP]
by (auto intro: derivative_intros)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?f7 has_derivative ?f'7) (at ?x7 within ?s7); (?g7 has_derivative ?g'7) (at (?f7 ?x7) within ?f7 ` ?s7)\<rbrakk> \<Longrightarrow> (?g7 \<circ> ?f7 has_derivative ?g'7 \<circ> ?f'7) (at ?x7 within ?s7)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
let ?f = "(\<lambda>x. Functions I a x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
let ?g = "(\<lambda> R. (\<chi> i. dterm_sem
                       \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I,
                          Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                       (args i) \<nu>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
let ?myf' = "(\<lambda>x. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (?g x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
let ?myg' = "(\<lambda>x. (\<lambda>\<nu>'. \<chi> ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
have fg_eq:"(\<lambda>R. Functions I a
           (\<chi> i. dterm_sem
                  \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                  (args i) \<nu>)) = (?f \<circ> ?g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) = Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) = Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
have "\<forall>x. ((?f o ?g) has_derivative (?myf' x \<circ> ?myg' x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
apply (rule diff_chain_at)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ((\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
 2. \<And>x. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
subgoal for xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> xa \<nu>')) (at xa)
[PROOF STEP]
apply (rule has_derivative_vec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> xa) (at xa)
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> xa) (at xa)
[PROOF STEP]
using IH1'[of i xa]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> xa) (at xa)

goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> xa) (at xa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
subgoal for xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
have deriv:"\<And>x. (Functions I a has_derivative FunctionFrechet I a x) (at x)"
         and cont:"continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I a x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (Functions I a has_derivative FunctionFrechet I a x) (at x)) &&& continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I a x))
[PROOF STEP]
using good_interp[unfolded is_interp_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))

goal (1 subgoal):
 1. (\<And>x. (Functions I a has_derivative FunctionFrechet I a x) (at x)) &&& continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I a x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Functions I a has_derivative FunctionFrechet I a ?x8) (at ?x8)
continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I a x))

goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
apply(rule has_derivative_at_withinI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
using deriv
[PROOF STATE]
proof (prove)
using this:
(Functions I a has_derivative FunctionFrechet I a ?x8) (at ?x8)

goal (1 subgoal):
 1. (Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Functions I a has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) (at (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>x. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
have "((?f o ?g) has_derivative (?myf' x \<circ> ?myg' x)) (at x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)

goal (1 subgoal):
 1. (Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. \<forall>x. ((\<lambda>R. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative extendf_deriv I i_f (args i) \<nu> x) (at x); i = Inl a\<rbrakk> \<Longrightarrow> ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
show "((\<lambda>R. Functions I a
           (\<chi> i. dterm_sem
                  \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                  (args i) \<nu>)) has_derivative
              (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
      (\<chi> i. dterm_sem
             \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
             (args i) \<nu>) \<circ>
     (\<lambda>\<nu>'. \<chi> ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>'))
     (at x) "
[PROOF STATE]
proof (prove)
using this:
(Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)

goal (1 subgoal):
 1. ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
using fg_eq
[PROOF STATE]
proof (prove)
using this:
(Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
(\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) = Functions I a \<circ> (\<lambda>R. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)

goal (1 subgoal):
 1. ((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>R. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) has_derivative (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i_f (args ia) \<nu> x \<nu>')) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done