[STATEMENT]
lemma uadmit_sterm_adjoint:
  assumes TUA:"TUadmit \<sigma> \<theta> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dsafe:"\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'"
  assumes fsafe:"\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'"
  shows  "sterm_sem (adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (adjoint I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>
[PROOF STEP]
using uadmit_sterm_adjoint'[OF dsafe fsafe VA']
[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> sterm_sem (local.adjoint ?I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint ?I \<sigma> \<omega>) \<theta>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uadmit_sterm_ntadjoint':
  assumes dsafe:"\<And>i. dsafe (\<sigma> i)"
  shows  "Vagree \<nu> \<omega> ((\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
proof (induct "\<theta>")
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
case (Plus \<theta>1 \<theta>2)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume IH1:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1

goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume IH2:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2

goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> ((\<Union> i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i)))"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
from VA
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))
[PROOF STEP]
have VA1:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))"
    and  VA2:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) &&& Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) &&& (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))

goal (7 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Plus \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
[PROOF STEP]
using IH1[OF VA1] IH2[OF VA2]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1
sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2

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

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
case (Times \<theta>1 \<theta>2)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume IH1:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume IH2:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> ((\<Union> i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i)))"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
from VA
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))
[PROOF STEP]
have VA1:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))"
  and  VA2:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) &&& Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) &&& (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))

goal (6 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Times \<theta>1 \<theta>2)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 5. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 6. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (adjointFO I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
[PROOF STEP]
using IH1[OF VA1] IH2[OF VA2]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>1}. FVT (\<sigma> i))
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>2}. FVT (\<sigma> i))
sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>1 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>1
sterm_sem (adjointFO I \<sigma> \<nu>) \<theta>2 = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>2

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

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
case (Function x1a x2a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2aa7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ?x2aa7}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ?x2aa7 = sterm_sem (adjointFO I \<sigma> \<omega>) ?x2aa7
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume IH:"\<And>x. x \<in> range x2a \<Longrightarrow> Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT x}. FVT (\<sigma> i)) \<Longrightarrow>
    sterm_sem (adjointFO I \<sigma> \<nu>) x = sterm_sem (adjointFO I \<sigma> \<omega>) x"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ?x7}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ?x7 = sterm_sem (adjointFO I \<sigma> \<omega>) ?x7

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ?x7}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ?x7 = sterm_sem (adjointFO I \<sigma> \<omega>) ?x7
[PROOF STEP]
have IH':"\<And>j. Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<Longrightarrow>
    sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ?x7}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ?x7 = sterm_sem (adjointFO I \<sigma> \<omega>) ?x7

goal (1 subgoal):
 1. \<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j)
[PROOF STEP]
using rangeI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ?x7}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ?x7 = sterm_sem (adjointFO I \<sigma> \<omega>) ?x7
?f ?x \<in> range ?f

goal (1 subgoal):
 1. \<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a ?j7)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (x2a ?j7) = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a ?j7)

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
assume VA:"Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i)) "
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
from VA
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))
[PROOF STEP]
have VAs:"\<And>j. Vagree \<nu> \<omega> (\<Union> i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))

goal (1 subgoal):
 1. \<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i))
[PROOF STEP]
unfolding Vagree_def SIGT.simps
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> {x1a} \<union> (\<Union>i. SIGT (x2a i))}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> {x1a} \<union> (\<Union>i. SIGT (x2a i))}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)

goal (1 subgoal):
 1. \<And>j. (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
using rangeI
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> {x1a} \<union> (\<Union>i. SIGT (x2a i))}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> {x1a} \<union> (\<Union>i. SIGT (x2a i))}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
?f ?x \<in> range ?f

goal (1 subgoal):
 1. \<And>j. (\<forall>i. Inl i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a j)}. FVT (\<sigma> i)) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (x2a ?j7)}. FVT (\<sigma> i))

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have SIGT:"x1a \<in> SIGT ($f x1a x2a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1a \<in> SIGT ($f x1a x2a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1a \<in> SIGT ($f x1a x2a)

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have VAsub:"\<And>a. x1a = Inr a \<Longrightarrow> (FVT (\<sigma> a)) \<subseteq> (\<Union> i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. x1a = Inr a \<Longrightarrow> FVT (\<sigma> a) \<subseteq> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))
[PROOF STEP]
using SIGT
[PROOF STATE]
proof (prove)
using this:
x1a \<in> SIGT ($f x1a x2a)

goal (1 subgoal):
 1. \<And>a. x1a = Inr a \<Longrightarrow> FVT (\<sigma> a) \<subseteq> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1a = Inr ?a7 \<Longrightarrow> FVT (\<sigma> ?a7) \<subseteq> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have VAf:"\<And>a. x1a = Inr a \<Longrightarrow>Vagree \<nu> \<omega> (FVT (\<sigma> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a))
[PROOF STEP]
using agree_sub[OF VAsub VA]
[PROOF STATE]
proof (prove)
using this:
x1a = Inr ?a8 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a8))

