[STATEMENT]
lemma subst_ode:
  fixes I:: "('sf, 'sc, 'sz) interp" and \<nu> :: "'sz state"
  assumes good_interp:"is_interp I"
  shows "osafe ODE \<Longrightarrow>
         ssafe \<sigma> \<Longrightarrow>
         Oadmit \<sigma> ODE (BVO ODE) \<Longrightarrow>
         ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>) = ODE_sem (adjoint I \<sigma> \<nu>) ODE (fst \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>osafe ODE; ssafe \<sigma>; Oadmit \<sigma> ODE (BVO ODE)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE (fst \<nu>)
[PROOF STEP]
proof (induction rule: osafe.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> (OVar c) (BVO (OVar c))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OVar c) (fst \<nu>)
 2. \<And>\<theta> x. \<lbrakk>dfree \<theta>; ssafe \<sigma>; Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 3. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
case (osafe_Var c)
[PROOF STATE]
proof (state)
this:
ssafe \<sigma>
Oadmit \<sigma> (OVar c) (BVO (OVar c))

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

goal (1 subgoal):
 1. ODE_sem I (Osubst (OVar c) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OVar c) (fst \<nu>)
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
using this:
ssafe \<sigma>
Oadmit \<sigma> (OVar c) (BVO (OVar c))

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

goal (2 subgoals):
 1. \<And>\<theta> x. \<lbrakk>dfree \<theta>; ssafe \<sigma>; Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint 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>; ssafe \<sigma>; Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
 2. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
case (osafe_Sing \<theta> x)
[PROOF STATE]
proof (state)
this:
dfree \<theta>
ssafe \<sigma>
Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))

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

goal (1 subgoal):
 1. ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
