[STATEMENT]
lemma uadmit_mkv_ntadjoint:
  assumes ssafe:"\<And>i. dsafe (\<sigma> i)"
  assumes good_interp:"is_interp I"
  assumes VA:"Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE}. FVT (\<sigma> y))"
  assumes osafe:"osafe ODE"
  shows "mk_v (adjointFO I \<sigma> \<nu>) ODE = mk_v (adjointFO I \<sigma> \<omega>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE = mk_v (adjointFO I \<sigma> \<omega>) ODE
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mk_v (adjointFO I \<sigma> \<nu>) ODE x = mk_v (adjointFO I \<sigma> \<omega>) ODE x
[PROOF STEP]
subgoal for R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE R = mk_v (adjointFO I \<sigma> \<omega>) ODE R
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mk_v (adjointFO I \<sigma> \<nu>) ODE R x = mk_v (adjointFO I \<sigma> \<omega>) ODE R x
[PROOF STEP]
subgoal for solt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE R solt = mk_v (adjointFO I \<sigma> \<omega>) ODE R solt
[PROOF STEP]
apply(rule agree_UNIV_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using mk_v_agree[of "(adjointFO I \<sigma> \<nu>)" ODE "R" solt]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using mk_v_agree[of "(adjointFO I \<sigma> \<omega>)" ODE "R" solt]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)
Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<omega>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) (semBV (adjointFO I \<sigma> \<omega>) ODE)

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using uadmit_ode_ntadjoint'[OF ssafe good_interp VA osafe]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)
Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<omega>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) (semBV (adjointFO I \<sigma> \<omega>) ODE)
ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
((\<forall>i. Inl i \<in> - semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) $ i)
((\<forall>i. Inl i \<in> - semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) $ i)
ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
 2. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
[PROOF STEP]
using adjointFO_ode_vars
[PROOF STATE]
proof (prove)
using this:
ODE_vars (adjointFO ?I ?\<sigma> ?\<nu>) ?ODE = ODE_vars (adjointFO ?I ?\<sigma> ?\<omega>) ?ODE

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
 2. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
[PROOF STEP]
by metis+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done