[STATEMENT]
theorem finite_alt_consistency:
  assumes altconc: \<open>alt_consistency C\<close>
    and \<open>subset_closed C\<close>
  shows \<open>alt_consistency (mk_finite_char C)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alt_consistency (mk_finite_char C)
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. S \<in> mk_finite_char C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> mk_finite_char C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> mk_finite_char C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C)
[PROOF STEP]
proof (intro allI impI conjI)
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
assume \<open>S \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (state)
this:
S \<in> mk_finite_char C

goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<in> mk_finite_char C
[PROOF STEP]
have finc: \<open>\<forall>S' \<subseteq> S. finite S' \<longrightarrow> S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S \<in> mk_finite_char C

goal (1 subgoal):
 1. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
using this:
S \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}

goal (1 subgoal):
 1. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
have \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
using \<open>subset_closed C\<close>
[PROOF STATE]
proof (prove)
using this:
subset_closed C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
unfolding subset_closed_def
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
have sc: \<open>\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S \<subseteq> S' \<union> x. S \<in> C)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
fix p ts
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>S p ts. S \<in> mk_finite_char C \<Longrightarrow> \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 3. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 4. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 10. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
A total of 14 subgoals...
[PROOF STEP]
show \<open>\<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
assume \<open>Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S

goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S
[PROOF STEP]
have \<open>{Pred p ts, Neg (Pred p ts)} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S

