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

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TadmitF \<sigma> (args ?i7)
SFunctions \<sigma> f = Some f'
dfree (Tsubst (args ?i7) \<sigma>)
TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) (fst \<nu>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7
[PROOF STEP]
have subFree:" TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'"
      and frees:"\<And>i. dfree (Tsubst (args i) \<sigma>)"
      and TFA:"\<And>i. TadmitF \<sigma> (args i)"
      and NTFA:"TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'"
      and theIH:"\<And>i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>)"
[PROOF STATE]
proof (prove)
using this:
TadmitF \<sigma> (args ?i7)
SFunctions \<sigma> f = Some f'
dfree (Tsubst (args ?i7) \<sigma>)
TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) (fst \<nu>)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7

goal (1 subgoal):
 1. (TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f' &&& (\<And>i. dfree (Tsubst (args i) \<sigma>))) &&& (\<And>i. TadmitF \<sigma> (args i)) &&& TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f' &&& (\<And>i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
dfree (Tsubst (args ?i7) \<sigma>)
TadmitF \<sigma> (args ?i7)
TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
sterm_sem I (Tsubst (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) (fst \<nu>)

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

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

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
assume subFreeer:"(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f')"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
note admit = TadmitF_Fun1.hyps(1) and sfree = TadmitF_Fun1.prems(1)
[PROOF STATE]
proof (state)
this:
TadmitF \<sigma> (args ?i7)
SFunctions \<sigma> ?i7 = Some ?f'7 \<Longrightarrow> dfree ?f'7

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

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

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
have vec_eq:"(\<chi> i. sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>)) = (\<chi> i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>)) = (\<chi>i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>))
[PROOF STEP]
apply(rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>)) $ i = (\<chi>i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>)) $ i
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
sterm_sem I (Tsubst (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args ?i7) (fst \<nu>)

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

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
assume some:"SFunctions \<sigma> f = Some f'"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> f = Some f'

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
let ?sub = "(\<lambda> i. Tsubst (args i) \<sigma>)"
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
have IH2:"sterm_sem I (TsubstFO f' ?sub) (fst \<nu>) = sterm_sem (adjointFO I ?sub \<nu>) f' (fst \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (TsubstFO f' (\<lambda>i. Tsubst (args i) \<sigma>)) (fst \<nu>) = sterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' (fst \<nu>)
[PROOF STEP]
apply(rule nsubst_sterm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'
 2. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
apply(rule subFree)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dsafe (Tsubst (args i) \<sigma>)
[PROOF STEP]
by (rule safes)
[PROOF STATE]
proof (state)
this:
sterm_sem I (TsubstFO f' (\<lambda>i. Tsubst (args i) \<sigma>)) (fst \<nu>) = sterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' (fst \<nu>)

goal (8 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f f'. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = Some f'; \<And>i. dfree (Tsubst (args i) \<sigma>); TadmitFFO (\<lambda>i. Tsubst (args i) \<sigma>) f'; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 7. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 8. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
[PROOF STEP]
apply (simp add: some)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (TsubstFO f' (\<lambda>i. Tsubst (args i) \<sigma>)) (fst \<nu>) = Functions (local.adjoint I \<sigma> \<nu>) f (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>))
[PROOF STEP]
unfolding vec_eq IH2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (adjointFO I (\<lambda>i. Tsubst (args i) \<sigma>) \<nu>) f' (fst \<nu>) = Functions (local.adjoint I \<sigma> \<nu>) f (\<chi>i. sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>))
[PROOF STEP]
by (auto simp add: some adjoint_free[OF subFreeer, of \<sigma> "(\<lambda> x y. x)" I \<nu>] adjointFO_free[OF frees])
[PROOF STATE]
proof (state)
this:
sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)

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

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 7. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
assume none:"SFunctions \<sigma> f = None"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> f = None

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

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

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

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

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitF \<sigma> (args i); \<And>i. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (args i) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (args i) (fst \<nu>); SFunctions \<sigma> f = None; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 7. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)
[PROOF STEP]
by(auto simp add: none IH adjoint_def vec_extensionality eqs)
[PROOF STATE]
proof (state)
this:
sterm_sem I (Tsubst ($f f args) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($f f args) (fst \<nu>)

goal (6 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitF \<sigma> \<theta>; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>); TUadmit \<sigma> \<theta> UNIV; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitF \<sigma> \<theta>1; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitF \<sigma> \<theta>2; (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 4. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst ($' x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) (fst \<nu>)
 5. \<And>\<sigma> x. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Var x) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) (fst \<nu>)
 6. \<And>\<sigma> r. (\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> sterm_sem I (Tsubst (Const r) \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
qed auto