[STATEMENT]
lemma alphaAll_refl:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
shows
"(qGood X \<longrightarrow> X #= X) \<and> (qGoodAbs A \<longrightarrow> A $= A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> X #= X) \<and> (qGoodAbs A \<longrightarrow> A $= A)
[PROOF STEP]
apply(rule qGood_qTerm_induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>|{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> X #= X) inp; liftAll (\<lambda>A. qGoodAbs A \<and> A $= A) binp\<rbrakk> \<Longrightarrow> sameDom inp inp \<and> sameDom binp binp \<and> liftAll2 (#=) inp inp \<and> liftAll2 ($=) binp binp
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
unfolding liftAll_def sameDom_def liftAll2_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>|{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; \<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> v #= v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> v $= v\<rbrakk> \<Longrightarrow> (\<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)
 2. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
proof-
[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> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
fix xs x X
[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> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
assume "qGood X" and
        IH: "\<And>Y. (X,Y) \<in> qSwapped \<Longrightarrow> Y #= Y"
[PROOF STATE]
proof (state)
this:
qGood X
(X, ?Y11) \<in> qSwapped \<Longrightarrow> ?Y11 #= ?Y11

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qGood X
(X, ?Y11) \<in> qSwapped \<Longrightarrow> ?Y11 #= ?Y11
[PROOF STEP]
obtain y where 1: "y \<noteq> x \<and> qAFresh xs y X"
[PROOF STATE]
proof (prove)
using this:
qGood X
(X, ?Y11) \<in> qSwapped \<Longrightarrow> ?Y11 #= ?Y11

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

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

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
hence "(X, X #[[y \<and> x]]_xs) \<in> qSwapped"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x \<and> qAFresh xs y X

goal (1 subgoal):
 1. (X, X #[[y \<and> x]]_xs) \<in> qSwapped
[PROOF STEP]
using qSwap_qSwapped
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x \<and> qAFresh xs y X
(?X, ?X #[[?x \<and> ?y]]_?zs) \<in> qSwapped

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

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
hence "(X #[[y \<and> x]]_xs) #= (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped

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

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

goal (1 subgoal):
 1. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> Y #= Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> Y #= Y\<rbrakk> \<Longrightarrow> \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
thus "\<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> (X #[[y \<and> x]]_xs) #= (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs

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

goal (1 subgoal):
 1. \<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> x \<and> qAFresh xs y X \<and> X #[[y \<and> x]]_xs #= X #[[y \<and> x]]_xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAll_preserves_qGoodAll1:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
shows
"(qGood X \<longrightarrow> (\<forall> X'. X #= X' \<longrightarrow> qGood X')) \<and>
 (qGoodAbs A \<longrightarrow> (\<forall> A'. A $= A' \<longrightarrow> qGoodAbs A'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> (\<forall>X'. X #= X' \<longrightarrow> qGood X')) \<and> (qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A'))
[PROOF STEP]
apply(rule qTerm_induct, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs x X'. qVar xs x #= X' \<Longrightarrow> qGood X'
 2. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 3. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
unfolding qVar_alpha_iff
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs x X'. X' = qVar xs x \<Longrightarrow> qGood X'
 2. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 3. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 2. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 2. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
fix delta inp binp X'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 2. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
assume
  IH1: "liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp"
  and IH2: "liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp"
  and *: "liftAll qGood inp"  "liftAll qGoodAbs binp"
  and **: "|{i. \<exists>Y. inp i = Some Y}| <o |UNIV :: 'var set|"
          "|{i. \<exists>A. binp i = Some A}| <o |UNIV :: 'var set|"
  and "qOp delta inp binp #= X'"
[PROOF STATE]
proof (state)
this:
liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp
liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp
liftAll qGood inp
liftAll qGoodAbs binp
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
qOp delta inp binp #= X'

goal (2 subgoals):
 1. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 2. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp
liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp
liftAll qGood inp
liftAll qGoodAbs binp
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
qOp delta inp binp #= X'
[PROOF STEP]
obtain inp' binp' where
  X'eq: "X' = qOp delta inp' binp'" and
  2: "sameDom inp inp' \<and> sameDom binp binp'" and
  3: "liftAll2 (\<lambda>Y Y'. Y #= Y') inp inp' \<and>
      liftAll2 (\<lambda>A A'. A $= A') binp binp'"
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp
liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp
liftAll qGood inp
liftAll qGoodAbs binp
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
qOp delta inp binp #= X'

goal (1 subgoal):
 1. (\<And>inp' binp'. \<lbrakk>X' = qOp delta inp' binp'; sameDom inp inp' \<and> sameDom binp binp'; liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding qOp_alpha_iff
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp
liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp
liftAll qGood inp
liftAll qGoodAbs binp
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
\<exists>inp' binp'. X' = qOp delta inp' binp' \<and> sameDom inp inp' \<and> sameDom binp binp' \<and> liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

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

goal (2 subgoals):
 1. \<And>delta inp binp X'. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> (\<forall>X'. a #= X' \<longrightarrow> qGood X')) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> (\<forall>A'. a $= A' \<longrightarrow> qGoodAbs A')) binp; liftAll qGood inp; liftAll qGoodAbs binp; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; qOp delta inp binp #= X'\<rbrakk> \<Longrightarrow> qGood X'
 2. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
show "qGood X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
unfolding X'eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (qOp delta inp' binp')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll qGood inp' \<and> liftAll qGoodAbs binp' \<and> |{i. \<exists>y. inp' i = Some y}| <o |UNIV| \<and> |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v. inp' i = Some v \<longrightarrow> qGood v) \<and> (\<forall>i v. binp' i = Some v \<longrightarrow> qGoodAbs v) \<and> |{i. \<exists>y. inp' i = Some y}| <o |UNIV| \<and> |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
fix i Y'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
assume inp': "inp' i = Some Y'"
[PROOF STATE]
proof (state)
this:
inp' i = Some Y'

goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[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 2
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
sameDom inp inp' \<and> sameDom binp binp'

goal (1 subgoal):
 1. (\<And>Y. inp i = Some Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
using this:
inp' i = Some Y'
(\<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 (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
hence "Y #= Y'"
[PROOF STATE]
proof (prove)
using this:
inp i = Some Y

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

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

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

goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y #= Y'

goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
have "qGood Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood Y
[PROOF STEP]
using * inp
[PROOF STATE]
proof (prove)
using this:
liftAll qGood inp
liftAll qGoodAbs binp
inp i = Some Y

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

goal (1 subgoal):
 1. qGood Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qGood Y

goal (4 subgoals):
 1. \<And>i v. inp' i = Some v \<Longrightarrow> qGood v
 2. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 3. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 4. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y #= Y'
qGood Y
[PROOF STEP]
show "qGood Y'"
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
qGood Y

goal (1 subgoal):
 1. qGood Y'
[PROOF STEP]
using IH1 inp
[PROOF STATE]
proof (prove)
using this:
Y #= Y'
qGood Y
liftAll (\<lambda>Y. qGood Y \<longrightarrow> (\<forall>Y'. Y #= Y' \<longrightarrow> qGood Y')) inp
inp i = Some Y

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

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

goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
fix i A'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
assume binp': "binp' i = Some A'"
[PROOF STATE]
proof (state)
this:
binp' i = Some A'

goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[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 2
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
sameDom inp inp' \<and> sameDom binp binp'

goal (1 subgoal):
 1. (\<And>A. binp i = Some A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
using this:
binp' i = Some A'
(\<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 (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
hence "A $= A'"
[PROOF STATE]
proof (prove)
using this:
binp i = Some A

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

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

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

goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $= A'

goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
have "qGoodAbs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
using * binp
[PROOF STATE]
proof (prove)
using this:
liftAll qGood inp
liftAll qGoodAbs binp
binp i = Some A

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

goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qGoodAbs A

goal (3 subgoals):
 1. \<And>i v. binp' i = Some v \<Longrightarrow> qGoodAbs v
 2. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 3. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A $= A'
qGoodAbs A
[PROOF STEP]
show "qGoodAbs A'"
[PROOF STATE]
proof (prove)
using this:
A $= A'
qGoodAbs A

goal (1 subgoal):
 1. qGoodAbs A'
[PROOF STEP]
using IH2 binp
[PROOF STATE]
proof (prove)
using this:
A $= A'
qGoodAbs A
liftAll (\<lambda>A. qGoodAbs A \<longrightarrow> (\<forall>A'. A $= A' \<longrightarrow> qGoodAbs A')) binp
binp i = Some A

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

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

goal (2 subgoals):
 1. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 2. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 2. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
have "{i. \<exists>Y'. inp' i = Some Y'} = {i. \<exists>Y. inp i = Some Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. \<exists>Y'. inp' i = Some Y'} = {i. \<exists>Y. inp i = Some Y}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
sameDom inp inp' \<and> sameDom binp binp'

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

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

goal (2 subgoals):
 1. |{i. \<exists>y. inp' i = Some y}| <o |UNIV|
 2. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
thus "|{i. \<exists>Y'. inp' i = Some Y'}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
{i. \<exists>Y'. inp' i = Some Y'} = {i. \<exists>Y. inp i = Some Y}

goal (1 subgoal):
 1. |{i. \<exists>Y'. inp' i = Some Y'}| <o |UNIV|
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
{i. \<exists>Y'. inp' i = Some Y'} = {i. \<exists>Y. inp i = Some Y}
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|

goal (1 subgoal):
 1. |{i. \<exists>Y'. inp' i = Some Y'}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{i. \<exists>Y'. inp' i = Some Y'}| <o |UNIV|

goal (1 subgoal):
 1. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
have "{i. \<exists>A'. binp' i = Some A'} = {i. \<exists>A. binp i = Some A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. \<exists>A'. binp' i = Some A'} = {i. \<exists>A. binp i = Some A}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
sameDom inp inp' \<and> sameDom binp binp'

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

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

goal (1 subgoal):
 1. |{i. \<exists>y. binp' i = Some y}| <o |UNIV|
[PROOF STEP]
thus "|{i. \<exists>A'. binp' i = Some A'}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
{i. \<exists>A'. binp' i = Some A'} = {i. \<exists>A. binp i = Some A}

goal (1 subgoal):
 1. |{i. \<exists>A'. binp' i = Some A'}| <o |UNIV|
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
{i. \<exists>A'. binp' i = Some A'} = {i. \<exists>A. binp i = Some A}
|{i. \<exists>Y. inp i = Some Y}| <o |UNIV|
|{i. \<exists>A. binp i = Some A}| <o |UNIV|

goal (1 subgoal):
 1. |{i. \<exists>A'. binp' i = Some A'}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{i. \<exists>A'. binp' i = Some A'}| <o |UNIV|

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

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

goal (1 subgoal):
 1. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(X, ?Y11) \<in> qSwapped \<Longrightarrow> qGood ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> qGood X')
qGood X
qAbs xs x X $= A'
[PROOF STEP]
obtain x' y X' where "A' = qAbs xs x' X'" and
       1: "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
(X, ?Y11) \<in> qSwapped \<Longrightarrow> qGood ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> qGood X')
qGood X
qAbs xs x X $= A'

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' 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:
(X, ?Y11) \<in> qSwapped \<Longrightarrow> qGood ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> qGood X')
qGood X
\<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

goal (1 subgoal):
 1. (\<And>x' X' y. \<lbrakk>A' = qAbs xs x' 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'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>xs x X A'. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> (\<forall>X'. Y #= X' \<longrightarrow> qGood X'); qGood X; qAbs xs x X $= A'\<rbrakk> \<Longrightarrow> qGoodAbs A'
[PROOF STEP]
thus "qGoodAbs A'"
[PROOF STATE]
proof (prove)
using this:
A' = qAbs xs x' X'
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

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

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

goal (1 subgoal):
 1. \<lbrakk>A' = qAbs xs x' X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> qGood 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 * 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. \<lbrakk>A' = qAbs xs x' X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> qGood X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
have "qGood(X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
qGood (X #[[y \<and> x]]_xs)

goal (1 subgoal):
 1. qGood (X' #[[y \<and> x']]_xs)
[PROOF STEP]
using 1 IH
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
qGood (X #[[y \<and> x]]_xs)
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
(X, ?Y11) \<in> qSwapped \<Longrightarrow> qGood ?Y11 \<longrightarrow> (\<forall>X'. ?Y11 #= X' \<longrightarrow> 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. \<lbrakk>A' = qAbs xs x' X'; X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs\<rbrakk> \<Longrightarrow> qGood X'
[PROOF STEP]
thus "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
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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
qGoodAbs A'

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

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


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

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


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

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


[STATEMENT]
lemma alpha_qSwap_preserves_qGood1:
assumes ALPHA: "(X #[[y \<and> x]]_zs) #= (X' #[[y' \<and> x']]_zs')" and
        GOOD: "qGood X"
shows "qGood X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
have "qGood(X #[[y \<and> x]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_zs)
[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]]_zs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X #[[y \<and> x]]_zs)

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

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

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

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

goal (1 subgoal):
 1. qGood X'
[PROOF STEP]
using qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood (X' #[[y' \<and> x']]_zs')
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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alpha_qSwap_preserves_qGood2:
assumes ALPHA: "(X #[[y \<and> x]]_zs) #= (X' #[[y' \<and> x']]_zs')" and
        GOOD': "qGood X'"
shows "qGood X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qGood X
[PROOF STEP]
have "qGood(X' #[[y' \<and> x']]_zs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X' #[[y' \<and> x']]_zs')
[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']]_zs')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X' #[[y' \<and> x']]_zs')

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

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

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

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

goal (1 subgoal):
 1. qGood X
[PROOF STEP]
using qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood (X #[[y \<and> x]]_zs)
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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qSwapAbs_preserves_qGoodAbs2:
assumes ALPHA: "(A $[[y \<and> x]]_zs) $= (A' $[[y' \<and> x']]_zs')" and
        GOOD': "qGoodAbs A'"
shows "qGoodAbs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
have "qGoodAbs(A' $[[y' \<and> x']]_zs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (A' $[[y' \<and> x']]_zs')
[PROOF STEP]
using GOOD' qSwapAbs_preserves_qGoodAbs
[PROOF STATE]
proof (prove)
using this:
qGoodAbs A'
qGoodAbs (?A $[[?x \<and> ?y]]_?zs) = qGoodAbs ?A

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

goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
hence "qGoodAbs (A $[[y \<and> x]]_zs)"
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (A' $[[y' \<and> x']]_zs')

goal (1 subgoal):
 1. qGoodAbs (A $[[y \<and> x]]_zs)
[PROOF STEP]
using ALPHA alphaAbs_preserves_qGoodAbs
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (A' $[[y' \<and> x']]_zs')
A $[[y \<and> x]]_zs $= A' $[[y' \<and> x']]_zs'
?A $= ?A' \<Longrightarrow> qGoodAbs ?A = qGoodAbs ?A'

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

goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
thus "qGoodAbs A"
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (A $[[y \<and> x]]_zs)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alpha_qSwap_preserves_qGood:
assumes ALPHA: "(X #[[y \<and> x]]_zs) #= (X' #[[y' \<and> x']]_zs')"
shows "qGood X = qGood X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X = qGood X'
[PROOF STEP]
using assms alpha_qSwap_preserves_qGood1
      alpha_qSwap_preserves_qGood2
[PROOF STATE]
proof (prove)
using this:
X #[[y \<and> x]]_zs #= X' #[[y' \<and> x']]_zs'
\<lbrakk>?X #[[?y \<and> ?x]]_?zs #= ?X' #[[?y' \<and> ?x']]_?zs'; qGood ?X\<rbrakk> \<Longrightarrow> qGood ?X'
\<lbrakk>?X #[[?y \<and> ?x]]_?zs #= ?X' #[[?y' \<and> ?x']]_?zs'; qGood ?X'\<rbrakk> \<Longrightarrow> qGood ?X

goal (1 subgoal):
 1. qGood X = qGood X'
[PROOF STEP]
by auto


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

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

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

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

goal (1 subgoal):
 1. \<And>X' zs z1 z2. qOp delta inp binp #= X' \<Longrightarrow> qOp delta inp binp #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
term X'
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X'

goal (1 subgoal):
 1. \<And>X' zs z1 z2. qOp delta inp binp #= X' \<Longrightarrow> qOp delta inp binp #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
term binp
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X'

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

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

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

goal (1 subgoal):
 1. \<And>X' zs z1 z2. qOp delta inp binp #= X' \<Longrightarrow> qOp delta inp binp #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
thus "((qOp delta inp binp) #[[z1 \<and> z2]]_zs) #= (X' #[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
using this:
X' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. qOp delta inp binp #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
[PROOF STEP]
unfolding X'eq
[PROOF STATE]
proof (prove)
using this:
qOp delta inp' binp' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. qOp delta inp binp #[[z1 \<and> z2]]_zs #= qOp delta inp' binp' #[[z1 \<and> z2]]_zs
[PROOF STEP]
using Op.IH
[PROOF STATE]
proof (prove)
using this:
qOp delta inp' binp' = qOp delta inp' binp'
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'
liftAll (\<lambda>X. qGood X \<and> (\<forall>X' zs z1 z2. X #= X' \<longrightarrow> X #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs)) inp
liftAll (\<lambda>A. qGoodAbs A \<and> (\<forall>A' zs z1 z2. A $= A' \<longrightarrow> A $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs)) binp

goal (1 subgoal):
 1. qOp delta inp binp #[[z1 \<and> z2]]_zs #= qOp delta inp' binp' #[[z1 \<and> z2]]_zs
[PROOF STEP]
by (auto simp add: fun_eq_iff option.case_eq_if
       lift_def liftAll_def sameDom_def liftAll2_def)
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs

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

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

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

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

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

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' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
hence goodX': "qGood X'"
[PROOF STATE]
proof (prove)
using 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. qGood X'
[PROOF STEP]
using \<open>qGood X\<close> alpha_qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using 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
qGood X
?X #[[?y \<and> ?x]]_?zs #= ?X' #[[?y' \<and> ?x']]_?zs' \<Longrightarrow> qGood ?X = qGood ?X'

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
(* *)
[PROOF STATE]
proof (state)
this:
qGood X'

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
obtain u where u_notin: "u \<notin> {x,x',z1,z2,y}" and
                   u_freshXX': "qAFresh xs u X \<and> qAFresh xs u X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<notin> {x, x', z1, z2, y}; qAFresh xs u X \<and> qAFresh xs u X'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  \<open>qGood X\<close> goodX' obtain_qFresh[of "{x,x',z1,z2,y}" "{X,X'}"]
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>finite {x, x', z1, z2, y} \<or> |{x, x', z1, z2, y}| <o |UNIV|; finite {X, X'} \<or> |{X, X'}| <o |UNIV|; Ball {X, X'} qGood\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<notin> {x, x', z1, z2, y} \<and> (\<forall>X\<in>{X, X'}. qAFresh ?xs xa X \<and> qFresh ?xs xa X)

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
hence u_not: "u \<noteq> (x @xs[z1 \<and> z2]_zs) \<and> u \<noteq> (x' @xs[z1 \<and> z2]_zs)"
[PROOF STATE]
proof (prove)
using this:
u \<notin> {x, x', z1, z2, y}
qAFresh xs u X \<and> qAFresh xs u X'

goal (1 subgoal):
 1. u \<noteq> x @xs[z1 \<and> z2]_zs \<and> u \<noteq> x' @xs[z1 \<and> z2]_zs
[PROOF STEP]
unfolding sw_def
[PROOF STATE]
proof (prove)
using this:
u \<notin> {x, x', z1, z2, y}
qAFresh xs u X \<and> qAFresh xs u X'

goal (1 subgoal):
 1. u \<noteq> (if zs = xs then if x = z1 then z2 else if x = z2 then z1 else x else x) \<and> u \<noteq> (if zs = xs then if x' = z1 then z2 else if x' = z2 then z1 else x' else x')
[PROOF STEP]
using u_notin
[PROOF STATE]
proof (prove)
using this:
u \<notin> {x, x', z1, z2, y}
qAFresh xs u X \<and> qAFresh xs u X'
u \<notin> {x, x', z1, z2, y}

goal (1 subgoal):
 1. u \<noteq> (if zs = xs then if x = z1 then z2 else if x = z2 then z1 else x else x) \<and> u \<noteq> (if zs = xs then if x' = z1 then z2 else if x' = z2 then z1 else x' else x')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> x @xs[z1 \<and> z2]_zs \<and> u \<noteq> x' @xs[z1 \<and> z2]_zs

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
have u_fresh: "qAFresh xs u (X #[[z1 \<and> z2]]_zs) \<and> qAFresh xs u (X' #[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAFresh xs u (X #[[z1 \<and> z2]]_zs) \<and> qAFresh xs u (X' #[[z1 \<and> z2]]_zs)
[PROOF STEP]
using u_freshXX' u_notin
[PROOF STATE]
proof (prove)
using this:
qAFresh xs u X \<and> qAFresh xs u X'
u \<notin> {x, x', z1, z2, y}

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
qAFresh xs u (X #[[z1 \<and> z2]]_zs) \<and> qAFresh xs u (X' #[[z1 \<and> z2]]_zs)

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
have "((X #[[z1 \<and> z2]]_zs) #[[u \<and> (x @xs[z1 \<and> z2]_zs)]]_xs) =
          (((X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs) #[[z1 \<and> z2]]_zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #[[u \<and> x @xs[z1 \<and> z2]_zs]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #[[z1 \<and> z2]]_zs
[PROOF STEP]
using y_fresh u_freshXX' u_notin
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X \<and> qAFresh xs y X'
qAFresh xs u X \<and> qAFresh xs u X'
u \<notin> {x, x', z1, z2, y}

goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #[[u \<and> x @xs[z1 \<and> z2]_zs]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #[[z1 \<and> z2]]_zs
[PROOF STEP]
by (simp add: qSwap_3commute)
[PROOF STATE]
proof (state)
this:
X #[[z1 \<and> z2]]_zs #[[u \<and> x @xs[z1 \<and> z2]_zs]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #[[z1 \<and> z2]]_zs

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X #[[z1 \<and> z2]]_zs #[[u \<and> x @xs[z1 \<and> z2]_zs]]_xs = X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #[[z1 \<and> z2]]_zs

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
hence "((X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs) #= ((X' #[[y \<and> x']]_xs) #[[u \<and> y]]_xs)"
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped

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 alpha Abs.IH
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
qGood ?Y11 \<and> qSkel ?Y11 = qSkel X \<Longrightarrow> \<forall>X' zs z1 z2. ?Y11 #= X' \<longrightarrow> ?Y11 #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_zs
(X, ?Y11) \<in> qSwapped \<Longrightarrow> \<forall>X' zs z1 z2. ?Y11 #= X' \<longrightarrow> ?Y11 #[[z1 \<and> z2]]_zs #= X' #[[z1 \<and> z2]]_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 auto
[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' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #[[u \<and> y]]_xs #= X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
have "(X, (X #[[y \<and> x]]_xs) #[[u \<and> y]]_xs) \<in> qSwapped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, X #[[y \<and> x]]_xs #[[u \<and> y]]_xs) \<in> qSwapped
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(X, X #[[y \<and> x]]_xs) \<in> qSwapped

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>A' zs z1 z2. qAbs xs x X $= A' \<Longrightarrow> qAbs xs x X $[[z1 \<and> z2]]_zs $= A' $[[z1 \<and> z2]]_zs
[PROOF STEP]
have "(((X' #[[y \<and> x']]_xs) #[[u \<and> y]]_xs) #[[z1 \<and> z2]]_zs) =
          ((X' #[[z1 \<and> z2]]_zs) #[[u \<and> (x' @xs[z1 \<and> z2]_zs)]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #[[u \<and> y]]_xs #[[z1 \<and> z2]]_zs = X' #[[z1 \<and> z2]]_zs #[[u \<and> x' @xs[z1 \<and> z2]_zs]]_xs
[PROOF STEP]
using y_fresh u_freshXX' u_notin
[PROOF STATE]
proof (prove)
using this:
qAFresh xs y X \<and> qAFresh xs y X'
qAFresh xs u X \<and> qAFresh xs u X'
u \<notin> {x, x', z1, z2, y}

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

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

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

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

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

goal (1 subgoal):
 1. qAbs xs x X $[[z1 \<and> z2]]_zs $= qAbs xs x' X' $[[z1 \<and> z2]]_zs
[PROOF STEP]
using u_not u_fresh
[PROOF STATE]
proof (prove)
using this:
X #[[z1 \<and> z2]]_zs #[[u \<and> x @xs[z1 \<and> z2]_zs]]_xs #= X' #[[z1 \<and> z2]]_zs #[[u \<and> x' @xs[z1 \<and> z2]_zs]]_xs
u \<noteq> x @xs[z1 \<and> z2]_zs \<and> u \<noteq> x' @xs[z1 \<and> z2]_zs
qAFresh xs u (X #[[z1 \<and> z2]]_zs) \<and> qAFresh xs u (X' #[[z1 \<and> z2]]_zs)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qSwap_twice_preserves_alpha:
assumes "qGood X \<or> qGood X'" and "X #= X'"
shows "((X #[[z1 \<and> z2]]_zs) #[[u1 \<and> u2]]_us) #= ((X' #[[z1 \<and> z2]]_zs) #[[u1 \<and> u2]]_us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[[z1 \<and> z2]]_zs #[[u1 \<and> u2]]_us #= X' #[[z1 \<and> z2]]_zs #[[u1 \<and> u2]]_us
[PROOF STEP]
by (simp add: assms qSwap_preserves_alpha qSwap_preserves_qGood)