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

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

goal (1 subgoal):
 1. (\<And>f. psubst f ` S \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
S \<in> {S. \<exists>f. psubst f ` S \<in> C}

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

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

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

goal (1 subgoal):
 1. psubst f (Pred p ts) \<in> psubst f ` S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f (Pred p ts) \<in> psubst f ` S

goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
psubst f (Pred p ts) \<in> psubst f ` S
[PROOF STEP]
have \<open>Pred p (psubstts f ts) \<in> ?S'\<close>
[PROOF STATE]
proof (prove)
using this:
psubst f (Pred p ts) \<in> psubst f ` S

goal (1 subgoal):
 1. Pred p (psubstts f ts) \<in> psubst f ` S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Pred p (psubstts f ts) \<in> psubst f ` S

goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pred p (psubstts f ts) \<in> psubst f ` S
[PROOF STEP]
have \<open>Neg (Pred p (psubstts f ts)) \<notin> ?S'\<close>
[PROOF STATE]
proof (prove)
using this:
Pred p (psubstts f ts) \<in> psubst f ` S

goal (1 subgoal):
 1. Neg (Pred p (psubstts f ts)) \<notin> psubst f ` S
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
Pred p (psubstts f ts) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

goal (1 subgoal):
 1. Neg (Pred p (psubstts f ts)) \<notin> psubst f ` S
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
Neg (Pred p (psubstts f ts)) \<notin> psubst f ` S

goal (1 subgoal):
 1. Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Pred p (psubstts f ts)) \<notin> psubst f ` S
[PROOF STEP]
have \<open>Neg (Pred p ts) \<notin> S\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Pred p (psubstts f ts)) \<notin> psubst f ` S

goal (1 subgoal):
 1. Neg (Pred p ts) \<notin> S
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Neg (Pred p ts) \<notin> S

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Neg (Pred p ts) \<notin> S
Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S

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

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

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

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

goal (1 subgoal):
 1. FF \<notin> psubst f ` S &&& Neg TT \<notin> psubst f ` S
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
FF \<notin> psubst f ` S
Neg TT \<notin> psubst f ` S

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f Z} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Neg (Neg Z)) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f Z} \<in> C
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {psubst f Z} \<in> C

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

goal (1 subgoal):
 1. S \<union> {Z} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {psubst f Z} \<in> C

goal (1 subgoal):
 1. S \<union> {Z} \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<union> {Z} \<in> mk_alt_consistency C

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f A, psubst f B} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (And A B) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {A, B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {psubst f A, psubst f B} \<in> C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {Neg (psubst f A), Neg (psubst f B)} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Neg (Or A B)) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {Neg A, Neg B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {Neg (psubst f A), Neg (psubst f B)} \<in> C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f A, Neg (psubst f B)} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Neg (Impl A B)) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {A, Neg B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {psubst f A, Neg (psubst f B)} \<in> C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f A} \<in> C \<or> psubst f ` S \<union> {psubst f B} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Or A B) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {A} \<in> mk_alt_consistency C \<or> S \<union> {B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {psubst f A} \<in> C \<or> psubst f ` S \<union> {psubst f B} \<in> C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {Neg (psubst f A)} \<in> C \<or> psubst f ` S \<union> {Neg (psubst f B)} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Neg (And A B)) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {Neg A} \<in> mk_alt_consistency C \<or> S \<union> {Neg B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {Neg (psubst f A)} \<in> C \<or> psubst f ` S \<union> {Neg (psubst f B)} \<in> C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {Neg (psubst f A)} \<in> C \<or> psubst f ` S \<union> {psubst f B} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Impl A B) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {Neg A} \<in> mk_alt_consistency C \<or> S \<union> {B} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {Neg (psubst f A)} \<in> C \<or> psubst f ` S \<union> {psubst f B} \<in> C

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {psubst f P[psubstt f t/0]} \<in> C
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {psubst f P[psubstt f t/0]} \<in> C

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

goal (1 subgoal):
 1. S \<union> {P[t/0]} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {psubst f P[psubstt f t/0]} \<in> C

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. psubst f ` S \<union> {Neg (psubst f P[psubstt f t/0])} \<in> C
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {Neg (psubst f P[psubstt f t/0])} \<in> C

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

