[STATEMENT]
lemma uadmit_dterm_ntadjoint:
  assumes TUA:"NTUadmit \<sigma> \<theta> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dfree:"\<And>i . dsafe (\<sigma> i)"
  assumes dsafe:"dsafe \<theta>"
  assumes good_interp:"is_interp I"
  shows  "dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
have duh:"\<And>A B. A \<inter> B = {} \<Longrightarrow> A \<subseteq> -B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. A \<inter> B = {} \<Longrightarrow> A \<subseteq> - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?A7 \<inter> ?B7 = {} \<Longrightarrow> ?A7 \<subseteq> - ?B7

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
have duh:"\<And>A B. A \<inter> B = {} \<Longrightarrow> A \<subseteq> -B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. A \<inter> B = {} \<Longrightarrow> A \<subseteq> - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?A8 \<inter> ?B8 = {} \<Longrightarrow> ?A8 \<subseteq> - ?B8

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
have "\<And>x. x \<in> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> x \<in> (-U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> x \<in> - U
[PROOF STEP]
using TUA
[PROOF STATE]
proof (prove)
using this:
NTUadmit \<sigma> \<theta> U

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> x \<in> - U
[PROOF STEP]
unfolding NTUadmit_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<inter> U = {}

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> x \<in> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x9 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x9 \<in> - U

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x9 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x9 \<in> - U
[PROOF STEP]
have sub1:"(\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> -U"
[PROOF STATE]
proof (prove)
using this:
?x9 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x9 \<in> - U

goal (1 subgoal):
 1. (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> - U

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> - U
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))"
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> - U

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))
[PROOF STEP]
using agree_sub[OF sub1 VA]
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<subseteq> - U
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))

goal (1 subgoal):
 1. dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
using uadmit_dterm_ntadjoint'[OF dfree good_interp VA' dsafe]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))
dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uadmit_dterm_adjointS:
  assumes ssafe:"ssafe \<sigma>"
  assumes good_interp:"is_interp I"
  fixes \<nu> \<omega>
  assumes VA:"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
  assumes dsafe:"dsafe \<theta>"
  shows  "dterm_sem (adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (adjoint I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