[PROOF STEP]
using subst_sterm [of  \<sigma> \<theta> I "\<nu>"]
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
ssafe \<sigma>
Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))
\<lbrakk>TadmitF \<sigma> \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>
(\<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')
Oadmit \<sigma> (OSing x \<theta>) (BVO (OSing x \<theta>))
\<lbrakk>TadmitF \<sigma> \<theta>; \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'\<rbrakk> \<Longrightarrow> sterm_sem I (Tsubst \<theta> \<sigma>) (fst \<nu>) = sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> (fst \<nu>)

goal (1 subgoal):
 1. ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (Osubst (OSing x \<theta>) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x \<theta>) (fst \<nu>)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint 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>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint 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>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
ssafe \<sigma>
Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint 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>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
ssafe \<sigma>
Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))
[PROOF STEP]
have NOU1:"Oadmit \<sigma> ODE1  (BVO (OProd ODE1 ODE2))" and NOU2:"Oadmit \<sigma> ODE2  (BVO (OProd ODE1 ODE2))"
[PROOF STATE]
proof (prove)
using this:
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
ssafe \<sigma>
Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))

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

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have TUA_sub:"\<And>\<sigma> \<theta> A B. TUadmit \<sigma> \<theta> B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> TUadmit \<sigma> \<theta> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> \<theta> A B. \<lbrakk>TUadmit \<sigma> \<theta> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> TUadmit \<sigma> \<theta> A
[PROOF STEP]
unfolding TUadmit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> \<theta> A B. \<lbrakk>(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<inter> B = {}; A \<subseteq> B\<rbrakk> \<Longrightarrow> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<inter> A = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>TUadmit ?\<sigma>7 ?\<theta>7 ?B7; ?A7 \<subseteq> ?B7\<rbrakk> \<Longrightarrow> TUadmit ?\<sigma>7 ?\<theta>7 ?A7

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have OA_sub:"\<And>ODE A B. Oadmit \<sigma> ODE B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Oadmit \<sigma> ODE A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ODE A B. \<lbrakk>Oadmit \<sigma> ODE B; A \<subseteq> B\<rbrakk> \<Longrightarrow> Oadmit \<sigma> ODE A
[PROOF STEP]
subgoal for ODE A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Oadmit \<sigma> ODE B; A \<subseteq> B\<rbrakk> \<Longrightarrow> Oadmit \<sigma> ODE A
[PROOF STEP]
proof (induction rule: Oadmit.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<sigma> c U. A \<subseteq> U \<Longrightarrow> Oadmit \<sigma> (OVar c) A
 2. \<And>\<sigma> \<theta> U x. \<lbrakk>TUadmit \<sigma> \<theta> U; TadmitF \<sigma> \<theta>; A \<subseteq> U\<rbrakk> \<Longrightarrow> Oadmit \<sigma> (OSing x \<theta>) A
 3. \<And>\<sigma> ODE1 U ODE2. \<lbrakk>Oadmit \<sigma> ODE1 U; A \<subseteq> U \<Longrightarrow> Oadmit \<sigma> ODE1 A; Oadmit \<sigma> ODE2 U; A \<subseteq> U \<Longrightarrow> Oadmit \<sigma> ODE2 A; ODE_dom (Osubst ODE1 \<sigma>) \<inter> ODE_dom (Osubst ODE2 \<sigma>) = {}; A \<subseteq> U\<rbrakk> \<Longrightarrow> Oadmit \<sigma> (OProd ODE1 ODE2) A
[PROOF STEP]
case (Oadmit_Var \<sigma> c U)
[PROOF STATE]
proof (state)
this:
A \<subseteq> U

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

goal (1 subgoal):
 1. Oadmit \<sigma> (OVar c) A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Oadmit \<sigma> (OVar c) A

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

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

goal (1 subgoal):
 1. Oadmit \<sigma> (OSing x \<theta>) A
[PROOF STEP]
using TUA_sub[of \<sigma> \<theta> U A]
[PROOF STATE]
proof (prove)
using this:
TUadmit \<sigma> \<theta> U
TadmitF \<sigma> \<theta>
A \<subseteq> U
\<lbrakk>TUadmit \<sigma> \<theta> U; A \<subseteq> U\<rbrakk> \<Longrightarrow> TUadmit \<sigma> \<theta> A

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>Oadmit \<sigma> ?ODE8 ?B8; ?A8 \<subseteq> ?B8\<rbrakk> \<Longrightarrow> Oadmit \<sigma> ?ODE8 ?A8

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have sub1:"(BVO ODE1) \<subseteq> (BVO (OProd ODE1 ODE2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BVO ODE1 \<subseteq> BVO (OProd ODE1 ODE2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
BVO ODE1 \<subseteq> BVO (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have sub2: "(BVO ODE2) \<subseteq> (BVO (OProd ODE1 ODE2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BVO ODE2 \<subseteq> BVO (OProd ODE1 ODE2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
BVO ODE2 \<subseteq> BVO (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
have "ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)"
    "ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>) &&& ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint 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>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
ssafe \<sigma>
Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}

goal (1 subgoal):
 1. ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>) &&& ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
using OA_sub[OF NOU1 sub1] OA_sub[OF NOU2 sub2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
\<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
ssafe \<sigma>
Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))
osafe ODE1
osafe ODE2
ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}
Oadmit \<sigma> ODE1 (BVO ODE1)
Oadmit \<sigma> ODE2 (BVO ODE2)

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

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>osafe ODE1; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE1 (BVO ODE1)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>); osafe ODE2; \<lbrakk>ssafe \<sigma>; Oadmit \<sigma> ODE2 (BVO ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>); ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}; ssafe \<sigma>; Oadmit \<sigma> (OProd ODE1 ODE2) (BVO (OProd ODE1 ODE2))\<rbrakk> \<Longrightarrow> ODE_sem I (Osubst (OProd ODE1 ODE2) \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) (fst \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (Osubst ODE1 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 (fst \<nu>)
ODE_sem I (Osubst ODE2 \<sigma>) (fst \<nu>) = ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 (fst \<nu>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma osubst_eq_ODE_vars: "ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (adjoint I \<sigma> \<nu>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE
[PROOF STEP]
proof (induction ODE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. ODE_vars I (Osubst (OVar x) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OVar x)
 2. \<And>x1a x2. ODE_vars I (Osubst (OSing x1a x2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars I (Osubst ODE1 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE1; ODE_vars I (Osubst ODE2 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars I (Osubst (OProd ODE1 ODE2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OVar x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. ODE_vars I (Osubst (OVar x) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OVar x)
 2. \<And>x1a x2. ODE_vars I (Osubst (OSing x1a x2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars I (Osubst ODE1 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE1; ODE_vars I (Osubst ODE2 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars I (Osubst (OProd ODE1 ODE2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_vars I (Osubst (OVar x) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OVar x)
[PROOF STEP]
by (cases "SODEs \<sigma> x", auto simp add: adjoint_def)
[PROOF STATE]
proof (state)
this:
ODE_vars I (Osubst (OVar x) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OVar x)

goal (2 subgoals):
 1. \<And>x1a x2. ODE_vars I (Osubst (OSing x1a x2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OSing x1a x2)
 2. \<And>ODE1 ODE2. \<lbrakk>ODE_vars I (Osubst ODE1 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE1; ODE_vars I (Osubst ODE2 \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars I (Osubst (OProd ODE1 ODE2) \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2)
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma subst_semBV:"semBV (adjoint I \<sigma> \<nu>') ODE = (semBV I (Osubst ODE \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semBV (local.adjoint I \<sigma> \<nu>') ODE = semBV I (Osubst ODE \<sigma>)
[PROOF STEP]
proof (induction ODE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. semBV (local.adjoint I \<sigma> \<nu>') (OVar x) = semBV I (Osubst (OVar x) \<sigma>)
 2. \<And>x1a x2. semBV (local.adjoint I \<sigma> \<nu>') (OSing x1a x2) = semBV I (Osubst (OSing x1a x2) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>semBV (local.adjoint I \<sigma> \<nu>') ODE1 = semBV I (Osubst ODE1 \<sigma>); semBV (local.adjoint I \<sigma> \<nu>') ODE2 = semBV I (Osubst ODE2 \<sigma>)\<rbrakk> \<Longrightarrow> semBV (local.adjoint I \<sigma> \<nu>') (OProd ODE1 ODE2) = semBV I (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
case (OVar x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. semBV (local.adjoint I \<sigma> \<nu>') (OVar x) = semBV I (Osubst (OVar x) \<sigma>)
 2. \<And>x1a x2. semBV (local.adjoint I \<sigma> \<nu>') (OSing x1a x2) = semBV I (Osubst (OSing x1a x2) \<sigma>)
 3. \<And>ODE1 ODE2. \<lbrakk>semBV (local.adjoint I \<sigma> \<nu>') ODE1 = semBV I (Osubst ODE1 \<sigma>); semBV (local.adjoint I \<sigma> \<nu>') ODE2 = semBV I (Osubst ODE2 \<sigma>)\<rbrakk> \<Longrightarrow> semBV (local.adjoint I \<sigma> \<nu>') (OProd ODE1 ODE2) = semBV I (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semBV (local.adjoint I \<sigma> \<nu>') (OVar x) = semBV I (Osubst (OVar x) \<sigma>)
[PROOF STEP]
by (cases "SODEs \<sigma> x", auto simp add: adjoint_def)
[PROOF STATE]
proof (state)
this:
semBV (local.adjoint I \<sigma> \<nu>') (OVar x) = semBV I (Osubst (OVar x) \<sigma>)

goal (2 subgoals):
 1. \<And>x1a x2. semBV (local.adjoint I \<sigma> \<nu>') (OSing x1a x2) = semBV I (Osubst (OSing x1a x2) \<sigma>)
 2. \<And>ODE1 ODE2. \<lbrakk>semBV (local.adjoint I \<sigma> \<nu>') ODE1 = semBV I (Osubst ODE1 \<sigma>); semBV (local.adjoint I \<sigma> \<nu>') ODE2 = semBV I (Osubst ODE2 \<sigma>)\<rbrakk> \<Longrightarrow> semBV (local.adjoint I \<sigma> \<nu>') (OProd ODE1 ODE2) = semBV I (Osubst (OProd ODE1 ODE2) \<sigma>)
[PROOF STEP]
qed (auto)