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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Middle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_qAFresh_def alphaAbs_ex_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle = ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' = (qAbs xs x X $= qAbs xs' x' X')
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qAFresh[of X]
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X \<Longrightarrow> (qAbs ?xs ?x X $= qAbs ?xs' ?x' ?X') = alphaAbs_ex_equal_or_qAFresh ?xs ?x X ?xs' ?x' ?X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qAFresh:
assumes "qGood X" and "qAbs xs x X $= qAbs xs' x' X'"
shows "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qAFresh
      alphaAbs_weakestEx_imp_strongestAll
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'
qGood ?X \<Longrightarrow> (qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X') = alphaAbs_ex_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'
\<lbrakk>qGood ?X; alphaAbs_ex_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_all_equal_or_qAFresh:
assumes "qGood X" and "qGood X'"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleEx = "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleAll = "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?MiddleAll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qAFresh_def alphaAbs_all_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?MiddleAll \<Longrightarrow> ?MiddleEx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_weakestAll_imp_strongestEx
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qGood ?X'; alphaAbs_all_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_ex_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?MiddleEx \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using alphaAbs_qAbs_iff_alphaAbs_ex_distinct_qAFresh[of _ _ X]
[PROOF STATE]
proof (prove)
using this:
(qAbs ?xs ?x X $= qAbs ?xs' ?x' ?X') = alphaAbs_ex_distinct_qAFresh ?xs ?x X ?xs' ?x' ?X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_imp_alphaAbs_all_qAFresh:
assumes "qGood X" and "qAbs xs x X $= qAbs xs' x' X'"
shows "alphaAbs_all_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_qAFresh_def alphaAbs_all_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
xs = xs' \<and> (\<forall>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_all_qAFresh:
assumes "qGood X" and "qGood X'"
shows "(qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleEx = "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleAll = "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?MiddleAll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_qAFresh_def alphaAbs_all_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?MiddleAll \<Longrightarrow> ?MiddleEx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_weakestAll_imp_strongestEx
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qGood ?X'; alphaAbs_all_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_ex_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_imp_alphaAbs_all_distinct_qAFresh:
assumes "qGood X" and "qAbs xs x X $= qAbs xs' x' X'"
shows "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'

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

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

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_all_distinct_qAFresh:
assumes "qGood X" and "qGood X'"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleEx = "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?MiddleAll = "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_distinct_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?MiddleAll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_distinct_qAFresh_def alphaAbs_all_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
have "?MiddleAll \<Longrightarrow> ?MiddleEx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_weakestAll_imp_strongestEx
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qGood ?X'; alphaAbs_all_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_ex_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_all_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_ex_equal_or_qAFresh_imp_qFresh:
"alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_equal_or_qAFresh_def alphaAbs_ex_equal_or_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
using qAFresh_imp_qFresh[of _ _ X] qAFresh_imp_qFresh[of _ _ X']
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x X \<Longrightarrow> qFresh ?xs ?x X
qAFresh ?xs ?x X' \<Longrightarrow> qFresh ?xs ?x X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma alphaAbs_ex_distinct_qAFresh_imp_qFresh:
"alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_ex_distinct_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_distinct_qAFresh_def alphaAbs_ex_distinct_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
using qAFresh_imp_qFresh[of _ _ X] qAFresh_imp_qFresh[of _ _ X']
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x X \<Longrightarrow> qFresh ?xs ?x X
qAFresh ?xs ?x X' \<Longrightarrow> qFresh ?xs ?x X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma alphaAbs_ex_qAFresh_imp_qFresh:
"alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_ex_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_qAFresh_def alphaAbs_ex_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
using qAFresh_imp_qFresh[of _ _ X] qAFresh_imp_qFresh[of _ _ X']
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x X \<Longrightarrow> qFresh ?xs ?x X
qAFresh ?xs ?x X' \<Longrightarrow> qFresh ?xs ?x X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma alphaAbs_all_equal_or_qFresh_imp_qAFresh:
"alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qAFresh_def alphaAbs_all_equal_or_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
using qAFresh_imp_qFresh[of _ _ X] qAFresh_imp_qFresh[of _ _ X']
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x X \<Longrightarrow> qFresh ?xs ?x X
qAFresh ?xs ?x X' \<Longrightarrow> qFresh ?xs ?x X'

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. (y = x \<or> qAFresh xs y X) \<and> (y = x' \<or> qAFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma alphaAbs_all_distinct_qFresh_imp_qAFresh:
"alphaAbs_all_distinct_qFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_all_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_distinct_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X 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. alphaAbs_all_distinct_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_distinct_qAFresh_def alphaAbs_all_distinct_qFresh_def
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x ?X \<Longrightarrow> qFresh ?xs ?x ?X

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qFresh xs y X \<and> qFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma alphaAbs_all_qFresh_imp_qAFresh:
"alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow>
 alphaAbs_all_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X 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. alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_qAFresh_def alphaAbs_all_qFresh_def
[PROOF STATE]
proof (prove)
using this:
qAFresh ?xs ?x ?X \<Longrightarrow> qFresh ?xs ?x ?X

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. qFresh xs y X \<and> qFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. qAFresh xs y X \<and> qAFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by fastforce


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

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
have "\<exists> Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
proof(cases "y = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
 2. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
assume Case1: "y = x"
[PROOF STATE]
proof (state)
this:
y = x

goal (2 subgoals):
 1. y = x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
 2. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
hence "X #= X"
[PROOF STATE]
proof (prove)
using this:
y = x

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qFresh xs y X
[PROOF STEP]
obtain Y where "X #= Y" and "qAFresh xs y Y"
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>X #= Y; qAFresh xs y Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GOOD qFresh_imp_ex_qAFresh1
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X
qGood X
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?zs ?z X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
obtain Y where alphaXY: "X #= Y" and yEqAFresh: "y = x \<or> qAFresh xs y Y"
[PROOF STATE]
proof (prove)
using this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

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

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

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= Y #[[y \<and> x]]_xs
[PROOF STEP]
using GOOD qSwap_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
X #= Y
y = x \<or> qAFresh xs y Y
qGood X
\<lbrakk>qGood ?X \<or> qGood ?X'; ?X #= ?X'\<rbrakk> \<Longrightarrow> ?X #[[?z1.0 \<and> ?z2.0]]_?zs #= ?X' #[[?z1.0 \<and> ?z2.0]]_?zs

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
have "\<exists> Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
proof(cases "y = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
 2. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
assume Case1: "y = x'"
[PROOF STATE]
proof (state)
this:
y = x'

goal (2 subgoals):
 1. y = x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
 2. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
hence "X' #= X'"
[PROOF STATE]
proof (prove)
using this:
y = x'

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qFresh xs y X'
[PROOF STEP]
obtain Y' where "X' #= Y'" and "qAFresh xs y Y'"
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X'

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>X' #= Y'; qAFresh xs y Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using good' qFresh_imp_ex_qAFresh1
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X'
qGood X'
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?zs ?z X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
obtain Y' where alphaX'Y': "X' #= Y'" and
                       yEqAFresh': "y = x' \<or> qAFresh xs y Y'"
[PROOF STATE]
proof (prove)
using this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qAFresh xs x Y xs x' Y'
[PROOF STEP]
unfolding alphaAbs_ex_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs

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

goal (1 subgoal):
 1. xs = xs \<and> (\<exists>y. (y = x \<or> qAFresh xs y Y) \<and> (y = x' \<or> qAFresh xs y Y') \<and> Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_equal_or_qAFresh xs x Y xs x' Y'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
hence "qAbs xs x Y $= qAbs xs x' Y'"
[PROOF STATE]
proof (prove)
using this:
alphaAbs_ex_equal_or_qAFresh xs x Y xs x' Y'

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x' Y'
[PROOF STEP]
using goodY alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qAFresh[of Y xs x xs]
[PROOF STATE]
proof (prove)
using this:
alphaAbs_ex_equal_or_qAFresh xs x Y xs x' Y'
qGood Y
qGood Y \<Longrightarrow> (qAbs xs x Y $= qAbs xs ?x' ?X') = alphaAbs_ex_equal_or_qAFresh xs x Y xs ?x' ?X'

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

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

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

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

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
have 1: "Y' #= X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y' #= X'
[PROOF STEP]
using alphaX'Y' alpha_sym
[PROOF STATE]
proof (prove)
using this:
X' #= Y'
?X #= ?X' \<Longrightarrow> ?X' #= ?X

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

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

goal (1 subgoal):
 1. qGood Y'
[PROOF STEP]
using good' alpha_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
Y' #= X'
qGood X'
?X #= ?X' \<Longrightarrow> qGood ?X = qGood ?X'

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
hence "qAbs xs x' Y' $= qAbs xs x' X'"
[PROOF STATE]
proof (prove)
using this:
qGood Y'

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

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

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

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
have "qGoodAbs(qAbs xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
using GOOD
[PROOF STATE]
proof (prove)
using this:
qGood X

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

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x Y $= qAbs xs x' Y'
qAbs xs x X $= qAbs xs x Y
qAbs xs x' Y' $= qAbs xs x' X'
qGoodAbs (qAbs xs x X)
[PROOF STEP]
have "qAbs xs x X $= qAbs xs x' X'"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x' Y'
qAbs xs x X $= qAbs xs x Y
qAbs xs x' Y' $= qAbs xs x' X'
qGoodAbs (qAbs xs x X)

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qFresh:
assumes GOOD: "qGood X"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle = "alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_ex_equal_or_qFresh_imp_alphaAbs_qAbs
[PROOF STATE]
proof (prove)
using this:
qGood X
\<lbrakk>qGood ?X; alphaAbs_ex_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'

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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Middle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_ex_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood ?X \<Longrightarrow> (qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X') = alphaAbs_ex_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
using
  alphaAbs_ex_equal_or_qAFresh_imp_qFresh
[PROOF STATE]
proof (prove)
using this:
alphaAbs_ex_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle1 \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
using alphaAbs_ex_qAFresh_imp_qFresh
[PROOF STATE]
proof (prove)
using this:
alphaAbs_ex_qAFresh ?xs ?x ?X ?xs' ?x' ?X' \<Longrightarrow> alphaAbs_ex_qFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_qFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Middle2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_qFresh_def alphaAbs_ex_equal_or_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle2 \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_ex_equal_or_qFresh_imp_alphaAbs_qAbs
[PROOF STATE]
proof (prove)
using this:
qGood X
\<lbrakk>qGood ?X; alphaAbs_ex_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_ex_distinct_qFresh:
assumes GOOD: "qGood X"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_ex_distinct_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "qAbs xs x X $= qAbs xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle1 = "alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle2 = "alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_ex_distinct_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Middle1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_distinct_qAFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qAFresh xs y X \<and> qAFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qAFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle1 \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
using alphaAbs_ex_distinct_qAFresh_imp_qFresh
[PROOF STATE]
proof (prove)
using this:
alphaAbs_ex_distinct_qAFresh ?xs ?x ?X ?xs' ?x' ?X' \<Longrightarrow> alphaAbs_ex_distinct_qFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_distinct_qAFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_distinct_qFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Middle2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_distinct_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_ex_distinct_qFresh_def alphaAbs_ex_equal_or_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<exists>y. y \<notin> {x, x'} \<and> qFresh xs y X \<and> qFresh xs y X' \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<exists>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<and> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_ex_distinct_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_ex_equal_or_qFresh xs x X xs' x' X'

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

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_ex_distinct_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle2 \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_ex_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_ex_equal_or_qFresh_imp_alphaAbs_qAbs
[PROOF STATE]
proof (prove)
using this:
qGood X
\<lbrakk>qGood ?X; alphaAbs_ex_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed