[STATEMENT]
lemma osubst_preserves_safe:
  assumes ssafe:"ssafe \<sigma>"
  shows "(osafe ODE \<Longrightarrow> Oadmit \<sigma> ODE U \<Longrightarrow> osafe (Osubst ODE \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>osafe ODE; Oadmit \<sigma> ODE U\<rbrakk> \<Longrightarrow> osafe (Osubst ODE \<sigma>)
[PROOF STEP]
proof (induction rule: osafe.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c. Oadmit \<sigma> (OVar c) U \<Longrightarrow> osafe (Osubst (OVar c) \<sigma>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; Oadmit \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OSing x \<theta>) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Var c)
[PROOF STATE]
proof (state)
this:
Oadmit \<sigma> (OVar c) U

goal (3 subgoals):
 1. \<And>c. Oadmit \<sigma> (OVar c) U \<Longrightarrow> osafe (Osubst (OVar c) \<sigma>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; Oadmit \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OSing x \<theta>) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Oadmit \<sigma> (OVar c) U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Oadmit \<sigma> (OVar c) U

goal (1 subgoal):
 1. osafe (Osubst (OVar c) \<sigma>)
[PROOF STEP]
using ssafe
[PROOF STATE]
proof (prove)
using this:
Oadmit \<sigma> (OVar c) U
ssafe \<sigma>

goal (1 subgoal):
 1. osafe (Osubst (OVar c) \<sigma>)
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
Oadmit \<sigma> (OVar c) U
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. osafe (Osubst (OVar c) \<sigma>)
[PROOF STEP]
by (cases "SODEs \<sigma> c", auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (Osubst (OVar c) \<sigma>)

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; Oadmit \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; Oadmit \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Sing \<theta> x)
[PROOF STATE]
proof (state)
this:
dfree \<theta>
Oadmit \<sigma> (OSing x \<theta>) U

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; Oadmit \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>
Oadmit \<sigma> (OSing x \<theta>) U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
Oadmit \<sigma> (OSing x \<theta>) U

goal (1 subgoal):
 1. osafe (Osubst (OSing x \<theta>) \<sigma>)
[PROOF STEP]
using tsubst_preserves_free ssafe
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
Oadmit \<sigma> (OSing x \<theta>) U
\<lbrakk>dfree ?\<theta>; \<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dfree (Tsubst ?\<theta> ?\<sigma>)
ssafe \<sigma>

goal (1 subgoal):
 1. osafe (Osubst (OSing x \<theta>) \<sigma>)
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
Oadmit \<sigma> (OSing x \<theta>) U
\<lbrakk>dfree ?\<theta>; \<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> dfree (Tsubst ?\<theta> ?\<sigma>)
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. osafe (Osubst (OSing x \<theta>) \<sigma>)
[PROOF STEP]
by (auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (Osubst (OSing x \<theta>) \<sigma>)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Prod ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>)
Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>)
Oadmit \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>)
Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>)
Oadmit \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
have "Oadmit \<sigma> ODE1 U" "Oadmit \<sigma> ODE2 U" "ODE_dom (Osubst ODE1 \<sigma>) \<inter>  ODE_dom (Osubst ODE2 \<sigma>) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Oadmit \<sigma> ODE1 U &&& Oadmit \<sigma> ODE2 U &&& ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}
[PROOF STEP]
using osafe_Prod.prems
[PROOF STATE]
proof (prove)
using this:
Oadmit \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. Oadmit \<sigma> ODE1 U &&& Oadmit \<sigma> ODE2 U &&& ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}
[PROOF STEP]
by (auto dest: Oadmit.cases)
[PROOF STATE]
proof (state)
this:
Oadmit \<sigma> ODE1 U
Oadmit \<sigma> ODE2 U
ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>); osafe ODE2; Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; Oadmit \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>)
Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>)
Oadmit \<sigma> (OProd ODE1 ODE2) U
Oadmit \<sigma> ODE1 U
Oadmit \<sigma> ODE2 U
ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
Oadmit \<sigma> ODE1 U \<Longrightarrow> osafe (Osubst ODE1 \<sigma>)
Oadmit \<sigma> ODE2 U \<Longrightarrow> osafe (Osubst ODE2 \<sigma>)
Oadmit \<sigma> (OProd ODE1 ODE2) U
Oadmit \<sigma> ODE1 U
Oadmit \<sigma> ODE2 U
ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}