goal (1 subgoal):
 1. {Pred p ts, Neg (Pred p ts)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. {Pred p ts, Neg (Pred p ts)} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{Pred p ts, Neg (Pred p ts)} \<in> C

goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{Pred p ts, Neg (Pred p ts)} \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
{Pred p ts, Neg (Pred p ts)} \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
{Pred p ts, Neg (Pred p ts)} \<in> C
alt_consistency C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
{Pred p ts, Neg (Pred p ts)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. False
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)

goal (13 subgoals):
 1. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 3. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 10. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
A total of 13 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (Pred ?p2 ?ts2 \<in> S \<and> Neg (Pred ?p2 ?ts2) \<in> S)

goal (13 subgoals):
 1. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> FF \<notin> S
 2. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 3. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 9. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 10. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
A total of 13 subgoals...
[PROOF STEP]
show \<open>FF \<notin> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FF \<notin> S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FF \<in> S \<Longrightarrow> False
[PROOF STEP]
assume \<open>FF \<in> S\<close>
[PROOF STATE]
proof (state)
this:
FF \<in> S

goal (1 subgoal):
 1. FF \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FF \<in> S
[PROOF STEP]
have \<open>{FF} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
FF \<in> S

goal (1 subgoal):
 1. {FF} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
FF \<in> S
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. {FF} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{FF} \<in> C

goal (1 subgoal):
 1. FF \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{FF} \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
{FF} \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
{FF} \<in> C
alt_consistency C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
{FF} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. False
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
FF \<notin> S

goal (12 subgoals):
 1. \<And>S. S \<in> mk_finite_char C \<Longrightarrow> Neg TT \<notin> S
 2. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 8. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 9. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 10. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
A total of 12 subgoals...
[PROOF STEP]
show \<open>Neg TT \<notin> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg TT \<notin> S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Neg TT \<in> S \<Longrightarrow> False
[PROOF STEP]
assume \<open>Neg TT \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Neg TT \<in> S

goal (1 subgoal):
 1. Neg TT \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg TT \<in> S
[PROOF STEP]
have \<open>{Neg TT} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg TT \<in> S

goal (1 subgoal):
 1. {Neg TT} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
Neg TT \<in> S
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. {Neg TT} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{Neg TT} \<in> C

goal (1 subgoal):
 1. Neg TT \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{Neg TT} \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
{Neg TT} \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
{Neg TT} \<in> C
alt_consistency C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
{Neg TT} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. False
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Neg TT \<notin> S

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 9. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
A total of 11 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg TT \<notin> S

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 9. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
A total of 11 subgoals...
[PROOF STEP]
fix Z
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 9. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
A total of 11 subgoals...
[PROOF STEP]
assume *: \<open>Neg (Neg Z) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Neg (Neg Z) \<in> S

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> mk_finite_char C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 7. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 9. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
A total of 11 subgoals...
[PROOF STEP]
show \<open>S \<union> {Z} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Z} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Z} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {Z} \<union> {Neg (Neg Z)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {Z}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {Z}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {Z}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Z}
finite S'

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Z}
finite S'
Neg (Neg Z) \<in> S

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {Z} \<union> {Neg (Neg Z)})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {Z} \<union> {Neg (Neg Z)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {Z} \<union> {Neg (Neg Z)})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S
finite (S' - {Z} \<union> {Neg (Neg Z)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S
finite (S' - {Z} \<union> {Neg (Neg Z)})

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<subseteq> S
finite (S' - {Z} \<union> {Neg (Neg Z)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Z} \<union> {Neg (Neg Z)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Z} \<union> {Neg (Neg Z)} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {Z} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<in> C

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<in> C
alt_consistency C

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Z}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {Z} \<union> {Neg (Neg Z)} \<union> {Z} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Z} \<in> mk_finite_char C

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Neg ?Z2) \<in> S \<Longrightarrow> S \<union> {?Z2} \<in> mk_finite_char C

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg (Neg ?Z2) \<in> S \<Longrightarrow> S \<union> {?Z2} \<in> mk_finite_char C

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>And A B \<in> S\<close>
[PROOF STATE]
proof (state)
this:
And A B \<in> S

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 6. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 8. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 10. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {A, B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {A, B} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {A, B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {A, B} \<union> {And A B}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {A, B}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {A, B}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {A, B}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {A, B}
finite S'

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {A, B}
finite S'
And A B \<in> S

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {A, B} \<union> {And A B} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {A, B} \<union> {And A B} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {A, B} \<union> {And A B})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {A, B} \<union> {And A B})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {A, B} \<union> {And A B})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {A, B} \<union> {And A B} \<subseteq> S
finite (S' - {A, B} \<union> {And A B})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<subseteq> S
finite (S' - {A, B} \<union> {And A B})

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<subseteq> S
finite (S' - {A, B} \<union> {And A B})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {A, B} \<union> {And A B} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {A, B} \<union> {And A B} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {A, B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<in> C

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<in> C
alt_consistency C

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {A, B} \<union> {And A B} \<union> {A, B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {A, B} \<in> mk_finite_char C

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
And ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {?A2, ?B2} \<in> mk_finite_char C

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
And ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {?A2, ?B2} \<in> mk_finite_char C

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Neg (Or A B) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Neg (Or A B) \<in> S

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 5. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 7. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 9. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {Neg A, Neg B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg A, Neg B} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg A, Neg B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {Neg A, Neg B} \<union> {Neg (Or A B)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {Neg A, Neg B}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {Neg A, Neg B}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {Neg A, Neg B}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg A, Neg B}
finite S'

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg A, Neg B}
finite S'
Neg (Or A B) \<in> S

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S
finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S
finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<subseteq> S
finite (S' - {Neg A, Neg B} \<union> {Neg (Or A B)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {Neg A, Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C
alt_consistency C

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg A, Neg B} \<union> {Neg (Or A B)} \<union> {Neg A, Neg B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Neg A, Neg B} \<in> mk_finite_char C

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Or ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {Neg ?A2, Neg ?B2} \<in> mk_finite_char C

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg (Or ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {Neg ?A2, Neg ?B2} \<in> mk_finite_char C

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Neg (Impl A B) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Neg (Impl A B) \<in> S

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 6. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 8. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {A, Neg B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {A, Neg B} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {A, Neg B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {A, Neg B} \<union> {Neg (Impl A B)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {A, Neg B}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {A, Neg B}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {A, Neg B}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {A, Neg B}
finite S'

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {A, Neg B}
finite S'
Neg (Impl A B) \<in> S

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S
finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S
finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<subseteq> S
finite (S' - {A, Neg B} \<union> {Neg (Impl A B)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {A, Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C
alt_consistency C

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {A, Neg B}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {A, Neg B} \<union> {Neg (Impl A B)} \<union> {A, Neg B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {A, Neg B} \<in> mk_finite_char C

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Impl ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {?A2, Neg ?B2} \<in> mk_finite_char C

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg (Impl ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {?A2, Neg ?B2} \<in> mk_finite_char C

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Or A B \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Or A B \<in> S

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 3. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 5. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 7. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> ?thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)
[PROOF STEP]
obtain Sa and Sb
        where \<open>Sa \<subseteq> S \<union> {A}\<close> and \<open>finite Sa\<close> and \<open>Sa \<notin> C\<close>
          and \<open>Sb \<subseteq> S \<union> {B}\<close> and \<open>finite Sb\<close> and \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {A} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C} \<or> S \<union> {B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C})

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<subseteq> S \<union> {A}
finite Sa
Sa \<notin> C
Sb \<subseteq> S \<union> {B}
finite Sb
Sb \<notin> C

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
let ?S' = \<open>(Sa - {A}) \<union> (Sb - {B}) \<union> {Or A B}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S
[PROOF STEP]
using \<open>Sa \<subseteq> S \<union> {A}\<close> \<open>Sb \<subseteq> S \<union> {B}\<close> *
[PROOF STATE]
proof (prove)
using this:
Sa \<subseteq> S \<union> {A}
Sb \<subseteq> S \<union> {B}
Or A B \<in> S

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})
[PROOF STEP]
using \<open>finite Sa\<close> \<open>finite Sb\<close>
[PROOF STATE]
proof (prove)
using this:
finite Sa
finite Sb

goal (1 subgoal):
 1. finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S
finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S
finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<subseteq> S
finite (Sa - {A} \<union> (Sb - {B}) \<union> {Or A B})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {A} \<in> C \<or> ?S' \<union> {B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C
alt_consistency C

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C
[PROOF STEP]
have \<open>Sa \<in> C \<or> Sb \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {A} \<in> C \<or> Sa - {A} \<union> (Sb - {B}) \<union> {Or A B} \<union> {B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>Sa \<notin> C\<close> \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C
Sa \<notin> C
Sb \<notin> C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Or ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {?A2} \<in> mk_finite_char C \<or> S \<union> {?B2} \<in> mk_finite_char C

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Or ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {?A2} \<in> mk_finite_char C \<or> S \<union> {?B2} \<in> mk_finite_char C

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Neg (And A B) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Neg (And A B) \<in> S

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
 2. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 4. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 6. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> ?thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C)
[PROOF STEP]
obtain Sa and Sb
        where \<open>Sa \<subseteq> S \<union> {Neg A}\<close> and \<open>finite Sa\<close> and \<open>Sa \<notin> C\<close>
          and \<open>Sb \<subseteq> S \<union> {Neg B}\<close> and \<open>finite Sb\<close> and \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {Neg A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {Neg B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {Neg A} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C} \<or> S \<union> {Neg B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C})

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {Neg A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {Neg B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<subseteq> S \<union> {Neg A}
finite Sa
Sa \<notin> C
Sb \<subseteq> S \<union> {Neg B}
finite Sb
Sb \<notin> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
let ?S' = \<open>(Sa - {Neg A}) \<union> (Sb - {Neg B}) \<union> {Neg (And A B)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S
[PROOF STEP]
using \<open>Sa \<subseteq> S \<union> {Neg A}\<close> \<open>Sb \<subseteq> S \<union> {Neg B}\<close> *
[PROOF STATE]
proof (prove)
using this:
Sa \<subseteq> S \<union> {Neg A}
Sb \<subseteq> S \<union> {Neg B}
Neg (And A B) \<in> S

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})
[PROOF STEP]
using \<open>finite Sa\<close> \<open>finite Sb\<close>
[PROOF STATE]
proof (prove)
using this:
finite Sa
finite Sb

goal (1 subgoal):
 1. finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {Neg A} \<in> C \<or> ?S' \<union> {Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C
alt_consistency C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C
[PROOF STEP]
have \<open>Sa \<in> C \<or> Sb \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {Neg B}) \<union> {Neg (And A B)} \<union> {Neg B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>Sa \<notin> C\<close> \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C
Sa \<notin> C
Sb \<notin> C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {Neg B} \<in> mk_finite_char C

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (And ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {Neg ?A2} \<in> mk_finite_char C \<or> S \<union> {Neg ?B2} \<in> mk_finite_char C

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg (And ?A2 ?B2) \<in> S \<Longrightarrow> S \<union> {Neg ?A2} \<in> mk_finite_char C \<or> S \<union> {Neg ?B2} \<in> mk_finite_char C

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Impl A B \<in> S\<close>
[PROOF STATE]
proof (state)
this:
Impl A B \<in> S

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> mk_finite_char C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 3. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 5. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> ?thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)
[PROOF STEP]
obtain Sa and Sb
        where \<open>Sa \<subseteq> S \<union> {Neg A}\<close> and \<open>finite Sa\<close> and \<open>Sa \<notin> C\<close>
          and \<open>Sb \<subseteq> S \<union> {B}\<close> and \<open>finite Sb\<close> and \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C)

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {Neg A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
using this:
\<not> (S \<union> {Neg A} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C} \<or> S \<union> {B} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C})

goal (1 subgoal):
 1. (\<And>Sa Sb. \<lbrakk>Sa \<subseteq> S \<union> {Neg A}; finite Sa; Sa \<notin> C; Sb \<subseteq> S \<union> {B}; finite Sb; Sb \<notin> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<subseteq> S \<union> {Neg A}
finite Sa
Sa \<notin> C
Sb \<subseteq> S \<union> {B}
finite Sb
Sb \<notin> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
let ?S' = \<open>(Sa - {Neg A}) \<union> (Sb - {B}) \<union> {Impl A B}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S
[PROOF STEP]
using \<open>Sa \<subseteq> S \<union> {Neg A}\<close> \<open>Sb \<subseteq> S \<union> {B}\<close> *
[PROOF STATE]
proof (prove)
using this:
Sa \<subseteq> S \<union> {Neg A}
Sb \<subseteq> S \<union> {B}
Impl A B \<in> S

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})
[PROOF STEP]
using \<open>finite Sa\<close> \<open>finite Sb\<close>
[PROOF STATE]
proof (prove)
using this:
finite Sa
finite Sb

goal (1 subgoal):
 1. finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<subseteq> S
finite (Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {Neg A} \<in> C \<or> ?S' \<union> {B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C
[PROOF STEP]
using altconc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C
alt_consistency C

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C
[PROOF STEP]
have \<open>Sa \<in> C \<or> Sb \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {Neg A} \<in> C \<or> Sa - {Neg A} \<union> (Sb - {B}) \<union> {Impl A B} \<union> {B} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. \<not> (S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sa \<in> C \<or> Sb \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>Sa \<notin> C\<close> \<open>Sb \<notin> C\<close>
[PROOF STATE]
proof (prove)
using this:
Sa \<in> C \<or> Sb \<in> C
Sa \<notin> C
Sb \<notin> C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Neg A} \<in> mk_finite_char C \<or> S \<union> {B} \<in> mk_finite_char C

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Impl ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {Neg ?A2} \<in> mk_finite_char C \<or> S \<union> {?B2} \<in> mk_finite_char C

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Impl ?A2 ?B2 \<in> S \<Longrightarrow> S \<union> {Neg ?A2} \<in> mk_finite_char C \<or> S \<union> {?B2} \<in> mk_finite_char C

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix P and t :: \<open>'a term\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Forall P \<in> S\<close> and \<open>closedt 0 t\<close>
[PROOF STATE]
proof (state)
this:
Forall P \<in> S
closedt 0 t

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> mk_finite_char C
 2. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 4. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {P[t/0]} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {P[t/0]} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {P[t/0]} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {P[t/0]} \<union> {Forall P}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {P[t/0]}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {P[t/0]}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {P[t/0]}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {P[t/0]}
finite S'

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {P[t/0]}
finite S'
Forall P \<in> S

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {P[t/0]} \<union> {Forall P} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {P[t/0]} \<union> {Forall P} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {P[t/0]} \<union> {Forall P})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {P[t/0]} \<union> {Forall P})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {P[t/0]} \<union> {Forall P})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {P[t/0]} \<union> {Forall P} \<subseteq> S
finite (S' - {P[t/0]} \<union> {Forall P})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<subseteq> S
finite (S' - {P[t/0]} \<union> {Forall P})

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<subseteq> S
finite (S' - {P[t/0]} \<union> {Forall P})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {P[t/0]} \<union> {Forall P} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {P[t/0]} \<union> {Forall P} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {P[t/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<in> C

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C
[PROOF STEP]
using altconc \<open>closedt 0 t\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<in> C
alt_consistency C
closedt 0 t

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)
closedt 0 t

goal (1 subgoal):
 1. S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[t/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {P[t/0]} \<union> {Forall P} \<union> {P[t/0]} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {P[t/0]} \<in> mk_finite_char C

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Forall ?P2 \<in> S; closedt 0 ?t2\<rbrakk> \<Longrightarrow> S \<union> {?P2[?t2/0]} \<in> mk_finite_char C

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>Forall ?P2 \<in> S; closedt 0 ?t2\<rbrakk> \<Longrightarrow> S \<union> {?P2[?t2/0]} \<in> mk_finite_char C

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix P and t :: \<open>'a term\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Neg (Exists P) \<in> S\<close> and \<open>closedt 0 t\<close>
[PROOF STATE]
proof (state)
this:
Neg (Exists P) \<in> S
closedt 0 t

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> mk_finite_char C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 3. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {Neg (P[t/0])} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg (P[t/0])} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg (P[t/0])} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {Neg (P[t/0])} \<union> {Neg (Exists P)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {Neg (P[t/0])}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {Neg (P[t/0])}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {Neg (P[t/0])}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg (P[t/0])}
finite S'

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg (P[t/0])}
finite S'
Neg (Exists P) \<in> S

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S
finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S
finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<subseteq> S
finite (S' - {Neg (P[t/0])} \<union> {Neg (Exists P)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C
[PROOF STEP]
have \<open>?S' \<union> {Neg (P[t/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
using altconc \<open>closedt 0 t\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C
alt_consistency C
closedt 0 t

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)
closedt 0 t

