[STATEMENT]
lemma nsubst_dterm':
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  assumes good_interp:"is_interp I"
  shows "TadmitFO \<sigma> \<theta> \<Longrightarrow> dfree \<theta> \<Longrightarrow> (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dterm_sem I (TsubstFO \<theta> \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TadmitFO \<sigma> \<theta>; dfree \<theta>; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta> \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> \<nu>
[PROOF STEP]
proof (induction rule: TadmitFO.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
case (TadmitFO_Fun \<sigma> args f)
[PROOF STATE]
proof (state)
this:
TadmitFO \<sigma> (args ?i7)
\<lbrakk>dfree (args ?i7); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args ?i7) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) \<nu>
dfree ($f f args)
dsafe (\<sigma> ?i7)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
assume admit:"\<And>i. TadmitFO \<sigma> (args i)"
[PROOF STATE]
proof (state)
this:
TadmitFO \<sigma> (args ?i7)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
assume IH:"\<And>i. dfree (args i) \<Longrightarrow> (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>"
[PROOF STATE]
proof (state)
this:
\<lbrakk>dfree (args ?i7); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args ?i7) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) \<nu>

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
assume free:"dfree ($f f args)"
[PROOF STATE]
proof (state)
this:
dfree ($f f args)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
assume safe:"\<And>i. dsafe (\<sigma> i)"
[PROOF STATE]
proof (state)
this:
dsafe (\<sigma> ?i7)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
from free
[PROOF STATE]
proof (chain)
picking this:
dfree ($f f args)
[PROOF STEP]
have frees: "\<And>i. dfree (args i)"
[PROOF STATE]
proof (prove)
using this:
dfree ($f f args)

goal (1 subgoal):
 1. \<And>i. dfree (args i)
[PROOF STEP]
by (auto dest: dfree.cases)
[PROOF STATE]
proof (state)
this:
dfree (args ?i7)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have sem:"\<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
using IH[OF frees safe]
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (TsubstFO (args ?i7) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) \<nu>

goal (1 subgoal):
 1. \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO (args ?i7) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) \<nu>

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have vecEq:" (\<chi> i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) =
   (\<chi> i. dterm_sem
          \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I,
             Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
          (args i) \<nu>) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
