[STATEMENT]
lemma uadmit_ode_ntadjoint':
  fixes \<sigma> I
  assumes ssafe:"\<And>i. dsafe (\<sigma> i)"
  assumes good_interp:"is_interp I"
  shows"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE}. FVT (\<sigma> y)) \<Longrightarrow> osafe ODE \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE}. FVT (\<sigma> y)); osafe ODE\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE
[PROOF STEP]
proof (induction ODE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y)); osafe (OVar x)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OVar x) = ODE_sem (adjointFO I \<sigma> \<omega>) (OVar x)
 2. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 3. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OVar x)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y))
osafe (OVar x)

goal (3 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y)); osafe (OVar x)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OVar x) = ODE_sem (adjointFO I \<sigma> \<omega>) (OVar x)
 2. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 3. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y))
osafe (OVar x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y))
osafe (OVar x)

goal (1 subgoal):
 1. ODE_sem (adjointFO I \<sigma> \<nu>) (OVar x) = ODE_sem (adjointFO I \<sigma> \<omega>) (OVar x)
[PROOF STEP]
unfolding adjointFO_def
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OVar x)}. FVT (\<sigma> y))
osafe (OVar x)

goal (1 subgoal):
 1. 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 x) = ODE_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (OVar x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem (adjointFO I \<sigma> \<nu>) (OVar x) = ODE_sem (adjointFO I \<sigma> \<omega>) (OVar x)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OSing x1a x2)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y))
osafe (OSing x1a x2)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y))

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume osafe:"osafe (OSing x1a x2)"
[PROOF STATE]
proof (state)
this:
osafe (OSing x1a x2)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
osafe (OSing x1a x2)
[PROOF STEP]
have dfree:"dfree x2"
[PROOF STATE]
proof (prove)
using this:
osafe (OSing x1a x2)

goal (1 subgoal):
 1. dfree x2
[PROOF STEP]
by (auto dest: osafe.cases)
[PROOF STATE]
proof (state)
this:
dfree x2

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sem:"sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2
[PROOF STEP]
using uadmit_sterm_ntadjoint'[of \<sigma> \<nu> \<omega> x2 I, OF ssafe] VA
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y))

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OSing x1a x2)}. FVT (\<sigma> y)); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. \<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<nu>) x2 a else 0) = (\<lambda>a. \<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<omega>) x2 a else 0)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<nu>) x2 x else 0) = (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<omega>) x2 x else 0)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<nu>) x2 x else 0) = (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<omega>) x2 x else 0)
[PROOF STEP]
apply (rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<nu>) x2 x else 0) $ i = (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<omega>) x2 x else 0) $ i
[PROOF STEP]
using sem
[PROOF STATE]
proof (prove)
using this:
sterm_sem (adjointFO I \<sigma> \<nu>) x2 = sterm_sem (adjointFO I \<sigma> \<omega>) x2

goal (1 subgoal):
 1. \<And>i. (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<nu>) x2 x else 0) $ i = (\<chi>i. if i = x1a then sterm_sem (adjointFO I \<sigma> \<omega>) x2 x else 0) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ODE_sem (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OSing x1a x2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OProd ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> ?\<nu>7) ODE1 = ODE_sem (adjointFO I \<sigma> ?\<omega>7) ODE1
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> ?\<nu>7) ODE2 = ODE_sem (adjointFO I \<sigma> ?\<omega>7) ODE2
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))
osafe (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume IH1:"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)) \<Longrightarrow>
    osafe ODE1 \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1"
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> ?\<nu>7) ODE1 = ODE_sem (adjointFO I \<sigma> ?\<omega>7) ODE1

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume IH2:"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<Longrightarrow>
    osafe ODE2 \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2"
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> ?\<nu>7) ODE2 = ODE_sem (adjointFO I \<sigma> ?\<omega>7) ODE2

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume safe:"osafe (OProd ODE1 ODE2)"
[PROOF STATE]
proof (state)
this:
osafe (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
from safe
[PROOF STATE]
proof (chain)
picking this:
osafe (OProd ODE1 ODE2)
[PROOF STEP]
have safe1:"osafe ODE1" and safe2:"osafe ODE2"
[PROOF STATE]
proof (prove)
using this:
osafe (OProd ODE1 ODE2)

goal (1 subgoal):
 1. osafe ODE1 &&& osafe ODE2
[PROOF STEP]
by (auto dest: osafe.cases)
[PROOF STATE]
proof (state)
this:
osafe ODE1
osafe ODE2

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sub1:"(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sub2:"(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE1}. FVT (\<sigma> y)); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y)); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))

goal (1 subgoal):
 1. ODE_sem (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2]
[PROOF STATE]
proof (prove)
using this:
(\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO (OProd ODE1 ODE2)}. FVT (\<sigma> y))
ODE_sem (adjointFO I \<sigma> \<nu>) ODE1 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE1
ODE_sem (adjointFO I \<sigma> \<nu>) ODE2 = ODE_sem (adjointFO I \<sigma> \<omega>) ODE2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjoint_ode_vars:
  shows "ODE_vars (local.adjoint I \<sigma> \<nu>) ODE = ODE_vars (local.adjoint I \<sigma> \<omega>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_vars (local.adjoint I \<sigma> \<nu>) ODE = ODE_vars (local.adjoint I \<sigma> \<omega>) ODE
[PROOF STEP]
apply(induction ODE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ODE_vars (local.adjoint I \<sigma> \<nu>) (OVar x) = ODE_vars (local.adjoint I \<sigma> \<omega>) (OVar x)
 2. \<And>x1a x2. ODE_vars (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_vars (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_vars (local.adjoint I \<sigma> \<omega>) ODE1; ODE_vars (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_vars (local.adjoint I \<sigma> \<omega>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_vars (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ODE_vars \<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 x) = ODE_vars \<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' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<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 x)
 2. \<And>x1a x2. ODE_vars \<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> (OSing x1a x2) = ODE_vars \<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' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<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> (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars \<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> ODE1 = ODE_vars \<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' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<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> ODE1; ODE_vars \<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> ODE2 = ODE_vars \<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' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<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> ODE2\<rbrakk> \<Longrightarrow> ODE_vars \<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> (OProd ODE1 ODE2) = ODE_vars \<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' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<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> (OProd ODE1 ODE2)
[PROOF STEP]
by auto