[STATEMENT]
lemma non_qAFresh_or_in_ordLess_var:
assumes Var: "|V| <o |UNIV :: 'var set|" and "|XS| <o |UNIV :: 'var set|" and "\<forall> X \<in> XS. qGood X"
shows "|{x| x X. (x \<in> V \<or> (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> V \<or> 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> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|
[PROOF STEP]
define J and K where "J \<equiv> {x| x X. (x \<in> V \<or> (X \<in> XS \<and> \<not> qAFresh xs x X))}"  
  and "K \<equiv> {x| x X. 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)}
K \<equiv> {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X}

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]
have "J \<subseteq> K \<union> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> K \<union> V
[PROOF STEP]
unfolding J_def K_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)} \<subseteq> {uu_. \<exists>x X. uu_ = x \<and> X \<in> XS \<and> \<not> qAFresh xs x X} \<union> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
J \<subseteq> K \<union> V

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]
hence "|J| \<le>o |K \<union> V|"
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> K \<union> V

goal (1 subgoal):
 1. |J| \<le>o |K \<union> V|
[PROOF STEP]
using card_of_mono1
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> K \<union> V
?A \<subseteq> ?B \<Longrightarrow> |?A| \<le>o |?B|

goal (1 subgoal):
 1. |J| \<le>o |K \<union> V|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

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]
moreover
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

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]
{
[PROOF STATE]
proof (state)
this:
|J| \<le>o |K \<union> V|

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]
have "|K| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |K| <o |UNIV|
[PROOF STEP]
unfolding K_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}| <o |UNIV|
[PROOF STEP]
using assms non_qAFresh_ordLess_var
[PROOF STATE]
proof (prove)
using this:
|V| <o |UNIV|
|XS| <o |UNIV|
Ball XS qGood
\<lbrakk>Ball ?XS qGood; |?XS| <o |UNIV|\<rbrakk> \<Longrightarrow> |{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]
by auto
[PROOF STATE]
proof (state)
this:
|K| <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]
hence "|K \<union> V| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|K| <o |UNIV|

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

goal (1 subgoal):
 1. |K \<union> V| <o |UNIV|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|K \<union> V| <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]
}
[PROOF STATE]
proof (state)
this:
|K \<union> V| <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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|
[PROOF STEP]
have "|J| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|

goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
using ordLeq_ordLess_trans
[PROOF STATE]
proof (prove)
using this:
|J| \<le>o |K \<union> V|
|K \<union> V| <o |UNIV|
\<lbrakk>?r \<le>o ?r'; ?r' <o ?r''\<rbrakk> \<Longrightarrow> ?r <o ?r''

goal (1 subgoal):
 1. |J| <o |UNIV|
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
|J| <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]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
|J| <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]
unfolding J_def
[PROOF STATE]
proof (prove)
using this:
|{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]
.
[PROOF STATE]
proof (state)
this:
|{uu_. \<exists>x X. uu_ = x \<and> (x \<in> V \<or> X \<in> XS \<and> \<not> qAFresh xs x X)}| <o |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed