[STATEMENT]
lemma subst_dterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "
    Tadmit \<sigma> \<theta> \<Longrightarrow>
    dsafe \<theta> \<Longrightarrow>
    (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow>
    (\<And>f f'. SPredicates \<sigma> f = Some f'  \<Longrightarrow> fsafe f') \<Longrightarrow>
    (\<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (adjoint I \<sigma> \<nu>) \<theta> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tadmit \<sigma> \<theta>; dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> (\<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>)
[PROOF STEP]
proof (induction rule: Tadmit.induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
case (Tadmit_Fun1 \<sigma> args f f' \<nu>)
[PROOF STATE]
proof (state)
this:
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = Some f'
TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
\<lbrakk>dsafe (args ?i7); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) (args ?i7) ?\<nu>7
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
note safe = Tadmit_Fun1.prems(1) and sfree = Tadmit_Fun1.prems(2) and TA = Tadmit_Fun1.hyps(1)
    and some = Tadmit_Fun1.hyps(2) and NTA = Tadmit_Fun1.hyps(3)
[PROOF STATE]
proof (state)
this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = Some f'
TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
hence safes:"\<And>i. dsafe (args i)"
[PROOF STATE]
proof (prove)
using this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = Some f'
TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'

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

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have IH:"(\<And>\<nu>'. \<And>i. dsafe (args i) \<Longrightarrow>
      dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (adjoint I \<sigma> \<nu>) (args i) \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>' i. dsafe (args i) \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
using  Tadmit_Fun1.prems Tadmit_Fun1.IH
[PROOF STATE]
proof (prove)
using this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
\<lbrakk>dsafe (args ?i7); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) (args ?i7) ?\<nu>7

goal (1 subgoal):
 1. \<And>\<nu>' i. dsafe (args i) \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (args ?i7) \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) \<nu>

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have eqs:"\<And>i \<nu>'. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (adjoint I \<sigma> \<nu>) (args i) \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i \<nu>'. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by (auto simp add: IH safes)
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst (args ?i8) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i8) \<nu>

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
let ?sub = "(\<lambda> i. Tsubst (args i) \<sigma>)"
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have subSafe:"(\<And>i. dsafe (?sub i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
using tsubst_preserves_safe[OF safes sfree]
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i8 i f') = Some f') \<Longrightarrow> dsafe (Tsubst (args ?i16) ?\<sigma>)

goal (1 subgoal):
 1. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
by (simp add: safes sfree tsubst_preserves_safe)
[PROOF STATE]
proof (state)
this:
dsafe (Tsubst (args ?i9) \<sigma>)

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have freef:"dfree f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree f'
[PROOF STEP]
using sfree some
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SFunctions \<sigma> f = Some f'

goal (1 subgoal):
 1. dfree f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfree f'

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have IH2:"dterm_sem I (TsubstFO f' ?sub) \<nu> = dterm_sem (adjointFO I ?sub \<nu>) f' \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (TsubstFO f' (\<lambda>i. Tsubst (args i) \<sigma>)) \<nu> = dterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' \<nu>
[PROOF STEP]
by (simp add: nsubst_dterm'[OF good_interp NTA freef subSafe])
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO f' (\<lambda>i. Tsubst (args i) \<sigma>)) \<nu> = dterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' \<nu>

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have vec:"(\<chi> i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi> i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
apply(auto simp add: vec_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
using IH[of i, OF safes[of i]]
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>

goal (1 subgoal):
 1. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<chi>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)

goal (8 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f f' \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = Some f'; TadmitFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 7. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 8. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
using IH safes eqs
[PROOF STATE]
proof (prove)
using this:
dsafe (args ?i7) \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) \<nu>
dsafe (args ?i7)
dterm_sem I (Tsubst (args ?i8) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i8) \<nu>

goal (1 subgoal):
 1. dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
apply (auto simp add:  IH2  some good_interp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (args i); \<And>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' \<nu> = Functions (local.adjoint I \<sigma> \<nu>) f (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
using some
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> f = Some f'

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (args i); \<And>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' \<nu> = Functions (local.adjoint I \<sigma> \<nu>) f (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
unfolding adjoint_def adjointFO_def
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> f = Some f'

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dsafe (args i); \<And>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (args i) \<nu>\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (Tsubst (args f') \<sigma>) \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> f' \<nu> = Functions \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> f (\<chi>i. dterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (args i) \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
case (Tadmit_Fun2 \<sigma> args f \<nu>)
[PROOF STATE]
proof (state)
this:
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = None
\<lbrakk>dsafe (args ?i7); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) (args ?i7) ?\<nu>7
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
note safe = Tadmit_Fun2.prems(1) and sfree = Tadmit_Fun2.prems(2) and TA = Tadmit_Fun2.hyps(1)
  and none = Tadmit_Fun2.hyps(2)
[PROOF STATE]
proof (state)
this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = None

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
hence safes:"\<And>i. dsafe (args i)"
[PROOF STATE]
proof (prove)
using this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
Tadmit \<sigma> (args ?i7)
SFunctions \<sigma> f = None

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

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have IH:"(\<And>\<nu>'. \<And>i. dsafe (args i) \<Longrightarrow>
      dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (adjoint I \<sigma> \<nu>) (args i) \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>' i. dsafe (args i) \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
using  Tadmit_Fun2.prems Tadmit_Fun2.IH
[PROOF STATE]
proof (prove)
using this:
dsafe ($f f args)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
\<lbrakk>dsafe (args ?i7); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) (args ?i7) ?\<nu>7

goal (1 subgoal):
 1. \<And>\<nu>' i. dsafe (args i) \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (args ?i7) \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) \<nu>

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have Ieq:"Functions I f = Functions (adjoint I \<sigma> \<nu>) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functions I f = Functions (local.adjoint I \<sigma> \<nu>) f
[PROOF STEP]
using none
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> f = None

goal (1 subgoal):
 1. Functions I f = Functions (local.adjoint I \<sigma> \<nu>) f
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> f = None

goal (1 subgoal):
 1. Functions I f = Functions \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Functions I f = Functions (local.adjoint I \<sigma> \<nu>) f

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have vec:"(\<chi> i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi> i. dterm_sem (adjoint I \<sigma> \<nu>) (args i) \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
apply(auto simp add: vec_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
using IH[of i, OF safes[of i]]
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>

goal (1 subgoal):
 1. dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<chi>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)

goal (7 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> args f \<nu>. \<lbrakk>\<And>i. Tadmit \<sigma> (args i); \<And>i \<nu>. \<lbrakk>dsafe (args i); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (args i) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>; SFunctions \<sigma> f = None; dsafe ($f f args); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 6. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 7. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
using none IH Ieq vec
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> f = None
dsafe (args ?i7) \<Longrightarrow> dterm_sem I (Tsubst (args ?i7) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) \<nu>
Functions I f = Functions (local.adjoint I \<sigma> \<nu>) f
(\<chi>i. dterm_sem I (Tsubst (args i) \<sigma>) \<nu>) = (\<chi>i. dterm_sem (local.adjoint I \<sigma> \<nu>) (args i) \<nu>)

goal (1 subgoal):
 1. dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst ($f f args) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) \<nu>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
case (Tadmit_Diff \<sigma> \<theta>)
[PROOF STATE]
proof (state)
this:
Tadmit \<sigma> \<theta>
TUadmit \<sigma> \<theta> UNIV
\<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) \<theta> ?\<nu>7
dsafe (Differential \<theta>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Tadmit \<sigma> \<theta>
TUadmit \<sigma> \<theta> UNIV
\<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) \<theta> ?\<nu>7
dsafe (Differential \<theta>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
[PROOF STEP]
have TA:"Tadmit \<sigma> \<theta>"
    and TUA:"TUadmit \<sigma> \<theta> UNIV"
    and IH:"dsafe \<theta> \<Longrightarrow> (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> (\<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>)"
    and safe:"dsafe (Differential \<theta>)"
    and sfree:"\<And>i f'1. SFunctions \<sigma> i = Some f'1 \<Longrightarrow> dfree f'1"
    and spsafe:"\<And>f f'. SPredicates \<sigma> f = Some f'  \<Longrightarrow> fsafe f'"
[PROOF STATE]
proof (prove)
using this:
Tadmit \<sigma> \<theta>
TUadmit \<sigma> \<theta> UNIV
\<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) \<theta> ?\<nu>7
dsafe (Differential \<theta>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (1 subgoal):
 1. (Tadmit \<sigma> \<theta> &&& TUadmit \<sigma> \<theta> UNIV &&& (\<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> (\<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>))) &&& dsafe (Differential \<theta>) &&& (\<And>i f'1. SFunctions \<sigma> i = Some f'1 \<Longrightarrow> dfree f'1) &&& (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Tadmit \<sigma> \<theta>
TUadmit \<sigma> \<theta> UNIV
\<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) \<theta> ?\<nu>7
dsafe (Differential \<theta>)
SFunctions \<sigma> ?i7 = Some ?f'1.7 \<Longrightarrow> dfree ?f'1.7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
from sfree
[PROOF STATE]
proof (chain)
picking this:
SFunctions \<sigma> ?i7 = Some ?f'1.7 \<Longrightarrow> dfree ?f'1.7
[PROOF STEP]
have sdsafe:"\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'"
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> ?i7 = Some ?f'1.7 \<Longrightarrow> dfree ?f'1.7

goal (1 subgoal):
 1. \<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'
[PROOF STEP]
using dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> ?i7 = Some ?f'1.7 \<Longrightarrow> dfree ?f'1.7
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

goal (1 subgoal):
 1. \<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> dsafe ?f'7

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have VA:"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (-UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<omega>. Vagree \<nu> \<omega> (- UNIV)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<omega>. (\<forall>i. Inl i \<in> - UNIV \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> - UNIV \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree ?\<nu>7 ?\<omega>7 (- UNIV)

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
from safe
[PROOF STATE]
proof (chain)
picking this:
dsafe (Differential \<theta>)
[PROOF STEP]
have free:"dfree \<theta>"
[PROOF STATE]
proof (prove)
using this:
dsafe (Differential \<theta>)

goal (1 subgoal):
 1. dfree \<theta>
[PROOF STEP]
by (auto dest: dsafe.cases intro: dfree.intros)
[PROOF STATE]
proof (state)
this:
dfree \<theta>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
from free
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>
[PROOF STEP]
have tsafe:"dsafe \<theta>"
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>

goal (1 subgoal):
 1. dsafe \<theta>
[PROOF STEP]
using dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

goal (1 subgoal):
 1. dsafe \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe \<theta>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have freeSubst:"dfree (Tsubst \<theta> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree (Tsubst \<theta> \<sigma>)
[PROOF STEP]
using tsubst_preserves_free[OF free sfree]
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i8 i f') = Some f') \<Longrightarrow> dfree (Tsubst \<theta> ?\<sigma>)

goal (1 subgoal):
 1. dfree (Tsubst \<theta> \<sigma>)
[PROOF STEP]
using Tadmit_Diff.prems(2) free tsubst_preserves_free
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i8 i f') = Some f') \<Longrightarrow> dfree (Tsubst \<theta> ?\<sigma>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
dfree \<theta>
\<lbrakk>dfree ?\<theta>; \<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dfree (Tsubst ?\<theta> ?\<sigma>)

goal (1 subgoal):
 1. dfree (Tsubst \<theta> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dfree (Tsubst \<theta> \<sigma>)

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have IH':"\<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>
[PROOF STEP]
using IH[OF tsafe sfree]
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i15 i f') = Some f') \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>7 = dterm_sem (local.adjoint I \<sigma> ?\<nu>7) \<theta> ?\<nu>7

goal (1 subgoal):
 1. \<And>\<nu>. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>8 = dterm_sem (local.adjoint I \<sigma> ?\<nu>8) \<theta> ?\<nu>8

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have sem_eq:"\<And>\<nu>'. dsafe \<theta> \<Longrightarrow> is_interp I \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>'. \<lbrakk>dsafe \<theta>; is_interp I\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>
[PROOF STEP]
subgoal for \<nu>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dsafe \<theta>; is_interp I\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>
[PROOF STEP]
using uadmit_dterm_adjoint[OF TUA VA sfree spsafe, of "(\<lambda> x y. x)" "(\<lambda> x y. x)" I \<nu> \<nu>']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> SFunctions \<sigma> f = Some f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> SPredicates \<sigma> f = Some f'; dsafe \<theta>; is_interp I\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>

goal (1 subgoal):
 1. \<lbrakk>dsafe \<theta>; is_interp I\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>dsafe \<theta>; is_interp I\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> ?\<nu>'8) \<theta>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have IH'':"\<And>\<nu>'. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>'. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
subgoal for \<nu>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
using sem_eq[OF tsafe good_interp, of \<nu>'] IH'[of \<nu>']
[PROOF STATE]
proof (prove)
using this:
dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta>
dterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = dterm_sem (local.adjoint I \<sigma> \<nu>') \<theta> \<nu>'

goal (1 subgoal):
 1. dterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>'8 = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> ?\<nu>'8

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
have sem_eq:"sterm_sem I (Tsubst \<theta> \<sigma>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (Tsubst \<theta> \<sigma>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>
[PROOF STEP]
apply (auto simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. sterm_sem I (Tsubst \<theta> \<sigma>) x = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
subgoal for \<nu>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
apply (cases "\<nu>'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<nu>' = vec_lambda y; y \<in> UNIV\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
subgoal for \<nu>''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nu>' = vec_lambda \<nu>''; \<nu>'' \<in> UNIV\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) \<nu>' = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' = vec_lambda \<nu>'' \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'')
[PROOF STEP]
using dsem_to_ssem[OF free, of "(local.adjoint I \<sigma> \<nu>)" "(\<nu>',\<nu>')"] dsem_to_ssem[OF freeSubst, of I "(\<nu>',\<nu>')"] IH'[of "(\<nu>)"]
[PROOF STATE]
proof (prove)
using this:
dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (\<nu>', \<nu>') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst (\<nu>', \<nu>'))
dterm_sem I (Tsubst \<theta> \<sigma>) (\<nu>', \<nu>') = sterm_sem I (Tsubst \<theta> \<sigma>) (fst (\<nu>', \<nu>'))
dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>

goal (1 subgoal):
 1. \<nu>' = vec_lambda \<nu>'' \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nu>' = vec_lambda \<nu>''; dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'', vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>''); dterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'', vec_lambda \<nu>'') = sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>''); dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'')
[PROOF STEP]
using IH''
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (Tsubst \<theta> \<sigma>) ?\<nu>'8 = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> ?\<nu>'8

goal (1 subgoal):
 1. \<lbrakk>\<nu>' = vec_lambda \<nu>''; dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'', vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>''); dterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'', vec_lambda \<nu>'') = sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>''); dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (vec_lambda \<nu>'') = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (vec_lambda \<nu>'')
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sterm_sem I (Tsubst \<theta> \<sigma>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>

goal (6 subgoals):
 1. \<And>\<sigma> \<theta> \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>; \<And>\<nu>. \<lbrakk>dsafe \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta> \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> \<nu>; TUadmit \<sigma> \<theta> UNIV; dsafe (Differential \<theta>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 5. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 6. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>
[PROOF STEP]
apply (auto simp add: directional_derivative_def fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet I (Tsubst \<theta> \<sigma>) (fst \<nu>) (snd \<nu>) = frechet (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>) (snd \<nu>)
[PROOF STEP]
using sterm_determines_frechet[OF
        good_interp
        adjoint_safe[OF good_interp sfree]
        tsubst_preserves_free[OF free sfree]
        free sem_eq]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i18 i f') = Some f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> SFunctions \<sigma> (?i9 i f') = Some f'\<rbrakk> \<Longrightarrow> frechet I (Tsubst \<theta> \<sigma>) (fst ?\<nu>) (snd ?\<nu>) = frechet (local.adjoint I \<sigma> \<nu>) \<theta> (fst ?\<nu>) (snd ?\<nu>)

goal (1 subgoal):
 1. frechet I (Tsubst \<theta> \<sigma>) (fst \<nu>) (snd \<nu>) = frechet (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>) (snd \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (Tsubst (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) \<nu>

goal (5 subgoals):
 1. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Plus \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) \<nu>
 2. \<And>\<sigma> \<theta>1 \<theta>2 \<nu>. \<lbrakk>Tadmit \<sigma> \<theta>1; \<And>\<nu>. \<lbrakk>dsafe \<theta>1; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>1 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 \<nu>; Tadmit \<sigma> \<theta>2; \<And>\<nu>. \<lbrakk>dsafe \<theta>2; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst \<theta>2 \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 \<nu>; dsafe (Times \<theta>1 \<theta>2); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) \<nu>
 3. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe ($' x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst ($' x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) \<nu>
 4. \<And>\<sigma> x \<nu>. \<lbrakk>dsafe (Var x); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Var x) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) \<nu>
 5. \<And>\<sigma> r \<nu>. \<lbrakk>dsafe (Const r); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'\<rbrakk> \<Longrightarrow> dterm_sem I (Tsubst (Const r) \<sigma>) \<nu> = dterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) \<nu>
[PROOF STEP]
qed auto