[STATEMENT]
theorem extend_hintikka:
  assumes fin_ch: \<open>finite_char C\<close>
    and infin_p: \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
    and surj: \<open>\<forall>y. \<exists>n. y = f n\<close>
    and altc: \<open>alt_consistency C\<close>
    and \<open>S \<in> C\<close>
  shows \<open>hintikka (Extend S C f)\<close> (is \<open>hintikka ?H\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hintikka (Extend S C f)
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)) \<and> FF \<notin> Extend S C f \<and> Neg TT \<notin> Extend S C f \<and> (\<forall>Z. Neg (Neg Z) \<in> Extend S C f \<longrightarrow> Z \<in> Extend S C f) \<and> (\<forall>A B. And A B \<in> Extend S C f \<longrightarrow> A \<in> Extend S C f \<and> B \<in> Extend S C f) \<and> (\<forall>A B. Neg (Or A B) \<in> Extend S C f \<longrightarrow> Neg A \<in> Extend S C f \<and> Neg B \<in> Extend S C f) \<and> (\<forall>A B. Or A B \<in> Extend S C f \<longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f) \<and> (\<forall>A B. Neg (And A B) \<in> Extend S C f \<longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f) \<and> (\<forall>A B. Impl A B \<in> Extend S C f \<longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f) \<and> (\<forall>A B. Neg (Impl A B) \<in> Extend S C f \<longrightarrow> A \<in> Extend S C f \<and> Neg B \<in> Extend S C f) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> Extend S C f \<longrightarrow> P[t/0] \<in> Extend S C f) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> Extend S C f \<longrightarrow> Neg (P[t/0]) \<in> Extend S C f) \<and> (\<forall>P. Exists P \<in> Extend S C f \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f)) \<and> (\<forall>P. Neg (Forall P) \<in> Extend S C f \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f))
[PROOF STEP]
proof (intro allI impI conjI)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
have \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal (Extend S C f) C
[PROOF STEP]
by (simp add: extend_maximal fin_ch surj)
[PROOF STATE]
proof (state)
this:
maximal (Extend S C f) C

goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
have \<open>?H \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Extend S C f \<in> C
[PROOF STEP]
using Extend_in_C assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alt_consistency ?C; finite_char ?C; ?S \<in> ?C; infinite (- \<Union> (params ` ?S))\<rbrakk> \<Longrightarrow> Extend ?S ?C ?f \<in> ?C
finite_char C
infinite (- \<Union> (params ` S))
\<forall>y. \<exists>n. y = f n
alt_consistency C
S \<in> C

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

goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
have \<open>\<forall>S' \<in> C. ?H \<subseteq> S' \<longrightarrow> ?H = S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
maximal (Extend S C f) C

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

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

goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
fix p ts
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>p ts. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
 2. FF \<notin> Extend S C f
 3. Neg TT \<notin> Extend S C f
 4. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 6. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 8. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 9. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
A total of 17 subgoals...
[PROOF STEP]
show \<open>\<not> (Pred p ts \<in> ?H \<and> Neg (Pred p ts) \<in> ?H)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<in> C
alt_consistency C

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

goal (1 subgoal):
 1. \<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> (Pred p ts \<in> Extend S C f \<and> Neg (Pred p ts) \<in> Extend S C f)

goal (16 subgoals):
 1. FF \<notin> Extend S C f
 2. Neg TT \<notin> Extend S C f
 3. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 4. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 6. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 8. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 10. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
A total of 16 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (Pred ?p2 ?ts2 \<in> Extend S C f \<and> Neg (Pred ?p2 ?ts2) \<in> Extend S C f)

goal (16 subgoals):
 1. FF \<notin> Extend S C f
 2. Neg TT \<notin> Extend S C f
 3. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 4. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 5. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 6. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 7. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 8. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 10. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
A total of 16 subgoals...
[PROOF STEP]
show \<open>FF \<notin> ?H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FF \<notin> Extend S C f
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<in> C
alt_consistency C

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

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

goal (15 subgoals):
 1. Neg TT \<notin> Extend S C f
 2. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 4. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 6. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 7. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 8. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 9. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
A total of 15 subgoals...
[PROOF STEP]
show \<open>Neg TT \<notin> ?H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg TT \<notin> Extend S C f
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<in> C
alt_consistency C

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

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