goal (1 subgoal):
 1. S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[t/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[t/0])} \<union> {Neg (Exists P)} \<union> {Neg (P[t/0])} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Neg (P[t/0])} \<in> mk_finite_char C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Neg (Exists ?P2) \<in> S; closedt 0 ?t2\<rbrakk> \<Longrightarrow> S \<union> {Neg (?P2[?t2/0])} \<in> mk_finite_char C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>Neg (Exists ?P2) \<in> S; closedt 0 ?t2\<rbrakk> \<Longrightarrow> S \<union> {Neg (?P2[?t2/0])} \<in> mk_finite_char C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix P x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Exists P \<in> S\<close> and \<open>\<forall>a \<in> S. x \<notin> params a\<close>
[PROOF STATE]
proof (state)
this:
Exists P \<in> S
\<forall>a\<in>S. x \<notin> params a

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_finite_char C
 2. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {P[App x []/0]} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {P[App x []/0]} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {P[App x []/0]} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {P[App x []/0]} \<union> {Exists P}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {P[App x []/0]}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {P[App x []/0]}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {P[App x []/0]}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {P[App x []/0]}
finite S'

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {P[App x []/0]}
finite S'
Exists P \<in> S

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {P[App x []/0]} \<union> {Exists P})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {P[App x []/0]} \<union> {Exists P})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {P[App x []/0]} \<union> {Exists P})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S
finite (S' - {P[App x []/0]} \<union> {Exists P})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S
finite (S' - {P[App x []/0]} \<union> {Exists P})

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S
finite (S' - {P[App x []/0]} \<union> {Exists P})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>\<forall>a \<in> ?S'. x \<notin> params a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a
[PROOF STEP]
using \<open>\<forall>a \<in> S. x \<notin> params a\<close> \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
S' - {P[App x []/0]} \<union> {Exists P} \<subseteq> S

goal (1 subgoal):
 1. \<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C
\<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a
[PROOF STEP]
have \<open>?S' \<union> {P[App x []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C
\<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C
[PROOF STEP]
using altconc \<open>\<forall>a \<in> S. x \<notin> params a\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C
\<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a
alt_consistency C
\<forall>a\<in>S. x \<notin> params a

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<in> C
\<forall>a\<in>S' - {P[App x []/0]} \<union> {Exists P}. x \<notin> params a
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)
\<forall>a\<in>S. x \<notin> params a

goal (1 subgoal):
 1. S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {P[App x []/0]}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {P[App x []/0]} \<union> {Exists P} \<union> {P[App x []/0]} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {P[App x []/0]} \<in> mk_finite_char C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Exists ?P2 \<in> S; \<forall>a\<in>S. ?x2 \<notin> params a\<rbrakk> \<Longrightarrow> S \<union> {?P2[App ?x2 []/0]} \<in> mk_finite_char C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>Exists ?P2 \<in> S; \<forall>a\<in>S. ?x2 \<notin> params a\<rbrakk> \<Longrightarrow> S \<union> {?P2[App ?x2 []/0]} \<in> mk_finite_char C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
fix P x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
assume *: \<open>Neg (Forall P) \<in> S\<close> and \<open>\<forall>a \<in> S. x \<notin> params a\<close>
[PROOF STATE]
proof (state)
this:
Neg (Forall P) \<in> S
\<forall>a\<in>S. x \<notin> params a

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_finite_char C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
show \<open>S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> {Neg (P[App x []/0])} \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
proof (intro allI impI CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
let ?S' = \<open>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
assume \<open>S' \<subseteq> S \<union> {Neg (P[App x []/0])}\<close> and \<open>finite S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<subseteq> S \<union> {Neg (P[App x []/0])}
finite S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> S \<union> {Neg (P[App x []/0])}
finite S'
[PROOF STEP]
have \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg (P[App x []/0])}
finite S'

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> S \<union> {Neg (P[App x []/0])}
finite S'
Neg (Forall P) \<in> S

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>finite ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})
[PROOF STEP]
using \<open>finite S'\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'

