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

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> C; S \<subseteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding close_def
[PROOF STATE]
proof (prove)
using this:
S \<in> {S. Bex C ((\<subseteq>) S)}

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> C; S \<subseteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> C
S \<subseteq> x

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

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

goal (1 subgoal):
 1. \<not> (Pred p ts \<in> x \<and> Neg (Pred p ts) \<in> x)
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

goal (1 subgoal):
 1. \<not> (Pred p ts \<in> x \<and> Neg (Pred p ts) \<in> x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (Pred p ts \<in> x \<and> Neg (Pred p ts) \<in> x)

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

goal (1 subgoal):
 1. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (Pred p ts \<in> x \<and> Neg (Pred p ts) \<in> x)
S \<subseteq> x

goal (1 subgoal):
 1. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)
[PROOF STEP]
by blast
[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> close C \<Longrightarrow> FF \<notin> S
 2. \<And>S. S \<in> close C \<Longrightarrow> Neg TT \<notin> S
 3. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 8. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 9. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 10. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close 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> close C \<Longrightarrow> FF \<notin> S
 2. \<And>S. S \<in> close C \<Longrightarrow> Neg TT \<notin> S
 3. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 8. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 9. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 10. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close 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> close C \<Longrightarrow> FF \<notin> S
 2. \<And>S. S \<in> close C \<Longrightarrow> Neg TT \<notin> S
 3. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 8. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 9. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 10. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
A total of 13 subgoals...
[PROOF STEP]
have \<open>FF \<notin> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FF \<notin> x
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
x \<in> C
consistency C

goal (1 subgoal):
 1. FF \<notin> x
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

goal (1 subgoal):
 1. FF \<notin> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FF \<notin> x

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

goal (1 subgoal):
 1. FF \<notin> S
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
FF \<notin> x
S \<subseteq> x

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

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

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

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

goal (1 subgoal):
 1. Neg TT \<notin> x
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

goal (1 subgoal):
 1. Neg TT \<notin> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg TT \<notin> x

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

goal (1 subgoal):
 1. Neg TT \<notin> S
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg TT \<notin> x
S \<subseteq> x

goal (1 subgoal):
 1. Neg TT \<notin> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg TT \<notin> S

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close 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> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close 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> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
A total of 11 subgoals...
[PROOF STEP]
fix Z
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close 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> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Neg Z) \<in> S
[PROOF STEP]
have \<open>Neg (Neg Z) \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> S

goal (1 subgoal):
 1. Neg (Neg Z) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (Neg Z) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Neg Z) \<in> x

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Neg Z) \<in> x
[PROOF STEP]
have \<open>x \<union> {Z} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> x

goal (1 subgoal):
 1. x \<union> {Z} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {Z} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (11 subgoals):
 1. \<And>S Z. \<lbrakk>S \<in> close C; Neg (Neg Z) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Z} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 7. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 9. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {Z} \<in> C
[PROOF STEP]
show \<open>S \<union> {Z} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {Z} \<in> C

goal (1 subgoal):
 1. S \<union> {Z} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {Z} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close 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> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
And A B \<in> S
[PROOF STEP]
have \<open>And A B \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
And A B \<in> S

goal (1 subgoal):
 1. And A B \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
