[STATEMENT]
lemma adjointFO_ode_vars:
  shows "ODE_vars (adjointFO I \<sigma> \<nu>) ODE = ODE_vars (adjointFO I \<sigma> \<omega>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_vars (adjointFO I \<sigma> \<nu>) ODE = ODE_vars (adjointFO I \<sigma> \<omega>) ODE
[PROOF STEP]
apply(induction ODE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ODE_vars (adjointFO I \<sigma> \<nu>) (OVar x) = ODE_vars (adjointFO I \<sigma> \<omega>) (OVar x)
 2. \<And>x1a x2. ODE_vars (adjointFO I \<sigma> \<nu>) (OSing x1a x2) = ODE_vars (adjointFO I \<sigma> \<omega>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars (adjointFO I \<sigma> \<nu>) ODE1 = ODE_vars (adjointFO I \<sigma> \<omega>) ODE1; ODE_vars (adjointFO I \<sigma> \<nu>) ODE2 = ODE_vars (adjointFO I \<sigma> \<omega>) ODE2\<rbrakk> \<Longrightarrow> ODE_vars (adjointFO I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_vars (adjointFO I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
unfolding adjointFO_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ODE_vars \<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_vars \<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)
 2. \<And>x1a x2. ODE_vars \<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> (OSing x1a x2) = ODE_vars \<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> (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_vars \<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> ODE1 = ODE_vars \<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> ODE1; ODE_vars \<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> ODE2 = ODE_vars \<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> ODE2\<rbrakk> \<Longrightarrow> ODE_vars \<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> (OProd ODE1 ODE2) = ODE_vars \<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> (OProd ODE1 ODE2)
[PROOF STEP]
by auto