goal (1 subgoal):
 1. finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S
finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})
[PROOF STEP]
have \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S
finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
[PROOF STEP]
using finc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S
finite (S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)})
\<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
have \<open>\<forall>a \<in> ?S'. x \<notin> params a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a
[PROOF STEP]
using \<open>\<forall>a \<in> S. x \<notin> params a\<close> \<open>?S' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<subseteq> S

goal (1 subgoal):
 1. \<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
\<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a
[PROOF STEP]
have \<open>?S' \<union> {Neg (P[App x []/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
\<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C
[PROOF STEP]
using altconc \<open>\<forall>a \<in> S. x \<notin> params a\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
\<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a
alt_consistency C
\<forall>a\<in>S. x \<notin> params a

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<in> C
\<forall>a\<in>S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)}. x \<notin> params a
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)
\<forall>a\<in>S. x \<notin> params a

goal (1 subgoal):
 1. S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<subseteq> S \<union> {Neg (P[App x []/0])}; finite S'\<rbrakk> \<Longrightarrow> S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
S' - {Neg (P[App x []/0])} \<union> {Neg (Forall P)} \<union> {Neg (P[App x []/0])} \<in> C
\<forall>S' x. S' \<union> x \<in> C \<longrightarrow> (\<forall>S\<subseteq>S' \<union> x. S \<in> C)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> {Neg (P[App x []/0])} \<in> mk_finite_char C

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Neg (Forall ?P2) \<in> S; \<forall>a\<in>S. ?x2 \<notin> params a\<rbrakk> \<Longrightarrow> S \<union> {Neg (?P2[App ?x2 []/0])} \<in> mk_finite_char C

goal:
No subgoals!
[PROOF STEP]
qed