[STATEMENT]
lemma errMOD_igSubstIGAbsSTR:
fixes MOD :: "('index,'bindex,'varSort,'sort,'opSym,'var,'gTerm,'gAbs)model"
assumes *: "igAbsIPresIGWls MOD" and **: "igWlsDisj MOD"
and ***: "igSubstIPresIGWls MOD" and ****: "igSubstIGAbs MOD"
shows "igSubstIGAbsSTR (errMOD MOD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igSubstIGAbsSTR (errMOD MOD)
[PROOF STEP]
unfolding igSubstIGAbsSTR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys y Y xs x X. (xs \<noteq> ys \<or> x \<noteq> y) \<and> eFresh MOD xs x Y \<longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
proof(clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
fix ys xs ::'varSort and y x ::'var and eX eY
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
assume diff: "xs \<noteq> ys \<or> x \<noteq> y"
  and x_fresh_Y: "eFresh MOD xs x eY"
[PROOF STATE]
proof (state)
this:
xs \<noteq> ys \<or> x \<noteq> y
eFresh MOD xs x eY

goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
show "eSubstAbs MOD ys eY y (eAbs MOD xs x eX) =
        eAbs MOD xs x (eSubst MOD ys eY y eX)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "eX \<noteq> ERR \<and> eY \<noteq> ERR")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
eX \<noteq> ERR \<and> eY \<noteq> ERR

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
define X and Y where "X \<equiv> check eX" and "Y \<equiv> check eY"
[PROOF STATE]
proof (state)
this:
X \<equiv> check eX
Y \<equiv> check eY

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence eX: "eX = OK X" and eY: "eY = OK Y"
[PROOF STATE]
proof (prove)
using this:
X \<equiv> check eX
Y \<equiv> check eY

goal (1 subgoal):
 1. eX = OK X &&& eY = OK Y
[PROOF STEP]
unfolding X_def Y_def
[PROOF STATE]
proof (prove)
using this:
check eX \<equiv> check eX
check eY \<equiv> check eY

goal (1 subgoal):
 1. eX = OK (check eX) &&& eY = OK (check eY)
[PROOF STEP]
using True OK_check
[PROOF STATE]
proof (prove)
using this:
check eX \<equiv> check eX
check eY \<equiv> check eY
eX \<noteq> ERR \<and> eY \<noteq> ERR
?eX \<noteq> ERR \<Longrightarrow> OK (check ?eX) = ?eX

goal (1 subgoal):
 1. eX = OK (check eX) &&& eY = OK (check eY)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eX = OK X
eY = OK Y

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "(\<exists> s. isInBar (xs,s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y
[PROOF STEP]
obtain s where xs_s: "isInBar (xs, s)" and X: "igWls MOD s X" 
      and Y: "igWls MOD (asSort ys) Y"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence "igWlsAbs MOD (xs,s) (igAbs MOD xs x X)"
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y
igAbsIPresIGWls MOD

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
unfolding igAbsIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y
\<forall>xs s x X. isInBar (xs, s) \<and> igWls MOD s X \<longrightarrow> igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have "igWls MOD s (igSubst MOD ys Y y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
using X Y ***
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
igSubstIPresIGWls MOD

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
\<forall>ys Y y s X. igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> igWls MOD s (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have "igFresh MOD xs x Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
using x_fresh_Y Y
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
unfolding eY
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x (OK Y)
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igFresh MOD xs x Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
unfolding eX eY
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y

goal (1 subgoal):
 1. eSubstAbs MOD ys (OK Y) y (eAbs MOD xs x (OK X)) = eAbs MOD xs x (eSubst MOD ys (OK Y) y (OK X))
[PROOF STEP]
using xs_s X Y
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. eSubstAbs MOD ys (OK Y) y (eAbs MOD xs x (OK X)) = eAbs MOD xs x (eSubst MOD ys (OK Y) y (OK X))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
using x_fresh_Y diff ****
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
xs \<noteq> ys \<or> x \<noteq> y
igSubstIGAbs MOD

goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIGAbs_def
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
xs \<noteq> ys \<or> x \<noteq> y
\<forall>ys y Y xs x s X. isInBar (xs, s) \<and> igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> (xs \<noteq> ys \<or> x \<noteq> y) \<and> igFresh MOD xs x Y \<longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)

goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "(EX s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y
[PROOF STEP]
obtain s where X: "igWls MOD s X" and Y: "igWls MOD (asSort ys) Y"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
igWls MOD s X
igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence 2: "~ isInBar (xs,s)"
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. \<not> isInBar (xs, s)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)

goal (1 subgoal):
 1. \<not> isInBar (xs, s)
[PROOF STEP]
by (auto simp: eX eY)
[PROOF STATE]
proof (state)
this:
\<not> isInBar (xs, s)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
let ?Xsb = "igSubst MOD ys Y y X"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have Xsb: "igWls MOD s ?Xsb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
using Y X ***
[PROOF STATE]
proof (prove)
using this:
igWls MOD (asSort ys) Y
igWls MOD s X
igSubstIPresIGWls MOD

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
igWls MOD (asSort ys) Y
igWls MOD s X
\<forall>ys Y y s X. igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> igWls MOD s (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
assume 3: "isInBar (xs,s')" and "igWls MOD s' ?Xsb"
[PROOF STATE]
proof (state)
this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence "s = s'"
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using Xsb **
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)
igWls MOD s (igSubst MOD ys Y y X)
igWlsDisj MOD

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
unfolding igWlsDisj_def
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)
igWls MOD s (igSubst MOD ys Y y X)
\<forall>s s' X. igWls MOD s X \<and> igWls MOD s' X \<longrightarrow> s = s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = s'

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
s = s'

goal (1 subgoal):
 1. False
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
s = s'
\<not> isInBar (xs, s)
isInBar (xs, s')

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: eX eY)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
using False Y eAbs_simp2 X eX eY
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)
igWls MOD (asSort ys) Y
\<forall>s. \<not> (isInBar (?xs, s) \<and> igWls ?MOD s ?X) \<Longrightarrow> eAbs ?MOD ?xs ?x (OK ?X) = ERR
igWls MOD s X
eX = OK X
eY = OK Y

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
qed(auto simp add: eX eY)
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal:
No subgoals!
[PROOF STEP]
qed