[STATEMENT]
lemma qGood_qTerm_rawInduct[case_names Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and phi phiAbs
assumes
Var: "\<And> xs x. phi (qVar xs x)" and
Op: "\<And> delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV :: 'var set|;
                        |{i. binp i \<noteq> None}| <o |UNIV :: 'var set|;
                        liftAll (\<lambda> X. qGood X \<and> phi X) inp;
                        liftAll (\<lambda> A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk>
                       \<Longrightarrow> phi (qOp delta inp binp)" and
Abs: "\<And> xs x X. \<lbrakk>qGood X; phi X\<rbrakk>  \<Longrightarrow> phiAbs (qAbs xs x X)"
shows "(qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)
[PROOF STEP]
apply(induct rule: qGood_qTerm_templateInduct [of Id])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>X Y. \<lbrakk>qGood X; (X, Y) \<in> Id\<rbrakk> \<Longrightarrow> qGood Y \<and> qSkel Y = qSkel X
 2. \<And>xs x. phi (qVar xs x)
 3. \<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> phi X) inp; liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk> \<Longrightarrow> phi (qOp delta inp binp)
 4. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. (X, Y) \<in> Id \<Longrightarrow> phi Y\<rbrakk> \<Longrightarrow> phiAbs (qAbs xs x X)
[PROOF STEP]
by(simp_all add: assms)


[STATEMENT]
lemma qGood_qTerm_induct[case_names Var Op Abs]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and phi phiAbs
assumes
Var: "\<And> xs x. phi (qVar xs x)" and
Op: "\<And> delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV :: 'var set|;
                        |{i. binp i \<noteq> None}| <o |UNIV :: 'var set|;
                        liftAll (\<lambda> X. qGood X \<and> phi X) inp;
                        liftAll (\<lambda> A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk>
                       \<Longrightarrow> phi (qOp delta inp binp)" and
Abs: "\<And> xs x X. \<lbrakk>qGood X;
                 \<And> Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi Y;
                 \<And> Y. (X,Y) \<in> qSwapped \<Longrightarrow> phi Y\<rbrakk>
                 \<Longrightarrow> phiAbs (qAbs xs x X)"
shows
"(qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)
[PROOF STEP]
apply(induct rule: qGood_qTerm_templateInduct
           [of "qSwapped \<union> {(X,Y). qGood Y \<and> qSkel Y = qSkel X}"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>X Y. \<lbrakk>qGood X; (X, Y) \<in> qSwapped \<union> {(X, Y). qGood Y \<and> qSkel Y = qSkel X}\<rbrakk> \<Longrightarrow> qGood Y \<and> qSkel Y = qSkel X
 2. \<And>xs x. phi (qVar xs x)
 3. \<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> phi X) inp; liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk> \<Longrightarrow> phi (qOp delta inp binp)
 4. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. (X, Y) \<in> qSwapped \<union> {(X, Y). qGood Y \<and> qSkel Y = qSkel X} \<Longrightarrow> phi Y\<rbrakk> \<Longrightarrow> phiAbs (qAbs xs x X)
[PROOF STEP]
using qSwapped_qSkel qSwapped_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
(?X, ?Y) \<in> qSwapped \<Longrightarrow> qSkel ?Y = qSkel ?X
(?X, ?Y) \<in> qSwapped \<Longrightarrow> qGood ?Y = qGood ?X

goal (4 subgoals):
 1. \<And>X Y. \<lbrakk>qGood X; (X, Y) \<in> qSwapped \<union> {(X, Y). qGood Y \<and> qSkel Y = qSkel X}\<rbrakk> \<Longrightarrow> qGood Y \<and> qSkel Y = qSkel X
 2. \<And>xs x. phi (qVar xs x)
 3. \<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> phi X) inp; liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk> \<Longrightarrow> phi (qOp delta inp binp)
 4. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. (X, Y) \<in> qSwapped \<union> {(X, Y). qGood Y \<and> qSkel Y = qSkel X} \<Longrightarrow> phi Y\<rbrakk> \<Longrightarrow> phiAbs (qAbs xs x X)
[PROOF STEP]
by(auto simp add: assms)


[STATEMENT]
lemma qGood_qTerm_induct_mutual[case_names Var1 Var2 Op1 Op2 Abs1 Abs2]:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and phi1 phi2 phiAbs1 phiAbs2
assumes
Var1: "\<And> xs x. phi1 (qVar xs x)" and
Var2: "\<And> xs x. phi2 (qVar xs x)" and
Op1: "\<And> delta inp binp. \<lbrakk>liftAll (\<lambda> X. qGood X \<and> phi1 X) inp;
                         liftAll (\<lambda> A. qGoodAbs A \<and> phiAbs1 A) binp\<rbrakk>
                        \<Longrightarrow> phi1 (qOp delta inp binp)" and
Op2: "\<And> delta inp binp. \<lbrakk>liftAll (\<lambda> X. qGood X \<and> phi2 X) inp;
                         liftAll (\<lambda> A. qGoodAbs A \<and> phiAbs2 A) binp\<rbrakk>
                        \<Longrightarrow> phi2 (qOp delta inp binp)" and
Abs1: "\<And> xs x X. \<lbrakk>qGood X;
                  \<And> Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi1 Y;
                  \<And> Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi2 Y;
                  \<And> Y. (X,Y) \<in> qSwapped \<Longrightarrow> phi1 Y;
                  \<And> Y. (X,Y) \<in> qSwapped \<Longrightarrow> phi2 Y\<rbrakk>
                 \<Longrightarrow> phiAbs1 (qAbs xs x X)" and
Abs2: "\<And> xs x X. \<lbrakk>qGood X;
                  \<And> Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi1 Y;
                  \<And> Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi2 Y;
                  \<And> Y. (X,Y) \<in> qSwapped \<Longrightarrow> phi1 Y;
                  \<And> Y. (X,Y) \<in> qSwapped \<Longrightarrow> phi2 Y;
                  phiAbs1 (qAbs xs x X)\<rbrakk>
                 \<Longrightarrow> phiAbs2 (qAbs xs x X)"
shows
"(qGood X \<longrightarrow> (phi1 X \<and> phi2 X)) \<and>
 (qGoodAbs A \<longrightarrow> (phiAbs1 A \<and> phiAbs2 A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> phi1 X \<and> phi2 X) \<and> (qGoodAbs A \<longrightarrow> phiAbs1 A \<and> phiAbs2 A)
[PROOF STEP]
apply(induct rule: qGood_qTerm_induct[of _ _ X A])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs x. phi1 (qVar xs x) \<and> phi2 (qVar xs 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> phi1 X \<and> phi2 X) inp; liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs1 A \<and> phiAbs2 A) binp\<rbrakk> \<Longrightarrow> phi1 (qOp delta inp binp) \<and> phi2 (qOp delta inp binp)
 3. \<And>xs x X. \<lbrakk>qGood X; \<And>Y. qGood Y \<and> qSkel Y = qSkel X \<Longrightarrow> phi1 Y \<and> phi2 Y; \<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> phi1 Y \<and> phi2 Y\<rbrakk> \<Longrightarrow> phiAbs1 (qAbs xs x X) \<and> phiAbs2 (qAbs xs x X)
[PROOF STEP]
by(auto simp add: assms liftAll_and)


[STATEMENT]
lemma single_non_qAFreshAll_ordLess_var:
fixes X :: "('index,'bindex,'varSort,'var,'opSym)qTerm"
and A::"('index,'bindex,'varSort,'var,'opSym)qAbs"
shows
"(qGood X \<longrightarrow> |{x. \<not> qAFresh xs x X}| <o |UNIV :: 'var set| ) \<and>
 (qGoodAbs A \<longrightarrow> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV :: 'var set| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> |{x. \<not> qAFresh xs x X}| <o |UNIV|) \<and> (qGoodAbs A \<longrightarrow> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|)
[PROOF STEP]
proof(induct rule: qGood_qTerm_rawInduct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xsa x. |{xa. \<not> qAFresh xs xa (qVar xsa x)}| <o |UNIV|
 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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 3. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
case (Var xs x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>xsa x. |{xa. \<not> qAFresh xs xa (qVar xsa x)}| <o |UNIV|
 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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 3. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{xa. \<not> qAFresh xs xa (qVar xs x)}| <o |UNIV|
[PROOF STEP]
using infinite_var_regular_INNER
[PROOF STATE]
proof (prove)
using this:
infinite UNIV \<and> regular |UNIV|

goal (1 subgoal):
 1. |{xa. \<not> qAFresh xs xa (qVar xs x)}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{xa. \<not> qAFresh xs xa (qVar xs x)}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp
liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) 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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
let ?Left = "{x. \<not> qAFresh xs x (qOp delta inp binp)}"
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
obtain J where J_def: "J = {i. \<exists> X. inp i = Some X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>J. J = {i. \<exists>X. inp i = Some X} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
J = {i. \<exists>X. inp i = Some 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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
let ?S = "\<Union> i \<in> J. {x. \<exists> X. inp i = Some X \<and> \<not> qAFresh xs x X}"
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
{
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
fix i
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
obtain K where K_def: "K = {X. inp i = Some X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. K = {X. inp i = Some X} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
K = {X. inp i = Some 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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "finite K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite K
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {X. inp i = Some X}
[PROOF STEP]
by (cases "inp i", auto)
[PROOF STATE]
proof (state)
this:
finite K

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
hence "|K| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
finite K

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
using var_infinite_INNER finite_ordLess_infinite2
[PROOF STATE]
proof (prove)
using this:
finite K
infinite UNIV
\<lbrakk>finite ?A; infinite ?B\<rbrakk> \<Longrightarrow> |?A| <o |?B|

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "\<forall> X \<in> K. |{x. \<not> qAFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>K. |{x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X. inp i = Some X}. |{x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using Op
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp
liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp

goal (1 subgoal):
 1. \<forall>X\<in>{X. inp i = Some X}. |{x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> |{x. \<not> qAFresh xs x v}| <o |UNIV|
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> |{x. \<not> qAFreshAbs xs x v}| <o |UNIV|

goal (1 subgoal):
 1. \<forall>X\<in>{X. inp i = Some X}. |{x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>K. |{x. \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|K| <o |UNIV|
\<forall>X\<in>K. |{x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
have "|\<Union> X \<in> K. {x. \<not> qAFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|
\<forall>X\<in>K. |{x. \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. |\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using var_regular_INNER
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|
\<forall>X\<in>K. |{x. \<not> qAFresh xs x X}| <o |UNIV|
regular |UNIV|

goal (1 subgoal):
 1. |\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by (simp add: regular_UNION)
[PROOF STATE]
proof (state)
this:
|\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} =
         (\<Union> X \<in> K. {x. \<not> qAFresh xs x X})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>K. {x. \<not> qAFresh xs x X})
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>{X. inp i = Some X}. {x. \<not> qAFresh xs x X})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>K. {x. \<not> qAFresh xs x X})

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV|; |{i. binp i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|
{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>K. {x. \<not> qAFresh xs x X})
[PROOF STEP]
have "|{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|\<Union>X\<in>K. {x. \<not> qAFresh xs x X}| <o |UNIV|
{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>K. {x. \<not> qAFresh xs x X})

goal (1 subgoal):
 1. |{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
|{x. \<exists>X. inp ?i13 = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|{x. \<exists>X. inp ?i13 = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "|J| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
unfolding J_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{i. \<exists>X. inp i = Some X}| <o |UNIV|
[PROOF STEP]
using Op
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp
liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp

goal (1 subgoal):
 1. |{i. \<exists>X. inp i = Some X}| <o |UNIV|
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> |{x. \<not> qAFresh xs x v}| <o |UNIV|
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> |{x. \<not> qAFreshAbs xs x v}| <o |UNIV|

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

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|{x. \<exists>X. inp ?i13 = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|J| <o |UNIV|
[PROOF STEP]
have 1: "|?S| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|{x. \<exists>X. inp ?i13 = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|J| <o |UNIV|

goal (1 subgoal):
 1. |\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using var_regular_INNER
[PROOF STATE]
proof (prove)
using this:
|{x. \<exists>X. inp ?i13 = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|J| <o |UNIV|
regular |UNIV|

goal (1 subgoal):
 1. |\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by (simp add: regular_UNION)
[PROOF STATE]
proof (state)
this:
|\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
|\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
obtain Ja where Ja_def: "Ja = {i. \<exists> A. binp i = Some A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ja. Ja = {i. \<exists>A. binp i = Some A} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ja = {i. \<exists>A. binp i = Some A}

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
let ?Sa = "\<Union> i \<in> Ja. {x. \<exists> A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}"
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
{
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
fix i
[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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
obtain K where K_def: "K = {A. binp i = Some A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. K = {A. binp i = Some A} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
K = {A. binp i = Some A}

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "finite K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite K
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {A. binp i = Some A}
[PROOF STEP]
by (cases "binp i", auto)
[PROOF STATE]
proof (state)
this:
finite K

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
hence "|K| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
finite K

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
using var_infinite_INNER finite_ordLess_infinite2
[PROOF STATE]
proof (prove)
using this:
finite K
infinite UNIV
\<lbrakk>finite ?A; infinite ?B\<rbrakk> \<Longrightarrow> |?A| <o |?B|

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "\<forall> A \<in> K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>{A. binp i = Some A}. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
using Op
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp
liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp

goal (1 subgoal):
 1. \<forall>A\<in>{A. binp i = Some A}. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> |{x. \<not> qAFresh xs x v}| <o |UNIV|
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> |{x. \<not> qAFreshAbs xs x v}| <o |UNIV|

goal (1 subgoal):
 1. \<forall>A\<in>{A. binp i = Some A}. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|K| <o |UNIV|
\<forall>A\<in>K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
have "|\<Union> A \<in> K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|
\<forall>A\<in>K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|

goal (1 subgoal):
 1. |\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
using var_regular_INNER
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|
\<forall>A\<in>K. |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|
regular |UNIV|

goal (1 subgoal):
 1. |\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
by (simp add: regular_UNION)
[PROOF STATE]
proof (state)
this:
|\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "{x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} =
         (\<Union> A \<in> K. {x. \<not> qAFreshAbs xs x A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} = (\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A})
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} = (\<Union>A\<in>{A. binp i = Some A}. {x. \<not> qAFreshAbs xs x A})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} = (\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A})

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|
{x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} = (\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A})
[PROOF STEP]
have "|{x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A}| <o |UNIV|
{x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A} = (\<Union>A\<in>K. {x. \<not> qAFreshAbs xs x A})

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

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
|{x. \<exists>A. binp ?i13 = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|{x. \<exists>A. binp ?i13 = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "|Ja| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |Ja| <o |UNIV|
[PROOF STEP]
unfolding Ja_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{i. \<exists>A. binp i = Some A}| <o |UNIV|
[PROOF STEP]
using Op
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
liftAll (\<lambda>X. qGood X \<and> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp
liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp

goal (1 subgoal):
 1. |{i. \<exists>A. binp i = Some A}| <o |UNIV|
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
|{i. inp i \<noteq> None}| <o |UNIV|
|{i. binp i \<noteq> None}| <o |UNIV|
\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<and> |{x. \<not> qAFresh xs x v}| <o |UNIV|
\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<and> |{x. \<not> qAFreshAbs xs x v}| <o |UNIV|

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

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|{x. \<exists>A. binp ?i13 = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
|Ja| <o |UNIV|
[PROOF STEP]
have "|?Sa| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|{x. \<exists>A. binp ?i13 = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
|Ja| <o |UNIV|

goal (1 subgoal):
 1. |\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
using var_regular_INNER
[PROOF STATE]
proof (prove)
using this:
|{x. \<exists>A. binp ?i13 = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
|Ja| <o |UNIV|
regular |UNIV|

goal (1 subgoal):
 1. |\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
by (simp add: regular_UNION)
[PROOF STATE]
proof (state)
this:
|\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
|\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
have "|?S Un ?Sa| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|

goal (1 subgoal):
 1. |(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|
[PROOF STEP]
using var_infinite_INNER card_of_Un_ordLess_infinite
[PROOF STATE]
proof (prove)
using this:
|\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}| <o |UNIV|
|\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A}| <o |UNIV|
infinite UNIV
\<lbrakk>infinite ?C; |?A| <o |?C|; |?B| <o |?C|\<rbrakk> \<Longrightarrow> |?A \<union> ?B| <o |?C|

goal (1 subgoal):
 1. |(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "?Left = ?S Un ?Sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. \<not> qAFresh xs x (qOp delta inp binp)} = (\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})
[PROOF STEP]
by (auto simp: J_def Ja_def liftAll_def )
[PROOF STATE]
proof (state)
this:
{x. \<not> qAFresh xs x (qOp delta inp binp)} = (\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})

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> |{x. \<not> qAFresh xs x X}| <o |UNIV|) inp; liftAll (\<lambda>A. qGoodAbs A \<and> |{x. \<not> qAFreshAbs xs x A}| <o |UNIV|) binp\<rbrakk> \<Longrightarrow> |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
 2. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|
{x. \<not> qAFresh xs x (qOp delta inp binp)} = (\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
|(\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})| <o |UNIV|
{x. \<not> qAFresh xs x (qOp delta inp binp)} = (\<Union>i\<in>J. {x. \<exists>X. inp i = Some X \<and> \<not> qAFresh xs x X}) \<union> (\<Union>i\<in>Ja. {x. \<exists>A. binp i = Some A \<and> \<not> qAFreshAbs xs x A})

goal (1 subgoal):
 1. |{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{x. \<not> qAFresh xs x (qOp delta inp binp)}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
case (Abs xsa x X)
[PROOF STATE]
proof (state)
this:
qGood X
|{x. \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
let ?Left = "{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "|{x}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{x}| <o |UNIV|
[PROOF STEP]
by (auto simp add: var_infinite_INNER)
[PROOF STATE]
proof (state)
this:
|{x}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
hence "|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|{x}| <o |UNIV|

goal (1 subgoal):
 1. |{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using Abs var_infinite_INNER card_of_Un_ordLess_infinite
[PROOF STATE]
proof (prove)
using this:
|{x}| <o |UNIV|
qGood X
|{x. \<not> qAFresh xs x X}| <o |UNIV|
infinite UNIV
\<lbrakk>infinite ?C; |?A| <o |?C|; |?B| <o |?C|\<rbrakk> \<Longrightarrow> |?A \<union> ?B| <o |?C|

goal (1 subgoal):
 1. |{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
have "?Left \<subseteq> {x} \<union> {x. \<not> qAFresh xs x X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X} \<subseteq> {x} \<union> {x. \<not> qAFresh xs x X}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X} \<subseteq> {x} \<union> {x. \<not> qAFresh xs x X}

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
hence "|?Left| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|"
[PROOF STATE]
proof (prove)
using this:
{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X} \<subseteq> {x} \<union> {x. \<not> qAFresh xs x X}

goal (1 subgoal):
 1. |{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|
[PROOF STEP]
using card_of_mono1
[PROOF STATE]
proof (prove)
using this:
{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X} \<subseteq> {x} \<union> {x. \<not> qAFresh xs x X}
?A \<subseteq> ?B \<Longrightarrow> |?A| \<le>o |?B|

goal (1 subgoal):
 1. |{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
|{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|

goal (1 subgoal):
 1. \<And>xsa x X. \<lbrakk>qGood X; |{x. \<not> qAFresh xs x X}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|
|{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|
|{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|

goal (1 subgoal):
 1. |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
using ordLeq_ordLess_trans
[PROOF STATE]
proof (prove)
using this:
|{x} \<union> {x. \<not> qAFresh xs x X}| <o |UNIV|
|{xa. xs = xsa \<and> xa = x \<or> \<not> qAFresh xs xa X}| \<le>o |{x} \<union> {x. \<not> qAFresh xs x X}|
\<lbrakk>?r \<le>o ?r'; ?r' <o ?r''\<rbrakk> \<Longrightarrow> ?r <o ?r''

goal (1 subgoal):
 1. |{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|{xa. \<not> qAFreshAbs xs xa (qAbs xsa x X)}| <o |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma single_non_qFresh_ordLess_var:
assumes "qGood X"
shows "|{x. \<not> qFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{x. \<not> qFresh xs x X}| <o |UNIV|
[PROOF STEP]
using qAFresh_imp_qFresh card_of_mono1 single_non_qAFresh_ordLess_var
ordLeq_ordLess_trans
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x ?X \<Longrightarrow> qFresh ?xs ?x ?X
?A \<subseteq> ?B \<Longrightarrow> |?A| \<le>o |?B|
qGood ?X \<Longrightarrow> |{x. \<not> qAFresh ?xs x ?X}| <o |UNIV|
\<lbrakk>?r \<le>o ?r'; ?r' <o ?r''\<rbrakk> \<Longrightarrow> ?r <o ?r''

goal (1 subgoal):
 1. |{x. \<not> qFresh xs x X}| <o |UNIV|
[PROOF STEP]
by (metis Collect_mono assms)


[STATEMENT]
lemma single_non_qFreshAbs_ordLess_var:
assumes "qGoodAbs A"
shows "|{x. \<not> qFreshAbs xs x A}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{x. \<not> qFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
using qAFreshAll_imp_qFreshAll card_of_mono1 single_non_qAFreshAbs_ordLess_var
ordLeq_ordLess_trans
[PROOF STATE]
proof (prove)
using this:
(qAFresh ?xs ?x ?X \<longrightarrow> qFresh ?xs ?x ?X) \<and> (qAFreshAbs ?xs ?x ?A \<longrightarrow> qFreshAbs ?xs ?x ?A)
?A \<subseteq> ?B \<Longrightarrow> |?A| \<le>o |?B|
qGoodAbs ?A \<Longrightarrow> |{x. \<not> qAFreshAbs ?xs x ?A}| <o |UNIV|
\<lbrakk>?r \<le>o ?r'; ?r' <o ?r''\<rbrakk> \<Longrightarrow> ?r <o ?r''

goal (1 subgoal):
 1. |{x. \<not> qFreshAbs xs x A}| <o |UNIV|
[PROOF STEP]
by (metis Collect_mono assms)


[STATEMENT]
lemma non_qAFresh_ordLess_var:
assumes GOOD: "\<forall> X \<in> XS. qGood X" and Var: "|XS| <o |UNIV :: 'var set|"
shows "|{x| x X. X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
define K and F where "K \<equiv> {x| x X. X \<in> XS \<and> \<not> qAFresh xs x X}"
  and "F \<equiv> (\<lambda> X. {x. X \<in> XS \<and> \<not> qAFresh xs x X})"
[PROOF STATE]
proof (state)
this:
K \<equiv> {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}
F \<equiv> \<lambda>X. {x. X \<in> XS \<and> \<not> qAFresh xs x X}

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
have "K = (\<Union> X \<in> XS. F X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K = \<Union> (F ` XS)
[PROOF STEP]
unfolding K_def F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X} = (\<Union>X\<in>XS. {x. X \<in> XS \<and> \<not> qAFresh xs x X})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K = \<Union> (F ` XS)

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K = \<Union> (F ` XS)

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
have "\<forall> X \<in> XS. |F X| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>XS. |F X| <o |UNIV|
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>XS. |{x. X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
using GOOD single_non_qAFresh_ordLess_var
[PROOF STATE]
proof (prove)
using this:
Ball XS qGood
qGood ?X \<Longrightarrow> |{x. \<not> qAFresh ?xs x ?X}| <o |UNIV|

goal (1 subgoal):
 1. \<forall>X\<in>XS. |{x. X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>XS. |F X| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
K = \<Union> (F ` XS)
\<forall>X\<in>XS. |F X| <o |UNIV|
[PROOF STEP]
have "|K| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
K = \<Union> (F ` XS)
\<forall>X\<in>XS. |F X| <o |UNIV|

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
using var_regular_INNER Var
[PROOF STATE]
proof (prove)
using this:
K = \<Union> (F ` XS)
\<forall>X\<in>XS. |F X| <o |UNIV|
regular |UNIV|
|XS| <o |UNIV|

goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
by(auto simp add: regular_UNION)
[PROOF STATE]
proof (state)
this:
|K| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
using this:
|{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
|{uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}| <o |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_set_qFresh_card_of:
assumes  "|V| <o |UNIV :: 'var set|" and "|XS| <o |UNIV :: 'var set|" and "\<forall> X \<in> XS. qGood X"
shows "\<exists> W. infinite W \<and> W Int V = {} \<and>
             (\<forall> x \<in> W. \<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
define J where "J \<equiv> {x| x X. (x \<in> V \<or> (X \<in> XS \<and> \<not> qAFresh xs x X))}"
[PROOF STATE]
proof (state)
this:
J \<equiv> {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
let ?W = "UNIV - J"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
have "|J| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
unfolding J_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
using assms non_qAFresh_or_in_ordLess_var
[PROOF STATE]
proof (prove)
using this:
|V| <o |UNIV|
|XS| <o |UNIV|
Ball XS qGood
\<lbrakk>|?V| <o |UNIV|; |?XS| <o |UNIV|; Ball ?XS qGood\<rbrakk> \<Longrightarrow> |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> ?V \<or> X \<in> ?XS \<and> \<not> qAFresh ?xs x X)}| <o |UNIV|

goal (1 subgoal):
 1. |{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|J| <o |UNIV|

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
hence  "infinite ?W"
[PROOF STATE]
proof (prove)
using this:
|J| <o |UNIV|

goal (1 subgoal):
 1. infinite (UNIV - J)
[PROOF STEP]
using var_infinite_INNER subset_ordLeq_diff_infinite[of _ J]
[PROOF STATE]
proof (prove)
using this:
|J| <o |UNIV|
infinite UNIV
\<lbrakk>infinite ?B; J \<subseteq> ?B; |J| <o |?B|\<rbrakk> \<Longrightarrow> infinite (?B - J)

goal (1 subgoal):
 1. infinite (UNIV - J)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite (UNIV - J)

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
infinite (UNIV - J)

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
have "?W \<inter> V = {} \<and> (\<forall> x \<in> ?W. \<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (UNIV - J) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - J. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
unfolding J_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (UNIV - {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
using qAFresh_imp_qFresh
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x ?X \<Longrightarrow> qFresh ?xs ?x ?X

goal (1 subgoal):
 1. (UNIV - {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - {uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(UNIV - J) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - J. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
infinite (UNIV - J)
(UNIV - J) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - J. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite (UNIV - J)
(UNIV - J) \<inter> V = {} \<and> (\<forall>x\<in>UNIV - J. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_set_qFresh:
assumes "finite V \<or> |V| <o |UNIV :: 'var set|" and "finite XS \<or> |XS| <o |UNIV :: 'var set|" and
        "\<forall> X \<in> XS. qGood X"
shows "\<exists> W. infinite W \<and> W Int V = {} \<and>
            (\<forall> x \<in> W. \<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V \<or> |V| <o |UNIV|
finite XS \<or> |XS| <o |UNIV|
Ball XS qGood

goal (1 subgoal):
 1. \<exists>W. infinite W \<and> W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
by(fastforce simp add: var_infinite_INNER obtain_set_qFresh_card_of)


[STATEMENT]
lemma obtain_qFresh_card_of:
assumes "|V| <o |UNIV :: 'var set|" and "|XS| <o |UNIV :: 'var set|" and "\<forall> X \<in> XS. qGood X"
shows "\<exists> x. x \<notin> V \<and> (\<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
obtain W where "infinite W" and
  *: "W \<inter> V = {} \<and> (\<forall> x \<in> W. \<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>infinite W; W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms obtain_set_qFresh_card_of
[PROOF STATE]
proof (prove)
using this:
|V| <o |UNIV|
|XS| <o |UNIV|
Ball XS qGood
\<lbrakk>|?V| <o |UNIV|; |?XS| <o |UNIV|; Ball ?XS qGood\<rbrakk> \<Longrightarrow> \<exists>W. infinite W \<and> W \<inter> ?V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>?XS. qAFresh ?xs x X \<and> qFresh ?xs x X)

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>infinite W; W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite W
W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite W
W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
obtain x where "x \<in> W"
[PROOF STATE]
proof (prove)
using this:
infinite W
W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal (1 subgoal):
 1. (\<And>x. x \<in> W \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infinite_imp_nonempty
[PROOF STATE]
proof (prove)
using this:
infinite W
W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
infinite ?S \<Longrightarrow> ?S \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> W \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> W

goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> W

goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
x \<in> W
W \<inter> V = {} \<and> (\<forall>x\<in>W. \<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_qFresh:
assumes "finite V \<or> |V| <o |UNIV :: 'var set|" and "finite XS \<or> |XS| <o |UNIV :: 'var set|" and
        "\<forall> X \<in> XS. qGood X"
shows "\<exists> x. x \<notin> V \<and> (\<forall> X \<in> XS. qAFresh xs x X \<and> qFresh xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V \<or> |V| <o |UNIV|
finite XS \<or> |XS| <o |UNIV|
Ball XS qGood

goal (1 subgoal):
 1. \<exists>x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)
[PROOF STEP]
by(fastforce simp add: var_infinite_INNER obtain_qFresh_card_of)


[STATEMENT]
lemma pickQFresh_card_of:
assumes "|V| <o |UNIV :: 'var set|" and "|XS| <o |UNIV :: 'var set|" and "\<forall> X \<in> XS. qGood X"
shows "pickQFresh xs V XS \<notin> V \<and>
       (\<forall> X \<in> XS. qAFresh xs (pickQFresh xs V XS) X \<and> qFresh xs (pickQFresh xs V XS) X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pickQFresh xs V XS \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs (pickQFresh xs V XS) X \<and> qFresh xs (pickQFresh xs V XS) X)
[PROOF STEP]
unfolding pickQFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) X \<and> qFresh xs (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) X)
[PROOF STEP]
apply(rule someI_ex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X. X \<notin> V \<and> (\<forall>Xa\<in>XS. qAFresh xs X Xa \<and> qFresh xs X Xa)
[PROOF STEP]
using assms obtain_qFresh_card_of
[PROOF STATE]
proof (prove)
using this:
|V| <o |UNIV|
|XS| <o |UNIV|
Ball XS qGood
\<lbrakk>|?V| <o |UNIV|; |?XS| <o |UNIV|; Ball ?XS qGood\<rbrakk> \<Longrightarrow> \<exists>x. x \<notin> ?V \<and> (\<forall>X\<in>?XS. qAFresh ?xs x X \<and> qFresh ?xs x X)

goal (1 subgoal):
 1. \<exists>X. X \<notin> V \<and> (\<forall>Xa\<in>XS. qAFresh xs X Xa \<and> qFresh xs X Xa)
[PROOF STEP]
by blast


[STATEMENT]
lemma pickQFresh:
assumes "finite V \<or> |V| <o |UNIV :: 'var set|" and "finite XS \<or> |XS| <o |UNIV :: 'var set|" and
        "\<forall> X \<in> XS. qGood X"
shows "pickQFresh xs V XS \<notin> V \<and>
       (\<forall> X \<in> XS. qAFresh xs (pickQFresh xs V XS) X \<and> qFresh xs (pickQFresh xs V XS) X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pickQFresh xs V XS \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs (pickQFresh xs V XS) X \<and> qFresh xs (pickQFresh xs V XS) X)
[PROOF STEP]
unfolding pickQFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) X \<and> qFresh xs (SOME x. x \<notin> V \<and> (\<forall>X\<in>XS. qAFresh xs x X \<and> qFresh xs x X)) X)
[PROOF STEP]
apply(rule someI_ex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X. X \<notin> V \<and> (\<forall>Xa\<in>XS. qAFresh xs X Xa \<and> qFresh xs X Xa)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V \<or> |V| <o |UNIV|
finite XS \<or> |XS| <o |UNIV|
Ball XS qGood

goal (1 subgoal):
 1. \<exists>X. X \<notin> V \<and> (\<forall>Xa\<in>XS. qAFresh xs X Xa \<and> qFresh xs X Xa)
[PROOF STEP]
by(auto simp add: obtain_qFresh)


[STATEMENT]
lemma aux_alpha_ignoreSecond_qTermLessQSwapped_wf:
"wf(inv_image qTermQSwappedLess aux_alpha_ignoreSecond)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image qTermQSwappedLess aux_alpha_ignoreSecond)
[PROOF STEP]
using qTermQSwappedLess_wf wf_inv_image
[PROOF STATE]
proof (prove)
using this:
wf qTermQSwappedLess
wf ?r \<Longrightarrow> wf (inv_image ?r ?f)

goal (1 subgoal):
 1. wf (inv_image qTermQSwappedLess aux_alpha_ignoreSecond)
[PROOF STEP]
by auto


[STATEMENT]
lemma alpha_inp_None:
"qOp delta inp binp #= qOp delta' inp' binp' \<Longrightarrow>
 (inp i = None) = (inp' i = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qOp delta inp binp #= qOp delta' inp' binp' \<Longrightarrow> (inp i = None) = (inp' i = None)
[PROOF STEP]
by(auto simp add: sameDom_def)


[STATEMENT]
lemma alpha_binp_None:
"qOp delta inp binp #= qOp delta' inp' binp' \<Longrightarrow>
 (binp i = None) = (binp' i = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qOp delta inp binp #= qOp delta' inp' binp' \<Longrightarrow> (binp i = None) = (binp' i = None)
[PROOF STEP]
by(auto simp add: sameDom_def)


[STATEMENT]
lemma qVar_alpha_iff:
"qVar xs x #= X' \<longleftrightarrow> X' = qVar xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qVar xs x #= X') = (X' = qVar xs x)
[PROOF STEP]
by(cases X', auto)


[STATEMENT]
lemma alpha_qVar_iff:
"X #= qVar xs' x' \<longleftrightarrow> X = qVar xs' x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X #= qVar xs' x') = (X = qVar xs' x')
[PROOF STEP]
by(cases X, auto)


[STATEMENT]
lemma qOp_alpha_iff:
"qOp delta inp binp #= X' \<longleftrightarrow>
 (\<exists> inp' binp'.
    X' = qOp delta inp' binp' \<and> sameDom inp inp' \<and> sameDom binp binp' \<and>
    liftAll2 (\<lambda>Y Y'. Y #= Y') inp inp' \<and>
    liftAll2 (\<lambda>A A'. A $= A') binp binp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qOp delta inp binp #= X') = (\<exists>inp' binp'. X' = qOp delta inp' binp' \<and> sameDom inp inp' \<and> sameDom binp binp' \<and> liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp')
[PROOF STEP]
by(cases X') auto


[STATEMENT]
lemma alpha_qOp_iff:
"X #= qOp delta' inp' binp' \<longleftrightarrow>
 (\<exists> inp binp. X = qOp delta' inp binp \<and> sameDom inp inp' \<and> sameDom binp binp' \<and>
    liftAll2 (\<lambda>Y Y'. Y #= Y') inp inp' \<and>
    liftAll2 (\<lambda>A A'. A $= A') binp binp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X #= qOp delta' inp' binp') = (\<exists>inp binp. X = qOp delta' inp binp \<and> sameDom inp inp' \<and> sameDom binp binp' \<and> liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp')
[PROOF STEP]
by(cases X) auto


[STATEMENT]
lemma qAbs_alphaAbs_iff:
"qAbs xs x X $= A' \<longleftrightarrow>
 (\<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))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= A') = (\<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)
[PROOF STEP]
by(cases A') auto


[STATEMENT]
lemma alphaAbs_qAbs_iff:
"A $= qAbs xs' x' X' \<longleftrightarrow>
 (\<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'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A $= qAbs xs' x' 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')
[PROOF STEP]
by(cases A) auto


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

goal (3 subgoals):
 1. \<And>xs x. \<forall>X'. qVar xs x #= X' \<longrightarrow> qSkel (qVar xs x) = qSkel X'
 2. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
 3. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. qVar xs x #= X' \<longrightarrow> qSkel (qVar xs x) = qSkel X'
[PROOF STEP]
unfolding qVar_alpha_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. X' = qVar xs x \<longrightarrow> qSkel (qVar xs x) = qSkel X'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>X'. qVar xs x #= X' \<longrightarrow> qSkel (qVar xs x) = qSkel X'

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
case (Op delta inp binp)
[PROOF STATE]
proof (state)
this:
liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp
liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp

goal (2 subgoals):
 1. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp; liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp\<rbrakk> \<Longrightarrow> \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
 2. \<And>xs x X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'; \<And>Y. qSkel Y = qSkel X \<Longrightarrow> \<forall>X'. Y #= X' \<longrightarrow> qSkel Y = qSkel X'\<rbrakk> \<Longrightarrow> \<forall>A'. qAbs xs x X $= A' \<longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X'. qOp delta inp binp #= X' \<longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
[PROOF STEP]
fix X'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
[PROOF STEP]
assume "qOp delta inp binp #= X'"
[PROOF STATE]
proof (state)
this:
qOp delta inp binp #= X'

goal (1 subgoal):
 1. \<And>X'. qOp delta inp binp #= X' \<Longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
[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'. qOp delta inp binp #= X' \<Longrightarrow> qSkel (qOp delta inp binp) = qSkel X'
[PROOF STEP]
from Op.IH 1 2
[PROOF STATE]
proof (chain)
picking this:
liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp
liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'
[PROOF STEP]
show "qSkel (qOp delta inp binp) = qSkel X'"
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>a. \<forall>X'. a #= X' \<longrightarrow> qSkel a = qSkel X') inp
liftAll (\<lambda>a. \<forall>A'. a $= A' \<longrightarrow> qSkelAbs a = qSkelAbs A') binp
sameDom inp inp' \<and> sameDom binp binp'
liftAll2 (#=) inp inp' \<and> liftAll2 ($=) binp binp'

goal (1 subgoal):
 1. qSkel (qOp delta inp binp) = qSkel X'
[PROOF STEP]
by (simp add: X'eq fun_eq_iff option.case_eq_if
        lift_def liftAll_def sameDom_def liftAll2_def)
[PROOF STATE]
proof (state)
this:
qSkel (qOp delta inp binp) = qSkel X'

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

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

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

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= A'
[PROOF STEP]
obtain X' x' y where A'eq: "A' = qAbs xs x' X'" and
    *: "(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'; 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'; 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>A'. qAbs xs x X $= A' \<Longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
moreover
[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>A'. qAbs xs x X $= A' \<Longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[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]
using qSwap_qSwapped
[PROOF STATE]
proof (prove)
using this:
(?X, ?X #[[?x \<and> ?y]]_?zs) \<in> qSwapped

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>A'. qAbs xs x X $= A' \<Longrightarrow> qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
thus "qSkelAbs (qAbs xs x X) = qSkelAbs A'"
[PROOF STATE]
proof (prove)
using this:
qSkel X = qSkel X'

goal (1 subgoal):
 1. qSkelAbs (qAbs xs x X) = qSkelAbs A'
[PROOF STEP]
unfolding A'eq
[PROOF STATE]
proof (prove)
using this:
qSkel X = qSkel X'

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

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

goal:
No subgoals!
[PROOF STEP]
qed