[STATEMENT]
lemma uadmit_prog_ntadjoint:
  assumes TUA:"PUadmitFO \<sigma> \<alpha> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dfree:"\<And>i . dsafe (\<sigma> i)"
  assumes hpsafe:"hpsafe \<alpha>"
  assumes good_interp:"is_interp I"
  shows  "prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>
[PROOF STEP]
have sub:"(\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x)) \<subseteq> -U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
using TUA
[PROOF STATE]
proof (prove)
using this:
PUadmitFO \<sigma> \<alpha> U

goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
unfolding PUadmitFO_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inl (Inr i) \<in> SIGP \<alpha>}. FVT (\<sigma> i)) \<inter> U = {}

goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x)) \<subseteq> - U

goal (1 subgoal):
 1. prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))
[PROOF STEP]
using agree_sub[OF sub VA]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))

goal (1 subgoal):
 1. prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>
[PROOF STEP]
apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))
 2. hpsafe \<alpha>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGP \<alpha>}. FVT (\<sigma> x))
[PROOF STEP]
by (rule VA')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hpsafe \<alpha>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hpsafe \<alpha>
[PROOF STEP]
by (rule hpsafe)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
prog_sem (adjointFO I \<sigma> \<nu>) \<alpha> = prog_sem (adjointFO I \<sigma> \<omega>) \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uadmit_fml_ntadjoint:
  assumes TUA:"FUadmitFO \<sigma> \<phi> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dfree:"\<And>i . dsafe (\<sigma> i)"
  assumes fsafe:"fsafe \<phi>"
  assumes good_interp:"is_interp I"
  shows  "fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>
[PROOF STEP]
have sub:"(\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x)) \<subseteq> -U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
using TUA
[PROOF STATE]
proof (prove)
using this:
FUadmitFO \<sigma> \<phi> U

goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
unfolding FUadmitFO_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inl (Inr i) \<in> SIGF \<phi>}. FVT (\<sigma> i)) \<inter> U = {}

goal (1 subgoal):
 1. (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x)) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x)) \<subseteq> - U

goal (1 subgoal):
 1. fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))
[PROOF STEP]
using agree_sub[OF sub VA]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))

goal (1 subgoal):
 1. fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>
[PROOF STEP]
apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))
 2. fsafe \<phi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>x\<in>{x. Inl (Inr x) \<in> SIGF \<phi>}. FVT (\<sigma> x))
[PROOF STEP]
by (rule VA')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe \<phi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe \<phi>
[PROOF STEP]
by (rule fsafe)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fml_sem (adjointFO I \<sigma> \<nu>) \<phi> = fml_sem (adjointFO I \<sigma> \<omega>) \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (7 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>); NTUadmit \<sigma> \<theta> UNIV; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFFO \<sigma> (args i); \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (args i) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (args i) (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO ($f (Inl f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inl f) args) (fst \<nu>)
 3. \<And>\<sigma> args f. \<lbrakk>\<And>i. TadmitFFO \<sigma> (args i); \<And>i. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (args i) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (args i) (fst \<nu>); dfree (\<sigma> f); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO ($f (Inr f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inr f) args) (fst \<nu>)
 4. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFFO \<sigma> \<theta>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitFFO \<sigma> \<theta>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 5. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFFO \<sigma> \<theta>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitFFO \<sigma> \<theta>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 6. \<And>\<sigma> x. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (Var x) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) (fst \<nu>)
 7. \<And>\<sigma> r. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (Const r) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TadmitFFO \<sigma> (args ?i7)
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) (fst \<nu>)
dsafe (\<sigma> ?i7)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
TadmitFFO \<sigma> (args ?i7)
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (args ?i7) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (args ?i7) (fst \<nu>)
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. sterm_sem I (TsubstFO ($f (Inl f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inl f) args) (fst \<nu>)
[PROOF STEP]
by(auto simp add:  adjointFO_def)
[PROOF STATE]
proof (state)
this:
sterm_sem I (TsubstFO ($f (Inl f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inl f) args) (fst \<nu>)

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

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

goal (1 subgoal):
 1. sterm_sem I (TsubstFO ($f (Inr f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inr f) args) (fst \<nu>)
[PROOF STEP]
apply(auto simp add: adjointFO_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. TadmitFFO \<sigma> (args i); dfree (\<sigma> f); \<And>i. sterm_sem I (TsubstFO (args i) \<sigma>) (fst \<nu>) = sterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (\<sigma> f) (fst \<nu>) = dterm_sem I (\<sigma> f) \<nu>
[PROOF STEP]
by (simp add: dsem_to_ssem)
[PROOF STATE]
proof (state)
this:
sterm_sem I (TsubstFO ($f (Inr f) args) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) ($f (Inr f) args) (fst \<nu>)

goal (5 subgoals):
 1. \<And>\<sigma> \<theta>. \<lbrakk>TadmitFFO \<sigma> \<theta>; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>); NTUadmit \<sigma> \<theta> UNIV; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) (fst \<nu>)
 2. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFFO \<sigma> \<theta>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitFFO \<sigma> \<theta>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Plus \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) (fst \<nu>)
 3. \<And>\<sigma> \<theta>1 \<theta>2. \<lbrakk>TadmitFFO \<sigma> \<theta>1; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>1 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 (fst \<nu>); TadmitFFO \<sigma> \<theta>2; (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta>2 \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 (fst \<nu>); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO (Times \<theta>1 \<theta>2) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) (fst \<nu>)
 4. \<And>\<sigma> x. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (Var x) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) (fst \<nu>)
 5. \<And>\<sigma> r. (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO (Const r) \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) (Const r) (fst \<nu>)
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma nsubst_sterm':
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes a b::"'sz simple_state"
  shows "TadmitFFO \<sigma> \<theta> \<Longrightarrow> (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) a = sterm_sem (adjointFO I \<sigma> (a,b)) \<theta> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TadmitFFO \<sigma> \<theta>; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) a = sterm_sem (adjointFO I \<sigma> (a, b)) \<theta> a
[PROOF STEP]
using nsubst_sterm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>TadmitFFO ?\<sigma> ?\<theta>; \<And>i. dsafe (?\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem ?I (TsubstFO ?\<theta> ?\<sigma>) (fst ?\<nu>) = sterm_sem (adjointFO ?I ?\<sigma> ?\<nu>) ?\<theta> (fst ?\<nu>)

goal (1 subgoal):
 1. \<lbrakk>TadmitFFO \<sigma> \<theta>; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) a = sterm_sem (adjointFO I \<sigma> (a, b)) \<theta> a
[PROOF STEP]
by (metis fst_conv)


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

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

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

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


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

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

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

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