goal (1 subgoal):
 1. \<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1a = Inr ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a7))

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT x2aa}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) x2aa = sterm_sem (adjointFO I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($f x1a x2a)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x1a = Inr ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a7))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x1a = Inr ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a7))

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
[PROOF STEP]
using IH'[OF VAs]
[PROOF STATE]
proof (prove)
using this:
x1a = Inr ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a7))
sterm_sem (adjointFO I \<sigma> \<nu>) (x2a ?j7) = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a ?j7)

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)
[PROOF STEP]
apply (auto simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
apply(cases "x1a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inl a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
 2. \<And>x b. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr b\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x b. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr b\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
 2. \<And>x a. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inl a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
subgoal for x a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
assume VA:"(\<And>a.  x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)))"
[PROOF STATE]
proof (state)
this:
x1a = Inr ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> ?a7))

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
assume sems:"(\<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x)"
[PROOF STATE]
proof (state)
this:
\<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a ?j7) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a ?j7) x

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
assume some:"x1a = Inr a"
[PROOF STATE]
proof (state)
this:
x1a = Inr a

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
note FVT = VAf[OF some]
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (FVT (\<sigma> a))

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
from dsafe
[PROOF STATE]
proof (chain)
picking this:
dsafe (\<sigma> ?i7)
[PROOF STEP]
have dsafer:"\<And>i. dsafe (\<sigma> i)"
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. \<And>i. dsafe (\<sigma> i)
[PROOF STEP]
using dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

goal (1 subgoal):
 1. \<And>i. dsafe (\<sigma> i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
have dsem:"dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>
[PROOF STEP]
using coincidence_dterm[OF dsafer FVT] some
[PROOF STATE]
proof (prove)
using this:
dterm_sem ?I (\<sigma> a) \<nu> = dterm_sem ?I (\<sigma> a) \<omega>
x1a = Inr a

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

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>
[PROOF STEP]
have "\<And>R. Functions (adjointFO I \<sigma> \<nu>) x1a R = Functions (adjointFO I \<sigma> \<omega>) x1a R"
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>

goal (1 subgoal):
 1. \<And>R. Functions (adjointFO I \<sigma> \<nu>) x1a R = Functions (adjointFO I \<sigma> \<omega>) x1a R
[PROOF STEP]
using some
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>
x1a = Inr a

goal (1 subgoal):
 1. \<And>R. Functions (adjointFO I \<sigma> \<nu>) x1a R = Functions (adjointFO I \<sigma> \<omega>) x1a R
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>
x1a = Inr a

goal (1 subgoal):
 1. \<And>R. Functions (adjointFO I \<sigma> \<nu>) x1a R = Functions (adjointFO I \<sigma> \<omega>) x1a R
[PROOF STEP]
unfolding adjointFO_def
[PROOF STATE]
proof (prove)
using this:
dterm_sem I (\<sigma> a) \<nu> = dterm_sem I (\<sigma> a) \<omega>
x1a = Inr a

goal (1 subgoal):
 1. \<And>R. Functions \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> x1a R = Functions \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> x1a R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Functions (adjointFO I \<sigma> \<nu>) x1a ?R7 = Functions (adjointFO I \<sigma> \<omega>) x1a ?R7

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Functions (adjointFO I \<sigma> \<nu>) x1a ?R7 = Functions (adjointFO I \<sigma> \<omega>) x1a ?R7
[PROOF STEP]
show "Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi> i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) =
                  Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi> i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)"
[PROOF STATE]
proof (prove)
using this:
Functions (adjointFO I \<sigma> \<nu>) x1a ?R7 = Functions (adjointFO I \<sigma> \<omega>) x1a ?R7

goal (1 subgoal):
 1. Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) x = sterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) x; x1a = Inl a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
unfolding adjointFO_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>x. sterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (x2a j) x = sterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (x2a j) x; x1a = Inl a\<rbrakk> \<Longrightarrow> Functions \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> x1a (\<chi>i. sterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (x2a i) x) = Functions \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> x1a (\<chi>i. sterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<omega>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (x2a i) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sterm_sem (adjointFO I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (adjointFO I \<sigma> \<omega>) ($f x1a x2a)

goal (4 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = sterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = sterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i))\<rbrakk> \<Longrightarrow> sterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma uadmit_sterm_ntadjoint:
  assumes TUA:"NTUadmit \<sigma> \<theta> U"
  assumes VA:"Vagree \<nu> \<omega> (-U)"
  assumes dsafe:"\<And>i . dsafe (\<sigma> i)"
  assumes good_interp:"is_interp I"
  shows  "sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_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:
?x8 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x8 \<in> - U

goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x8 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x8 \<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:
?x8 \<in> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)) \<Longrightarrow> ?x8 \<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. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_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. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
using uadmit_sterm_ntadjoint'[OF  dsafe VA']
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i))
sterm_sem (adjointFO ?I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO ?I \<sigma> \<omega>) \<theta>

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

goal:
No subgoals!
[PROOF STEP]
qed