[STATEMENT]
lemma uadmit_dterm_adjoint:
  assumes TUA:"TUadmit \<sigma> \<theta> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dfree:"\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dfree f'"
  assumes fsafe:"\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow>  fsafe f'"
  assumes dsafe:"dsafe \<theta>"
  assumes good_interp:"is_interp I"
  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]
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 (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
have "\<And>x. x \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> x \<in> (-U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> x \<in> - U
[PROOF STEP]
using TUA
[PROOF STATE]
proof (prove)
using this:
TUadmit \<sigma> \<theta> U

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> x \<in> - U
[PROOF STEP]
unfolding TUadmit_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<inter> U = {}

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> x \<in> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x8 \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> ?x8 \<in> - U

goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x8 \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> ?x8 \<in> - U
[PROOF STEP]
have sub1:"(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<subseteq> -U"
[PROOF STATE]
proof (prove)
using this:
?x8 \<in> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> ?x8 \<in> - U

goal (1 subgoal):
 1. (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> - U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> - U

goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> - U
[PROOF STEP]
have VA':"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<subseteq> - U

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

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)

goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)

goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
using uadmit_dterm_adjoint'[OF dfree fsafe good_interp VA' dsafe]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
\<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> SFunctions \<sigma> (?f16 f f') = Some f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> SPredicates \<sigma> (?f8 f f') = Some f'\<rbrakk> \<Longrightarrow> dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>

goal (1 subgoal):
 1. dterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = dterm_sem (local.adjoint I \<sigma> \<omega>) \<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