[STATEMENT]
lemma uadmit_sterm_adjoint':
  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  "Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> sterm_sem (adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (adjoint I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint 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>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus \<theta>1 \<theta>2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>1; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>2; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times \<theta>1 \<theta>2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
 6. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 7. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
case (Plus \<theta>1 \<theta>2)
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>1
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>2
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus \<theta>1 \<theta>2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

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

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

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

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

goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) (Plus \<theta>1 \<theta>2) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Plus \<theta>1 \<theta>2)
[PROOF STEP]
using IH1[OF SIGT_plus1[OF VA]] IH2[OF SIGT_plus2[OF VA]]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus \<theta>1 \<theta>2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>1
sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>2

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

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

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

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

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

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

goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) (Times \<theta>1 \<theta>2) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Times \<theta>1 \<theta>2)
[PROOF STEP]
using IH1[OF SIGT_times1[OF VA]] IH2[OF SIGT_times2[OF VA]]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times \<theta>1 \<theta>2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>1 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>1
sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta>2 = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>2

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

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint 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>SIGT ?x2aa7. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ?x2aa7 = sterm_sem (local.adjoint I \<sigma> \<omega>) ?x2aa7
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

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

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint 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>SIGT ?x7. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ?x7 = sterm_sem (local.adjoint I \<sigma> \<omega>) ?x7
[PROOF STEP]
have IH':"\<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of Some a \<Rightarrow> FVT a | None \<Rightarrow> {}) \<Longrightarrow>
    sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x7 \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ?x7. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ?x7 = sterm_sem (local.adjoint I \<sigma> \<omega>) ?x7

goal (1 subgoal):
 1. \<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) = sterm_sem (local.adjoint 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>SIGT ?x7. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ?x7 = sterm_sem (local.adjoint I \<sigma> \<omega>) ?x7
?f ?x \<in> range ?f

goal (1 subgoal):
 1. \<And>j. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (x2a ?j7). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a ?j7) = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a ?j7)

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

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

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

goal (1 subgoal):
 1. \<And>j. (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<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>{x1a} \<union> (\<Union>i. SIGT (x2a i)). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>{x1a} \<union> (\<Union>i. SIGT (x2a i)). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<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>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (x2a j). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (x2a ?j7). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)

goal (5 subgoals):
 1. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint 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>SIGT (Var x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Var x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Var x)
 2. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Const x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Const x) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT x2aa. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) x2aa = sterm_sem (local.adjoint I \<sigma> \<omega>) x2aa; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)
 4. \<And>x. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT ($' x). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) ($' x) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($' x)
 5. \<And>\<theta>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>SIGT \<theta>. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) \<theta> = sterm_sem (local.adjoint I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Differential \<theta>). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> sterm_sem (local.adjoint I \<sigma> \<nu>) (Differential \<theta>) = sterm_sem (local.adjoint I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have VAsub:"\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> (FVT a) \<subseteq> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of Some a \<Rightarrow> FVT a | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> FVT a \<subseteq> (\<Union>i\<in>SIGT ($f x1a x2a). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some a \<Rightarrow> FVT a)
[PROOF STEP]
using SIGT
[PROOF STATE]
proof (prove)
using this:
x1a \<in> SIGT ($f x1a x2a)

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

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

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

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

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

goal (1 subgoal):
 1. sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint 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. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
apply(cases "SFunctions \<sigma> x1a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = None\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
 2. \<And>x a. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = Some a\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = Some a\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
 2. \<And>x. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = None\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
subgoal for x a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = Some a\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = Some a\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
assume VA:"(\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a))"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> x1a = Some ?a7 \<Longrightarrow> Vagree \<nu> \<omega> (FVT ?a7)

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = Some a\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
have "\<And>R. Functions (local.adjoint I \<sigma> \<nu>) x1a R = Functions (local.adjoint I \<sigma> \<omega>) x1a R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>R. Functions (local.adjoint I \<sigma> \<nu>) x1a R = Functions (local.adjoint I \<sigma> \<omega>) x1a R
[PROOF STEP]
using dsem some
[PROOF STATE]
proof (prove)
using this:
dterm_sem (extendf I ?R7) a \<nu> = dterm_sem (extendf I ?R7) a \<omega>
SFunctions \<sigma> x1a = Some a

goal (1 subgoal):
 1. \<And>R. Functions (local.adjoint I \<sigma> \<nu>) x1a R = Functions (local.adjoint I \<sigma> \<omega>) x1a R
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
using this:
dterm_sem (extendf I ?R7) a \<nu> = dterm_sem (extendf I ?R7) a \<omega>
SFunctions \<sigma> x1a = Some a

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem (local.adjoint I \<sigma> \<nu>) (x2a j) x = sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a j) x; SFunctions \<sigma> x1a = None\<rbrakk> \<Longrightarrow> Functions (local.adjoint I \<sigma> \<nu>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x) = Functions (local.adjoint I \<sigma> \<omega>) x1a (\<chi>i. sterm_sem (local.adjoint I \<sigma> \<omega>) (x2a i) x)
[PROOF STEP]
unfolding adjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>a. SFunctions \<sigma> x1a = Some a \<Longrightarrow> Vagree \<nu> \<omega> (FVT a); \<And>j. \<forall>x. sterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (x2a j) x = sterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (x2a j) x; SFunctions \<sigma> x1a = None\<rbrakk> \<Longrightarrow> Functions \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> x1a (\<chi>i. sterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (x2a i) x) = Functions \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> x1a (\<chi>i. sterm_sem \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> (x2a i) x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sterm_sem (local.adjoint I \<sigma> \<nu>) ($f x1a x2a) = sterm_sem (local.adjoint I \<sigma> \<omega>) ($f x1a x2a)

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

\<comment> \<open>Not used, but good practice for \<open>dterm\<close> adjoint\<close>