apply(rule uadmit_dterm_adjoint')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dfree f'
 2. \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'
 3. is_interp I
 4. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
 5. dsafe \<theta>
[PROOF STEP]
using good_interp ssafe VA dsafe
[PROOF STATE]
proof (prove)
using this:
is_interp I
ssafe \<sigma>
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
dsafe \<theta>

goal (5 subgoals):
 1. \<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dfree f'
 2. \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'
 3. is_interp I
 4. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
 5. dsafe \<theta>
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
is_interp I
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
dsafe \<theta>

goal (5 subgoals):
 1. \<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dfree f'
 2. \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'
 3. is_interp I
 4. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
 5. dsafe \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adj_sub_assign_fact:"\<And>i j e. i\<in>SIGT e \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
        {Inl x |x. x \<in> SIGT e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j e. \<lbrakk>i \<in> SIGT e; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j e. \<lbrakk>i \<in> SIGT e; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j e. \<lbrakk>i \<in> SIGT e; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT e_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT e_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>i \<in> SIGT e_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_geq1_fact:"\<And>i j x1 x2. i\<in>SIGT x1 \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
        {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1. \<lbrakk>i \<in> SIGT x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>i \<in> SIGT x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_prop_fact:"\<And>i j x1 x2 k. i\<in>SIGT (x2 k) \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
         insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2 k. \<lbrakk>i \<in> SIGT (x2 k); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2 k. \<lbrakk>i \<in> SIGT (x2 k); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x2 k. \<lbrakk>i \<in> SIGT (x2 k); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT (x2_ k_); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT (x2_ k_); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>i \<in> SIGT (x2_ k_); j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_ode_fact:"\<And>i j x1 x2. Inl i \<in> SIGO x1 \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
         (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>Inl i \<in> SIGO x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1})
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>Inl i \<in> SIGO x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1. \<lbrakk>Inl i \<in> SIGO x1; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Inl i \<in> SIGO x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Inl i \<in> SIGO x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>Inl i \<in> SIGO x1_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_assign:"\<And>e \<sigma> x. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGP (x := e). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e \<sigma> x. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (x := e)))
[PROOF STEP]
subgoal for e \<sigma> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (x := e)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGP (x := e)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> SIGT e; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
apply (cases "SFunctions \<sigma> j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> j = None\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
 2. \<And>a. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
using adj_sub_assign_fact[of j e i]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions ?\<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl j \<in> ({Inl x |x. x \<in> dom (SFunctions ?\<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts ?\<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates ?\<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms ?\<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}

goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_diff_assign:"\<And>e \<sigma> x. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGP (DiffAssign x e). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e \<sigma> x. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (DiffAssign x e)))
[PROOF STEP]
subgoal for e \<sigma> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (DiffAssign x e)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT e. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGP (DiffAssign x e)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> SIGT e; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
apply (cases "SFunctions \<sigma> j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> j = None\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
 2. \<And>a. \<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions \<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
using adj_sub_assign_fact[of j e i]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>j \<in> SIGT e; i \<in> (case SFunctions ?\<sigma> j of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl j \<in> ({Inl x |x. x \<in> dom (SFunctions ?\<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts ?\<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates ?\<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms ?\<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}

goal (1 subgoal):
 1. \<lbrakk>j \<in> SIGT e; i \<in> FVT a; SFunctions \<sigma> j = Some a\<rbrakk> \<Longrightarrow> \<exists>x\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT e}. i \<in> SFV \<sigma> x
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_geq1:"\<And>\<sigma> x1 x2. (\<Union>i\<in>SIGT x1. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGF (Geq x1 x2). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>i\<in>SIGT x1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
subgoal for \<sigma> x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT x1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT x1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> SIGT x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
 2. \<And>a. \<lbrakk>i \<in> SIGT x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>i \<in> SIGT x1; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x1; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
using adj_sub_geq1_fact[of i x1 x \<sigma>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in> SIGT x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT ?x2.0}

goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x1; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_geq2:"\<And>\<sigma> x1 x2. (\<Union>i\<in>SIGT x2. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGF (Geq x1 x2). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>i\<in>SIGT x2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
subgoal for \<sigma> x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT x2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT x2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGF (Geq x1 x2)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> SIGT x2; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x2; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT x2; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
 2. \<And>a. \<lbrakk>i \<in> SIGT x2; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>i \<in> SIGT x2; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x2; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
using adj_sub_geq2_fact[of i x2 x \<sigma>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in> SIGT x2; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT ?x1.0 \<or> x \<in> SIGT x2}

goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x2; x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}. x \<in> SFV \<sigma> xa
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_prop:"\<And>\<sigma> x1 x2 j . (\<Union>i\<in>SIGT (x2 j). case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGF ($\<phi> x1 x2). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2 j. (\<Union>i\<in>SIGT (x2 j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF ($\<phi> x1 x2)))
[PROOF STEP]
subgoal for \<sigma> x1 x2 j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT (x2 j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF ($\<phi> x1 x2)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>SIGT (x2 j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGF ($\<phi> x1 x2)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> SIGT (x2 j); x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT (x2 j); x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT (x2 j); x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
 2. \<And>a. \<lbrakk>i \<in> SIGT (x2 j); x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>i \<in> SIGT (x2 j); x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT (x2 j); x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
using adj_sub_prop_fact[of i x2 j x \<sigma> x1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in> SIGT (x2 j); x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}

goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT (x2 j); x \<in> FVT a; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> insert (Inr (Inr x1)) {Inl x |x. \<exists>xa. x \<in> SIGT (x2 xa)}. x \<in> SFV \<sigma> xa
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adj_sub_ode:"\<And>\<sigma> x1 x2. (\<Union>i\<in>{i |i. Inl i \<in> SIGO x1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> (\<Union>a\<in>SDom \<sigma> \<inter> SIGP (EvolveODE x1 x2). SFV \<sigma> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>i\<in>{i |i. Inl i \<in> SIGO x1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (EvolveODE x1 x2)))
[PROOF STEP]
subgoal for \<sigma> x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i |i. Inl i \<in> SIGO x1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP (EvolveODE x1 x2)))
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i |i. Inl i \<in> SIGO x1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> \<Union> (SFV \<sigma> ` (({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> SIGP (EvolveODE x1 x2)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> (case SFunctions \<sigma> xa of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); Inl xa \<in> SIGO x1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); Inl i \<in> SIGO x1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); Inl i \<in> SIGO x1; SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
 2. \<And>a. \<lbrakk>x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); Inl i \<in> SIGO x1; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>x \<in> FVT a; Inl i \<in> SIGO x1; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> FVT a; Inl i \<in> SIGO x1; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
using adj_sub_ode_fact[of i x1 x \<sigma> x2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Inl i \<in> SIGO x1; x \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1})

goal (1 subgoal):
 1. \<lbrakk>x \<in> FVT a; Inl i \<in> SIGO x1; SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>xa\<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> (SIGF x2 \<union> {Inl x |x. Inl x \<in> SIGO x1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO x1}). x \<in> SFV \<sigma> xa
[PROOF STEP]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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

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

goal (1 subgoal):
 1. ODE_sem (local.adjoint I \<sigma> \<nu>) (OVar x) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OVar x)
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OVar x)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
osafe (OVar x)

goal (1 subgoal):
 1. ODE_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (OVar x) = ODE_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (OVar x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem (local.adjoint I \<sigma> \<nu>) (OVar x) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OVar x)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OSing x1a x2)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
osafe (OSing x1a x2)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume osafe:"osafe (OSing x1a x2)"
[PROOF STATE]
proof (state)
this:
osafe (OSing x1a x2)

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
osafe (OSing x1a x2)
[PROOF STEP]
have dfree:"dfree x2"
[PROOF STATE]
proof (prove)
using this:
osafe (OSing x1a x2)

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

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have safes:"(\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f')"
      "(\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f') &&& (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')
[PROOF STEP]
using ssafe
[PROOF STATE]
proof (prove)
using this:
ssafe \<sigma>

goal (1 subgoal):
 1. (\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f') &&& (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. (\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f') &&& (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')
[PROOF STEP]
using dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

goal (1 subgoal):
 1. (\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f') &&& (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> dsafe ?f'7
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (2 subgoals):
 1. \<And>x1a x2 \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OSing x1a x2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OSing x1a x2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OSing x1a x2)
 2. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sem:"sterm_sem (local.adjoint I \<sigma> \<nu>) x2 = sterm_sem (local.adjoint I \<sigma> \<omega>) x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) x2 = sterm_sem (local.adjoint I \<sigma> \<omega>) x2
[PROOF STEP]
using uadmit_sterm_adjoint'[of \<sigma> \<nu> \<omega> x2 I, OF safes, of "(\<lambda> x y. x)" "(\<lambda> x y. x)"] VA
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> SFunctions \<sigma> f = Some f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> SPredicates \<sigma> f = Some f'; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2 = sterm_sem (local.adjoint I \<sigma> \<omega>) x2
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OSing x1a x2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

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

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

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

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OProd ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> ?\<nu>7) ODE1 = ODE_sem (local.adjoint I \<sigma> ?\<omega>7) ODE1
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> ?\<nu>7) ODE2 = ODE_sem (local.adjoint I \<sigma> ?\<omega>7) ODE2
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
osafe (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume IH1:"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow>
      osafe ODE1 \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1"
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> ?\<nu>7) ODE1 = ODE_sem (local.adjoint I \<sigma> ?\<omega>7) ODE1

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume IH2:"\<And>\<nu> \<omega>. Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow>
    osafe ODE2 \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2"
[PROOF STATE]
proof (state)
this:
\<lbrakk>Vagree ?\<nu>7 ?\<omega>7 (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> ?\<nu>7) ODE2 = ODE_sem (local.adjoint I \<sigma> ?\<omega>7) ODE2

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
assume safe:"osafe (OProd ODE1 ODE2)"
[PROOF STATE]
proof (state)
this:
osafe (OProd ODE1 ODE2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
from safe
[PROOF STATE]
proof (chain)
picking this:
osafe (OProd ODE1 ODE2)
[PROOF STEP]
have safe1:"osafe ODE1" and safe2:"osafe ODE2"
[PROOF STATE]
proof (prove)
using this:
osafe (OProd ODE1 ODE2)

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

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sub1:"(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
have sub2:"(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (1 subgoal):
 1. \<And>ODE1 ODE2 \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE1}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE1\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1; \<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe ODE2\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2; Vagree \<nu> \<omega> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); osafe (OProd ODE1 ODE2)\<rbrakk> \<Longrightarrow> ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (1 subgoal):
 1. ODE_sem (local.adjoint I \<sigma> \<nu>) (OProd ODE1 ODE2) = ODE_sem (local.adjoint I \<sigma> \<omega>) (OProd ODE1 ODE2)
[PROOF STEP]
using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2]
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{i |i. Inl i \<in> SIGO ODE2}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<subseteq> (\<Union>i\<in>{i |i. Inl i \<in> SIGO (OProd ODE1 ODE2)}. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
ODE_sem (local.adjoint I \<sigma> \<nu>) ODE1 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE1
ODE_sem (local.adjoint I \<sigma> \<nu>) ODE2 = ODE_sem (local.adjoint I \<sigma> \<omega>) ODE2

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

goal:
No subgoals!
[PROOF STEP]
qed