[STATEMENT]
lemma Red_F_subs_Red_F_diff_Red_F: "Red_F N \<subseteq> Red_F (N - Red_F N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Red_F N \<subseteq> Red_F (N - Red_F N)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
assume c_rf: "C \<in> Red_F N"
[PROOF STATE]
proof (state)
this:
C \<in> Red_F N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Red_F N
[PROOF STEP]
obtain CC :: "'f set" where
    cc_subs: "CC \<subseteq> N - Red_F N" and
    cc_fin: "finite CC" and
    cc_ent_c: "CC \<Turnstile> {C}" and
    cc_lt_c: "\<forall>C' \<in> CC. C' \<prec> C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Red_F N

goal (1 subgoal):
 1. (\<And>CC. \<lbrakk>CC \<subseteq> N - Red_F N; finite CC; CC \<Turnstile> {C}; \<forall>C'\<in>CC. C' \<prec> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Red_F_imp_ex_non_Red_F[of C N]
[PROOF STATE]
proof (prove)
using this:
C \<in> Red_F N
C \<in> Red_F N \<Longrightarrow> \<exists>CC\<subseteq>N - Red_F N. finite CC \<and> CC \<Turnstile> {C} \<and> (\<forall>C'\<in>CC. C' \<prec> C)

goal (1 subgoal):
 1. (\<And>CC. \<lbrakk>CC \<subseteq> N - Red_F N; finite CC; CC \<Turnstile> {C}; \<forall>C'\<in>CC. C' \<prec> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N - Red_F N
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
have "\<forall>D \<in> CC. D \<notin> Red_F N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
using cc_subs
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - Red_F N

goal (1 subgoal):
 1. \<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>D\<in>CC. D \<notin> Red_F N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
have cc_nr:
    "\<forall>C \<in> CC. \<forall>DD \<subseteq> N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D \<in> DD. \<not> D \<prec> C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>CC. D \<notin> Red_F N

goal (1 subgoal):
 1. \<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)
[PROOF STEP]
unfolding Red_F_def
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>CC. D \<notin> {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. \<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
have "CC \<subseteq> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CC \<subseteq> N
[PROOF STEP]
using cc_subs
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - Red_F N

goal (1 subgoal):
 1. CC \<subseteq> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CC \<subseteq> N
[PROOF STEP]
have "CC \<subseteq> N - {C. \<exists>DD \<subseteq> N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D \<in> DD. D \<prec> C)}"
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N

goal (1 subgoal):
 1. CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
using cc_nr
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N
\<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)

goal (1 subgoal):
 1. CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
show "C \<in> Red_F (N - Red_F N)"
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. C \<in> Red_F (N - Red_F N)
[PROOF STEP]
using cc_fin cc_ent_c cc_lt_c
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. C \<in> Red_F (N - Red_F N)
[PROOF STEP]
unfolding Red_F_def
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. C \<in> {C. \<exists>DD\<subseteq>N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<in> Red_F (N - Red_F N)

goal:
No subgoals!
[PROOF STEP]
qed