apply(rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) $ i = (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) $ i
[PROOF STEP]
by (auto simp add: adjointFO_def)
[PROOF STATE]
proof (state)
this:
(\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. \<lbrakk>dfree (args i); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; dfree ($f f args); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
show " dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
apply (cases "f")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. f = Inl a \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
 2. \<And>b. f = Inr b \<Longrightarrow> dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
apply (auto simp add: vec_extensionality  adjointFO_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. f = Inl a \<Longrightarrow> Functions I a (\<chi>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu>) = Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
using sem
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (TsubstFO (args ?i7) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) \<nu>

goal (1 subgoal):
 1. \<And>a. f = Inl a \<Longrightarrow> Functions I a (\<chi>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu>) = Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f = Inl a; \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>\<rbrakk> \<Longrightarrow> Functions I a (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = Inl a; \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>\<rbrakk> \<Longrightarrow> Functions I a (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
using vecEq
[PROOF STATE]
proof (prove)
using this:
(\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)

goal (1 subgoal):
 1. \<lbrakk>f = Inl a; \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>\<rbrakk> \<Longrightarrow> Functions I a (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>) = Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), 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 (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
case (TadmitFO_Diff \<sigma> \<theta>)
[PROOF STATE]
proof (state)
this:
TadmitFFO \<sigma> \<theta>
NTUadmit \<sigma> \<theta> UNIV
dfree (TsubstFO \<theta> \<sigma>)
dfree (Differential \<theta>)
dsafe (\<sigma> ?i7)

goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
hence admit:"TadmitFFO \<sigma> \<theta>"
    and admitU:"NTUadmit \<sigma> \<theta> UNIV"
    (*and IH : "dfree \<theta> \<Longrightarrow>
          (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dterm_sem I (TsubstFO \<theta> \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> \<nu>"*)
    and safe: "dfree (Differential \<theta>)"
    and freeSub:"\<And>i. dsafe (\<sigma> i)"
[PROOF STATE]
proof (prove)
using this:
TadmitFFO \<sigma> \<theta>
NTUadmit \<sigma> \<theta> UNIV
dfree (TsubstFO \<theta> \<sigma>)
dfree (Differential \<theta>)
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. (TadmitFFO \<sigma> \<theta> &&& NTUadmit \<sigma> \<theta> UNIV) &&& dfree (Differential \<theta>) &&& (\<And>i. dsafe (\<sigma> i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TadmitFFO \<sigma> \<theta>
NTUadmit \<sigma> \<theta> UNIV
dfree (Differential \<theta>)
dsafe (\<sigma> ?i7)

goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
from safe
[PROOF STATE]
proof (chain)
picking this:
dfree (Differential \<theta>)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
dfree (Differential \<theta>)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest: dfree.cases)
[PROOF STATE]
proof (state)
this:
False

goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; NTUadmit \<sigma> \<theta> UNIV; dfree (TsubstFO \<theta> \<sigma>); dfree (Differential \<theta>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show "dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>

goal (5 subgoals):
 1. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Plus \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFO \<sigma> \<theta>1; \<lbrakk>dfree \<theta>1; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>1 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 \<nu>; TadmitFO \<sigma> \<theta>2; \<lbrakk>dfree \<theta>2; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO \<theta>2 \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 \<nu>; dfree (Times \<theta>1 \<theta>2); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> x. \<lbrakk>dfree ($' x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO ($' x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) \<nu>
 4. \<And>\<sigma> x. \<lbrakk>dfree (Var x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Var x) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) \<nu>
 5. \<And>\<sigma> r. \<lbrakk>dfree (Const r); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (TsubstFO (Const r) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
qed (auto simp add: TadmitFO.cases)


[STATEMENT]
lemma ntsubst_free_to_safe:
  "dfree \<theta> \<Longrightarrow> (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO \<theta> \<sigma>)
[PROOF STEP]
proof (induction rule: dfree.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args i) \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
[PROOF STEP]
case (dfree_Fun args i)
[PROOF STATE]
proof (state)
this:
dfree (args ?i7)
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dsafe (\<sigma> ?i7)

goal (5 subgoals):
 1. \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args i) \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree (args ?i7)
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dsafe (\<sigma> ?i7)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
dfree (args ?i7)
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. dsafe (TsubstFO ($f i args) \<sigma>)
[PROOF STEP]
by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free)
[PROOF STATE]
proof (state)
this:
dsafe (TsubstFO ($f i args) \<sigma>)

goal (4 subgoals):
 1. \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dfree \<theta>\<^sub>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
[PROOF STEP]
qed (auto intro: dsafe.intros)


[STATEMENT]
lemma ntsubst_preserves_safe:
"dsafe \<theta> \<Longrightarrow> (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dsafe \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO \<theta> \<sigma>)
[PROOF STEP]
proof (induction rule: dsafe.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args i) \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
case (dsafe_Fun args i)
[PROOF STATE]
proof (state)
this:
dsafe (args ?i7)
(\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dfree (\<sigma> ?i7)

goal (7 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args i) \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dsafe (args ?i7)
(\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dfree (\<sigma> ?i7)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
dsafe (args ?i7)
(\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (args ?i7) \<sigma>)
dfree (\<sigma> ?i7)

goal (1 subgoal):
 1. dsafe (TsubstFO ($f i args) \<sigma>)
[PROOF STEP]
by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free dfree_is_dsafe)
[PROOF STATE]
proof (state)
this:
dsafe (TsubstFO ($f i args) \<sigma>)

goal (6 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Differential \<theta>) \<sigma>)
 6. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Differential \<theta>) \<sigma>)
 6. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
case (dsafe_Diff \<theta>)
[PROOF STATE]
proof (state)
this:
dfree \<theta>
dfree (\<sigma> ?i7)

goal (6 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Differential \<theta>) \<sigma>)
 6. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>
dfree (\<sigma> ?i7)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
dfree (\<sigma> ?i7)

goal (1 subgoal):
 1. dsafe (TsubstFO (Differential \<theta>) \<sigma>)
[PROOF STEP]
by  (auto intro:dsafe.intros ntsubst_preserves_free)
[PROOF STATE]
proof (state)
this:
dsafe (TsubstFO (Differential \<theta>) \<sigma>)

goal (5 subgoals):
 1. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Var i) \<sigma>)
 2. \<And>r. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO \<theta>\<^sub>2 \<sigma>); \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>i. (\<And>i. dfree (\<sigma> i)) \<Longrightarrow> dsafe (TsubstFO ($' i) \<sigma>)
[PROOF STEP]
qed (auto simp add: ntsubst_preserves_free intro: dsafe.intros)


[STATEMENT]
lemma tsubst_preserves_safe:
"dsafe \<theta> \<Longrightarrow>  (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe(Tsubst \<theta> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst \<theta> \<sigma>)
[PROOF STEP]
proof (induction rule: dsafe.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
case (dsafe_Fun args i)
[PROOF STATE]
proof (state)
this:
dsafe (args ?i7)
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args ?i7) \<sigma>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7

goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
assume dsafes:"\<And>i. dsafe (args i)"
[PROOF STATE]
proof (state)
this:
dsafe (args ?i7)

goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
assume IH:"\<And>j. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args j) \<sigma>)"
[PROOF STATE]
proof (state)
this:
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args ?j7) \<sigma>)

goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
assume frees:"\<And>i f. SFunctions \<sigma> i = Some f \<Longrightarrow> dfree f"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> ?i7 = Some ?f7 \<Longrightarrow> dfree ?f7

goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
have IH':"\<And>i. dsafe (Tsubst (args i) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
using frees IH
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> ?i7 = Some ?f7 \<Longrightarrow> dfree ?f7
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args ?j7) \<sigma>)

