[STATEMENT]
lemma alphaAll_trans:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
shows
"(qGood X \<longrightarrow> (\<forall> X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) \<and>
 (qGoodAbs A \<longrightarrow> (\<forall> A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) \<and> (qGoodAbs A \<longrightarrow> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A''))
[PROOF STEP]
proof(induction rule: qGood_qTerm_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs x. \<forall>X' X''. qVar xs x #= X' \<and> X' #= X'' \<longrightarrow> qVar xs x #= X''
 2. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp\<rbrakk> \<Longrightarrow> \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
case (Var xs x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>xs x. \<forall>X' X''. qVar xs x #= X' \<and> X' #= X'' \<longrightarrow> qVar xs x #= X''
 2. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp\<rbrakk> \<Longrightarrow> \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X' X''. qVar xs x #= X' \<and> X' #= X'' \<longrightarrow> qVar xs x #= X''
[PROOF STEP]
by (simp add: qVar_alpha_iff)
[PROOF STATE]
proof (state)
this:
\<forall>X' X''. qVar xs x #= X' \<and> X' #= X'' \<longrightarrow> qVar xs x #= X''

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp\<rbrakk> \<Longrightarrow> \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp\<rbrakk> \<Longrightarrow> \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
case (Op delta inp binp)
[PROOF STATE]
proof (state)
this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp
liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp\<rbrakk> \<Longrightarrow> \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
fix X' X''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
assume "qOp delta inp binp #= X'" and *: "X' #= X''"
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X'
X' #= X''

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qOp delta inp binp #= X'
X' #= X''
[PROOF STEP]
obtain inp' binp' where
    1: "X' = qOp delta inp' binp'" and
    2: "sameDom inp inp' \<and> sameDom binp binp'" and
    3: "liftAll2 (\<lambda>Y Y'. Y #= Y') inp inp' \<and>
      liftAll2 (\<lambda>A A'. A $= A') binp binp'"
[PROOF STATE]
proof (prove)
using this:
qOp delta inp binp #= X'
X' #= X''

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; sameDom inp inp' \<and> sameDom binp binp'; liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qOp_alpha_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>inp' binp'. X' = qOp delta inp' binp' \<and> sameDom inp inp' \<and> sameDom binp binp' \<and> liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'
X' #= X''

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; sameDom inp inp' \<and> sameDom binp binp'; liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
obtain inp'' binp'' where
    11: "X'' = qOp delta inp'' binp''" and
    22: "sameDom inp' inp'' \<and> sameDom binp' binp''" and
    33: "liftAll2 (\<lambda>Y' Y''. Y' #= Y'') inp' inp'' \<and>
         liftAll2 (\<lambda>A' A''. A' $= A'') binp' binp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>inp'' binp''. \<lbrakk>X'' = qOp delta inp'' binp''; sameDom inp' inp'' \<and> sameDom binp' binp''; liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
X' #= X''

goal (1 subgoal):
 1. (\<And>inp'' binp''. \<lbrakk>X'' = qOp delta inp'' binp''; sameDom inp' inp'' \<and> sameDom binp' binp''; liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
using this:
qOp delta inp' binp' #= X''

goal (1 subgoal):
 1. (\<And>inp'' binp''. \<lbrakk>X'' = qOp delta inp'' binp''; sameDom inp' inp'' \<and> sameDom binp' binp''; liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qOp_alpha_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>inp'a binp'a. X'' = qOp delta inp'a binp'a \<and> sameDom inp' inp'a \<and> sameDom binp' binp'a \<and> liftAll2 (#=) inp' inp'a \<and> liftAll2 ($=) binp' binp'a

goal (1 subgoal):
 1. (\<And>inp'' binp''. \<lbrakk>X'' = qOp delta inp'' binp''; sameDom inp' inp'' \<and> sameDom binp' binp''; liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X'' = qOp delta inp'' binp''
sameDom inp' inp'' \<and> sameDom binp' binp''
liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
have "liftAll2 (#=) inp inp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 (#=) inp inp''
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i v1 v2. inp i = Some v1 \<and> inp'' i = Some v2 \<longrightarrow> v1 #= v2
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
fix i Y Y''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
assume inp: "inp i = Some Y" and inp'': "inp'' i = Some Y''"
[PROOF STATE]
proof (state)
this:
inp i = Some Y
inp'' i = Some Y''

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inp i = Some Y
inp'' i = Some Y''
[PROOF STEP]
obtain Y' where inp': "inp' i = Some Y'"
[PROOF STATE]
proof (prove)
using this:
inp i = Some Y
inp'' i = Some Y''

goal (1 subgoal):
 1. (\<And>Y'. inp' i = Some Y' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
inp i = Some Y
inp'' i = Some Y''
sameDom inp inp' \<and> sameDom binp binp'

goal (1 subgoal):
 1. (\<And>Y'. inp' i = Some Y' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
using this:
inp i = Some Y
inp'' i = Some Y''
(\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None))

goal (1 subgoal):
 1. (\<And>Y'. inp' i = Some Y' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inp' i = Some Y'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
hence "Y #= Y'"
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'

goal (1 subgoal):
 1. Y #= Y'
[PROOF STEP]
using inp 3
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
inp i = Some Y
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. Y #= Y'
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
inp i = Some Y
(\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> v1 #= v2) \<and> (\<forall>i v1 v2. binp i = Some v1 \<and> binp' i = Some v2 \<longrightarrow> v1 $= v2)

goal (1 subgoal):
 1. Y #= Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y #= Y'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y #= Y'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
have "Y' #= Y''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y' #= Y''
[PROOF STEP]
using inp' inp'' 33
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
inp'' i = Some Y''
liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''

goal (1 subgoal):
 1. Y' #= Y''
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
inp'' i = Some Y''
(\<forall>i v1 v2. inp' i = Some v1 \<and> inp'' i = Some v2 \<longrightarrow> v1 #= v2) \<and> (\<forall>i v1 v2. binp' i = Some v1 \<and> binp'' i = Some v2 \<longrightarrow> v1 $= v2)

goal (1 subgoal):
 1. Y' #= Y''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y' #= Y''

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>inp i = Some v1; inp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 #= v2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y #= Y'
Y' #= Y''
[PROOF STEP]
show "Y #= Y''"
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
Y' #= Y''

goal (1 subgoal):
 1. Y #= Y''
[PROOF STEP]
using inp Op.IH
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
Y' #= Y''
inp i = Some Y
liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp
liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp

goal (1 subgoal):
 1. Y #= Y''
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
Y' #= Y''
inp i = Some Y
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> (\<forall>X' X''. v #= X' \<and> X' #= X'' \<longrightarrow> v #= X'')
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> (\<forall>A' A''. v $= A' \<and> A' $= A'' \<longrightarrow> v $= A'')

goal (1 subgoal):
 1. Y #= Y''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y #= Y''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
liftAll2 (#=) inp inp''

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
liftAll2 (#=) inp inp''

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
have "liftAll2 ($=) binp binp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 ($=) binp binp''
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i v1 v2. binp i = Some v1 \<and> binp'' i = Some v2 \<longrightarrow> v1 $= v2
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
fix i A A''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
assume binp: "binp i = Some A" and binp'': "binp'' i = Some A''"
[PROOF STATE]
proof (state)
this:
binp i = Some A
binp'' i = Some A''

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
binp i = Some A
binp'' i = Some A''
[PROOF STEP]
obtain A' where binp': "binp' i = Some A'"
[PROOF STATE]
proof (prove)
using this:
binp i = Some A
binp'' i = Some A''

goal (1 subgoal):
 1. (\<And>A'. binp' i = Some A' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
binp i = Some A
binp'' i = Some A''
sameDom inp inp' \<and> sameDom binp binp'

goal (1 subgoal):
 1. (\<And>A'. binp' i = Some A' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
using this:
binp i = Some A
binp'' i = Some A''
(\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None))

goal (1 subgoal):
 1. (\<And>A'. binp' i = Some A' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
binp' i = Some A'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
hence "A $= A'"
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'

goal (1 subgoal):
 1. A $= A'
[PROOF STEP]
using binp 3
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
binp i = Some A
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. A $= A'
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
binp i = Some A
(\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> v1 #= v2) \<and> (\<forall>i v1 v2. binp i = Some v1 \<and> binp' i = Some v2 \<longrightarrow> v1 $= v2)

goal (1 subgoal):
 1. A $= A'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $= A'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $= A'

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
have "A' $= A''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $= A''
[PROOF STEP]
using binp' binp'' 33
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
binp'' i = Some A''
liftAll2 (#=) inp' inp'' \<and> liftAll2 ($=) binp' binp''

goal (1 subgoal):
 1. A' $= A''
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
binp'' i = Some A''
(\<forall>i v1 v2. inp' i = Some v1 \<and> inp'' i = Some v2 \<longrightarrow> v1 #= v2) \<and> (\<forall>i v1 v2. binp' i = Some v1 \<and> binp'' i = Some v2 \<longrightarrow> v1 $= v2)

goal (1 subgoal):
 1. A' $= A''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A' $= A''

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>binp i = Some v1; binp'' i = Some v2\<rbrakk> \<Longrightarrow> v1 $= v2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A $= A'
A' $= A''
[PROOF STEP]
show "A $= A''"
[PROOF STATE]
proof (prove)
using this:
A $= A'
A' $= A''

goal (1 subgoal):
 1. A $= A''
[PROOF STEP]
using binp Op.IH
[PROOF STATE]
proof (prove)
using this:
A $= A'
A' $= A''
binp i = Some A
liftAll (\<lambda>X. qGood X \<and> (\<forall>X' X''. X #= X' \<and> X' #= X'' \<longrightarrow> X #= X'')) inp
liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' A''. A $= A' \<and> A' $= A'' \<longrightarrow> A $= A'')) binp

goal (1 subgoal):
 1. A $= A''
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
A $= A'
A' $= A''
binp i = Some A
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> (\<forall>X' X''. v #= X' \<and> X' #= X'' \<longrightarrow> v #= X'')
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> (\<forall>A' A''. v $= A' \<and> A' $= A'' \<longrightarrow> v $= A'')

goal (1 subgoal):
 1. A $= A''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $= A''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
liftAll2 ($=) binp binp''

goal (1 subgoal):
 1. \<And>X' X''. \<lbrakk>qOp delta inp binp #= X'; X' #= X''\<rbrakk> \<Longrightarrow> qOp delta inp binp #= X''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
liftAll2 (#=) inp inp''
liftAll2 ($=) binp binp''
[PROOF STEP]
show "qOp delta inp binp #= X''"
[PROOF STATE]
proof (prove)
using this:
liftAll2 (#=) inp inp''
liftAll2 ($=) binp binp''

goal (1 subgoal):
 1. qOp delta inp binp #= X''
[PROOF STEP]
by (simp add: 11 2 22 sameDom_trans[of inp inp'] sameDom_trans[of binp binp'])
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>X' X''. qOp delta inp binp #= X' \<and> X' #= X'' \<longrightarrow> qOp delta inp binp #= X''

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
case (Abs xs x X)
[PROOF STATE]
proof (state)
this:
qGood X
qGood ?Y11 \<and> qSkel ?Y11 = qSkel X \<Longrightarrow> \<forall>X' X''. ?Y11 #= X' \<and> X' #= X'' \<longrightarrow> ?Y11 #= X''
(X, ?Y11) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. ?Y11 #= X' \<and> X' #= X'' \<longrightarrow> ?Y11 #= X''

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. Y #= X' \<and> X' #= X'' \<longrightarrow> Y #= X''\<rbrakk> \<Longrightarrow> \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
fix A' A''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
assume "qAbs xs x X $= A'" and *: "A' $= A''"
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= A'
A' $= A''

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= A'
A' $= A''
[PROOF STEP]
obtain x' y X' where A': "A' = qAbs xs x' X'" and y_not: "y \<notin> {x, x'}" and
    y_fresh: "qAFresh xs y X \<and> qAFresh xs y X'" and
    alpha: "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= A'
A' $= A''

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' X'; y \<notin> {x, x'}; qAFresh xs y X \<and> qAFresh xs y X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qAbs_alphaAbs_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x' y X'. A' = qAbs xs x' X' \<and> y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
A' $= A''

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' X'; y \<notin> {x, x'}; qAFresh xs y X \<and> qAFresh xs y X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' = qAbs xs x' X'
y \<notin> {x, x'}
qAFresh xs y X \<and> qAFresh xs y X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
obtain x'' z X'' where A'': "A'' = qAbs xs x'' X''" and z_not: "z \<notin> {x', x''}" and
    z_fresh: "qAFresh xs z X' \<and> qAFresh xs z X''" and
    alpha': "(X' #[[z \<and> x']]_xs) #= (X'' #[[z \<and> x'']]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'' X'' z. \<lbrakk>A'' = qAbs xs x'' X''; z \<notin> {x', x''}; qAFresh xs z X' \<and> qAFresh xs z X''; X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
A' $= A''

goal (1 subgoal):
 1. (\<And>x'' X'' z. \<lbrakk>A'' = qAbs xs x'' X''; z \<notin> {x', x''}; qAFresh xs z X' \<and> qAFresh xs z X''; X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A' qAbs_alphaAbs_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>x'a y X'a. A'' = qAbs xs x'a X'a \<and> y \<notin> {x', x'a} \<and> qAFresh xs y X' \<and> qAFresh xs y X'a \<and> X' #[[y \<and> x']]_xs #= X'a #[[y \<and> x'a]]_xs

goal (1 subgoal):
 1. (\<And>x'' X'' z. \<lbrakk>A'' = qAbs xs x'' X''; z \<notin> {x', x''}; qAFresh xs z X' \<and> qAFresh xs z X''; X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A'' = qAbs xs x'' X''
z \<notin> {x', x''}
qAFresh xs z X' \<and> qAFresh xs z X''
X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have goodX': "qGood X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
using alpha \<open>qGood X\<close> alpha_qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
qGood X
?X #[[?y \<and> ?x]]_?zs #= ?X' #[[?y' \<and> ?x']]_?zs' \<Longrightarrow> qGood ?X = qGood ?X'

goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qGood X'

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
hence goodX'': "qGood X''"
[PROOF STATE]
proof (prove)
using this:
qGood X'

goal (1 subgoal):
 1. qGood X''
[PROOF STEP]
using alpha' alpha_qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X'
X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs
?X #[[?y \<and> ?x]]_?zs #= ?X' #[[?y' \<and> ?x']]_?zs' \<Longrightarrow> qGood ?X = qGood ?X'

goal (1 subgoal):
 1. qGood X''
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qGood X''

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have good: "qGood((X #[[y \<and> x]]_xs)) \<and> qGood((X' #[[z \<and> x']]_xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)
[PROOF STEP]
using \<open>qGood X\<close> goodX' qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
(* *)
[PROOF STATE]
proof (state)
this:
qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
obtain u where u_not: "u \<notin> {x,x',x'',y,z}" and
             u_fresh: "qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<notin> {x, x', x'', y, z}; qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>qGood X\<close> goodX' goodX''
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
qGood X''

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<notin> {x, x', x'', y, z}; qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_qFresh[of "{x,x',x'',y,z}" "{X, X', X''}"]
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
qGood X''
\<lbrakk>finite {x, x', x'', y, z} \<or> |{x, x', x'', y, z}| <o |UNIV|; finite {X, X', X''} \<or> |{X, X', X''}| <o |UNIV|; Ball {X, X', X''} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> {x, x', x'', y, z} \<and> (\<forall>X\<in>{X, X', X''}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<notin> {x, x', x'', y, z}; qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<notin> {x, x', x'', y, z}
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
u \<notin> {x, x', x'', y, z}
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u \<notin> {x, x', x'', y, z}
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "(X #[[u \<and> x]]_xs) = ((X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs
[PROOF STEP]
using u_fresh y_fresh
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs
[PROOF STEP]
by (auto simp add: qAFresh_qSwap_compose)
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "((X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs) #= ((X' #[[y \<and> x']]_xs) #[[u \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs
[PROOF STEP]
using good alpha qSwap_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
\<lbrakk>qGood ?X \<or> qGood ?X'; ?X #= ?X'\<rbrakk> \<Longrightarrow> ?X #[[?z1.0 \<and> ?z2.0]]_?zs #= ?X' #[[?z1.0 \<and> ?z2.0]]_?zs

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "((X' #[[y \<and> x']]_xs) #[[u \<and> y]]_xs) = (X' #[[u \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs = X' #[[u \<and> x']]_xs
[PROOF STEP]
using u_fresh y_fresh
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs = X' #[[u \<and> x']]_xs
[PROOF STEP]
by (auto simp add: qAFresh_qSwap_compose)
[PROOF STATE]
proof (state)
this:
X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs = X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs
X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs
X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs = X' #[[u \<and> x']]_xs
[PROOF STEP]
have "(X #[[u \<and> x]]_xs) #= (X' #[[u \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs
X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs
X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs = X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "(X' #[[u \<and> x']]_xs) = ((X' #[[z \<and> x']]_xs) #[[u \<and> z]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs
[PROOF STEP]
using u_fresh z_fresh
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''
qAFresh xs z X' \<and> qAFresh xs z X''

goal (1 subgoal):
 1. X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs
[PROOF STEP]
by (auto simp add: qAFresh_qSwap_compose)
[PROOF STATE]
proof (state)
this:
X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "((X' #[[z \<and> x']]_xs) #[[u \<and> z]]_xs) #= ((X'' #[[z \<and> x'']]_xs) #[[u \<and> z]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs
[PROOF STEP]
using good alpha' qSwap_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<and> x]]_xs) \<and> qGood (X' #[[z \<and> x']]_xs)
X' #[[z \<and> x']]_xs #= X'' #[[z \<and> x'']]_xs
\<lbrakk>qGood ?X \<or> qGood ?X'; ?X #= ?X'\<rbrakk> \<Longrightarrow> ?X #[[?z1.0 \<and> ?z2.0]]_?zs #= ?X' #[[?z1.0 \<and> ?z2.0]]_?zs

goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "((X'' #[[z \<and> x'']]_xs) #[[u \<and> z]]_xs) = (X'' #[[u \<and> x'']]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs = X'' #[[u \<and> x'']]_xs
[PROOF STEP]
using u_fresh z_fresh
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''
qAFresh xs z X' \<and> qAFresh xs z X''

goal (1 subgoal):
 1. X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs = X'' #[[u \<and> x'']]_xs
[PROOF STEP]
by (auto simp add: qAFresh_qSwap_compose)
[PROOF STATE]
proof (state)
this:
X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs = X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs
X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs
X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs = X'' #[[u \<and> x'']]_xs
[PROOF STEP]
have "(X' #[[u \<and> x']]_xs) #= (X'' #[[u \<and> x'']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X' #[[u \<and> x']]_xs = X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs
X' #[[z \<and> x']]_xs #[[u \<and> z]]_xs #= X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs
X'' #[[z \<and> x'']]_xs #[[u \<and> z]]_xs = X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
have "(X, X #[[u \<and> x]]_xs) \<in> qSwapped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, X #[[u \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
by (simp add: qSwap_qSwapped)
[PROOF STATE]
proof (state)
this:
(X, X #[[u \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs
(X, X #[[u \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
have "(X #[[u \<and> x]]_xs) #= (X'' #[[u \<and> x'']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs
(X, X #[[u \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs
[PROOF STEP]
using Abs.IH
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs
X' #[[u \<and> x']]_xs #= X'' #[[u \<and> x'']]_xs
(X, X #[[u \<and> x]]_xs) \<in> qSwapped
qGood ?Y11 \<and> qSkel ?Y11 = qSkel X \<Longrightarrow> \<forall>X' X''. ?Y11 #= X' \<and> X' #= X'' \<longrightarrow> ?Y11 #= X''
(X, ?Y11) \<in> qSwapped \<Longrightarrow> \<forall>X' X''. ?Y11 #= X' \<and> X' #= X'' \<longrightarrow> ?Y11 #= X''

goal (1 subgoal):
 1. X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. \<And>A' A''. \<lbrakk>qAbs xs x X $= A'; A' $= A''\<rbrakk> \<Longrightarrow> qAbs xs x X $= A''
[PROOF STEP]
thus "qAbs xs x X $= A''"
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. qAbs xs x X $= A''
[PROOF STEP]
unfolding A''
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x'' X''
[PROOF STEP]
using u_not u_fresh
[PROOF STATE]
proof (prove)
using this:
X #[[u \<and> x]]_xs #= X'' #[[u \<and> x'']]_xs
u \<notin> {x, x', x'', y, z}
qAFresh xs u X \<and> qAFresh xs u X' \<and> qAFresh xs u X''

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x'' X''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= A''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>A' A''. qAbs xs x X $= A' \<and> A' $= A'' \<longrightarrow> qAbs xs x X $= A''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alpha_trans_twice:
"\<lbrakk>qGood X \<or> qGood X' \<or> qGood X'' \<or> qGood X''';
  X #= X'; X' #= X''; X'' #= X'''\<rbrakk> \<Longrightarrow> X #= X'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qGood X \<or> qGood X' \<or> qGood X'' \<or> qGood X'''; X #= X'; X' #= X''; X'' #= X'''\<rbrakk> \<Longrightarrow> X #= X'''
[PROOF STEP]
using alpha_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qGood ?X \<or> qGood ?X' \<or> qGood ?X''; ?X #= ?X'; ?X' #= ?X''\<rbrakk> \<Longrightarrow> ?X #= ?X''

goal (1 subgoal):
 1. \<lbrakk>qGood X \<or> qGood X' \<or> qGood X'' \<or> qGood X'''; X #= X'; X' #= X''; X'' #= X'''\<rbrakk> \<Longrightarrow> X #= X'''
[PROOF STEP]
by blast


[STATEMENT]
lemma alphaAbs_trans_twice:
"\<lbrakk>qGoodAbs A \<or> qGoodAbs A' \<or> qGoodAbs A'' \<or> qGoodAbs A''';
  A $= A'; A' $= A''; A'' $= A'''\<rbrakk> \<Longrightarrow> A $= A'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qGoodAbs A \<or> qGoodAbs A' \<or> qGoodAbs A'' \<or> qGoodAbs A'''; A $= A'; A' $= A''; A'' $= A'''\<rbrakk> \<Longrightarrow> A $= A'''
[PROOF STEP]
using alphaAbs_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qGoodAbs ?A \<or> qGoodAbs ?A' \<or> qGoodAbs ?A''; ?A $= ?A'; ?A' $= ?A''\<rbrakk> \<Longrightarrow> ?A $= ?A''

goal (1 subgoal):
 1. \<lbrakk>qGoodAbs A \<or> qGoodAbs A' \<or> qGoodAbs A'' \<or> qGoodAbs A'''; A $= A'; A' $= A''; A'' $= A'''\<rbrakk> \<Longrightarrow> A $= A'''
[PROOF STEP]
by blast


[STATEMENT]
lemma qAbs_preserves_alpha:
assumes ALPHA: "X #= X'" and GOOD: "qGood X \<or> qGood X'"
shows "qAbs xs x X $= qAbs xs x X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
have "qGood X \<and> qGood X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X \<and> qGood X'
[PROOF STEP]
using GOOD ALPHA
[PROOF STATE]
proof (prove)
using this:
qGood X \<or> qGood X'
X #= X'

goal (1 subgoal):
 1. qGood X \<and> qGood X'
[PROOF STEP]
by(auto simp add: alpha_preserves_qGood)
[PROOF STATE]
proof (state)
this:
qGood X \<and> qGood X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qGood X \<and> qGood X'
[PROOF STEP]
obtain y where y_not: "y \<noteq> x" and
                      y_fresh: "qAFresh xs y X \<and> qAFresh xs y X'"
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> x; qAFresh xs y X \<and> qAFresh xs y X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GOOD obtain_qFresh[of "{x}" "{X,X'}"]
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'
qGood X \<or> qGood X'
\<lbrakk>finite {x} \<or> |{x}| <o |UNIV|; finite {X, X'} \<or> |{X, X'}| <o |UNIV|; Ball {X, X'} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> {x} \<and> (\<forall>X\<in>{X, X'}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> x; qAFresh xs y X \<and> qAFresh xs y X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> x
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
hence "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= X' #[[y \<and> x]]_xs
[PROOF STEP]
using ALPHA GOOD
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
qAFresh xs y X \<and> qAFresh xs y X'
X #= X'
qGood X \<or> qGood X'

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= X' #[[y \<and> x]]_xs
[PROOF STEP]
by(simp add: qSwap_preserves_alpha)
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x]]_xs

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x]]_xs

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
using y_not y_fresh
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x]]_xs
y \<noteq> x
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs x X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qAbs_alphaAbs_qSwap_qAFresh:
assumes GOOD: "qGood X" and FRESH: "qAFresh ys x' X"
shows "qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
obtain y where 1: "y \<notin> {x,x'}" and 2: "qAFresh ys y X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<notin> {x, x'}; qAFresh ys y X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GOOD obtain_qFresh[of "{x,x'}" "{X}"]
[PROOF STATE]
proof (prove)
using this:
qGood X
\<lbrakk>finite {x, x'} \<or> |{x, x'}| <o |UNIV|; finite {X} \<or> |{X}| <o |UNIV|; Ball {X} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> {x, x'} \<and> (\<forall>X\<in>{X}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<notin> {x, x'}; qAFresh ys y X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> {x, x'}
qAFresh ys y X

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
hence 3: "qAFresh ys y (X #[[x' \<and> x]]_ys)"
[PROOF STATE]
proof (prove)
using this:
y \<notin> {x, x'}
qAFresh ys y X

goal (1 subgoal):
 1. qAFresh ys y (X #[[x' \<and> x]]_ys)
[PROOF STEP]
by (auto simp add: qSwap_preserves_qAFresh_distinct)
[PROOF STATE]
proof (state)
this:
qAFresh ys y (X #[[x' \<and> x]]_ys)

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
qAFresh ys y (X #[[x' \<and> x]]_ys)

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
have "(X #[[y \<and> x]]_ys) = ((X #[[x' \<and> x]]_ys) #[[y \<and> x']]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
[PROOF STEP]
using FRESH 2
[PROOF STATE]
proof (prove)
using this:
qAFresh ys x' X
qAFresh ys y X

goal (1 subgoal):
 1. X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
[PROOF STEP]
by (auto simp add: qAFresh_qSwap_compose)
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
have "qGood (X #[[y \<and> x]]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_ys)
[PROOF STEP]
using 1 GOOD qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
y \<notin> {x, x'}
qGood X
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X #[[y \<and> x]]_ys)

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
qGood (X #[[y \<and> x]]_ys)
[PROOF STEP]
have "(X #[[y \<and> x]]_ys) #= ((X #[[x' \<and> x]]_ys) #[[y \<and> x']]_ys)"
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
qGood (X #[[y \<and> x]]_ys)

goal (1 subgoal):
 1. X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
[PROOF STEP]
using alpha_refl
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_ys = X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
qGood (X #[[y \<and> x]]_ys)
qGood ?X \<Longrightarrow> ?X #= ?X

goal (1 subgoal):
 1. X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
using 1 2 3 assms
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_ys #= X #[[x' \<and> x]]_ys #[[y \<and> x']]_ys
y \<notin> {x, x'}
qAFresh ys y X
qAFresh ys y (X #[[x' \<and> x]]_ys)
qGood X
qAFresh ys x' X

goal (1 subgoal):
 1. qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAbs ys x X $= qAbs ys x' (X #[[x' \<and> x]]_ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qAbs_ex_qAFresh_rep:
assumes GOOD: "qGood X" and FRESH: "qAFresh xs x' X"
shows "\<exists> X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
have 1: "qGood (X #[[x' \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[x' \<and> x]]_xs)
[PROOF STEP]
using assms qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X
qAFresh xs x' X
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (1 subgoal):
 1. qGood (X #[[x' \<and> x]]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X #[[x' \<and> x]]_xs)

goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
apply(rule exI[of _ "X #[[x' \<and> x]]_xs"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[x' \<and> x]]_xs) \<and> qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
using assms 1 qAbs_alphaAbs_qSwap_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qAFresh xs x' X
qGood (X #[[x' \<and> x]]_xs)
\<lbrakk>qGood ?X; qAFresh ?ys ?x' ?X\<rbrakk> \<Longrightarrow> qAbs ?ys ?x ?X $= qAbs ?ys ?x' (?X #[[?x' \<and> ?x]]_?ys)

goal (1 subgoal):
 1. qGood (X #[[x' \<and> x]]_xs) \<and> qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>X'. qGood X' \<and> qAbs xs x X $= qAbs xs x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qFreshAll_imp_ex_qAFreshAll:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs fZs
assumes FIN: "finite V"
shows
"(qGood X \<longrightarrow>
  ((\<forall> z \<in> V. \<forall> zs \<in> fZs z. qFresh zs z X) \<longrightarrow>
   (\<exists> X'. X #= X' \<and> (\<forall> z \<in> V. \<forall> zs \<in> fZs z. qAFresh zs z X')))) \<and>
 (qGoodAbs A \<longrightarrow>
  ((\<forall> z \<in> V. \<forall> zs \<in> fZs z. qFreshAbs zs z A) \<longrightarrow>
   (\<exists> A'. A $= A' \<and> (\<forall> z \<in> V. \<forall> zs \<in> fZs z. qAFreshAbs zs z A'))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))) \<and> (qGoodAbs A \<longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))
[PROOF STEP]
proof(induction rule: qGood_qTerm_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs x. (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qVar xs x)) \<longrightarrow> (\<exists>X'. qVar xs x #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 2. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
case (Var xs x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>xs x. (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qVar xs x)) \<longrightarrow> (\<exists>X'. qVar xs x #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 2. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qVar xs x)) \<longrightarrow> (\<exists>X'. qVar xs x #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
[PROOF STEP]
by (metis alpha_qVar_iff qAFreshAll_simps(1) qFreshAll_simps(1))
[PROOF STATE]
proof (state)
this:
(\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qVar xs x)) \<longrightarrow> (\<exists>X'. qVar xs x #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
case (Op delta inp binp)
[PROOF STATE]
proof (state)
this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp
liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
assume *: "\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)"
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
define phi and phiAbs where
    "phi \<equiv> (\<lambda>(Y::('index,'bindex,'varSort,'var,'opSym)qTerm) Y'.
            Y #= Y' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'))" and
    "phiAbs \<equiv> (\<lambda>(A::('index,'bindex,'varSort,'var,'opSym)qAbs) A'.
               A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))"
[PROOF STATE]
proof (state)
this:
phi \<equiv> \<lambda>Y Y'. Y #= Y' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y')
phiAbs \<equiv> \<lambda>A A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
have ex_phi: "\<And> i Y. inp i = Some Y \<Longrightarrow> \<exists>Y'. phi Y Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i Y. inp i = Some Y \<Longrightarrow> \<exists>Y'. phi Y Y'
[PROOF STEP]
unfolding phi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i Y. inp i = Some Y \<Longrightarrow> \<exists>Y'. Y #= Y' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y')
[PROOF STEP]
using Op.IH *
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp
liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)

goal (1 subgoal):
 1. \<And>i Y. inp i = Some Y \<Longrightarrow> \<exists>Y'. Y #= Y' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y')
[PROOF STEP]
by (auto simp add: liftAll_def)
[PROOF STATE]
proof (state)
this:
inp ?i11 = Some ?Y11 \<Longrightarrow> \<exists>Y'. phi ?Y11 Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
have ex_phiAbs: "\<And> i A. binp i = Some A \<Longrightarrow> \<exists>A'. phiAbs A A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i A. binp i = Some A \<Longrightarrow> \<exists>A'. phiAbs A A'
[PROOF STEP]
unfolding phiAbs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i A. binp i = Some A \<Longrightarrow> \<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
using Op.IH *
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>X. qGood X \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z X) \<longrightarrow> (\<exists>X'. X #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')))) inp
liftAll (\<lambda>A. qGoodAbs A \<and> ((\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z A) \<longrightarrow> (\<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')))) binp
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)

goal (1 subgoal):
 1. \<And>i A. binp i = Some A \<Longrightarrow> \<exists>A'. A $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
by (auto simp add: liftAll_def)
[PROOF STATE]
proof (state)
this:
binp ?i11 = Some ?A11 \<Longrightarrow> \<exists>A'. phiAbs ?A11 A'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
define inp' and binp' where
    "inp' \<equiv> \<lambda> i. case inp i of Some Y \<Rightarrow> Some (SOME Y'. phi Y Y') |None \<Rightarrow> None" and
    "binp' \<equiv> \<lambda> i. case binp i of Some A \<Rightarrow> Some (SOME A'. phiAbs A A') |None \<Rightarrow> None"
[PROOF STATE]
proof (state)
this:
inp' \<equiv> \<lambda>i. case inp i of None \<Rightarrow> None | Some Y \<Rightarrow> Some (SOME Y'. phi Y Y')
binp' \<equiv> \<lambda>i. case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (SOME A'. phiAbs A A')

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp) \<Longrightarrow> \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
show "\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')
[PROOF STEP]
by (intro exI[of _ "qOp delta inp' binp'"])
    (auto simp add: inp'_def binp'_def option.case_eq_if sameDom_def liftAll_def liftAll2_def,
    (meson ex_phi phi_def ex_phiAbs phiAbs_def some_eq_ex)+)
[PROOF STATE]
proof (state)
this:
\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (qOp delta inp binp)) \<longrightarrow> (\<exists>X'. qOp delta inp binp #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
case (Abs xs x X)
[PROOF STATE]
proof (state)
this:
qGood X
qGood ?Y11 \<and> qSkel ?Y11 = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z ?Y11) \<longrightarrow> (\<exists>X'. ?Y11 #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
(X, ?Y11) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z ?Y11) \<longrightarrow> (\<exists>X'. ?Y11 #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X')); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y) \<longrightarrow> (\<exists>X'. Y #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))\<rbrakk> \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
assume *: "\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)"
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
obtain y where y_not_x: "y \<noteq> x" and y_not_V: "y \<notin> V"
    and y_afresh: "qAFresh xs y X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> x; y \<notin> V; qAFresh xs y X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using FIN \<open>qGood X\<close> obtain_qFresh[of "V \<union> {x}" "{X}"]
[PROOF STATE]
proof (prove)
using this:
finite V
qGood X
\<lbrakk>finite (V \<union> {x}) \<or> |V \<union> {x}| <o |UNIV|; finite {X} \<or> |{X}| <o |UNIV|; Ball {X} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> V \<union> {x} \<and> (\<forall>X\<in>{X}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> x; y \<notin> V; qAFresh xs y X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> x
y \<notin> V
qAFresh xs y X

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
hence y_fresh: "qFresh xs y X"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
y \<notin> V
qAFresh xs y X

goal (1 subgoal):
 1. qFresh xs y X
[PROOF STEP]
using qAFresh_imp_qFresh
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
y \<notin> V
qAFresh xs y X
qAFresh ?xs ?x ?X \<Longrightarrow> qFresh ?xs ?x ?X

goal (1 subgoal):
 1. qFresh xs y X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qFresh xs y X

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
obtain Y where Y_def: "Y = (X #[[y \<and> x ]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. Y = X #[[y \<and> x]]_xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y = X #[[y \<and> x]]_xs

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have alphaXY: "qAbs xs x X $= qAbs xs y Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs y Y
[PROOF STEP]
using \<open>qGood X\<close> y_afresh qAbs_alphaAbs_qSwap_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qAFresh xs y X
\<lbrakk>qGood ?X; qAFresh ?ys ?x' ?X\<rbrakk> \<Longrightarrow> qAbs ?ys ?x ?X $= qAbs ?ys ?x' (?X #[[?x' \<and> ?x]]_?ys)

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs y Y
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
using this:
qGood X
qAFresh xs y X
\<lbrakk>qGood ?X; qAFresh ?ys ?x' ?X\<rbrakk> \<Longrightarrow> qAbs ?ys ?x ?X $= qAbs ?ys ?x' (?X #[[?x' \<and> ?x]]_?ys)

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs y (X #[[y \<and> x]]_xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs y Y

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have "\<forall>z\<in>V. \<forall>zs \<in> fZs z. qFresh zs z Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z (X #[[y \<and> x]]_xs)
[PROOF STEP]
by (metis * not_equals_and_not_equals_not_in qAFresh_imp_qFresh qAFresh_qSwap_exchange1
        qFreshAbs.simps qSwap_preserves_qFresh_distinct y_afresh y_not_V)
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have "(X,Y) \<in> qSwapped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, Y) \<in> qSwapped
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, X #[[y \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
by(simp add: qSwap_qSwapped)
[PROOF STATE]
proof (state)
this:
(X, Y) \<in> qSwapped

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y
(X, Y) \<in> qSwapped
[PROOF STEP]
obtain Y' where "Y #= Y'" and **: "\<forall>z\<in>V. \<forall>zs \<in> fZs z. qAFresh zs z Y'"
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y
(X, Y) \<in> qSwapped

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>Y #= Y'; \<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Abs.IH
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z Y
(X, Y) \<in> qSwapped
qGood ?Y11 \<and> qSkel ?Y11 = qSkel X \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z ?Y11) \<longrightarrow> (\<exists>X'. ?Y11 #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))
(X, ?Y11) \<in> qSwapped \<Longrightarrow> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFresh zs z ?Y11) \<longrightarrow> (\<exists>X'. ?Y11 #= X' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z X'))

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>Y #= Y'; \<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y #= Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y #= Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have "qGood Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood Y
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
using  \<open>qGood X\<close> qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood Y

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y #= Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'
qGood Y
[PROOF STEP]
have "qAbs xs y Y $= qAbs xs y Y'"
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'
qGood Y

goal (1 subgoal):
 1. qAbs xs y Y $= qAbs xs y Y'
[PROOF STEP]
using qAbs_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'
qGood Y
\<lbrakk>?X #= ?X'; qGood ?X \<or> qGood ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs ?x ?X'

goal (1 subgoal):
 1. qAbs xs y Y $= qAbs xs y Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs y Y $= qAbs xs y Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs y Y $= qAbs xs y Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have "qGoodAbs(qAbs xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
using  \<open>qGood X\<close>
[PROOF STATE]
proof (prove)
using this:
qGood X

goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs y Y $= qAbs xs y Y'
qGoodAbs (qAbs xs x X)
[PROOF STEP]
have "qAbs xs x X $= qAbs xs y Y'"
[PROOF STATE]
proof (prove)
using this:
qAbs xs y Y $= qAbs xs y Y'
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs y Y'
[PROOF STEP]
using alphaXY alphaAbs_trans
[PROOF STATE]
proof (prove)
using this:
qAbs xs y Y $= qAbs xs y Y'
qGoodAbs (qAbs xs x X)
qAbs xs x X $= qAbs xs y Y
\<lbrakk>qGoodAbs ?A \<or> qGoodAbs ?A' \<or> qGoodAbs ?A''; ?A $= ?A'; ?A' $= ?A''\<rbrakk> \<Longrightarrow> ?A $= ?A''

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs y Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs y Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs y Y'

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
have "\<forall>z\<in>V. \<forall>zs \<in> fZs z. qAFreshAbs zs z (qAbs xs y Y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z (qAbs xs y Y')
[PROOF STEP]
using ** y_not_V
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFresh zs z Y'
y \<notin> V

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z (qAbs xs y Y')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z (qAbs xs y Y')

goal (1 subgoal):
 1. \<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X) \<Longrightarrow> \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= qAbs xs y Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z (qAbs xs y Y')
[PROOF STEP]
show "\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs \<in> fZs z. qAFreshAbs zs z A')"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs y Y'
\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z (qAbs xs y Y')

goal (1 subgoal):
 1. \<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>z\<in>V. \<forall>zs\<in>fZs z. qFreshAbs zs z (qAbs xs x X)) \<longrightarrow> (\<exists>A'. qAbs xs x X $= A' \<and> (\<forall>z\<in>V. \<forall>zs\<in>fZs z. qAFreshAbs zs z A'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qFresh_imp_ex_qAFresh1:
assumes "qGood X" and "qFresh zs z X"
shows "\<exists> X'. qGood X' \<and> X #= X' \<and> qAFresh zs z X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> X #= X' \<and> qAFresh zs z X'
[PROOF STEP]
using assms qFresh_imp_ex_qAFresh[of "{z}" _ "undefined(z := {zs})"]
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh zs z X
\<lbrakk>finite {z}; qGood ?X; \<forall>za\<in>{z}. \<forall>zs\<in>(undefined(z := {zs})) za. qFresh zs za ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> (\<forall>za\<in>{z}. \<forall>zs\<in>(undefined(z := {zs})) za. qAFresh zs za X')

goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> X #= X' \<and> qAFresh zs z X'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma qFreshAbs_imp_ex_qAFreshAbs1:
assumes "finite V" and "qGoodAbs A" and "qFreshAbs zs z A"
shows "\<exists> A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs zs z A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs zs z A'
[PROOF STEP]
using assms qFreshAbs_imp_ex_qAFreshAbs[of "{z}" _ "undefined(z := {zs})"]
[PROOF STATE]
proof (prove)
using this:
finite V
qGoodAbs A
qFreshAbs zs z A
\<lbrakk>finite {z}; qGoodAbs ?A; \<forall>za\<in>{z}. \<forall>zs\<in>(undefined(z := {zs})) za. qFreshAbs zs za ?A\<rbrakk> \<Longrightarrow> \<exists>A'. qGoodAbs A' \<and> ?A $= A' \<and> (\<forall>za\<in>{z}. \<forall>zs\<in>(undefined(z := {zs})) za. qAFreshAbs zs za A')

goal (1 subgoal):
 1. \<exists>A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs zs z A'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma qFresh_imp_ex_qAFresh2:
assumes "qGood X" and "qFresh xs x X" and "qFresh ys y X"
shows "\<exists> X'. qGood X' \<and> X #= X' \<and> qAFresh xs x X' \<and> qAFresh ys y X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> X #= X' \<and> qAFresh xs x X' \<and> qAFresh ys y X'
[PROOF STEP]
using assms
qFresh_imp_ex_qAFresh[of "{x}" _ "undefined(x := {xs,ys})"]
qFresh_imp_ex_qAFresh[of "{x,y}" _ "(undefined(x := {xs}))(y := {ys})"]
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh xs x X
qFresh ys y X
\<lbrakk>finite {x}; qGood ?X; \<forall>z\<in>{x}. \<forall>zs\<in>(undefined(x := {xs, ys})) z. qFresh zs z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> (\<forall>z\<in>{x}. \<forall>zs\<in>(undefined(x := {xs, ys})) z. qAFresh zs z X')
\<lbrakk>finite {x, y}; qGood ?X; \<forall>z\<in>{x, y}. \<forall>zs\<in>(undefined(x := {xs}, y := {ys})) z. qFresh zs z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> (\<forall>z\<in>{x, y}. \<forall>zs\<in>(undefined(x := {xs}, y := {ys})) z. qAFresh zs z X')

goal (1 subgoal):
 1. \<exists>X'. qGood X' \<and> X #= X' \<and> qAFresh xs x X' \<and> qAFresh ys y X'
[PROOF STEP]
by (cases "x = y") auto


[STATEMENT]
lemma qFreshAbs_imp_ex_qAFreshAbs2:
assumes "finite V" and "qGoodAbs A" and "qFreshAbs xs x A" and "qFreshAbs ys y A"
shows "\<exists> A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs xs x A' \<and> qAFreshAbs ys y A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs xs x A' \<and> qAFreshAbs ys y A'
[PROOF STEP]
using assms
qFreshAbs_imp_ex_qAFreshAbs[of "{x}" _ "undefined(x := {xs,ys})"]
qFreshAbs_imp_ex_qAFreshAbs[of "{x,y}" _ "(undefined(x := {xs}))(y := {ys})"]
[PROOF STATE]
proof (prove)
using this:
finite V
qGoodAbs A
qFreshAbs xs x A
qFreshAbs ys y A
\<lbrakk>finite {x}; qGoodAbs ?A; \<forall>z\<in>{x}. \<forall>zs\<in>(undefined(x := {xs, ys})) z. qFreshAbs zs z ?A\<rbrakk> \<Longrightarrow> \<exists>A'. qGoodAbs A' \<and> ?A $= A' \<and> (\<forall>z\<in>{x}. \<forall>zs\<in>(undefined(x := {xs, ys})) z. qAFreshAbs zs z A')
\<lbrakk>finite {x, y}; qGoodAbs ?A; \<forall>z\<in>{x, y}. \<forall>zs\<in>(undefined(x := {xs}, y := {ys})) z. qFreshAbs zs z ?A\<rbrakk> \<Longrightarrow> \<exists>A'. qGoodAbs A' \<and> ?A $= A' \<and> (\<forall>z\<in>{x, y}. \<forall>zs\<in>(undefined(x := {xs}, y := {ys})) z. qAFreshAbs zs z A')

goal (1 subgoal):
 1. \<exists>A'. qGoodAbs A' \<and> A $= A' \<and> qAFreshAbs xs x A' \<and> qAFreshAbs ys y A'
[PROOF STEP]
by (cases "x = y") auto