And A B \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. And A B \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
And A B \<in> x

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
And A B \<in> x
[PROOF STEP]
have \<open>x \<union> {A, B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
And A B \<in> x

goal (1 subgoal):
 1. x \<union> {A, B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
And A B \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {A, B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
And A B \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (10 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; And A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 6. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 8. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 10. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {A, B} \<in> C
[PROOF STEP]
show \<open>S \<union> {A, B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {A, B} \<in> C

goal (1 subgoal):
 1. S \<union> {A, B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {A, B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close 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> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Or A B) \<in> S
[PROOF STEP]
have \<open>Neg (Or A B) \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> S

goal (1 subgoal):
 1. Neg (Or A B) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (Or A B) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Or A B) \<in> x

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Or A B) \<in> x
[PROOF STEP]
have \<open>x \<union> {Neg A, Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> x

goal (1 subgoal):
 1. x \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (9 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Or A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A, Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 5. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 7. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 9. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
show \<open>S \<union> {Neg A, Neg B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A, Neg B} \<in> C

goal (1 subgoal):
 1. S \<union> {Neg A, Neg B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A, Neg B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Or A B \<in> S
[PROOF STEP]
have \<open>Or A B \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> S

goal (1 subgoal):
 1. Or A B \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Or A B \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Or A B \<in> x

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Or A B \<in> x
[PROOF STEP]
have \<open>x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> x

goal (1 subgoal):
 1. x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (8 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Or A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 4. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 6. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 8. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
show \<open>S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C

goal (1 subgoal):
 1. S \<union> {A} \<in> close C \<or> S \<union> {B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {A} \<in> C \<or> x \<union> {B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (And A B) \<in> S
[PROOF STEP]
have \<open>Neg (And A B) \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> S

goal (1 subgoal):
 1. Neg (And A B) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (And A B) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (And A B) \<in> x

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (And A B) \<in> x
[PROOF STEP]
have \<open>x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> x

goal (1 subgoal):
 1. x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (7 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (And A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 3. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 5. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 7. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C
[PROOF STEP]
show \<open>S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C

goal (1 subgoal):
 1. S \<union> {Neg A} \<in> close C \<or> S \<union> {Neg B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A} \<in> C \<or> x \<union> {Neg B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Impl A B \<in> S
[PROOF STEP]
have \<open>Impl A B \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> S

goal (1 subgoal):
 1. Impl A B \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Impl A B \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Impl A B \<in> x

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Impl A B \<in> x
[PROOF STEP]
have \<open>x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> x

goal (1 subgoal):
 1. x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (6 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Impl A B \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
 2. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 4. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 6. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C
[PROOF STEP]
show \<open>S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C

goal (1 subgoal):
 1. S \<union> {Neg A} \<in> close C \<or> S \<union> {B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg A} \<in> C \<or> x \<union> {B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Impl A B) \<in> S
[PROOF STEP]
have \<open>Neg (Impl A B) \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> S

goal (1 subgoal):
 1. Neg (Impl A B) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (Impl A B) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Impl A B) \<in> x

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Impl A B) \<in> x
[PROOF STEP]
have \<open>x \<union> {A, Neg B} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> x

goal (1 subgoal):
 1. x \<union> {A, Neg B} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. x \<union> {A, Neg B} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (5 subgoals):
 1. \<And>S A B. \<lbrakk>S \<in> close C; Neg (Impl A B) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {A, Neg B} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 3. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 5. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {A, Neg B} \<in> C
[PROOF STEP]
show \<open>S \<union> {A, Neg B} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {A, Neg B} \<in> C

goal (1 subgoal):
 1. S \<union> {A, Neg B} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {A, Neg B} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close 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> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
assume \<open>closedt 0 t\<close> and \<open>Forall P \<in> S\<close>
[PROOF STATE]
proof (state)
this:
closedt 0 t
Forall P \<in> S

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedt 0 t
Forall P \<in> S
[PROOF STEP]
have \<open>Forall P \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t
Forall P \<in> S

goal (1 subgoal):
 1. Forall P \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t
Forall P \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Forall P \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Forall P \<in> x

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Forall P \<in> x
[PROOF STEP]
have \<open>x \<union> {P[t/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Forall P \<in> x

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

goal (1 subgoal):
 1. x \<union> {P[t/0]} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Forall P \<in> x
closedt 0 t
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (4 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Forall P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[t/0]} \<in> close C
 2. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 4. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {P[t/0]} \<in> C
[PROOF STEP]
show \<open>S \<union> {P[t/0]} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {P[t/0]} \<in> C

goal (1 subgoal):
 1. S \<union> {P[t/0]} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {P[t/0]} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close 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> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
assume \<open>closedt 0 t\<close> and \<open>Neg (Exists P) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
closedt 0 t
Neg (Exists P) \<in> S

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedt 0 t
Neg (Exists P) \<in> S
[PROOF STEP]
have \<open>Neg (Exists P) \<in> x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t
Neg (Exists P) \<in> S

goal (1 subgoal):
 1. Neg (Exists P) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t
Neg (Exists P) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (Exists P) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Exists P) \<in> x

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Exists P) \<in> x
[PROOF STEP]
have \<open>x \<union> {Neg (P[t/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Exists P) \<in> x

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

goal (1 subgoal):
 1. x \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Exists P) \<in> x
closedt 0 t
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

goal (3 subgoals):
 1. \<And>S P t. \<lbrakk>S \<in> close C; closedt 0 t; Neg (Exists P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[t/0])} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 3. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<union> {Neg (P[t/0])} \<in> C
[PROOF STEP]
show \<open>S \<union> {Neg (P[t/0])} \<in> close C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg (P[t/0])} \<in> C

goal (1 subgoal):
 1. S \<union> {Neg (P[t/0])} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
x \<union> {Neg (P[t/0])} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

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

goal (1 subgoal):
 1. Exists P \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Exists P \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Exists P \<in> x

goal (2 subgoals):
 1. \<And>S P. \<lbrakk>S \<in> close C; Exists P \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {P[App x []/0]} \<in> close C
 2. \<And>S P. \<lbrakk>S \<in> close C; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. S \<union> {Neg (P[App x []/0])} \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Exists P \<in> x
[PROOF STEP]
have \<open>\<exists>c. x \<union> {P[App c []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> x

goal (1 subgoal):
 1. \<exists>c. x \<union> {P[App c []/0]} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. \<exists>c. x \<union> {P[App c []/0]} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

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

goal (1 subgoal):
 1. \<exists>c. S \<union> {P[App c []/0]} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
\<exists>c. x \<union> {P[App c []/0]} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

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

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

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

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

goal (1 subgoal):
 1. Neg (Forall P) \<in> x
[PROOF STEP]
using \<open>S \<subseteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> S
S \<subseteq> x

goal (1 subgoal):
 1. Neg (Forall P) \<in> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Forall P) \<in> x

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

goal (1 subgoal):
 1. \<exists>c. x \<union> {Neg (P[App c []/0])} \<in> C
[PROOF STEP]
using \<open>x \<in> C\<close> conc
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> x
x \<in> C
consistency C

goal (1 subgoal):
 1. \<exists>c. x \<union> {Neg (P[App c []/0])} \<in> C
[PROOF STEP]
unfolding consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> x
x \<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. Exists P \<in> S \<longrightarrow> (\<exists>x. S \<union> {P[App x []/0]} \<in> C)) \<and> (\<forall>P. Neg (Forall P) \<in> S \<longrightarrow> (\<exists>x. S \<union> {Neg (P[App x []/0])} \<in> C))

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

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

goal (1 subgoal):
 1. \<exists>c. S \<union> {Neg (P[App c []/0])} \<in> close C
[PROOF STEP]
using \<open>S \<subseteq> x\<close> subset_in_close
[PROOF STATE]
proof (prove)
using this:
\<exists>c. x \<union> {Neg (P[App c []/0])} \<in> C
S \<subseteq> x
?S \<subseteq> ?S' \<Longrightarrow> ?S' \<union> ?x \<in> ?C \<longrightarrow> ?S \<union> ?x \<in> close ?C

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

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Forall ?P2) \<in> S \<Longrightarrow> \<exists>c. S \<union> {Neg (?P2[App c []/0])} \<in> close C

goal:
No subgoals!
[PROOF STEP]
qed