[STATEMENT]
lemma qAFreshAll_qFreshAll_preserves_alphaAll:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs z
shows
"(qGood X \<longrightarrow>
  (qAFresh zs z X \<longrightarrow> (\<forall> X'. X #= X' \<longrightarrow> qFresh zs z X'))) \<and>
 (qGoodAbs A \<longrightarrow>
  (qAFreshAbs zs z A \<longrightarrow> (\<forall> A'. A $= A' \<longrightarrow> qFreshAbs zs z A')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X')) \<and> (qGoodAbs A \<longrightarrow> qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))
[PROOF STEP]
proof(induction rule: qGood_qTerm_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs x. qAFresh zs z (qVar xs x) \<longrightarrow> (\<forall>X'. qVar xs x #= X' \<longrightarrow> qFresh 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))) binp\<rbrakk> \<Longrightarrow> qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs zs z A')
[PROOF STEP]
case (Var xs x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>xs x. qAFresh zs z (qVar xs x) \<longrightarrow> (\<forall>X'. qVar xs x #= X' \<longrightarrow> qFresh 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))) binp\<rbrakk> \<Longrightarrow> qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs zs z A')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAFresh zs z (qVar xs x) \<longrightarrow> (\<forall>X'. qVar xs x #= X' \<longrightarrow> qFresh zs z X')
[PROOF STEP]
unfolding qVar_alpha_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAFresh zs z (qVar xs x) \<longrightarrow> (\<forall>X'. X' = qVar xs x \<longrightarrow> qFresh zs z X')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qAFresh zs z (qVar xs x) \<longrightarrow> (\<forall>X'. qVar xs x #= X' \<longrightarrow> qFresh 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))) binp\<rbrakk> \<Longrightarrow> qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))) binp\<rbrakk> \<Longrightarrow> qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp
liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs 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> (qAFresh zs z X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qFresh zs z X'))) inp; liftAll (\<lambda>A. qGoodAbs A \<and> (qAFreshAbs zs z A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qFreshAbs zs z A'))) binp\<rbrakk> \<Longrightarrow> qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs zs z A')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAFresh zs z (qOp delta inp binp) \<longrightarrow> (\<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qFresh zs z X')
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
fix X'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
assume afresh: "qAFresh zs z (qOp delta inp binp)"
    and "qOp delta inp binp #= X'"
