[STATEMENT]
lemma nsubst_mkv:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  fixes \<nu>'::"'sz state"
  assumes good_interp:"is_interp I"
  assumes NOU:"OadmitFO \<sigma> ODE U"
  assumes osafe:"osafe ODE "
  assumes frees:"(\<And>i. dsafe (\<sigma> i))"
  shows "(mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>'))
    = (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>') = mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')
[PROOF STEP]
apply(rule agree_UNIV_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) UNIV
[PROOF STEP]
using mk_v_agree[of "adjointFO I \<sigma> \<nu>'" "ODE" \<nu> "fst \<nu>'"]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) \<nu> (- semBV (adjointFO I \<sigma> \<nu>') ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) (mk_xode (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')) (semBV (adjointFO I \<sigma> \<nu>') ODE)

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

goal (1 subgoal):
 1. Vagree (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst (mk_xode (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd (mk_xode (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')) $ i)
((\<forall>i. Inl i \<in> - semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_xode I (OsubstFO ODE \<sigma>) (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_xode I (OsubstFO ODE \<sigma>) (fst \<nu>')) $ i)

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i)
[PROOF STEP]
using nsubst_ode[OF good_interp osafe NOU frees, of \<nu>']
[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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst (mk_xode (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd (mk_xode (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')) $ i)
((\<forall>i. Inl i \<in> - semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_xode I (OsubstFO ODE \<sigma>) (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_xode I (OsubstFO ODE \<sigma>) (fst \<nu>')) $ i)
ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>')

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); \<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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<And>i. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); \<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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); \<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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(erule allE[where x=i])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(cases "Inl i \<in> semBV I (OsubstFO ODE \<sigma>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<in> semBV I (OsubstFO ODE \<sigma>)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> semBV I (OsubstFO ODE \<sigma>)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using  osubst_preserves_ODE_vars
[PROOF STATE]
proof (prove)
using this:
ODE_vars ?I (OsubstFO ?ODE ?\<sigma>) = ODE_vars (adjointFO ?I ?\<sigma> ?\<nu>) ?ODE

goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<in> semBV I (OsubstFO ODE \<sigma>)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> semBV I (OsubstFO ODE \<sigma>)\<rbrakk> \<Longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
by (metis (full_types))+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); \<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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); \<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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(erule allE[where x=i])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(cases "Inr i \<in> BVO ODE")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<in> BVO ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> BVO ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using  osubst_preserves_ODE_vars
[PROOF STATE]
proof (prove)
using this:
ODE_vars ?I (OsubstFO ?ODE ?\<sigma>) = ODE_vars (adjointFO ?I ?\<sigma> ?\<nu>) ?ODE

goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<in> BVO ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (OsubstFO ODE \<sigma>) (fst \<nu>') = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>'); 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 \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ 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 \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> fst (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (OsubstFO ODE \<sigma>) \<longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (adjointFO I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> BVO ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (OsubstFO ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (adjointFO I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
by (metis (full_types))+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ODE_unbound_zero:
  fixes i
  shows "Inl i \<notin> BVO ODE \<Longrightarrow> ODE_sem I ODE x $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inl i \<notin> BVO ODE \<Longrightarrow> ODE_sem I ODE x $ i = 0
[PROOF STEP]
proof (induction ODE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa. Inl i \<notin> BVO (OVar xa) \<Longrightarrow> ODE_sem I (OVar xa) x $ i = 0
 2. \<And>x1a x2. Inl i \<notin> BVO (OSing x1a x2) \<Longrightarrow> ODE_sem I (OSing x1a x2) x $ i = 0
 3. \<And>ODE1 ODE2. \<lbrakk>Inl i \<notin> BVO ODE1 \<Longrightarrow> ODE_sem I ODE1 x $ i = 0; Inl i \<notin> BVO ODE2 \<Longrightarrow> ODE_sem I ODE2 x $ i = 0; Inl i \<notin> BVO (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) x $ i = 0
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma ODE_bound_effect:
  fixes s t sol ODE X b
  assumes s:"s \<in> {0..t}"
  assumes sol:"(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t}  X"
  shows "Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree (sol 0, b) (sol s, b) (- BVO ODE)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Vagree (sol 0, b) (sol s, b) (- BVO ODE)
[PROOF STEP]
have "\<And>i. Inl i \<notin> BVO ODE \<Longrightarrow>  (\<forall> s. s \<in> {0..t} \<longrightarrow> sol s $ i = sol 0 $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Inl i \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ i = sol 0 $ i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> sol s $ i = sol 0 $ i
[PROOF STEP]
apply (rule constant_when_zero)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> sol (?t0.6 i s) $ i = sol 0 $ i
 2. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> (sol solves_ode ?f6 i s) (?T6 i s) (?S6 i s)
 3. \<And>i s sa x. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t; sa \<in> ?T6 i s\<rbrakk> \<Longrightarrow> ?f6 i s sa x $ i = 0
 4. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> ?t0.6 i s \<in> ?T6 i s
 5. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> s \<in> ?T6 i s
 6. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> convex (?T6 i s)
[PROOF STEP]
using s sol
[PROOF STATE]
proof (prove)
using this:
s \<in> {0..t}
(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} X

goal (6 subgoals):
 1. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> sol (?t0.6 i s) $ i = sol 0 $ i
 2. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> (sol solves_ode ?f6 i s) (?T6 i s) (?S6 i s)
 3. \<And>i s sa x. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t; sa \<in> ?T6 i s\<rbrakk> \<Longrightarrow> ?f6 i s sa x $ i = 0
 4. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> ?t0.6 i s \<in> ?T6 i s
 5. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> s \<in> ?T6 i s
 6. \<And>i s. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> convex (?T6 i s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i sa saa x. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> sa; sa \<le> t; (sol solves_ode (\<lambda>a. ODE_sem I ODE)) {0..t} X; 0 \<le> s; s \<le> t; 0 \<le> saa; saa \<le> t\<rbrakk> \<Longrightarrow> ODE_sem I ODE x $ i = 0
[PROOF STEP]
using ODE_unbound_zero solves_ode_subset
[PROOF STATE]
proof (prove)
using this:
Inl ?i \<notin> BVO ?ODE \<Longrightarrow> ODE_sem ?I ?ODE ?x $ ?i = 0
\<lbrakk>(?x solves_ode ?f) ?T ?X; ?S \<subseteq> ?T\<rbrakk> \<Longrightarrow> (?x solves_ode ?f) ?S ?X

goal (1 subgoal):
 1. \<And>i sa saa x. \<lbrakk>Inl i \<notin> BVO ODE; 0 \<le> sa; sa \<le> t; (sol solves_ode (\<lambda>a. ODE_sem I ODE)) {0..t} X; 0 \<le> s; s \<le> t; 0 \<le> saa; saa \<le> t\<rbrakk> \<Longrightarrow> ODE_sem I ODE x $ i = 0
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
Inl ?i7 \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ ?i7 = sol 0 $ ?i7

goal (1 subgoal):
 1. Vagree (sol 0, b) (sol s, b) (- BVO ODE)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inl ?i7 \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ ?i7 = sol 0 $ ?i7
[PROOF STEP]
show "Vagree (sol 0, b) (sol s, b) (- BVO ODE)"
[PROOF STATE]
proof (prove)
using this:
Inl ?i7 \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ ?i7 = sol 0 $ ?i7

goal (1 subgoal):
 1. Vagree (sol 0, b) (sol s, b) (- BVO ODE)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
Inl ?i7 \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ ?i7 = sol 0 $ ?i7

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> - BVO ODE \<longrightarrow> fst (sol 0, b) $ i = fst (sol s, b) $ i) \<and> (\<forall>i. Inr i \<in> - BVO ODE \<longrightarrow> snd (sol 0, b) $ i = snd (sol s, b) $ i)
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
Inl ?i7 \<notin> BVO ODE \<Longrightarrow> \<forall>s. s \<in> {0..t} \<longrightarrow> sol s $ ?i7 = sol 0 $ ?i7
s \<in> {0..t}

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> - BVO ODE \<longrightarrow> fst (sol 0, b) $ i = fst (sol s, b) $ i) \<and> (\<forall>i. Inr i \<in> - BVO ODE \<longrightarrow> snd (sol 0, b) $ i = snd (sol s, b) $ i)
[PROOF STEP]
by (metis Compl_iff fst_conv  snd_conv)
[PROOF STATE]
proof (state)
this:
Vagree (sol 0, b) (sol s, b) (- BVO ODE)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NO_sub:"OadmitFO \<sigma> ODE A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> OadmitFO \<sigma> ODE B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OadmitFO \<sigma> ODE A; B \<subseteq> A\<rbrakk> \<Longrightarrow> OadmitFO \<sigma> ODE B
[PROOF STEP]
by(induction ODE, auto simp add: OUadmitFO_def)


[STATEMENT]
lemma NO_to_NOU:"OadmitFO \<sigma> ODE S \<Longrightarrow> OUadmitFO \<sigma> ODE S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OadmitFO \<sigma> ODE S \<Longrightarrow> OUadmitFO \<sigma> ODE S
[PROOF STEP]
by(induction ODE, auto simp add: OUadmitFO_def)