goal (14 subgoals):
 1. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 6. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 7. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 8. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
A total of 14 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg TT \<notin> Extend S C f

goal (14 subgoals):
 1. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 6. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 7. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 8. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
A total of 14 subgoals...
[PROOF STEP]
fix Z
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 6. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 7. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 8. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
A total of 14 subgoals...
[PROOF STEP]
assume \<open>Neg (Neg Z) \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
Neg (Neg Z) \<in> Extend S C f

goal (14 subgoals):
 1. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 6. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 7. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 8. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Neg Z) \<in> Extend S C f
[PROOF STEP]
have \<open>?H \<union> {Z} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> Extend S C f

goal (1 subgoal):
 1. Extend S C f \<union> {Z} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Neg (Neg Z) \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

goal (14 subgoals):
 1. \<And>Z. Neg (Neg Z) \<in> Extend S C f \<Longrightarrow> Z \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 3. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 5. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 6. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 7. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 8. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 10. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Extend S C f \<union> {Z} \<in> C
[PROOF STEP]
show \<open>Z \<in> ?H\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Z} \<in> C

goal (1 subgoal):
 1. Z \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Z} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. Z \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Z} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. Z \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Z \<in> Extend S C f

goal (13 subgoals):
 1. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 3. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 5. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 7. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 8. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 10. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
A total of 13 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Neg ?Z2) \<in> Extend S C f \<Longrightarrow> ?Z2 \<in> Extend S C f

goal (13 subgoals):
 1. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 3. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 5. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 7. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 8. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 10. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
A total of 13 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Neg (Neg ?Z2) \<in> Extend S C f \<Longrightarrow> ?Z2 \<in> Extend S C f

goal (13 subgoals):
 1. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 3. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 5. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 7. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 8. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 10. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
A total of 13 subgoals...
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 2. \<And>A B. And A B \<in> Extend S C f \<Longrightarrow> B \<in> Extend S C f
 3. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 4. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 5. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 7. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 8. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 9. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 10. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
A total of 13 subgoals...
[PROOF STEP]
assume \<open>And A B \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
And A B \<in> Extend S C f

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