[PROOF STATE]
proof (state)
this:
qAFresh zs z (qOp delta inp binp)
qOp delta inp binp #= X'

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qAFresh zs z (qOp delta inp binp)
qOp delta inp binp #= X'
[PROOF STEP]
obtain inp' and binp' where X'eq: "X' = qOp delta inp' binp'" and
    *: "(\<forall>i. (inp i = None) = (inp' i = None)) \<and>
      (\<forall>i. (binp i = None) = (binp' i = None))" and
    **: "(\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and>
       (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')"
[PROOF STATE]
proof (prove)
using this:
qAFresh zs z (qOp delta inp binp)
qOp delta inp binp #= X'

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; (\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None)); (\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qOp_alpha_iff sameDom_def liftAll2_def
[PROOF STATE]
proof (prove)
using this:
qAFresh zs z (qOp delta inp binp)
\<exists>inp' binp'. X' = qOp delta inp' binp' \<and> (\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None)) \<and> (\<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. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; (\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None)); (\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' = qOp delta inp' binp'
(\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None))
(\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X' = qOp delta inp' binp'
(\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i. (binp i = None) = (binp' i = None))
(\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
fix i Y'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
assume inp': "inp' i = Some Y'"
[PROOF STATE]
proof (state)
this:
inp' i = Some Y'

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inp' i = Some Y'
[PROOF STEP]
obtain Y where inp: "inp i = Some Y"
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'

goal (1 subgoal):
 1. (\<And>Y. inp i = Some Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
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 fastforce
[PROOF STATE]
proof (state)
this:
inp i = Some Y

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[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' **
[PROOF STATE]
proof (prove)
using this:
inp i = Some Y
inp' i = Some Y'
(\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')

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

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
hence "qFresh zs z Y'"
[PROOF STATE]
proof (prove)
using this:
Y #= Y'

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

goal (1 subgoal):
 1. qFresh zs z Y'
[PROOF STEP]
by (auto simp: liftAll_def)
[PROOF STATE]
proof (state)
this:
qFresh zs z Y'

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
fix i A'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
assume binp': "binp' i = Some A'"
[PROOF STATE]
proof (state)
this:
binp' i = Some A'

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
binp' i = Some A'
[PROOF STEP]
obtain A where binp: "binp i = Some A"
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'

goal (1 subgoal):
 1. (\<And>A. binp i = Some A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
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 fastforce
[PROOF STATE]
proof (state)
this:
binp i = Some A

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[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' **
[PROOF STATE]
proof (prove)
using this:
binp i = Some A
binp' i = Some A'
(\<forall>i Y Y'. inp i = Some Y \<and> inp' i = Some Y' \<longrightarrow> Y #= Y') \<and> (\<forall>i A A'. binp i = Some A \<and> binp' i = Some A' \<longrightarrow> A $= A')

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

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
hence "qFreshAbs zs z A'"
[PROOF STATE]
proof (prove)
using this:
A $= A'

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

goal (1 subgoal):
 1. qFreshAbs zs z A'
[PROOF STEP]
by (auto simp: liftAll_def)
[PROOF STATE]
proof (state)
this:
qFreshAbs zs z A'

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
binp' ?i13 = Some ?A'13 \<Longrightarrow> qFreshAbs zs z ?A'13

goal (1 subgoal):
 1. \<And>X'. \<lbrakk>qAFresh zs z (qOp delta inp binp); qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qFresh zs z X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13
binp' ?i13 = Some ?A'13 \<Longrightarrow> qFreshAbs zs z ?A'13
[PROOF STEP]
show "qFresh zs z X'"
[PROOF STATE]
proof (prove)
using this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13
binp' ?i13 = Some ?A'13 \<Longrightarrow> qFreshAbs zs z ?A'13

goal (1 subgoal):
 1. qFresh zs z X'
[PROOF STEP]
unfolding X'eq
[PROOF STATE]
proof (prove)
using this:
inp' ?i13 = Some ?Y'13 \<Longrightarrow> qFresh zs z ?Y'13
binp' ?i13 = Some ?A'13 \<Longrightarrow> qFreshAbs zs z ?A'13

goal (1 subgoal):
 1. qFresh zs z (qOp delta inp' binp')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i Y'. inp' i = Some Y' \<Longrightarrow> qFresh zs z Y'; \<And>i A'. binp' i = Some A' \<Longrightarrow> qFreshAbs zs z A'\<rbrakk> \<Longrightarrow> liftAll (qFresh zs z) inp' \<and> liftAll (qFreshAbs zs z) binp'
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i Y'. inp' i = Some Y' \<Longrightarrow> qFresh zs z Y'; \<And>i A'. binp' i = Some A' \<Longrightarrow> qFreshAbs zs z A'\<rbrakk> \<Longrightarrow> (\<forall>i v. inp' i = Some v \<longrightarrow> qFresh zs z v) \<and> (\<forall>i v. binp' i = Some v \<longrightarrow> qFreshAbs zs z v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qFresh zs z X'

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

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs 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> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X'); \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qAFresh zs z Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qFresh zs z X')\<rbrakk> \<Longrightarrow> qAFreshAbs zs z (qAbs xs x X) \<longrightarrow> (\<forall>A'. qAbs xs x X $= A' \<longrightarrow> qFreshAbs 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> qAFresh zs z ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> qFresh zs z X')
(X, ?Y11) \<in> qSwapped \<Longrightarrow> qAFresh zs z ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> qFresh zs z X')

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

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= A'
qAFreshAbs zs z (qAbs xs x X)
[PROOF STEP]
obtain x' y X' where A'eq: "A' = qAbs xs x' X'" and
    ynot: "y \<notin> {x, x'}" and y_afresh: "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'
qAFreshAbs zs z (qAbs xs x X)

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
qAFreshAbs zs z (qAbs xs x X)

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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
(*  *)
[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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
have goodXxy: "qGood(X #[[y \<and> x]]_xs)"
[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 (X #[[y \<and> x]]_xs)

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qGood X'
[PROOF STEP]
obtain u where u_afresh: "qAFresh xs u X \<and> qAFresh xs u X'"
    and unot: "u \<notin> {x,x',z}"
[PROOF STATE]
proof (prove)
using this:
qGood X'

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

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

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

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
have "(X #[[u \<and> x]]_xs) = ((X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs) \<and>
          (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 \<and> X' #[[u \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs
[PROOF STEP]
using u_afresh y_afresh qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X'
qAFresh xs y X \<and> qAFresh xs y X'
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

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

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z 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 goodXxy goodX'yx' alpha qSwap_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<and> x]]_xs)
qGood (X' #[[y \<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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X #[[u \<and> x]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs \<and> 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
[PROOF STEP]
have alpha: "(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 \<and> 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

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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
X #[[u \<and> x]]_xs #= X' #[[u \<and> x']]_xs

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z 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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z 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'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(X, X #[[u \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
have "qAFresh zs z (X #[[u \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAFresh zs z (X #[[u \<and> x]]_xs)
[PROOF STEP]
using unot afresh
[PROOF STATE]
proof (prove)
using this:
u \<notin> {x, x', z}
qAFreshAbs zs z (qAbs xs x X)

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

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

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

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

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

goal (1 subgoal):
 1. zs = xs \<and> z = x' \<or> qFresh zs z X'
[PROOF STEP]
using unot afresh qSwap_preserves_qFresh_distinct[of zs xs z]
[PROOF STATE]
proof (prove)
using this:
qFresh zs z (X' #[[u \<and> x']]_xs)
u \<notin> {x, x', z}
qAFreshAbs zs z (qAbs xs x X)
zs \<noteq> xs \<or> z \<notin> {?z1.0, ?z2.0} \<Longrightarrow> qFresh zs z (?X #[[?z1.0 \<and> ?z2.0]]_xs) = qFresh zs z ?X

goal (1 subgoal):
 1. zs = xs \<and> z = x' \<or> qFresh zs z X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
zs = xs \<and> z = x' \<or> qFresh zs z X'

goal (1 subgoal):
 1. \<And>A'. \<lbrakk>qAFreshAbs zs z (qAbs xs x X); qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qFreshAbs zs z A'
[PROOF STEP]
thus "qFreshAbs zs z A'"
[PROOF STATE]
proof (prove)
using this:
zs = xs \<and> z = x' \<or> qFresh zs z X'

goal (1 subgoal):
 1. qFreshAbs zs z A'
[PROOF STEP]
unfolding A'eq
[PROOF STATE]
proof (prove)
using this:
zs = xs \<and> z = x' \<or> qFresh zs z X'

goal (1 subgoal):
 1. qFreshAbs zs z (qAbs xs x' X')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qFreshAbs zs z A'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qFresh_preserves_alpha1:
assumes "qGood X" and "qFresh zs z X" and "X #= X'"
shows "qFresh zs z X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qFresh zs z X'
[PROOF STEP]
by (meson alpha_sym alpha_trans assms qAFresh_qFresh_preserves_alpha qFresh_imp_ex_qAFresh1)


[STATEMENT]
lemma qFreshAbs_preserves_alphaAbs1:
assumes "qGoodAbs A" and "qFreshAbs zs z A" and "A $= A'"
shows "qFreshAbs zs z A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qFreshAbs zs z A'
[PROOF STEP]
by (meson alphaAbs_sym alphaAbs_trans assms finite.emptyI
  qAFreshAbs_imp_qFreshAbs_preserves_alphaAbs qFreshAbs_imp_ex_qAFreshAbs1)


[STATEMENT]
lemma qFresh_preserves_alpha:
assumes "qGood X \<or> qGood X'" and "X #= X'"
shows "qFresh zs z X \<longleftrightarrow> qFresh zs z X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qFresh zs z X = qFresh zs z X'
[PROOF STEP]
using alpha_preserves_qGood alpha_sym assms qFresh_preserves_alpha1
[PROOF STATE]
proof (prove)
using this:
?X #= ?X' \<Longrightarrow> qGood ?X = qGood ?X'
?X #= ?X' \<Longrightarrow> ?X' #= ?X
qGood X \<or> qGood X'
X #= X'
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X; ?X #= ?X'\<rbrakk> \<Longrightarrow> qFresh ?zs ?z ?X'

goal (1 subgoal):
 1. qFresh zs z X = qFresh zs z X'
[PROOF STEP]
by blast


[STATEMENT]
lemma qFreshAbs_preserves_alphaAbs:
assumes "qGoodAbs A \<or> qGoodAbs A'" and "A $= A'"
shows "qFreshAbs zs z A = qFreshAbs zs z A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qFreshAbs zs z A = qFreshAbs zs z A'
[PROOF STEP]
using assms alphaAbs_preserves_qGoodAbs alphaAbs_sym qFreshAbs_preserves_alphaAbs1
[PROOF STATE]
proof (prove)
using this:
qGoodAbs A \<or> qGoodAbs A'
A $= A'
?A $= ?A' \<Longrightarrow> qGoodAbs ?A = qGoodAbs ?A'
?A $= ?A' \<Longrightarrow> ?A' $= ?A
\<lbrakk>qGoodAbs ?A; qFreshAbs ?zs ?z ?A; ?A $= ?A'\<rbrakk> \<Longrightarrow> qFreshAbs ?zs ?z ?A'

goal (1 subgoal):
 1. qFreshAbs zs z A = qFreshAbs zs z A'
[PROOF STEP]
by blast


[STATEMENT]
lemma alpha_qFresh_qSwap_id:
assumes "qGood X" and "qFresh zs z1 X" and "qFresh zs z2 X"
shows "(X #[[z1 \<and> z2]]_zs) #= X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
obtain X' where 1: "X #= X'" and "qAFresh zs z1 X' \<and> qAFresh zs z2 X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X #= X'; qAFresh zs z1 X' \<and> qAFresh zs z2 X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms qFresh_imp_ex_qAFresh2
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh zs z1 X
qFresh zs z2 X
\<lbrakk>qGood ?X; qFresh ?xs ?x ?X; qFresh ?ys ?y ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?xs ?x X' \<and> qAFresh ?ys ?y X'

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X #= X'; qAFresh zs z1 X' \<and> qAFresh zs z2 X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
X #= X'
qAFresh zs z1 X' \<and> qAFresh zs z2 X'

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
hence "(X' #[[z1 \<and> z2]]_zs) = X'"
[PROOF STATE]
proof (prove)
using this:
X #= X'
qAFresh zs z1 X' \<and> qAFresh zs z2 X'

goal (1 subgoal):
 1. X' #[[z1 \<and> z2]]_zs = X'
[PROOF STEP]
using qAFresh_qSwap_id
[PROOF STATE]
proof (prove)
using this:
X #= X'
qAFresh zs z1 X' \<and> qAFresh zs z2 X'
\<lbrakk>qAFresh ?zs ?z1.0 ?X; qAFresh ?zs ?z2.0 ?X\<rbrakk> \<Longrightarrow> ?X #[[?z1.0 \<and> ?z2.0]]_?zs = ?X

goal (1 subgoal):
 1. X' #[[z1 \<and> z2]]_zs = X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' #[[z1 \<and> z2]]_zs = X'

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #[[z1 \<and> z2]]_zs = X'

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
have "(X #[[z1 \<and> z2]]_zs) #= (X' #[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh zs z1 X
qFresh zs z2 X
X #= X'

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
by (auto simp add: qSwap_preserves_alpha)
[PROOF STATE]
proof (state)
this:
X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
have "X' #= X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #= X
[PROOF STEP]
using 1 alpha_sym
[PROOF STATE]
proof (prove)
using this:
X #= X'
?X #= ?X' \<Longrightarrow> ?X' #= ?X

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

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #= X

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
have "qGood(X #[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[z1 \<and> z2]]_zs)
[PROOF STEP]
using assms qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh zs z1 X
qFresh zs z2 X
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

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

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X' #[[z1 \<and> z2]]_zs = X'
X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
X' #= X
qGood (X #[[z1 \<and> z2]]_zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X' #[[z1 \<and> z2]]_zs = X'
X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
X' #= X
qGood (X #[[z1 \<and> z2]]_zs)

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
using alpha_trans
[PROOF STATE]
proof (prove)
using this:
X' #[[z1 \<and> z2]]_zs = X'
X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
X' #= X
qGood (X #[[z1 \<and> z2]]_zs)
\<lbrakk>qGood ?X \<or> qGood ?X' \<or> qGood ?X''; ?X #= ?X'; ?X' #= ?X''\<rbrakk> \<Longrightarrow> ?X #= ?X''

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #= X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X #[[z1 \<and> z2]]_zs #= X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qFreshAbs_qSwapAbs_id:
assumes "qGoodAbs A" and "qFreshAbs zs z1 A" and "qFreshAbs zs z2 A"
shows "(A $[[z1 \<and> z2]]_zs) $= A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
obtain A' where 1: "A $= A'" and "qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A'. \<lbrakk>A $= A'; qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms qFreshAbs_imp_ex_qAFreshAbs2
[PROOF STATE]
proof (prove)
using this:
qGoodAbs A
qFreshAbs zs z1 A
qFreshAbs zs z2 A
\<lbrakk>finite ?V; qGoodAbs ?A; qFreshAbs ?xs ?x ?A; qFreshAbs ?ys ?y ?A\<rbrakk> \<Longrightarrow> \<exists>A'. qGoodAbs A' \<and> ?A $= A' \<and> qAFreshAbs ?xs ?x A' \<and> qAFreshAbs ?ys ?y A'

goal (1 subgoal):
 1. (\<And>A'. \<lbrakk>A $= A'; qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
A $= A'
qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
hence "(A' $[[z1 \<and> z2]]_zs) = A'"
[PROOF STATE]
proof (prove)
using this:
A $= A'
qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'

goal (1 subgoal):
 1. A' $[[z1 \<and> z2]]_zs = A'
[PROOF STEP]
using qAFreshAll_qSwapAll_id
[PROOF STATE]
proof (prove)
using this:
A $= A'
qAFreshAbs zs z1 A' \<and> qAFreshAbs zs z2 A'
(qAFresh ?zs ?z1.0 ?X \<and> qAFresh ?zs ?z2.0 ?X \<longrightarrow> ?X #[[?z1.0 \<and> ?z2.0]]_?zs = ?X) \<and> (qAFreshAbs ?zs ?z1.0 ?A \<and> qAFreshAbs ?zs ?z2.0 ?A \<longrightarrow> ?A $[[?z1.0 \<and> ?z2.0]]_?zs = ?A)

goal (1 subgoal):
 1. A' $[[z1 \<and> z2]]_zs = A'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A' $[[z1 \<and> z2]]_zs = A'

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A' $[[z1 \<and> z2]]_zs = A'

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
have "(A $[[z1 \<and> z2]]_zs) $= (A' $[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
qGoodAbs A
qFreshAbs zs z1 A
qFreshAbs zs z2 A
A $= A'

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
by (auto simp add: qSwapAbs_preserves_alphaAbs)
[PROOF STATE]
proof (state)
this:
A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
have "A' $= A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $= A
[PROOF STEP]
using 1 alphaAbs_sym
[PROOF STATE]
proof (prove)
using this:
A $= A'
?A $= ?A' \<Longrightarrow> ?A' $= ?A

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

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A' $= A

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
have "qGoodAbs (A $[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (A $[[z1 \<and> z2]]_zs)
[PROOF STEP]
using assms qSwapAbs_preserves_qGoodAbs
[PROOF STATE]
proof (prove)
using this:
qGoodAbs A
qFreshAbs zs z1 A
qFreshAbs zs z2 A
qGoodAbs (?A $[[?x \<and> ?y]]_?zs) = qGoodAbs ?A

goal (1 subgoal):
 1. qGoodAbs (A $[[z1 \<and> z2]]_zs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGoodAbs (A $[[z1 \<and> z2]]_zs)

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A' $[[z1 \<and> z2]]_zs = A'
A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
A' $= A
qGoodAbs (A $[[z1 \<and> z2]]_zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A' $[[z1 \<and> z2]]_zs = A'
A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
A' $= A
qGoodAbs (A $[[z1 \<and> z2]]_zs)

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
using alphaAbs_trans
[PROOF STATE]
proof (prove)
using this:
A' $[[z1 \<and> z2]]_zs = A'
A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
A' $= A
qGoodAbs (A $[[z1 \<and> z2]]_zs)
\<lbrakk>qGoodAbs ?A \<or> qGoodAbs ?A' \<or> qGoodAbs ?A''; ?A $= ?A'; ?A' $= ?A''\<rbrakk> \<Longrightarrow> ?A $= ?A''

goal (1 subgoal):
 1. A $[[z1 \<and> z2]]_zs $= A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $[[z1 \<and> z2]]_zs $= A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alpha_qFresh_qSwap_compose:
assumes GOOD: "qGood X" and "qFresh zs y X" and "qFresh zs z X"
shows "((X #[[y \<and> x]]_zs) #[[z \<and> y]]_zs) #= (X #[[z \<and> x]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
obtain X' where 1: "X #= X'" and "qAFresh zs y X' \<and> qAFresh zs z X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X #= X'; qAFresh zs y X' \<and> qAFresh zs z X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms qFresh_imp_ex_qAFresh2
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh zs y X
qFresh zs z X
\<lbrakk>qGood ?X; qFresh ?xs ?x ?X; qFresh ?ys ?y ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?xs ?x X' \<and> qAFresh ?ys ?y X'

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X #= X'; qAFresh zs y X' \<and> qAFresh zs z X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
X #= X'
qAFresh zs y X' \<and> qAFresh zs z X'

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
hence "((X' #[[y \<and> x]]_zs) #[[z \<and> y]]_zs) = (X' #[[z \<and> x]]_zs)"
[PROOF STATE]
proof (prove)
using this:
X #= X'
qAFresh zs y X' \<and> qAFresh zs z X'

goal (1 subgoal):
 1. X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs = X' #[[z \<and> x]]_zs
[PROOF STEP]
using qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
X #= X'
qAFresh zs y X' \<and> qAFresh zs z X'
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

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

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
have "((X #[[y \<and> x]]_zs) #[[z \<and> y]]_zs) #= ((X' #[[y \<and> x]]_zs) #[[z \<and> y]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs
[PROOF STEP]
using GOOD 1
[PROOF STATE]
proof (prove)
using this:
qGood X
X #= X'

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

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

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
have "(X' #[[z \<and> x]]_zs) #= (X #[[z \<and> x]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
using GOOD 1
[PROOF STATE]
proof (prove)
using this:
qGood X
X #= X'

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

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

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
have "qGood ((X #[[y \<and> x]]_zs) #[[z \<and> y]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_zs #[[z \<and> y]]_zs)
[PROOF STEP]
using GOOD
[PROOF STATE]
proof (prove)
using this:
qGood X

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

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs = X' #[[z \<and> x]]_zs
X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs
X' #[[z \<and> x]]_zs #= X #[[z \<and> x]]_zs
qGood (X #[[y \<and> x]]_zs #[[z \<and> y]]_zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs = X' #[[z \<and> x]]_zs
X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs
X' #[[z \<and> x]]_zs #= X #[[z \<and> x]]_zs
qGood (X #[[y \<and> x]]_zs #[[z \<and> y]]_zs)

goal (1 subgoal):
 1. X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X #[[z \<and> x]]_zs
[PROOF STEP]
using alpha_trans
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs = X' #[[z \<and> x]]_zs
X #[[y \<and> x]]_zs #[[z \<and> y]]_zs #= X' #[[y \<and> x]]_zs #[[z \<and> y]]_zs
X' #[[z \<and> x]]_zs #= X #[[z \<and> x]]_zs
qGood (X #[[y \<and> x]]_zs #[[z \<and> y]]_zs)
\<lbrakk>qGood ?X \<or> qGood ?X' \<or> qGood ?X''; ?X #= ?X'; ?X' #= ?X''\<rbrakk> \<Longrightarrow> ?X #= ?X''

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qAbs_alphaAbs_qSwap_qFresh:
assumes GOOD: "qGood X" and FRESH: "qFresh xs x' X"
shows "qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
obtain Y where good_Y: "qGood Y" and alpha: "X #= Y" and fresh_Y: "qAFresh xs x' Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>qGood Y; X #= Y; qAFresh xs x' Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms qFresh_imp_ex_qAFresh1
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh xs x' X
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?zs ?z X'

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>qGood Y; X #= Y; qAFresh xs x' Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qGood Y
X #= Y
qAFresh xs x' Y

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

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)
[PROOF STEP]
using qAbs_alphaAbs_qSwap_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood Y
X #= Y
qAFresh xs x' Y
\<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 Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
have "qAbs xs x X $= qAbs xs x Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x Y
[PROOF STEP]
using GOOD alpha qAbs_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood X
X #= 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 x X $= qAbs xs x Y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs x Y

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
have "Y #[[x' \<and> x]]_xs #= X #[[x' \<and> x]]_xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y #[[x' \<and> x]]_xs #= X #[[x' \<and> x]]_xs
[PROOF STEP]
using GOOD alpha
[PROOF STATE]
proof (prove)
using this:
qGood X
X #= Y

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
have "qGood (Y #[[x' \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (Y #[[x' \<and> x]]_xs)
[PROOF STEP]
using good_Y qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood Y
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

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

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

goal (1 subgoal):
 1. qAbs xs x' (Y #[[x' \<and> x]]_xs) $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
using qAbs_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
Y #[[x' \<and> x]]_xs #= X #[[x' \<and> x]]_xs
qGood (Y #[[x' \<and> x]]_xs)
\<lbrakk>?X #= ?X'; qGood ?X \<or> qGood ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs ?x ?X'

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

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
have "qGoodAbs (qAbs xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
using GOOD
[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. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)
qAbs xs x X $= qAbs xs x Y
qAbs xs x' (Y #[[x' \<and> x]]_xs) $= qAbs xs x' (X #[[x' \<and> x]]_xs)
qGoodAbs (qAbs xs x X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)
qAbs xs x X $= qAbs xs x Y
qAbs xs x' (Y #[[x' \<and> x]]_xs) $= qAbs xs x' (X #[[x' \<and> x]]_xs)
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
using alphaAbs_trans
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x' (Y #[[x' \<and> x]]_xs)
qAbs xs x X $= qAbs xs x Y
qAbs xs x' (Y #[[x' \<and> x]]_xs) $= qAbs xs x' (X #[[x' \<and> x]]_xs)
qGoodAbs (qAbs xs x X)
\<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 x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_ex_qFresh_rep:
assumes GOOD: "qGood X" and FRESH: "qFresh xs x' X"
shows "\<exists> X'. (X,X') \<in> qSwapped \<and> qGood X' \<and> qAbs xs x X $= qAbs xs x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'. (X, X') \<in> qSwapped \<and> qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>X'. (X, X') \<in> qSwapped \<and> 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
qFresh 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'. (X, X') \<in> qSwapped \<and> qGood X' \<and> qAbs xs x X $= qAbs xs x' X'
[PROOF STEP]
have 2: "(X,X #[[x' \<and> x]]_xs) \<in> qSwapped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, X #[[x' \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
by(simp add: qSwap_qSwapped)
[PROOF STATE]
proof (state)
this:
(X, X #[[x' \<and> x]]_xs) \<in> qSwapped

goal (1 subgoal):
 1. \<exists>X'. (X, X') \<in> qSwapped \<and> 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'. (X, X') \<in> qSwapped \<and> 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. (X, X #[[x' \<and> x]]_xs) \<in> qSwapped \<and> qGood (X #[[x' \<and> x]]_xs) \<and> qAbs xs x X $= qAbs xs x' (X #[[x' \<and> x]]_xs)
[PROOF STEP]
using assms 1 2 qAbs_alphaAbs_qSwap_qFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qFresh xs x' X
qGood (X #[[x' \<and> x]]_xs)
(X, X #[[x' \<and> x]]_xs) \<in> qSwapped
\<lbrakk>qGood ?X; qFresh ?xs ?x' ?X\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs ?x' (?X #[[?x' \<and> ?x]]_?xs)

goal (1 subgoal):
 1. (X, X #[[x' \<and> x]]_xs) \<in> qSwapped \<and> 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'. (X, X') \<in> qSwapped \<and> qGood X' \<and> qAbs xs x X $= qAbs xs x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_weakestEx_imp_strongestAll:
assumes GOOD_X: "qGood X" and "alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'"
shows "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
obtain y where xs: "xs = xs'" and
  yEqFresh: "(y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')" and
  alpha: "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X'); X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGood X
alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
xs = xs'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
xs = xs'

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
proof(intro conjI allI impI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
assume zFresh: "(z = x \<or> qAFresh xs z X) \<and> (z = x' \<or> qAFresh xs z X')"
[PROOF STATE]
proof (state)
this:
(z = x \<or> qAFresh xs z X) \<and> (z = x' \<or> qAFresh xs z X')

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "(X #[[z \<and> x]]_xs) = ((X #[[y \<and> x]]_xs) #[[z \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "z = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
 2. z \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case1: "z = x"
[PROOF STATE]
proof (state)
this:
z = x

goal (2 subgoals):
 1. z = x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
 2. z \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z = x

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

goal (1 subgoal):
 1. z \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case2: "z \<noteq> x"
[PROOF STATE]
proof (state)
this:
z \<noteq> x

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

goal (1 subgoal):
 1. qAFresh xs z X
[PROOF STEP]
using zFresh
[PROOF STATE]
proof (prove)
using this:
z \<noteq> x
(z = x \<or> qAFresh xs z X) \<and> (z = x' \<or> qAFresh xs z X')

goal (1 subgoal):
 1. qAFresh xs z X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAFresh xs z X

goal (1 subgoal):
 1. z \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "y = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
 2. y \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case21: "y = x"
[PROOF STATE]
proof (state)
this:
y = x

goal (2 subgoals):
 1. y = x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
 2. y \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
unfolding Case21
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[x \<and> x]]_xs #[[z \<and> x]]_xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case22: "y \<noteq> x"
[PROOF STATE]
proof (state)
this:
y \<noteq> x

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

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

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

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

goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
using z_fresh qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X
qAFresh xs z X
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "(X' #[[z \<and> x']]_xs) = ((X' #[[y \<and> x']]_xs) #[[z \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "z = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
 2. z \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case1: "z = x'"
[PROOF STATE]
proof (state)
this:
z = x'

goal (2 subgoals):
 1. z = x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
 2. z \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z = x'

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

goal (1 subgoal):
 1. z \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case2: "z \<noteq> x'"
[PROOF STATE]
proof (state)
this:
z \<noteq> x'

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

goal (1 subgoal):
 1. qAFresh xs z X'
[PROOF STEP]
using zFresh
[PROOF STATE]
proof (prove)
using this:
z \<noteq> x'
(z = x \<or> qAFresh xs z X) \<and> (z = x' \<or> qAFresh xs z X')

goal (1 subgoal):
 1. qAFresh xs z X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAFresh xs z X'

goal (1 subgoal):
 1. z \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "y = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
 2. y \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case21: "y = x'"
[PROOF STATE]
proof (state)
this:
y = x'

goal (2 subgoals):
 1. y = x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
 2. y \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
unfolding Case21
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[x' \<and> x']]_xs #[[z \<and> x']]_xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume Case22: "y \<noteq> x'"
[PROOF STATE]
proof (state)
this:
y \<noteq> x'

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

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

goal (1 subgoal):
 1. qAFresh xs y X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAFresh xs y X'

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

goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
using z_fresh qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X'
qAFresh xs z X'
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

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

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "qGood (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
using GOOD_X 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 (X #[[y \<and> x]]_xs)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "((X #[[y \<and> x]]_xs) #[[z \<and> y]]_xs) #= ((X' #[[y \<and> x']]_xs) #[[z \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<and> x]]_xs)

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
using alpha qSwap_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<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 #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_weakestAll_imp_strongestEx:
assumes GOOD: "qGood X"  "qGood X'"
and "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
shows "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have xs: "xs = xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
unfolding alphaAbs_all_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)

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

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
obtain y where y_not:  "y \<notin> {x,x'}" and
                 yFresh: "qAFresh xs y X \<and> qAFresh xs y X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<notin> {x, 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,X'}"]
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>finite {x, x'} \<or> |{x, x'}| <o |UNIV|; finite {X, X'} \<or> |{X, X'}| <o |UNIV|; Ball {X, X'} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> {x, x'} \<and> (\<forall>X\<in>{X, X'}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<notin> {x, 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 \<notin> {x, x'}
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
hence "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
y \<notin> {x, 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 assms
[PROOF STATE]
proof (prove)
using this:
y \<notin> {x, x'}
qAFresh xs y X \<and> qAFresh xs y X'
qGood X
qGood X'
alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
unfolding alphaAbs_all_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
y \<notin> {x, x'}
qAFresh xs y X \<and> qAFresh xs y X'
qGood X
qGood X'
xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)

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

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X 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. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. 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)
[PROOF STEP]
using xs y_not yFresh
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
xs = xs'
y \<notin> {x, x'}
qAFresh xs y X \<and> qAFresh xs y X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. 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)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_weakestEx_imp_strongestEx:
assumes GOOD: "qGood X"
and "alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'"
shows "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
obtain y where xs: "xs = xs'" and
  yEqFresh: "(y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')" and
  alpha: "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X'); X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGood X
alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>xs = xs'; (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X'); X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding alphaAbs_ex_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
qGood X
xs = xs' \<and> (\<exists>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)

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

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

goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
using GOOD alpha_qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
xs = xs'
(y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X')
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. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qGood X'
[PROOF STEP]
obtain z where zNot: "z \<notin> {x,x',y}" and
                      zFresh: "qAFresh xs z X \<and> qAFresh xs z X'"
[PROOF STATE]
proof (prove)
using this:
qGood X'

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

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

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "(X #[[z \<and> x]]_xs) = ((X #[[y \<and> x]]_xs) #[[z \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "y = x", simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume "y \<noteq> x"
[PROOF STATE]
proof (state)
this:
y \<noteq> x

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

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

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

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

goal (1 subgoal):
 1. X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
[PROOF STEP]
using zFresh qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X
qAFresh xs z X \<and> qAFresh xs z X'
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "(X' #[[z \<and> x']]_xs) = ((X' #[[y \<and> x']]_xs) #[[z \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
proof(cases "y = x'", simp add: qSwap_ident)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
assume "y \<noteq> x'"
[PROOF STATE]
proof (state)
this:
y \<noteq> x'

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

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

goal (1 subgoal):
 1. qAFresh xs y X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAFresh xs y X'

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

goal (1 subgoal):
 1. X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
using zFresh qAFresh_qSwap_compose
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X'
qAFresh xs z X \<and> qAFresh xs z X'
\<lbrakk>qAFresh ?zs ?y ?X; qAFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> ?X #[[?y \<and> ?x]]_?zs #[[?z \<and> ?y]]_?zs = ?X #[[?z \<and> ?x]]_?zs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "qGood (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
using GOOD 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 (X #[[y \<and> x]]_xs)

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

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

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

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
X #[[y \<and> x]]_xs #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
[PROOF STEP]
have "(X #[[z \<and> x]]_xs) #= (X' #[[z \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X #[[z \<and> x]]_xs = X #[[y \<and> x]]_xs #[[z \<and> y]]_xs
X' #[[z \<and> x']]_xs = X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs
X #[[y \<and> x]]_xs #[[z \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[z \<and> y]]_xs

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

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

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

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. 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)
[PROOF STEP]
using xs zNot zFresh
[PROOF STATE]
proof (prove)
using this:
X #[[z \<and> x]]_xs #= X' #[[z \<and> x']]_xs
xs = xs'
z \<notin> {x, x', y}
qAFresh xs z X \<and> qAFresh xs z X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. 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)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_ex_distinct_qAFresh:
"(qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = (xs = xs' \<and> (\<exists>y. 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))
[PROOF STEP]
by auto


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qAFresh:
assumes "qGood X"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_ex_distinct_qAFresh[of _ _ X]
        alphaAbs_weakestEx_imp_strongestEx
[PROOF STATE]
proof (prove)
using this:
qGood X
(qAbs ?xs ?x X $= qAbs ?xs' ?x' ?X') = alphaAbs_ex_distinct_qAFresh ?xs ?x X ?xs' ?x' ?X'
\<lbrakk>qGood ?X; alphaAbs_ex_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_ex_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'

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

goal:
No subgoals!
[PROOF STEP]
qed