goal (1 subgoal):
 1. osafe (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
by (auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (Osubst (OProd ODE1 ODE2) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nosubst_preserves_safe:
  assumes sfree:"\<And>i. dfree (\<sigma> i)"
  fixes \<alpha> ::"('a + 'd, 'b, 'c) hp" and \<phi> ::"('a + 'd, 'b, 'c) formula"
  shows "(osafe ODE \<Longrightarrow> OUadmitFO \<sigma> ODE U \<Longrightarrow> osafe (OsubstFO ODE \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>osafe ODE; OUadmitFO \<sigma> ODE U\<rbrakk> \<Longrightarrow> osafe (OsubstFO ODE \<sigma>)
[PROOF STEP]
proof (induction rule: osafe.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c. OUadmitFO \<sigma> (OVar c) U \<Longrightarrow> osafe (OsubstFO (OVar c) \<sigma>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OUadmitFO \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OSing x \<theta>) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Var c)
[PROOF STATE]
proof (state)
this:
OUadmitFO \<sigma> (OVar c) U

goal (3 subgoals):
 1. \<And>c. OUadmitFO \<sigma> (OVar c) U \<Longrightarrow> osafe (OsubstFO (OVar c) \<sigma>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OUadmitFO \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OSing x \<theta>) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
OUadmitFO \<sigma> (OVar c) U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
OUadmitFO \<sigma> (OVar c) U

goal (1 subgoal):
 1. osafe (OsubstFO (OVar c) \<sigma>)
[PROOF STEP]
by (auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (OsubstFO (OVar c) \<sigma>)

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OUadmitFO \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OUadmitFO \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Sing \<theta> x)
[PROOF STATE]
proof (state)
this:
dfree \<theta>
OUadmitFO \<sigma> (OSing x \<theta>) U

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OUadmitFO \<sigma> (OSing x \<theta>) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OSing x \<theta>) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>
OUadmitFO \<sigma> (OSing x \<theta>) U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
OUadmitFO \<sigma> (OSing x \<theta>) U

goal (1 subgoal):
 1. osafe (OsubstFO (OSing x \<theta>) \<sigma>)
[PROOF STEP]
using sfree ntsubst_preserves_free[of \<theta> \<sigma>]
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
OUadmitFO \<sigma> (OSing x \<theta>) U
dfree (\<sigma> ?i7)
\<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)

goal (1 subgoal):
 1. osafe (OsubstFO (OSing x \<theta>) \<sigma>)
[PROOF STEP]
unfolding OUadmitFO_def
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
(\<Union>i\<in>{i. Inl (Inr i) \<in> SIGO (OSing x \<theta>)}. FVT (\<sigma> i)) \<inter> U = {}
dfree (\<sigma> ?i7)
\<lbrakk>dfree \<theta>; \<And>i. dfree (\<sigma> i)\<rbrakk> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)

goal (1 subgoal):
 1. osafe (OsubstFO (OSing x \<theta>) \<sigma>)