goal (1 subgoal):
 1. S \<union> {Neg (P[t/0])} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<union> {Neg (psubst f P[psubstt f t/0])} \<in> C

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Exists P) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

goal (1 subgoal):
 1. \<exists>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
\<exists>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
[PROOF STEP]
obtain y where \<open>?S' \<union> {psubst f P[App y []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C

goal (1 subgoal):
 1. (\<And>y. psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
have \<open>psubst (f(x := y)) ` S = ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (f(x := y)) ` S = psubst f ` S
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
Exists P \<in> S
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C

goal (1 subgoal):
 1. psubst (f(x := y)) ` S = psubst f ` S
[PROOF STEP]
by (simp cong add: image_cong)
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S = psubst f ` S

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S = psubst f ` S

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
have \<open>psubst (f(x := y)) `
        S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (f(x := y)) ` S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
Exists P \<in> S
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
psubst (f(x := y)) ` S = psubst f ` S

goal (1 subgoal):
 1. psubst (f(x := y)) ` S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C

goal (2 subgoals):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Exists P \<in> S\<rbrakk> \<Longrightarrow> S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
 2. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>S. x \<notin> params a
Exists P \<in> S
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
psubst (f(x := y)) ` S = psubst f ` S
psubst (f(x := y)) ` S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C
[PROOF STEP]
have \<open>\<exists>f. psubst f ` S \<union> {psubst f P[App (f x) []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
Exists P \<in> S
psubst f ` S \<union> {psubst f P[App y []/0]} \<in> C
psubst (f(x := y)) ` S = psubst f ` S
psubst (f(x := y)) ` S \<union> {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {P[App x []/0]} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f. psubst f ` S \<union> {psubst f P[App (f x) []/0]} \<in> C

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
[PROOF STEP]
using conc sc
[PROOF STATE]
proof (prove)
using this:
psubst f (Neg (Forall P)) \<in> psubst f ` S
consistency C
psubst f ` S \<in> C

goal (1 subgoal):
 1. \<exists>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
[PROOF STEP]
by (simp add: consistency_def)
[PROOF STATE]
proof (state)
this:
\<exists>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
[PROOF STEP]
obtain y where \<open>?S' \<union> {Neg (psubst f P[App y []/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C

goal (1 subgoal):
 1. (\<And>y. psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C

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

goal (1 subgoal):
 1. psubst (f(x := y)) ` S = psubst f ` S
[PROOF STEP]
by (simp cong add: image_cong)
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S = psubst f ` S

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S = psubst f ` S

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
have \<open>psubst (f(x := y)) `
    S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (f(x := y)) ` S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
Neg (Forall P) \<in> S
psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
psubst (f(x := y)) ` S = psubst f ` S

goal (1 subgoal):
 1. psubst (f(x := y)) ` S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst (f(x := y)) ` S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C

goal (1 subgoal):
 1. \<And>S P x. \<lbrakk>S \<in> mk_alt_consistency C; \<forall>a\<in>S. x \<notin> params a; Neg (Forall P) \<in> S\<rbrakk> \<Longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>S. x \<notin> params a
Neg (Forall P) \<in> S
psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
psubst (f(x := y)) ` S = psubst f ` S
psubst (f(x := y)) ` S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C
[PROOF STEP]
have \<open>\<exists>f. psubst f ` S \<union> {Neg (psubst f P[App (f x) []/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>S. x \<notin> params a
Neg (Forall P) \<in> S
psubst f ` S \<union> {Neg (psubst f P[App y []/0])} \<in> C
psubst (f(x := y)) ` S = psubst f ` S
psubst (f(x := y)) ` S \<union> {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} \<in> C

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

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

goal (1 subgoal):
 1. S \<union> {Neg (P[App x []/0])} \<in> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f. psubst f ` S \<union> {Neg (psubst f P[App (f x) []/0])} \<in> C

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

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

goal:
No subgoals!
[PROOF STEP]
qed