goal (1 subgoal):
 1. Extend S C f \<union> {A, B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
And A B \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. A \<in> Extend S C f &&& B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A, B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. A \<in> Extend S C f &&& B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A, B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. A \<in> Extend S C f &&& B \<in> Extend S C f
[PROOF STEP]
by fast+
[PROOF STATE]
proof (state)
this:
A \<in> Extend S C f
B \<in> Extend S C f

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

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

goal (11 subgoals):
 1. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 2. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 3. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 4. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 5. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 7. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 8. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 9. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 10. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
A total of 11 subgoals...
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f
 2. \<And>A B. Neg (Or A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 3. \<And>A B. Or A B \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f \<or> B \<in> Extend S C f
 4. \<And>A B. Neg (And A B) \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
 5. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 6. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> A \<in> Extend S C f
 7. \<And>A B. Neg (Impl A B) \<in> Extend S C f \<Longrightarrow> Neg B \<in> Extend S C f
 8. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 9. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 10. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
A total of 11 subgoals...
[PROOF STEP]
assume \<open>Neg (Or A B) \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
Neg (Or A B) \<in> Extend S C f

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

goal (1 subgoal):
 1. Extend S C f \<union> {Neg A, Neg B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. Neg A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A, Neg B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. Neg A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A, Neg B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. Neg A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
by fast+
[PROOF STATE]
proof (state)
this:
Neg A \<in> Extend S C f
Neg B \<in> Extend S C f

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

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

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

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

goal (1 subgoal):
 1. Extend S C f \<union> {A, Neg B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A, Neg B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A, Neg B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. A \<in> Extend S C f &&& Neg B \<in> Extend S C f
[PROOF STEP]
by fast+
[PROOF STATE]
proof (state)
this:
A \<in> Extend S C f
Neg B \<in> Extend S C f

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

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

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

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

goal (1 subgoal):
 1. Extend S C f \<union> {A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A \<in> Extend S C f \<or> B \<in> Extend S C f

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

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

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

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

goal (1 subgoal):
 1. Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {Neg B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {Neg B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {Neg B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Neg A \<in> Extend S C f \<or> Neg B \<in> Extend S C f

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

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

goal (5 subgoals):
 1. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 2. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 3. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 4. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 5. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>A B. Impl A B \<in> Extend S C f \<Longrightarrow> Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
 2. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 3. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 4. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 5. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
assume \<open>Impl A B \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
Impl A B \<in> Extend S C f

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

goal (1 subgoal):
 1. Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
[PROOF STEP]
using \<open>?H \<in> C\<close> altc
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> Extend S C f
Extend S C f \<in> C
alt_consistency C

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

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

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

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg A} \<in> C \<or> Extend S C f \<union> {B} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. Neg A \<in> Extend S C f \<or> B \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Neg A \<in> Extend S C f \<or> B \<in> Extend S C f

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

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

goal (4 subgoals):
 1. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 2. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 3. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 4. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
fix P and t :: \<open>nat term\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P t. \<lbrakk>closedt 0 t; Forall P \<in> Extend S C f\<rbrakk> \<Longrightarrow> P[t/0] \<in> Extend S C f
 2. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 3. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 4. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
assume \<open>Forall P \<in> ?H\<close> and \<open>closedt 0 t\<close>
[PROOF STATE]
proof (state)
this:
Forall P \<in> Extend S C f
closedt 0 t

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

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

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

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

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

goal (1 subgoal):
 1. P[t/0] \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {P[t/0]} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. P[t/0] \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {P[t/0]} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. P[t/0] \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
P[t/0] \<in> Extend S C f

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

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

goal (3 subgoals):
 1. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 2. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 3. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
fix P and t :: \<open>nat term\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P t. \<lbrakk>closedt 0 t; Neg (Exists P) \<in> Extend S C f\<rbrakk> \<Longrightarrow> Neg (P[t/0]) \<in> Extend S C f
 2. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 3. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
assume \<open>Neg (Exists P) \<in> ?H\<close> and \<open>closedt 0 t\<close>
[PROOF STATE]
proof (state)
this:
Neg (Exists P) \<in> Extend S C f
closedt 0 t

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

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

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

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

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

goal (1 subgoal):
 1. Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
using \<open>maximal ?H C\<close>
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg (P[t/0])} \<in> C
maximal (Extend S C f) C

goal (1 subgoal):
 1. Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
Extend S C f \<union> {Neg (P[t/0])} \<in> C
\<forall>S'\<in>C. Extend S C f \<subseteq> S' \<longrightarrow> Extend S C f = S'

goal (1 subgoal):
 1. Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Neg (P[t/0]) \<in> Extend S C f

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

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

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
assume \<open>Exists P \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
Exists P \<in> Extend S C f

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
obtain n where *: \<open>Exists P = f n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. Exists P = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using surj
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>n. y = f n

goal (1 subgoal):
 1. (\<And>n. Exists P = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Exists P = f n

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
let ?t = \<open>App (SOME k. k \<notin> (\<Union>p \<in> extend S C f n \<union> {f n}. params p)) []\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
have \<open>closedt 0 ?t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
have \<open>Exists P \<in> (\<Union>n. extend S C f n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Exists P \<in> \<Union> (range (extend S C f))
[PROOF STEP]
using \<open>Exists P \<in> ?H\<close> Extend_def
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> Extend S C f
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))

goal (1 subgoal):
 1. Exists P \<in> \<Union> (range (extend S C f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Exists P \<in> \<Union> (range (extend S C f))

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Exists P \<in> \<Union> (range (extend S C f))
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<subseteq> (\<Union>n. extend S C f n)\<close>
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Exists P \<in> \<Union> (range (extend S C f))
Exists P = f n

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
by (simp add: UN_upper)
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
using Extend_def \<open>Extend S C f \<in> C\<close> fin_ch finite_char_closed
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))
Extend S C f \<in> C
finite_char C
finite_char ?C \<Longrightarrow> subset_closed ?C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
unfolding subset_closed_def
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))
Extend S C f \<in> C
finite_char C
finite_char ?C \<Longrightarrow> \<forall>S'\<in>?C. \<forall>S\<subseteq>S'. S \<in> ?C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<in> C

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
have \<open>P[?t/0] \<in> extend S C f (Suc n)\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
using * Exists_in_extend
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C
Exists P = f n
\<lbrakk>extend ?S ?C ?f ?n \<union> {?f ?n} \<in> ?C; Exists ?P = ?f ?n\<rbrakk> \<Longrightarrow> ?P[App (SOME k. k \<notin> \<Union> (params ` (extend ?S ?C ?f ?n \<union> {?f ?n}))) []/0] \<in> extend ?S ?C ?f (Suc ?n)

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>P[?t/0] \<in> ?H\<close>
[PROOF STATE]
proof (prove)
using this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f
[PROOF STEP]
using Extend_def
[PROOF STATE]
proof (prove)
using this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f

goal (2 subgoals):
 1. \<And>P. Exists P \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
 2. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f
[PROOF STEP]
show \<open>\<exists>t. closedt 0 t \<and> P[t/0] \<in> ?H\<close>
[PROOF STATE]
proof (prove)
using this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
[PROOF STEP]
using \<open>closedt 0 ?t\<close>
[PROOF STATE]
proof (prove)
using this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> Extend S C f
closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. closedt 0 t \<and> P[t/0] \<in> Extend S C f

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Exists ?P2 \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> ?P2[t/0] \<in> Extend S C f

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Exists ?P2 \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> ?P2[t/0] \<in> Extend S C f

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
assume \<open>Neg (Forall P) \<in> ?H\<close>
[PROOF STATE]
proof (state)
this:
Neg (Forall P) \<in> Extend S C f

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
obtain n where *: \<open>Neg (Forall P) = f n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. Neg (Forall P) = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using surj
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>n. y = f n

goal (1 subgoal):
 1. (\<And>n. Neg (Forall P) = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Forall P) = f n

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
let ?t = \<open>App (SOME k. k \<notin> (\<Union>p \<in> extend S C f n \<union> {f n}. params p)) []\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
have \<open>closedt 0 ?t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
have \<open>Neg (Forall P) \<in> (\<Union>n. extend S C f n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg (Forall P) \<in> \<Union> (range (extend S C f))
[PROOF STEP]
using \<open>Neg (Forall P) \<in> ?H\<close> Extend_def
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> Extend S C f
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))

goal (1 subgoal):
 1. Neg (Forall P) \<in> \<Union> (range (extend S C f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (Forall P) \<in> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Forall P) \<in> \<Union> (range (extend S C f))
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<subseteq> (\<Union>n. extend S C f n)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> \<Union> (range (extend S C f))
Neg (Forall P) = f n

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
by (simp add: UN_upper)
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
using Extend_def \<open>Extend S C f \<in> C\<close> fin_ch finite_char_closed
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))
Extend S C f \<in> C
finite_char C
finite_char ?C \<Longrightarrow> subset_closed ?C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
unfolding subset_closed_def
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<subseteq> \<Union> (range (extend S C f))
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))
Extend S C f \<in> C
finite_char C
finite_char ?C \<Longrightarrow> \<forall>S'\<in>?C. \<forall>S\<subseteq>S'. S \<in> ?C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
have \<open>Neg (P[?t/0]) \<in> extend S C f (Suc n)\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
using * Neg_Forall_in_extend
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C
Neg (Forall P) = f n
\<lbrakk>extend ?S ?C ?f ?n \<union> {?f ?n} \<in> ?C; Neg (Forall ?P) = ?f ?n\<rbrakk> \<Longrightarrow> Neg (?P[App (SOME k. k \<notin> \<Union> (params ` (extend ?S ?C ?f ?n \<union> {?f ?n}))) []/0]) \<in> extend ?S ?C ?f (Suc ?n)

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>Neg (P[?t/0]) \<in> ?H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f
[PROOF STEP]
using Extend_def
[PROOF STATE]
proof (prove)
using this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
Extend ?S ?C ?f = \<Union> (range (extend ?S ?C ?f))

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f

goal (1 subgoal):
 1. \<And>P. Neg (Forall P) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f
[PROOF STEP]
show \<open>\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> ?H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
using \<open>closedt 0 ?t\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> Extend S C f
closedt 0 (App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) [])

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> Extend S C f

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Neg (Forall ?P2) \<in> Extend S C f \<Longrightarrow> \<exists>t. closedt 0 t \<and> Neg (?P2[t/0]) \<in> Extend S C f

goal:
No subgoals!
[PROOF STEP]
qed