[PROOF STEP]
by (auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (OsubstFO (OSing x \<theta>) \<sigma>)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (osafe_Prod ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>)
OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>)
OUadmitFO \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
assume safe1:"osafe ODE1"
    and safe2:"osafe ODE2"
    and disj:"ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}"
    and IH1:"OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>)"
    and IH2:"OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>)"
    and NOUA:"OUadmitFO \<sigma> (OProd ODE1 ODE2) U"
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>)
OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>)
OUadmitFO \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
have nosubst_preserves_ODE_dom:"\<And>ODE. ODE_dom (OsubstFO ODE \<sigma>) = ODE_dom ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ODE. ODE_dom (OsubstFO ODE \<sigma>) = ODE_dom ODE
[PROOF STEP]
subgoal for ODE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_dom (OsubstFO ODE \<sigma>) = ODE_dom ODE
[PROOF STEP]
apply(induction "ODE")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ODE_dom (OsubstFO (OVar x) \<sigma>) = ODE_dom (OVar x)
 2. \<And>x1a x2. ODE_dom (OsubstFO (OSing x1a x2) \<sigma>) = ODE_dom (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_dom (OsubstFO ODE1 \<sigma>) = ODE_dom ODE1; ODE_dom (OsubstFO ODE2 \<sigma>) = ODE_dom ODE2\<rbrakk> \<Longrightarrow> ODE_dom (OsubstFO (OProd ODE1 ODE2) \<sigma>) = ODE_dom (OProd ODE1 ODE2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ODE_dom (OsubstFO ?ODE7 \<sigma>) = ODE_dom ?ODE7

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
have disj':"ODE_dom (OsubstFO ODE1 \<sigma>) \<inter> ODE_dom (OsubstFO ODE2 \<sigma>) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_dom (OsubstFO ODE1 \<sigma>) \<inter> ODE_dom (OsubstFO ODE2 \<sigma>) = {}
[PROOF STEP]
using disj nosubst_preserves_ODE_dom
[PROOF STATE]
proof (prove)
using this:
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
ODE_dom (OsubstFO ?ODE7 \<sigma>) = ODE_dom ?ODE7

goal (1 subgoal):
 1. ODE_dom (OsubstFO ODE1 \<sigma>) \<inter> ODE_dom (OsubstFO ODE2 \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_dom (OsubstFO ODE1 \<sigma>) \<inter> ODE_dom (OsubstFO ODE2 \<sigma>) = {}

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
from NOUA
[PROOF STATE]
proof (chain)
picking this:
OUadmitFO \<sigma> (OProd ODE1 ODE2) U
[PROOF STEP]
have NOUA1:"OUadmitFO \<sigma> ODE1 U" and NOUA2:"OUadmitFO \<sigma>  ODE2 U"
[PROOF STATE]
proof (prove)
using this:
OUadmitFO \<sigma> (OProd ODE1 ODE2) U

goal (1 subgoal):
 1. OUadmitFO \<sigma> ODE1 U &&& OUadmitFO \<sigma> ODE2 U
[PROOF STEP]
unfolding OUadmitFO_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inl (Inr i) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> i)) \<inter> U = {}

goal (1 subgoal):
 1. (\<Union>i\<in>{i. Inl (Inr i) \<in> SIGO ODE1}. FVT (\<sigma> i)) \<inter> U = {} &&& (\<Union>i\<in>{i. Inl (Inr i) \<in> SIGO ODE2}. FVT (\<sigma> i)) \<inter> U = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
OUadmitFO \<sigma> ODE1 U
OUadmitFO \<sigma> ODE2 U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; OUadmitFO \<sigma> ODE1 U \<Longrightarrow> osafe (OsubstFO ODE1 \<sigma>); osafe ODE2; OUadmitFO \<sigma> ODE2 U \<Longrightarrow> osafe (OsubstFO ODE2 \<sigma>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OUadmitFO \<sigma> (OProd ODE1 ODE2) U\<rbrakk> \<Longrightarrow> osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
OUadmitFO \<sigma> ODE1 U
OUadmitFO \<sigma> ODE2 U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
OUadmitFO \<sigma> ODE1 U
OUadmitFO \<sigma> ODE2 U

goal (1 subgoal):
 1. osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
using IH1[OF NOUA1] IH2[OF NOUA2] disj'
[PROOF STATE]
proof (prove)
using this:
OUadmitFO \<sigma> ODE1 U
OUadmitFO \<sigma> ODE2 U
osafe (OsubstFO ODE1 \<sigma>)
osafe (OsubstFO ODE2 \<sigma>)
ODE_dom (OsubstFO ODE1 \<sigma>) \<inter> ODE_dom (OsubstFO ODE2 \<sigma>) = {}

goal (1 subgoal):
 1. osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
by (auto intro: osafe.intros)
[PROOF STATE]
proof (state)
this:
osafe (OsubstFO (OProd ODE1 ODE2) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

goal (1 subgoal):
 1. dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> directional_derivative I (TsubstFO \<theta> \<sigma>) \<nu> = directional_derivative (adjointFO I \<sigma> \<nu>) \<theta> \<nu>
[PROOF STEP]
apply (unfold directional_derivative_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> frechet I (TsubstFO \<theta> \<sigma>) (fst \<nu>) (snd \<nu>) = frechet (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>) (snd \<nu>)
[PROOF STEP]
apply (rule sterm_determines_frechet)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. dfree \<theta> \<Longrightarrow> is_interp I
 2. dfree \<theta> \<Longrightarrow> is_interp (adjointFO I \<sigma> \<nu>)
 3. dfree \<theta> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)
 4. dfree \<theta> \<Longrightarrow> dfree \<theta>
 5. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> is_interp I
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> is_interp I
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. dfree \<theta> \<Longrightarrow> is_interp (adjointFO I \<sigma> \<nu>)
 2. dfree \<theta> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)
 3. dfree \<theta> \<Longrightarrow> dfree \<theta>
 4. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> is_interp (adjointFO I \<sigma> \<nu>)
[PROOF STEP]
using adjointFO_safe[OF good_interp, of \<sigma>] subSafe
[PROOF STATE]
proof (prove)
using this:
(\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> is_interp (adjointFO I \<sigma> ?\<nu>)
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> is_interp (adjointFO I \<sigma> \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dfree \<theta> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)
 2. dfree \<theta> \<Longrightarrow> dfree \<theta>
 3. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)
[PROOF STEP]
using substFree
[PROOF STATE]
proof (prove)
using this:
dfree (TsubstFO \<theta> \<sigma>)

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> dfree (TsubstFO \<theta> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dfree \<theta> \<Longrightarrow> dfree \<theta>
 2. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> dfree \<theta>
[PROOF STEP]
using dfree
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> dfree \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
using nsubst_sterm'[of  \<sigma> \<theta> I "(fst \<nu>)" "(snd \<nu>)", OF NTFA subSafe]
[PROOF STATE]
proof (prove)
using this:
sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> (fst \<nu>, snd \<nu>)) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
assume sem:"sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)"
[PROOF STATE]
proof (state)
this:
sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
have VA:"\<And>\<nu> \<omega>. Vagree \<nu> (x,snd \<nu>) (-UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<omega>. Vagree \<nu> (x, snd \<nu>) (- UNIV)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<omega>. (\<forall>i. Inl i \<in> - UNIV \<longrightarrow> fst \<nu> $ i = fst (x, snd \<nu>) $ i) \<and> (\<forall>i. Inr i \<in> - UNIV \<longrightarrow> snd \<nu> $ i = snd (x, snd \<nu>) $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree ?\<nu>7 (x, snd ?\<nu>7) (- UNIV)

goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)\<rbrakk> \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
show "sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
using uadmit_sterm_ntadjoint[OF NTU VA subSafe, OF  good_interp, of "(x, snd \<nu>)"]
            nsubst_sterm[OF NTFA subSafe, of I \<nu> ]
[PROOF STATE]
proof (prove)
using this:
sterm_sem (adjointFO I \<sigma> (x, snd \<nu>)) \<theta> = sterm_sem (adjointFO I \<sigma> (x, snd (x, snd \<nu>))) \<theta>
sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>) \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
using NTU VA dfree_is_dsafe  dsafe subSafe substFree good_interp uadmit_sterm_ntadjoint
[PROOF STATE]
proof (prove)
using this:
NTUadmit \<sigma> \<theta> UNIV
Vagree ?\<nu>7 (x, snd ?\<nu>7) (- UNIV)
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>
dsafe (Differential \<theta>)
dsafe (\<sigma> ?i7)
dfree (TsubstFO \<theta> \<sigma>)
is_interp I
\<lbrakk>NTUadmit ?\<sigma> ?\<theta> ?U; Vagree ?\<nu> ?\<omega> (- ?U); \<And>i. dsafe (?\<sigma> i); is_interp ?I\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO ?I ?\<sigma> ?\<nu>) ?\<theta> = sterm_sem (adjointFO ?I ?\<sigma> ?\<omega>) ?\<theta>