goal (1 subgoal):
 1. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (Tsubst (args ?i7) \<sigma>)

goal (7 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>args i. \<lbrakk>\<And>i. dsafe (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args i) \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst ($f i args) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 6. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 7. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dsafe (Tsubst (args ?i7) \<sigma>)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
dsafe (Tsubst (args ?i7) \<sigma>)

goal (1 subgoal):
 1. dsafe (Tsubst ($f i args) \<sigma>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. dsafe (Tsubst (args i) \<sigma>)) \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
apply(cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
 2. \<And>a. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
using IH frees
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (args ?j7) \<sigma>)
SFunctions \<sigma> ?i7 = Some ?f7 \<Longrightarrow> dfree ?f7

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
using frees[of i a] ntsubst_free_to_safe[of a] IH'
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> i = Some a \<Longrightarrow> dfree a
\<lbrakk>dfree a; \<And>i. dsafe (?\<sigma> i)\<rbrakk> \<Longrightarrow> dsafe (TsubstFO a ?\<sigma>)
dsafe (Tsubst (args ?i7) \<sigma>)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (Tsubst (args i) \<sigma>); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> dsafe ((case SFunctions \<sigma> i of None \<Rightarrow> $f i | Some f' \<Rightarrow> TsubstFO f') (\<lambda>i. Tsubst (args i) \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
dsafe (Tsubst ($f i args) \<sigma>)

goal (6 subgoals):
 1. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Var i) \<sigma>)
 2. \<And>r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst (Const r) \<sigma>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dsafe \<theta>\<^sub>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>1 \<sigma>); dsafe \<theta>\<^sub>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst \<theta>\<^sub>2 \<sigma>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<sigma>)
 5. \<And>\<theta>. \<lbrakk>dfree \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dsafe (Tsubst (Differential \<theta>) \<sigma>)
 6. \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> dsafe (Tsubst ($' i) \<sigma>)
[PROOF STEP]
qed (auto intro: dsafe.intros tsubst_preserves_free)