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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>j. dsafe (x2a j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (x2a ?j7)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>a. x1a = Inr a \<Longrightarrow> Vagree \<nu> \<omega> (FVT (\<sigma> a)); \<And>j. \<forall>a b. dterm_sem (adjointFO I \<sigma> \<nu>) (x2a j) (a, b) = dterm_sem (adjointFO I \<sigma> \<omega>) (x2a j) (a, b); x1a = Inr a\<rbrakk> \<Longrightarrow> Functions (adjointFO I \<sigma> \<nu>) x1a (\<chi>i. dterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) (x1, x2)) = Functions (adjointFO I \<sigma> \<omega>) x1a (\<chi>i. dterm_sem (adjointFO I \<sigma> \<omega>) (x2a i) (x1, x2))
[PROOF STEP]
have dsafe:"\<And>i. dsafe (\<sigma> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dsafe (\<sigma> i)
[PROOF STEP]
using dfree dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dsafe (Differential \<theta>)
[PROOF STEP]
have free:"dfree \<theta>"
[PROOF STATE]
proof (prove)
using this:
dsafe (Differential \<theta>)

goal (1 subgoal):
 1. dfree \<theta>
[PROOF STEP]
by (auto dest: dsafe.cases)
[PROOF STATE]
proof (state)
this:
dfree \<theta>

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

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have dsafe:"\<And>i. dsafe (\<sigma> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. dsafe (\<sigma> i)
[PROOF STEP]
using dfree dfree_is_dsafe
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)
dfree ?\<theta> \<Longrightarrow> dsafe ?\<theta>

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have sem:"sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
using uadmit_sterm_ntadjoint'[OF dsafe  VA']
[PROOF STATE]
proof (prove)
using this:
sterm_sem (adjointFO ?I \<sigma> \<nu>) \<theta> = sterm_sem (adjointFO ?I \<sigma> \<omega>) \<theta>

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have good1:"is_interp (adjointFO I \<sigma> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp (adjointFO I \<sigma> \<nu>)
[PROOF STEP]
using adjointFO_safe[OF good_interp dsafe, of "\<lambda>i. i"]
[PROOF STATE]
proof (prove)
using this:
is_interp (adjointFO I \<sigma> ?\<nu>)

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have good2:"is_interp (adjointFO I \<sigma> \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp (adjointFO I \<sigma> \<omega>)
[PROOF STEP]
using adjointFO_safe[OF good_interp dsafe, of "\<lambda>i. i"]
[PROOF STATE]
proof (prove)
using this:
is_interp (adjointFO I \<sigma> ?\<nu>)

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

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
have frech:"frechet (adjointFO I \<sigma> \<nu>) \<theta> = frechet (adjointFO I \<sigma> \<omega>) \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet (adjointFO I \<sigma> \<nu>) \<theta> = frechet (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
apply (auto simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. frechet (adjointFO I \<sigma> \<nu>) \<theta> x xa = frechet (adjointFO I \<sigma> \<omega>) \<theta> x xa
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet (adjointFO I \<sigma> \<nu>) \<theta> a b = frechet (adjointFO I \<sigma> \<omega>) \<theta> a b
[PROOF STEP]
using sterm_determines_frechet [OF good1 good2 free free sem, of "(a,b)"]
[PROOF STATE]
proof (prove)
using this:
frechet (adjointFO I \<sigma> \<nu>) \<theta> (fst (a, b)) (snd (a, b)) = frechet (adjointFO I \<sigma> \<omega>) \<theta> (fst (a, b)) (snd (a, b))

goal (1 subgoal):
 1. frechet (adjointFO I \<sigma> \<nu>) \<theta> a b = frechet (adjointFO I \<sigma> \<omega>) \<theta> a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
frechet (adjointFO I \<sigma> \<nu>) \<theta> = frechet (adjointFO I \<sigma> \<omega>) \<theta>

goal (4 subgoals):
 1. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Var x)}. FVT (\<sigma> i)); dsafe (Var x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Var x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Var x)
 2. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Const x)}. FVT (\<sigma> i)); dsafe (Const x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Const x) = dterm_sem (adjointFO I \<sigma> \<omega>) (Const x)
 3. \<And>x \<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT ($' x)}. FVT (\<sigma> i)); dsafe ($' x)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) ($' x) = dterm_sem (adjointFO I \<sigma> \<omega>) ($' x)
 4. \<And>\<theta> \<nu> \<omega>. \<lbrakk>\<And>\<nu> \<omega>. \<lbrakk>Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT \<theta>}. FVT (\<sigma> i)); dsafe \<theta>\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) \<theta> = dterm_sem (adjointFO I \<sigma> \<omega>) \<theta>; Vagree \<nu> \<omega> (\<Union>i\<in>{i. Inr i \<in> SIGT (Differential \<theta>)}. FVT (\<sigma> i)); dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frechet (adjointFO I \<sigma> \<nu>) \<theta> = frechet (adjointFO I \<sigma> \<omega>) \<theta>
[PROOF STEP]
show "dterm_sem (adjointFO I \<sigma> \<nu>) (Differential \<theta>) = dterm_sem (adjointFO I \<sigma> \<omega>) (Differential \<theta>)"
[PROOF STATE]
proof (prove)
using this:
frechet (adjointFO I \<sigma> \<nu>) \<theta> = frechet (adjointFO I \<sigma> \<omega>) \<theta>

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

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