goal (1 subgoal):
 1. sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>) \<Longrightarrow> sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x
[PROOF STEP]
by (metis NTFA fst_eqD nsubst_sterm)
[PROOF STATE]
proof (state)
this:
sterm_sem I (TsubstFO \<theta> \<sigma>) x = sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO (Differential \<theta>) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) \<nu>

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

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

goal (1 subgoal):
 1. dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; \<forall>x. dsafe (args x); \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> dterm_sem I (case f of Inl f' \<Rightarrow> $f f' (\<lambda>i. TsubstFO (args i) \<sigma>) | Inr f' \<Rightarrow> \<sigma> f') \<nu> = Functions (adjointFO I \<sigma> \<nu>) f (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
apply(cases f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; \<forall>x. dsafe (args x); \<And>i. dsafe (\<sigma> i); f = Inl a\<rbrakk> \<Longrightarrow> dterm_sem I (case f of Inl f' \<Rightarrow> $f f' (\<lambda>i. TsubstFO (args i) \<sigma>) | Inr f' \<Rightarrow> \<sigma> f') \<nu> = Functions (adjointFO I \<sigma> \<nu>) f (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>)
 2. \<And>b. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>; \<forall>x. dsafe (args x); \<And>i. dsafe (\<sigma> i); f = Inr b\<rbrakk> \<Longrightarrow> dterm_sem I (case f of Inl f' \<Rightarrow> $f f' (\<lambda>i. TsubstFO (args i) \<sigma>) | Inr f' \<Rightarrow> \<sigma> f') \<nu> = Functions (adjointFO I \<sigma> \<nu>) f (\<chi>i. dterm_sem (adjointFO I \<sigma> \<nu>) (args i) \<nu>)
[PROOF STEP]
unfolding adjointFO_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>; \<forall>x. dsafe (args x); \<And>i. dsafe (\<sigma> i); f = Inl a\<rbrakk> \<Longrightarrow> dterm_sem I (case f of Inl f' \<Rightarrow> $f f' (\<lambda>i. TsubstFO (args i) \<sigma>) | Inr f' \<Rightarrow> \<sigma> f') \<nu> = Functions \<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> f (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 2. \<And>b. \<lbrakk>\<And>i. TadmitFO \<sigma> (args i); \<And>i. dterm_sem I (TsubstFO (args i) \<sigma>) \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>; \<forall>x. dsafe (args x); \<And>i. dsafe (\<sigma> i); f = Inr b\<rbrakk> \<Longrightarrow> dterm_sem I (case f of Inl f' \<Rightarrow> $f f' (\<lambda>i. TsubstFO (args i) \<sigma>) | Inr f' \<Rightarrow> \<sigma> f') \<nu> = Functions \<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> f (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem I (TsubstFO ($f f args) \<sigma>) \<nu> = dterm_sem (adjointFO I \<sigma> \<nu>) ($f f args) \<nu>

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


[STATEMENT]
lemma nsubst_ode:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  fixes \<nu>'::"'sz state"
  assumes good_interp:"is_interp I"
  shows "osafe ODE \<Longrightarrow> OadmitFO \<sigma> ODE U \<Longrightarrow> (\<And>i. dsafe (\<sigma> i)) \<Longrightarrow> ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>)= ODE_sem (adjointFO I \<sigma> \<nu>) ODE (fst \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>osafe ODE; OadmitFO \<sigma> ODE U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE (fst \<nu>)
[PROOF STEP]
proof (induction rule: osafe.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>OadmitFO \<sigma> (OVar c) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OVar c) (fst \<nu>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OadmitFO \<sigma> (OSing x \<theta>) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
case (osafe_Var c)
[PROOF STATE]
proof (state)
this:
OadmitFO \<sigma> (OVar c) U
dsafe (\<sigma> ?i7)

goal (3 subgoals):
 1. \<And>c. \<lbrakk>OadmitFO \<sigma> (OVar c) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OVar c) (fst \<nu>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OadmitFO \<sigma> (OSing x \<theta>) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
OadmitFO \<sigma> (OVar c) U
dsafe (\<sigma> ?i7)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
OadmitFO \<sigma> (OVar c) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. ODE_sem I (OsubstFO (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OVar c) (fst \<nu>)
[PROOF STEP]
unfolding OUadmitFO_def adjointFO_def
[PROOF STATE]
proof (prove)
using this:
OadmitFO \<sigma> (OVar c) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. ODE_sem I (OsubstFO (OVar c) \<sigma>) (fst \<nu>) = ODE_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> (OVar c) (fst \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OsubstFO (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OVar c) (fst \<nu>)

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OadmitFO \<sigma> (OSing x \<theta>) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OadmitFO \<sigma> (OSing x \<theta>) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
case (osafe_Sing \<theta> x)
[PROOF STATE]
proof (state)
this:
dfree \<theta>
OadmitFO \<sigma> (OSing x \<theta>) U
dsafe (\<sigma> ?i7)

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; OadmitFO \<sigma> (OSing x \<theta>) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>
OadmitFO \<sigma> (OSing x \<theta>) U
dsafe (\<sigma> ?i7)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
OadmitFO \<sigma> (OSing x \<theta>) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; \<And>i. dsafe (\<sigma> i); OUadmitFO \<sigma> (OSing x \<theta>) U; TadmitFFO \<sigma> \<theta>\<rbrakk> \<Longrightarrow> (\<lambda>i. if i = x then sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) else 0) = (\<lambda>i. if i = x then sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>) else 0)
[PROOF STEP]
using nsubst_sterm' [of  \<sigma> \<theta> I "(fst \<nu>)" "(snd \<nu>)"]
[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> (fst \<nu>, snd \<nu>)) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>; \<And>i. dsafe (\<sigma> i); OUadmitFO \<sigma> (OSing x \<theta>) U; TadmitFFO \<sigma> \<theta>\<rbrakk> \<Longrightarrow> (\<lambda>i. if i = x then sterm_sem I (TsubstFO \<theta> \<sigma>) (fst \<nu>) else 0) = (\<lambda>i. if i = x then sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> (fst \<nu>) else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OsubstFO (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
case (osafe_Prod ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)
[PROOF STEP]
have NO1:"OadmitFO \<sigma> ODE1 U" and NO2:"OadmitFO \<sigma> ODE2 U"
[PROOF STATE]
proof (prove)
using this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. OadmitFO \<sigma> ODE1 U &&& OadmitFO \<sigma> ODE2 U
[PROOF STEP]
unfolding OUadmitFO_def
[PROOF STATE]
proof (prove)
using this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. OadmitFO \<sigma> ODE1 U &&& OadmitFO \<sigma> ODE2 U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
OadmitFO \<sigma> ODE1 U
OadmitFO \<sigma> ODE2 U

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have "ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)"
    "ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>) &&& ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
using osafe_Prod.IH osafe_Prod.prems osafe_Prod.hyps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}

goal (1 subgoal):
 1. ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>) &&& ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
using NO1 NO2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
OadmitFO \<sigma> (OProd ODE1 ODE2) U
dsafe (\<sigma> ?i7)
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
OadmitFO \<sigma> ODE1 U
OadmitFO \<sigma> ODE2 U

goal (1 subgoal):
 1. ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>) &&& ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>OadmitFO \<sigma> ODE1 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>OadmitFO \<sigma> ODE2 U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; OadmitFO \<sigma> (OProd ODE1 ODE2) U; \<And>i. dsafe (\<sigma> i)\<rbrakk> \<Longrightarrow> ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (OsubstFO ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 (fst \<nu>)
ODE_sem I (OsubstFO ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 (fst \<nu>)

goal (1 subgoal):
 1. ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OsubstFO (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma osubst_preserves_BVO:
  shows "BVO (OsubstFO ODE \<sigma>) = BVO ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BVO (OsubstFO ODE \<sigma>) = BVO ODE
[PROOF STEP]
proof (induction "ODE")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. BVO (OsubstFO (OVar x) \<sigma>) = BVO (OVar x)
 2. \<And>x1a x2. BVO (OsubstFO (OSing x1a x2) \<sigma>) = BVO (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>BVO (OsubstFO ODE1 \<sigma>) = BVO ODE1; BVO (OsubstFO ODE2 \<sigma>) = BVO ODE2\<rbrakk> \<Longrightarrow> BVO (OsubstFO (OProd ODE1 ODE2) \<sigma>) = BVO (OProd ODE1 ODE2)
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma osubst_preserves_ODE_vars:
  shows "ODE_vars I (OsubstFO ODE \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_vars I (OsubstFO ODE \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) ODE
[PROOF STEP]
proof (induction "ODE")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. ODE_vars I (OsubstFO (OVar x) \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) (OVar x)
 2. \<And>x1a x2. ODE_vars I (OsubstFO (OSing x1a x2) \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars I (OsubstFO ODE1 \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) ODE1; ODE_vars I (OsubstFO ODE2 \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars I (OsubstFO (OProd ODE1 ODE2) \<sigma>) = ODE_vars (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2)
[PROOF STEP]
qed (auto simp add: adjointFO_def)


[STATEMENT]
lemma osubst_preserves_semBV:
  shows "semBV I (OsubstFO ODE \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semBV I (OsubstFO ODE \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) ODE
[PROOF STEP]
proof (induction "ODE")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. semBV I (OsubstFO (OVar x) \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) (OVar x)
 2. \<And>x1a x2. semBV I (OsubstFO (OSing x1a x2) \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>semBV I (OsubstFO ODE1 \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) ODE1; semBV I (OsubstFO ODE2 \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) ODE2\<rbrakk> \<Longrightarrow> semBV I (OsubstFO (OProd ODE1 ODE2) \<sigma>) = semBV (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2)
[PROOF STEP]
qed (auto simp add: adjointFO_def)