[STATEMENT]
lemma subst_mkv:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  fixes \<nu>'::"'sz state"
  assumes good_interp:"is_interp I"
  assumes NOU:"Oadmit \<sigma> ODE (BVO ODE)"
  assumes osafe:"osafe ODE "
  assumes frees:"ssafe \<sigma>"
  shows "(mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>'))
    = (mk_v (adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>') = mk_v (local.adjoint 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 (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) UNIV
[PROOF STEP]
using mk_v_agree[of "adjoint I \<sigma> \<nu>'" "ODE" \<nu> "fst \<nu>'"]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) \<nu> (- semBV (local.adjoint I \<sigma> \<nu>') ODE) \<and> Vagree (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) (mk_xode (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')) (semBV (local.adjoint I \<sigma> \<nu>') ODE)

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

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

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i)
[PROOF STEP]
using subst_ode[OF good_interp osafe  frees NOU, of \<nu>']
[PROOF STATE]
proof (prove)
using this:
((\<forall>i. Inl i \<in> - semBV (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst (mk_xode (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd (mk_xode (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')) $ i)
((\<forall>i. Inl i \<in> - semBV I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i) \<and> (\<forall>i. Inr i \<in> - semBV I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i)) \<and> (\<forall>i. Inl i \<in> semBV I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_xode I (Osubst ODE \<sigma>) (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> semBV I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_xode I (Osubst ODE \<sigma>) (fst \<nu>')) $ i)
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint 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 (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); \<forall>i. Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<And>i. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); \<forall>i. Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint 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 (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); \<forall>i. Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint 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 (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(cases "Inl i \<in> Inl ` ODE_vars (adjoint I \<sigma> \<nu>') ODE")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using osubst_eq_ODE_vars[of I ODE \<sigma> \<nu>']
[PROOF STATE]
proof (prove)
using this:
ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
assume "ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')"
       "Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow>
       fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i"
       "Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow>
       fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i"
       "Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE"
[PROOF STATE]
proof (state)
this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE
[PROOF STEP]
show
        "fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i"
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using osubst_eq_ODE_vars[of I ODE \<sigma> \<nu>']
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i
Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE
ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); \<forall>i. Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint 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 (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); \<forall>i. Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint 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 (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i)\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply(cases "Inr i \<in> Inr ` ODE_vars (adjoint I \<sigma> \<nu>') ODE")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using osubst_eq_ODE_vars[of I ODE \<sigma> \<nu>']
[PROOF STATE]
proof (prove)
using this:
ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (2 subgoals):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
 2. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
assume "ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')"
      "Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow>
      snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i"
      "Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow>
      snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i"
      "Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE"
[PROOF STATE]
proof (state)
this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. \<lbrakk>ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>'); Inl i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inl i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inl i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inl i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu> $ i; Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i; (Inl i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> fst (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); (Inl i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i) \<and> (Inl i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> fst (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = fst \<nu>' $ i); (Inr i \<in> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i) \<and> (Inr i \<in> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>') $ i); Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE\<rbrakk> \<Longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE
[PROOF STEP]
show "snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i"
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
using osubst_eq_ODE_vars[of I ODE \<sigma> \<nu>']
[PROOF STATE]
proof (prove)
using this:
ODE_sem I (Osubst ODE \<sigma>) (fst \<nu>') = ODE_sem (local.adjoint I \<sigma> \<nu>') ODE (fst \<nu>')
Inr i \<notin> Inl ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<and> Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE \<longrightarrow> snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inl ` ODE_vars I (Osubst ODE \<sigma>) \<and> Inr i \<notin> Inr ` ODE_vars I (Osubst ODE \<sigma>) \<longrightarrow> snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd \<nu> $ i
Inr i \<notin> Inr ` ODE_vars (local.adjoint I \<sigma> \<nu>') ODE
ODE_vars I (Osubst ODE \<sigma>) = ODE_vars (local.adjoint I \<sigma> \<nu>') ODE

goal (1 subgoal):
 1. snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (mk_v I (Osubst ODE \<sigma>) \<nu> (fst \<nu>')) $ i = snd (mk_v (local.adjoint I \<sigma> \<nu>') ODE \<nu> (fst \<nu>')) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done