[STATEMENT]
lemma uadmit_prog_adjoint:
  assumes PUA:"PUadmit \<sigma> a U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes hpsafe:"hpsafe a"
  assumes ssafe:"ssafe \<sigma>"
  assumes good_interp:"is_interp I"
  shows "prog_sem (adjoint I \<sigma> \<nu>) a = prog_sem (adjoint I \<sigma> \<omega>) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a
[PROOF STEP]
have sub:"(\<Union>x\<in>SDom \<sigma> \<inter> SIGP a. SFV \<sigma> x) \<subseteq> -U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)) \<subseteq> - U
[PROOF STEP]
using PUA
[PROOF STATE]
proof (prove)
using this:
PUadmit \<sigma> a U

goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)) \<subseteq> - U
[PROOF STEP]
unfolding PUadmit_def
[PROOF STATE]
proof (prove)
using this:
\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)) \<inter> U = {}

goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)) \<subseteq> - U

goal (1 subgoal):
 1. prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union>x\<in>SDom \<sigma> \<inter> SIGP a. SFV \<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))
[PROOF STEP]
using agree_sub[OF sub VA]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))

goal (1 subgoal):
 1. prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a
[PROOF STEP]
apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))
 2. hpsafe a
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGP a)))
[PROOF STEP]
by (rule VA')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hpsafe a
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hpsafe a
[PROOF STEP]
by (rule hpsafe)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
prog_sem (local.adjoint I \<sigma> \<nu>) a = prog_sem (local.adjoint I \<sigma> \<omega>) a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uadmit_fml_adjoint:
  assumes FUA:"FUadmit \<sigma> \<phi> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes fsafe:"fsafe \<phi>"
  assumes ssafe:"ssafe \<sigma>"
  assumes good_interp:"is_interp I"
  shows "fml_sem (adjoint I \<sigma> \<nu>) \<phi> = fml_sem (adjoint I \<sigma> \<omega>) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>
[PROOF STEP]
have sub:"(\<Union>x\<in>SDom \<sigma> \<inter> SIGF \<phi>. SFV \<sigma> x) \<subseteq> -U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)) \<subseteq> - U
[PROOF STEP]
using FUA
[PROOF STATE]
proof (prove)
using this:
FUadmit \<sigma> \<phi> U

goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)) \<subseteq> - U
[PROOF STEP]
unfolding FUadmit_def
[PROOF STATE]
proof (prove)
using this:
\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)) \<inter> U = {}

goal (1 subgoal):
 1. \<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)) \<subseteq> - U

goal (1 subgoal):
 1. fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union>x\<in>SDom \<sigma> \<inter> SIGF \<phi>. SFV \<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))
[PROOF STEP]
using agree_sub[OF sub VA]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))

goal (1 subgoal):
 1. fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>
[PROOF STEP]
apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))
 2. fsafe \<phi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union> (SFV \<sigma> ` (SDom \<sigma> \<inter> SIGF \<phi>)))
[PROOF STEP]
by (rule VA')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe \<phi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe \<phi>
[PROOF STEP]
by (rule fsafe)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fml_sem (local.adjoint I \<sigma> \<nu>) \<phi> = fml_sem (local.adjoint I \<sigma> \<omega>) \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntadj_sub_assign:"\<And>e \<sigma> x. (\<Union>y\<in>{y. Inr y \<in> SIGT e}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGP (Assign x e)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e \<sigma> x. (\<Union>y\<in>{y. Inr y \<in> SIGT e}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGP (x := e)}. FVT (\<sigma> y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ntadj_sub_diff_assign:"\<And>e \<sigma> x. (\<Union>y\<in>{y. Inl y \<in> SIGT e}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGP (DiffAssign x e)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e \<sigma> x. (\<Union>y\<in>{y. Inl y \<in> SIGT e}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGP (DiffAssign x e)}. FVT (\<sigma> y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ntadj_sub_geq1:"\<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl y \<in> SIGT x1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF (Geq x1 x2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl y \<in> SIGT x1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF (Geq x1 x2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ntadj_sub_geq2:"\<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl y \<in> SIGT x2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF (Geq x1 x2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl y \<in> SIGT x2}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF (Geq x1 x2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ntadj_sub_prop:"\<And>\<sigma> x1 x2 j. (\<Union>y\<in>{y. Inl y \<in> SIGT (x2 j)}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF ($\<phi> x1 x2)}.FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2 j. (\<Union>y\<in>{y. Inl y \<in> SIGT (x2 j)}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGF ($\<phi> x1 x2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto


[STATEMENT]
lemma ntadj_sub_ode:"\<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGO x1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGP (EvolveODE x1 x2)}. FVT (\<sigma> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x1 x2. (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGO x1}. FVT (\<sigma> y)) \<subseteq> (\<Union>y\<in>{y. Inl (Inl y) \<in> SIGP (EvolveODE x1 x2)}. FVT (\<sigma> y))
[PROOF STEP]
by auto