[STATEMENT]
lemma canonic_int_validates_all_clauses :
  assumes "saturated_binary_rule ordered_resolvent S"
  assumes "all_fulfill finite S"
  assumes "{} \<notin> S"
  assumes "C \<in> S"
  shows "validate_clause (canonic_int_ordered S) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume "(tautology C)"
[PROOF STATE]
proof (state)
this:
tautology C

goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
tautology C

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
using tautologies_are_valid [of "C" "(canonic_int_ordered S)"]
[PROOF STATE]
proof (prove)
using this:
tautology C
tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume "\<not>tautology C"
[PROOF STATE]
proof (state)
this:
\<not> tautology C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from \<open>all_fulfill finite S\<close> and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
C \<in> S
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
C \<in> S

goal (1 subgoal):
 1. finite C
[PROOF STEP]
using all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
C \<in> S
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)

goal (1 subgoal):
 1. finite C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from \<open>{} \<notin> S\<close> and \<open>C \<in> S\<close> and \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
{} \<notin> S
C \<in> S
finite C
[PROOF STEP]
have "card C \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
{} \<notin> S
C \<in> S
finite C

goal (1 subgoal):
 1. card C \<noteq> 0
[PROOF STEP]
using card_0_eq
[PROOF STATE]
proof (prove)
using this:
{} \<notin> S
C \<in> S
finite C
finite ?A \<Longrightarrow> (card ?A = 0) = (?A = {})

goal (1 subgoal):
 1. card C \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C \<noteq> 0

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from \<open>\<not>tautology C\<close> and \<open>finite C\<close> and \<open>card C \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology C
finite C
card C \<noteq> 0
[PROOF STEP]
obtain "L"
      where "strictly_maximal_literal C L"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
finite C
card C \<noteq> 0

goal (1 subgoal):
 1. (\<And>L. strictly_maximal_literal C L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using strictly_maximal_literal_exists
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
finite C
card C \<noteq> 0
\<forall>C. finite C \<and> card C = ?n \<and> ?n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal (1 subgoal):
 1. (\<And>L. strictly_maximal_literal C L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal C L

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
obtain A where "A = atom L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. A = atom L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = atom L

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
have inductive_lemma:
    "\<forall>C L. ((C \<in> S) \<longrightarrow> (strictly_maximal_literal C L) \<longrightarrow> (A = (atom L))
      \<longrightarrow> (validate_clause (canonic_int_ordered S) C))" (is "(?Q A)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> A = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof ((rule wf_induct [of "atom_ordering" "?Q" "A"]),(rule atom_ordering_wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C) \<Longrightarrow> \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C) \<Longrightarrow> \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C) \<Longrightarrow> \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume hyp_induct: "\<forall>y. (y,x) \<in> atom_ordering \<longrightarrow> (?Q y)"
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C)

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C) \<Longrightarrow> \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
show "?Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof (rule)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C L. \<lbrakk>C \<in> S; strictly_maximal_literal C L; x = atom L\<rbrakk> \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
fix C L
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C L. \<lbrakk>C \<in> S; strictly_maximal_literal C L; x = atom L\<rbrakk> \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume "C \<in> S" "strictly_maximal_literal C L" "x = (atom L)"
[PROOF STATE]
proof (state)
this:
C \<in> S
strictly_maximal_literal C L
x = atom L

goal (1 subgoal):
 1. \<And>C L. \<lbrakk>C \<in> S; strictly_maximal_literal C L; x = atom L\<rbrakk> \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
show "validate_clause (canonic_int_ordered S) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume "L = Pos x"
[PROOF STATE]
proof (state)
this:
L = Pos x

goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from \<open>L = Pos x\<close> and \<open>strictly_maximal_literal C L\<close> and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos x
strictly_maximal_literal C L
C \<in> S
[PROOF STEP]
show "validate_clause (canonic_int_ordered S) C"
[PROOF STATE]
proof (prove)
using this:
L = Pos x
strictly_maximal_literal C L
C \<in> S

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
using int_validate_cl_with_pos_max
[PROOF STATE]
proof (prove)
using this:
L = Pos x
strictly_maximal_literal C L
C \<in> S
\<lbrakk>strictly_maximal_literal ?C (Pos ?A); ?C \<in> ?S\<rbrakk> \<Longrightarrow> canonic_int_ordered ?S \<Turnstile> ?C

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. L \<noteq> Pos x \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<noteq> Pos x \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume "L \<noteq> Pos x"
[PROOF STATE]
proof (state)
this:
L \<noteq> Pos x

goal (1 subgoal):
 1. L \<noteq> Pos x \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
have "L = (Neg x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = Neg x
[PROOF STEP]
using \<open>L \<noteq> Pos x\<close> \<open>x = atom L\<close> atom_property
[PROOF STATE]
proof (prove)
using this:
L \<noteq> Pos x
x = atom L
?A = atom ?L \<Longrightarrow> ?L = Pos ?A \<or> ?L = Neg ?A

goal (1 subgoal):
 1. L = Neg x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
L = Neg x

goal (1 subgoal):
 1. L \<noteq> Pos x \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
show "(validate_clause (canonic_int_ordered S) C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
assume  "\<not> (validate_clause(canonic_int_ordered S) C)"
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>(L = (Neg x))\<close> and \<open>(strictly_maximal_literal C L)\<close>
              and \<open>(\<not> (validate_clause (canonic_int_ordered S) C))\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Neg x
strictly_maximal_literal C L
\<not> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
have "x \<in> canonic_int_ordered S"
[PROOF STATE]
proof (prove)
using this:
L = Neg x
strictly_maximal_literal C L
\<not> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. x \<in> canonic_int_ordered S
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
L = Neg x
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
\<not> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. x \<in> canonic_int_ordered S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> canonic_int_ordered S

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> canonic_int_ordered S\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> canonic_int_ordered S
[PROOF STEP]
have "(canonic_int_fun_ordered x) S"
[PROOF STATE]
proof (prove)
using this:
x \<in> canonic_int_ordered S

goal (1 subgoal):
 1. canonic_int_fun_ordered x S
[PROOF STEP]
unfolding canonic_int_ordered_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {A. canonic_int_fun_ordered A S}

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

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>(canonic_int_fun_ordered x) S\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_fun_ordered x S
[PROOF STEP]
have "(\<exists> C. (C \<in> S) \<and> (strictly_maximal_literal C (Pos x) )
            \<and> ( \<forall> B. ( Pos B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> (\<not>(canonic_int_fun_ordered B) S)))
            \<and> ( \<forall> B. ( Neg B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> ((canonic_int_fun_ordered B) S))))"
[PROOF STATE]
proof (prove)
using this:
canonic_int_fun_ordered x S

goal (1 subgoal):
 1. \<exists>C. C \<in> S \<and> strictly_maximal_literal C (Pos x) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)
[PROOF STEP]
by (simp only: canonic_int_fun_ordered.simps [of x])
[PROOF STATE]
proof (state)
this:
\<exists>C. C \<in> S \<and> strictly_maximal_literal C (Pos x) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. C \<in> S \<and> strictly_maximal_literal C (Pos x) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)
[PROOF STEP]
obtain D
            where "(D \<in> S)" and "(strictly_maximal_literal D (Pos x))"
            and a: "( \<forall> B. ( Pos B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering
                  \<longrightarrow> (\<not>(canonic_int_fun_ordered B) S)))"
            and b: "( \<forall> B. ( Neg B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering
                      \<longrightarrow> ((canonic_int_fun_ordered B) S)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. C \<in> S \<and> strictly_maximal_literal C (Pos x) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> S; strictly_maximal_literal D (Pos x); \<forall>B. Pos B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S; \<forall>B. Neg B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D \<in> S
strictly_maximal_literal D (Pos x)
\<forall>B. Pos B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S
\<forall>B. Neg B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
obtain R where "R = (resolvent_upon D C x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>R. R = resolvent_upon D C x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R = resolvent_upon D C x

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>R = resolvent_upon D C x\<close> and \<open>strictly_maximal_literal D (Pos x)\<close>
              and \<open>strictly_maximal_literal C L\<close> and \<open>L = (Neg x)\<close>
[PROOF STATE]
proof (chain)
picking this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
[PROOF STEP]
have "resolvent D C R"
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
L = Neg x

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
using resolvent_upon_is_resolvent
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
L = Neg x
\<lbrakk>Pos ?A \<in> ?P1.0; Neg ?A \<in> ?P2.0\<rbrakk> \<Longrightarrow> resolvent ?P1.0 ?P2.0 (resolvent_upon ?P1.0 ?P2.0 ?A)

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolvent D C R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>R = resolvent_upon D C x\<close> and \<open>strictly_maximal_literal D (Pos x)\<close>
              and \<open>strictly_maximal_literal C L\<close> and \<open>L = Neg x\<close>
[PROOF STATE]
proof (chain)
picking this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
[PROOF STEP]
have "ordered_resolvent D C R"
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x

goal (1 subgoal):
 1. ordered_resolvent D C R
[PROOF STEP]
using ordered_resolvent_upon_is_resolvent
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
\<lbrakk>strictly_maximal_literal ?P1.0 (Pos ?A); strictly_maximal_literal ?P2.0 (Neg ?A)\<rbrakk> \<Longrightarrow> ordered_resolvent ?P1.0 ?P2.0 (resolvent_upon ?P1.0 ?P2.0 ?A)

goal (1 subgoal):
 1. ordered_resolvent D C R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ordered_resolvent D C R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
have "\<not> validate_clause (canonic_int_ordered S) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> R
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> R \<Longrightarrow> False
[PROOF STEP]
assume "validate_clause (canonic_int_ordered S) R"
[PROOF STATE]
proof (state)
this:
canonic_int_ordered S \<Turnstile> R

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> R \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_clause (canonic_int_ordered S) R\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered S \<Turnstile> R
[PROOF STEP]
obtain M
                where "(M \<in> R)" and "validate_literal (canonic_int_ordered S) M"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered S \<Turnstile> R

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>M \<in> R; canonic_int_ordered S \<Turnstile> M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<in> R
canonic_int_ordered S \<Turnstile> M

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> R \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> R\<close> and \<open>R = resolvent_upon D C x\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> R
R = resolvent_upon D C x
[PROOF STEP]
have "(M \<in> (D - { Pos x })) \<or> (M \<in> (C - { Neg x }))"
[PROOF STATE]
proof (prove)
using this:
M \<in> R
R = resolvent_upon D C x

goal (1 subgoal):
 1. M \<in> D - {Pos x} \<or> M \<in> C - {Neg x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<in> D - {Pos x} \<or> M \<in> C - {Neg x}

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> R \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
M \<in> D - {Pos x} \<or> M \<in> C - {Neg x}

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M \<in> D - {Pos x} \<Longrightarrow> False
 2. M \<in> C - {Neg x} \<Longrightarrow> False
[PROOF STEP]
assume "M \<in> (D - { Pos x })"
[PROOF STATE]
proof (state)
this:
M \<in> D - {Pos x}

goal (2 subgoals):
 1. M \<in> D - {Pos x} \<Longrightarrow> False
 2. M \<in> C - {Neg x} \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>AA. M = (Pos AA)"
[PROOF STATE]
proof (state)
this:
\<exists>AA. M = Pos AA

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>AA. M = Pos AA
[PROOF STEP]
obtain AA where "M = Pos AA"
[PROOF STATE]
proof (prove)
using this:
\<exists>AA. M = Pos AA

goal (1 subgoal):
 1. (\<And>AA. M = Pos AA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M = Pos AA

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> D - { Pos x }\<close> and \<open>strictly_maximal_literal D (Pos x)\<close>
                    and \<open>(M = Pos AA)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> D - {Pos x}
strictly_maximal_literal D (Pos x)
M = Pos AA
[PROOF STEP]
have "(AA,x) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
M \<in> D - {Pos x}
strictly_maximal_literal D (Pos x)
M = Pos AA

goal (1 subgoal):
 1. (AA, x) \<in> atom_ordering
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
M \<in> D - {Pos x}
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
M = Pos AA

goal (1 subgoal):
 1. (AA, x) \<in> atom_ordering
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(AA, x) \<in> atom_ordering

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from a and \<open>(AA,x) \<in> atom_ordering\<close> and \<open>M = (Pos AA)\<close> and \<open>M \<in> (D - { Pos x })\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>B. Pos B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S
(AA, x) \<in> atom_ordering
M = Pos AA
M \<in> D - {Pos x}
[PROOF STEP]
have "\<not>(canonic_int_fun_ordered AA) S"
[PROOF STATE]
proof (prove)
using this:
\<forall>B. Pos B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S
(AA, x) \<in> atom_ordering
M = Pos AA
M \<in> D - {Pos x}

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>(canonic_int_fun_ordered AA) S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_fun_ordered AA S
[PROOF STEP]
have "AA \<notin> canonic_int_ordered S"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_fun_ordered AA S

goal (1 subgoal):
 1. AA \<notin> canonic_int_ordered S
[PROOF STEP]
unfolding canonic_int_ordered_def
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_fun_ordered AA S

goal (1 subgoal):
 1. AA \<notin> {A. canonic_int_fun_ordered A S}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AA \<notin> canonic_int_ordered S

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>AA \<notin> canonic_int_ordered S\<close> and \<open>M = Pos AA\<close>
                    and \<open>validate_literal (canonic_int_ordered S) M\<close>
[PROOF STATE]
proof (chain)
picking this:
AA \<notin> canonic_int_ordered S
M = Pos AA
canonic_int_ordered S \<Turnstile> M
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
AA \<notin> canonic_int_ordered S
M = Pos AA
canonic_int_ordered S \<Turnstile> M

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

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(\<exists>AA. M = (Pos AA))"
[PROOF STATE]
proof (state)
this:
\<nexists>AA. M = Pos AA

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
obtain AA where "M = (Pos AA) \<or> M = (Neg AA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>AA. M = Pos AA \<or> M = Neg AA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of M]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. M = Pos x1 \<Longrightarrow> ?P; \<And>x2. M = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>AA. M = Pos AA \<or> M = Neg AA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M = Pos AA \<or> M = Neg AA

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>(\<exists>AA. M = (Pos AA))\<close>
[PROOF STATE]
proof (chain)
picking this:
M = Pos AA \<or> M = Neg AA
\<nexists>AA. M = Pos AA
[PROOF STEP]
have "M = (Neg AA)"
[PROOF STATE]
proof (prove)
using this:
M = Pos AA \<or> M = Neg AA
\<nexists>AA. M = Pos AA

goal (1 subgoal):
 1. M = Neg AA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M = Neg AA

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> (D - { Pos x })\<close> and \<open>strictly_maximal_literal D (Pos x)\<close>
                    and \<open>M = (Neg AA)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> D - {Pos x}
strictly_maximal_literal D (Pos x)
M = Neg AA
[PROOF STEP]
have "(AA,x) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
M \<in> D - {Pos x}
strictly_maximal_literal D (Pos x)
M = Neg AA

goal (1 subgoal):
 1. (AA, x) \<in> atom_ordering
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
M \<in> D - {Pos x}
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
M = Neg AA

goal (1 subgoal):
 1. (AA, x) \<in> atom_ordering
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(AA, x) \<in> atom_ordering

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
from b and \<open>(AA,x) \<in> atom_ordering\<close> and \<open>M = (Neg AA)\<close> and \<open>M \<in> (D - { Pos x })\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>B. Neg B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S
(AA, x) \<in> atom_ordering
M = Neg AA
M \<in> D - {Pos x}
[PROOF STEP]
have "(canonic_int_fun_ordered AA) S"
[PROOF STATE]
proof (prove)
using this:
\<forall>B. Neg B \<in> D \<longrightarrow> (B, x) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S
(AA, x) \<in> atom_ordering
M = Neg AA
M \<in> D - {Pos x}

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

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
from \<open>(canonic_int_fun_ordered AA) S\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_fun_ordered AA S
[PROOF STEP]
have "AA \<in> canonic_int_ordered S"
[PROOF STATE]
proof (prove)
using this:
canonic_int_fun_ordered AA S

goal (1 subgoal):
 1. AA \<in> canonic_int_ordered S
[PROOF STEP]
unfolding canonic_int_ordered_def
[PROOF STATE]
proof (prove)
using this:
canonic_int_fun_ordered AA S

goal (1 subgoal):
 1. AA \<in> {A. canonic_int_fun_ordered A S}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AA \<in> canonic_int_ordered S

goal (1 subgoal):
 1. \<nexists>AA. M = Pos AA \<Longrightarrow> False
[PROOF STEP]
from \<open>AA \<in> canonic_int_ordered S\<close> and \<open>M = (Neg AA)\<close>
                    and \<open>validate_literal (canonic_int_ordered S) M\<close>
[PROOF STATE]
proof (chain)
picking this:
AA \<in> canonic_int_ordered S
M = Neg AA
canonic_int_ordered S \<Turnstile> M
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
AA \<in> canonic_int_ordered S
M = Neg AA
canonic_int_ordered S \<Turnstile> M

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. M \<in> C - {Neg x} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M \<in> C - {Neg x} \<Longrightarrow> False
[PROOF STEP]
assume "M \<in> (C - { Neg x })"
[PROOF STATE]
proof (state)
this:
M \<in> C - {Neg x}

goal (1 subgoal):
 1. M \<in> C - {Neg x} \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>validate_clause(canonic_int_ordered S) C\<close> and \<open>M \<in> (C - { Neg x })\<close>
                and \<open>validate_literal (canonic_int_ordered S) M\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered S \<Turnstile> C
M \<in> C - {Neg x}
canonic_int_ordered S \<Turnstile> M
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered S \<Turnstile> C
M \<in> C - {Neg x}
canonic_int_ordered S \<Turnstile> M

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered S \<Turnstile> R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>validate_clause (canonic_int_ordered S) R\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered S \<Turnstile> R
[PROOF STEP]
have "\<not>tautology R"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered S \<Turnstile> R

goal (1 subgoal):
 1. \<not> tautology R
[PROOF STEP]
using tautologies_are_valid
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered S \<Turnstile> R
tautology ?C \<Longrightarrow> ?I \<Turnstile> ?C

goal (1 subgoal):
 1. \<not> tautology R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> tautology R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>ordered_resolvent D C R\<close> and \<open>D \<in> S\<close> and \<open>C \<in> S\<close>
              and \<open>saturated_binary_rule ordered_resolvent S\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_resolvent D C R
D \<in> S
C \<in> S
saturated_binary_rule ordered_resolvent S
[PROOF STEP]
have "redundant R S"
[PROOF STATE]
proof (prove)
using this:
ordered_resolvent D C R
D \<in> S
C \<in> S
saturated_binary_rule ordered_resolvent S

goal (1 subgoal):
 1. redundant R S
[PROOF STEP]
unfolding saturated_binary_rule_def
[PROOF STATE]
proof (prove)
using this:
ordered_resolvent D C R
D \<in> S
C \<in> S
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_resolvent P1 P2 C \<longrightarrow> redundant C S

goal (1 subgoal):
 1. redundant R S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant R S

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>tautology R\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant R S
\<not> tautology R
[PROOF STEP]
obtain R' where "R' \<in> S" and "subsumes R' R"
[PROOF STATE]
proof (prove)
using this:
redundant R S
\<not> tautology R

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R' \<in> S; subsumes R' R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology R \<or> (\<exists>D. D \<in> S \<and> subsumes D R)
\<not> tautology R

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R' \<in> S; subsumes R' R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<in> S
subsumes R' R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>R = resolvent_upon D C x\<close> and \<open>strictly_maximal_literal D (Pos x)\<close>
              and \<open>strictly_maximal_literal C L\<close> and \<open>L = (Neg x)\<close>
[PROOF STATE]
proof (chain)
picking this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
[PROOF STEP]
have "resolvent D C R"
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
L = Neg x

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
using resolvent_upon_is_resolvent
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
Pos x \<in> D \<and> (\<forall>B. B \<in> D \<and> Pos x \<noteq> B \<longrightarrow> literal_ordering B (Pos x))
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
L = Neg x
\<lbrakk>Pos ?A \<in> ?P1.0; Neg ?A \<in> ?P2.0\<rbrakk> \<Longrightarrow> resolvent ?P1.0 ?P2.0 (resolvent_upon ?P1.0 ?P2.0 ?A)

goal (1 subgoal):
 1. resolvent D C R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolvent D C R

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>all_fulfill finite S\<close> and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
C \<in> S
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
C \<in> S

goal (1 subgoal):
 1. finite C
[PROOF STEP]
using all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
C \<in> S
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)

goal (1 subgoal):
 1. finite C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite C

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>all_fulfill finite S\<close> and \<open>D \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
D \<in> S
[PROOF STEP]
have "finite D"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
D \<in> S

goal (1 subgoal):
 1. finite D
[PROOF STEP]
using all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
D \<in> S
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)

goal (1 subgoal):
 1. finite D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite D

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>finite C\<close> and \<open>finite D\<close> and  \<open>(resolvent D C R)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite C
finite D
resolvent D C R
[PROOF STEP]
have "finite R"
[PROOF STATE]
proof (prove)
using this:
finite C
finite D
resolvent D C R

goal (1 subgoal):
 1. finite R
[PROOF STEP]
using resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
finite C
finite D
resolvent D C R
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. finite R
[PROOF STEP]
unfolding derived_clauses_are_finite_def
[PROOF STATE]
proof (prove)
using this:
finite C
finite D
resolvent D C R
\<forall>P1 P2 C. finite P1 \<longrightarrow> finite P2 \<longrightarrow> resolvent P1 P2 C \<longrightarrow> finite C

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

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>finite R\<close> and \<open>subsumes R' R\<close>
[PROOF STATE]
proof (chain)
picking this:
finite R
subsumes R' R
[PROOF STEP]
have "finite R'"
[PROOF STATE]
proof (prove)
using this:
finite R
subsumes R' R

goal (1 subgoal):
 1. finite R'
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
finite R
R' \<subseteq> R

goal (1 subgoal):
 1. finite R'
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
finite R
R' \<subseteq> R
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite R'

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>R' \<in> S\<close> and \<open>{} \<notin> S\<close> and \<open>(subsumes R' R)\<close>
[PROOF STATE]
proof (chain)
picking this:
R' \<in> S
{} \<notin> S
subsumes R' R
[PROOF STEP]
have "R' \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
R' \<in> S
{} \<notin> S
subsumes R' R

goal (1 subgoal):
 1. R' \<noteq> {}
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
R' \<in> S
{} \<notin> S
R' \<subseteq> R

goal (1 subgoal):
 1. R' \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<noteq> {}

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>finite R'\<close> and \<open>R' \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite R'
R' \<noteq> {}
[PROOF STEP]
have "card R' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite R'
R' \<noteq> {}

goal (1 subgoal):
 1. card R' \<noteq> 0
[PROOF STEP]
using card_0_eq
[PROOF STATE]
proof (prove)
using this:
finite R'
R' \<noteq> {}
finite ?A \<Longrightarrow> (card ?A = 0) = (?A = {})

goal (1 subgoal):
 1. card R' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card R' \<noteq> 0

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>subsumes R' R\<close> and \<open>\<not>tautology R\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes R' R
\<not> tautology R
[PROOF STEP]
have "\<not>tautology R'"
[PROOF STATE]
proof (prove)
using this:
subsumes R' R
\<not> tautology R

goal (1 subgoal):
 1. \<not> tautology R'
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> R
\<not> tautology R

goal (1 subgoal):
 1. \<not> tautology R'
[PROOF STEP]
using tautology_monotonous
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> R
\<not> tautology R
\<lbrakk>tautology ?C; ?C \<subseteq> ?D\<rbrakk> \<Longrightarrow> tautology ?D

goal (1 subgoal):
 1. \<not> tautology R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> tautology R'

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>tautology R'\<close> and \<open>finite R'\<close>  and \<open>card R' \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology R'
finite R'
card R' \<noteq> 0
[PROOF STEP]
obtain "LR'"
              where "strictly_maximal_literal R' LR'"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology R'
finite R'
card R' \<noteq> 0

goal (1 subgoal):
 1. (\<And>LR'. strictly_maximal_literal R' LR' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using strictly_maximal_literal_exists
[PROOF STATE]
proof (prove)
using this:
\<not> tautology R'
finite R'
card R' \<noteq> 0
\<forall>C. finite C \<and> card C = ?n \<and> ?n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal (1 subgoal):
 1. (\<And>LR'. strictly_maximal_literal R' LR' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal R' LR'

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>finite R\<close> and \<open>finite R'\<close> and \<open>card R' \<noteq> 0\<close> and \<open>subsumes R' R\<close>
[PROOF STATE]
proof (chain)
picking this:
finite R
finite R'
card R' \<noteq> 0
subsumes R' R
[PROOF STEP]
have "card R \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite R
finite R'
card R' \<noteq> 0
subsumes R' R

goal (1 subgoal):
 1. card R \<noteq> 0
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
finite R
finite R'
card R' \<noteq> 0
R' \<subseteq> R

goal (1 subgoal):
 1. card R \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card R \<noteq> 0

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>tautology R\<close> and \<open>finite R\<close>  and \<open>card R \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology R
finite R
card R \<noteq> 0
[PROOF STEP]
obtain "LR"
              where "strictly_maximal_literal R LR"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology R
finite R
card R \<noteq> 0

goal (1 subgoal):
 1. (\<And>LR. strictly_maximal_literal R LR \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using strictly_maximal_literal_exists
[PROOF STATE]
proof (prove)
using this:
\<not> tautology R
finite R
card R \<noteq> 0
\<forall>C. finite C \<and> card C = ?n \<and> ?n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal (1 subgoal):
 1. (\<And>LR. strictly_maximal_literal R LR \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal R LR

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
obtain AR and AR' where "AR = atom LR" and "AR' = atom LR'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>AR AR'. \<lbrakk>AR = atom LR; AR' = atom LR'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AR = atom LR
AR' = atom LR'

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>subsumes R' R\<close> and \<open>AR = atom LR\<close> and \<open>AR' = atom LR'\<close>
              and \<open>(strictly_maximal_literal R LR)\<close>
              and \<open>(strictly_maximal_literal R' LR')\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes R' R
AR = atom LR
AR' = atom LR'
strictly_maximal_literal R LR
strictly_maximal_literal R' LR'
[PROOF STEP]
have "(AR' = AR) \<or> (AR',AR) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
subsumes R' R
AR = atom LR
AR' = atom LR'
strictly_maximal_literal R LR
strictly_maximal_literal R' LR'

goal (1 subgoal):
 1. AR' = AR \<or> (AR', AR) \<in> atom_ordering
[PROOF STEP]
using subsumption_and_max_literal
[PROOF STATE]
proof (prove)
using this:
subsumes R' R
AR = atom LR
AR' = atom LR'
strictly_maximal_literal R LR
strictly_maximal_literal R' LR'
\<lbrakk>subsumes ?C1.0 ?C2.0; strictly_maximal_literal ?C1.0 ?L1.0; strictly_maximal_literal ?C2.0 ?L2.0; ?A1.0 = atom ?L1.0; ?A2.0 = atom ?L2.0\<rbrakk> \<Longrightarrow> ?A1.0 = ?A2.0 \<or> (?A1.0, ?A2.0) \<in> atom_ordering

goal (1 subgoal):
 1. AR' = AR \<or> (AR', AR) \<in> atom_ordering
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AR' = AR \<or> (AR', AR) \<in> atom_ordering

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>R = (resolvent_upon D C x)\<close> and \<open>AR = atom LR\<close>
              and \<open>strictly_maximal_literal R LR\<close>
              and \<open>strictly_maximal_literal D (Pos x)\<close>
              and \<open>strictly_maximal_literal C L\<close> and \<open>L = (Neg x)\<close>
[PROOF STATE]
proof (chain)
picking this:
R = resolvent_upon D C x
AR = atom LR
strictly_maximal_literal R LR
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
[PROOF STEP]
have "(AR,x) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
AR = atom LR
strictly_maximal_literal R LR
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x

goal (1 subgoal):
 1. (AR, x) \<in> atom_ordering
[PROOF STEP]
using resolution_and_max_literal
[PROOF STATE]
proof (prove)
using this:
R = resolvent_upon D C x
AR = atom LR
strictly_maximal_literal R LR
strictly_maximal_literal D (Pos x)
strictly_maximal_literal C L
L = Neg x
\<lbrakk>?R = resolvent_upon ?P1.0 ?P2.0 ?A; strictly_maximal_literal ?P1.0 (Pos ?A); strictly_maximal_literal ?P2.0 (Neg ?A); strictly_maximal_literal ?R ?M\<rbrakk> \<Longrightarrow> (atom ?M, ?A) \<in> atom_ordering

goal (1 subgoal):
 1. (AR, x) \<in> atom_ordering
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(AR, x) \<in> atom_ordering

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from \<open>(AR,x) \<in> atom_ordering\<close> and \<open>(AR' = AR) \<or> (AR',AR) \<in> atom_ordering\<close>
[PROOF STATE]
proof (chain)
picking this:
(AR, x) \<in> atom_ordering
AR' = AR \<or> (AR', AR) \<in> atom_ordering
[PROOF STEP]
have "(AR',x) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
(AR, x) \<in> atom_ordering
AR' = AR \<or> (AR', AR) \<in> atom_ordering

goal (1 subgoal):
 1. (AR', x) \<in> atom_ordering
[PROOF STEP]
using atom_ordering_trans
[PROOF STATE]
proof (prove)
using this:
(AR, x) \<in> atom_ordering
AR' = AR \<or> (AR', AR) \<in> atom_ordering
\<forall>x y z. (x, y) \<in> atom_ordering \<longrightarrow> (y, z) \<in> atom_ordering \<longrightarrow> (x, z) \<in> atom_ordering

goal (1 subgoal):
 1. (AR', x) \<in> atom_ordering
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(AR', x) \<in> atom_ordering

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from this and hyp_induct and \<open>R' \<in> S\<close> and \<open>strictly_maximal_literal R' LR'\<close>
              and \<open>AR' = atom LR'\<close>
[PROOF STATE]
proof (chain)
picking this:
(AR', x) \<in> atom_ordering
\<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C)
R' \<in> S
strictly_maximal_literal R' LR'
AR' = atom LR'
[PROOF STEP]
have "validate_clause (canonic_int_ordered S) R'"
[PROOF STATE]
proof (prove)
using this:
(AR', x) \<in> atom_ordering
\<forall>y. (y, x) \<in> atom_ordering \<longrightarrow> (\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> y = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C)
R' \<in> S
strictly_maximal_literal R' LR'
AR' = atom LR'

goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonic_int_ordered S \<Turnstile> R'

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>subsumes R' R\<close> and \<open>\<not>validate_clause (canonic_int_ordered S) R\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered S \<Turnstile> R'
subsumes R' R
\<not> canonic_int_ordered S \<Turnstile> R
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered S \<Turnstile> R'
subsumes R' R
\<not> canonic_int_ordered S \<Turnstile> R

goal (1 subgoal):
 1. False
[PROOF STEP]
using subsumption_and_semantics
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered S \<Turnstile> R'
subsumes R' R
\<not> canonic_int_ordered S \<Turnstile> R
\<lbrakk>subsumes ?C ?D; ?I \<Turnstile> ?C\<rbrakk> \<Longrightarrow> ?I \<Turnstile> ?D

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:
canonic_int_ordered S \<Turnstile> C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> x = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> A = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from inductive_lemma and \<open>C \<in> S\<close> and \<open>strictly_maximal_literal C L\<close> and \<open>A = atom L\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> A = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
C \<in> S
strictly_maximal_literal C L
A = atom L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>C L. C \<in> S \<longrightarrow> strictly_maximal_literal C L \<longrightarrow> A = atom L \<longrightarrow> canonic_int_ordered S \<Turnstile> C
C \<in> S
strictly_maximal_literal C L
A = atom L

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ordered_resolution_is_complete :
  "Complete ordered_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete ordered_resolvent
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Complete ordered_resolvent \<Longrightarrow> False
[PROOF STEP]
assume "\<not> Complete ordered_resolvent"
[PROOF STATE]
proof (state)
this:
\<not> Complete ordered_resolvent

goal (1 subgoal):
 1. \<not> Complete ordered_resolvent \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Complete ordered_resolvent
[PROOF STEP]
obtain S where "saturated_binary_rule ordered_resolvent S"
    and "all_fulfill finite S" and "{} \<notin> S" and "\<not>satisfiable S"
[PROOF STATE]
proof (prove)
using this:
\<not> Complete ordered_resolvent

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>saturated_binary_rule ordered_resolvent S; all_fulfill finite S; {} \<notin> S; \<not> satisfiable S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Complete_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>S. saturated_binary_rule ordered_resolvent S \<longrightarrow> all_fulfill finite S \<longrightarrow> {} \<notin> S \<longrightarrow> satisfiable S)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>saturated_binary_rule ordered_resolvent S; all_fulfill finite S; {} \<notin> S; \<not> satisfiable S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
saturated_binary_rule ordered_resolvent S
all_fulfill finite S
{} \<notin> S
\<not> satisfiable S

goal (1 subgoal):
 1. \<not> Complete ordered_resolvent \<Longrightarrow> False
[PROOF STEP]
have "validate_formula (canonic_int_ordered S) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>validate_formula (canonic_int_ordered S) S"
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered S \<Turnstile> S

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered S \<Turnstile> S
[PROOF STEP]
obtain C where "C \<in> S" and "\<not>validate_clause (canonic_int_ordered S) C"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered S \<Turnstile> S

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

goal (1 subgoal):
 1. \<not> canonic_int_ordered S \<Turnstile> S \<Longrightarrow> False
[PROOF STEP]
from \<open>saturated_binary_rule ordered_resolvent S\<close> and \<open>all_fulfill finite S\<close> and \<open>{} \<notin> S\<close>
      and \<open>C \<in> S\<close> and \<open>\<not>validate_clause (canonic_int_ordered S) C\<close>
[PROOF STATE]
proof (chain)
picking this:
saturated_binary_rule ordered_resolvent S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule ordered_resolvent S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered S \<Turnstile> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using canonic_int_validates_all_clauses
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule ordered_resolvent S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered S \<Turnstile> C
\<lbrakk>saturated_binary_rule ordered_resolvent ?S; all_fulfill finite ?S; {} \<notin> ?S; ?C \<in> ?S\<rbrakk> \<Longrightarrow> canonic_int_ordered ?S \<Turnstile> ?C

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

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

goal (1 subgoal):
 1. \<not> Complete ordered_resolvent \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_formula (canonic_int_ordered S) S\<close> and \<open>\<not>satisfiable S\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered S \<Turnstile> S
\<not> satisfiable S
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered S \<Turnstile> S
\<not> satisfiable S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding satisfiable_def
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered S \<Turnstile> S
\<nexists>I. I \<Turnstile> S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma saturated_ordered_sel_res_empty_sel :
  assumes "saturated_binary_rule (ordered_sel_resolvent Sel) S"
  shows "saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)"
[PROOF STATE]
proof (state)
this:
\<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
obtain P1 and P2 and C
    where "P1 \<in> empty_selected_part Sel S" and "P2 \<in> empty_selected_part Sel S"
      and "ordered_resolvent P1 P2 C"
      and "\<not>redundant C (empty_selected_part Sel S)"
[PROOF STATE]
proof (prove)
using this:
\<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>P1 \<in> empty_selected_part Sel S; P2 \<in> empty_selected_part Sel S; ordered_resolvent P1 P2 C; \<not> redundant C (empty_selected_part Sel S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding "saturated_binary_rule_def"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>P1 P2 C. P1 \<in> empty_selected_part Sel S \<and> P2 \<in> empty_selected_part Sel S \<and> ordered_resolvent P1 P2 C \<longrightarrow> redundant C (empty_selected_part Sel S))

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>P1 \<in> empty_selected_part Sel S; P2 \<in> empty_selected_part Sel S; ordered_resolvent P1 P2 C; \<not> redundant C (empty_selected_part Sel S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P1 \<in> empty_selected_part Sel S
P2 \<in> empty_selected_part Sel S
ordered_resolvent P1 P2 C
\<not> redundant C (empty_selected_part Sel S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>ordered_resolvent P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_resolvent P1 P2 C
[PROOF STEP]
obtain A where "C = ( (P1 - { Pos A}) \<union> ( P2 - { Neg A }))"
      and "strictly_maximal_literal P1 (Pos A)" and  "strictly_maximal_literal P2 (Neg A)"
[PROOF STATE]
proof (prove)
using this:
ordered_resolvent P1 P2 C

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>C = P1 - {Pos A} \<union> (P2 - {Neg A}); strictly_maximal_literal P1 (Pos A); strictly_maximal_literal P2 (Neg A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ordered_resolvent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>A. C = P1 - {Pos A} \<union> (P2 - {Neg A}) \<and> strictly_maximal_literal P1 (Pos A) \<and> strictly_maximal_literal P2 (Neg A)

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>C = P1 - {Pos A} \<union> (P2 - {Neg A}); strictly_maximal_literal P1 (Pos A); strictly_maximal_literal P2 (Neg A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal P2 (Neg A)

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from  \<open>P1 \<in> empty_selected_part Sel S\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> empty_selected_part Sel S
[PROOF STEP]
have "selected_part Sel P1 = {}"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> empty_selected_part Sel S

goal (1 subgoal):
 1. selected_part Sel P1 = {}
[PROOF STEP]
unfolding empty_selected_part_def
[PROOF STATE]
proof (prove)
using this:
P1 \<in> {C \<in> S. selected_part Sel C = {}}

goal (1 subgoal):
 1. selected_part Sel P1 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel P1 = {}

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from  \<open>P2 \<in> empty_selected_part Sel S\<close>
[PROOF STATE]
proof (chain)
picking this:
P2 \<in> empty_selected_part Sel S
[PROOF STEP]
have "selected_part Sel P2 = {}"
[PROOF STATE]
proof (prove)
using this:
P2 \<in> empty_selected_part Sel S

goal (1 subgoal):
 1. selected_part Sel P2 = {}
[PROOF STEP]
unfolding empty_selected_part_def
[PROOF STATE]
proof (prove)
using this:
P2 \<in> {C \<in> S. selected_part Sel C = {}}

goal (1 subgoal):
 1. selected_part Sel P2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel P2 = {}

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>C = ( (P1 - { Pos A}) \<union> ( P2 - { Neg A }))\<close> and \<open>strictly_maximal_literal P1 (Pos A)\<close>
    and \<open>strictly_maximal_literal P2 (Neg A)\<close> and \<open>(selected_part Sel P1) = {}\<close>
    and \<open>selected_part Sel P2 = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal P2 (Neg A)
selected_part Sel P1 = {}
selected_part Sel P2 = {}
[PROOF STEP]
have "ordered_sel_resolvent Sel P1 P2 C"
[PROOF STATE]
proof (prove)
using this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal P2 (Neg A)
selected_part Sel P1 = {}
selected_part Sel P2 = {}

goal (1 subgoal):
 1. ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
unfolding ordered_sel_resolvent_def
[PROOF STATE]
proof (prove)
using this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal P2 (Neg A)
selected_part Sel P1 = {}
selected_part Sel P2 = {}

goal (1 subgoal):
 1. \<exists>A. C = P1 - {Pos A} \<union> (P2 - {Neg A}) \<and> strictly_maximal_literal P1 (Pos A) \<and> selected_part Sel P1 = {} \<and> (strictly_maximal_literal P2 (Neg A) \<and> selected_part Sel P2 = {} \<or> strictly_maximal_literal (selected_part Sel P2) (Neg A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ordered_sel_resolvent Sel P1 P2 C

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>saturated_binary_rule (ordered_sel_resolvent Sel) S\<close>
[PROOF STATE]
proof (chain)
picking this:
saturated_binary_rule (ordered_sel_resolvent Sel) S
[PROOF STEP]
have "\<forall>P1 P2 C. (P1 \<in> S \<and> P2 \<in> S \<and> (ordered_sel_resolvent Sel P1 P2 C)) \<longrightarrow> redundant C S"
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent Sel) S

goal (1 subgoal):
 1. \<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S
[PROOF STEP]
unfolding saturated_binary_rule_def
[PROOF STATE]
proof (prove)
using this:
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S

goal (1 subgoal):
 1. \<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>P1 \<in> (empty_selected_part Sel S)\<close> and \<open>P2 \<in> (empty_selected_part Sel S)\<close>
    and \<open>ordered_sel_resolvent Sel P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S
P1 \<in> empty_selected_part Sel S
P2 \<in> empty_selected_part Sel S
ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
have "tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> redundant C S
P1 \<in> empty_selected_part Sel S
P2 \<in> empty_selected_part Sel S
ordered_sel_resolvent Sel P1 P2 C

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
[PROOF STEP]
unfolding empty_selected_part_def redundant_def
[PROOF STATE]
proof (prove)
using this:
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_sel_resolvent Sel P1 P2 C \<longrightarrow> tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
P1 \<in> {C \<in> S. selected_part Sel C = {}}
P2 \<in> {C \<in> S. selected_part Sel C = {}}
ordered_sel_resolvent Sel P1 P2 C

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)\<close>
      and \<open>\<not>redundant C (empty_selected_part Sel S)\<close>
[PROOF STATE]
proof (chain)
picking this:
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
\<not> redundant C (empty_selected_part Sel S)
[PROOF STEP]
obtain D where "D \<in> S" and "subsumes D C" and "D \<notin> empty_selected_part Sel S"
[PROOF STATE]
proof (prove)
using this:
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
\<not> redundant C (empty_selected_part Sel S)

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> S; subsumes D C; D \<notin> empty_selected_part Sel S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
\<not> (tautology C \<or> (\<exists>D. D \<in> empty_selected_part Sel S \<and> subsumes D C))

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> S; subsumes D C; D \<notin> empty_selected_part Sel S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<in> S
subsumes D C
D \<notin> empty_selected_part Sel S

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>D \<notin> empty_selected_part Sel S\<close> and \<open>D \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<notin> empty_selected_part Sel S
D \<in> S
[PROOF STEP]
obtain B where "B \<in> Sel" and "Neg B \<in> D"
[PROOF STATE]
proof (prove)
using this:
D \<notin> empty_selected_part Sel S
D \<in> S

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<in> Sel; Neg B \<in> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding empty_selected_part_def selected_part_def
[PROOF STATE]
proof (prove)
using this:
D \<notin> {C \<in> S. {L \<in> C. \<exists>A\<in>Sel. L = Neg A} = {}}
D \<in> S

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<in> Sel; Neg B \<in> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> Sel
Neg B \<in> D

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>Neg B \<in> D\<close> this and \<open>subsumes D C\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg B \<in> D
B \<in> Sel
Neg B \<in> D
subsumes D C
[PROOF STEP]
have "Neg B \<in> C"
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> D
B \<in> Sel
Neg B \<in> D
subsumes D C

goal (1 subgoal):
 1. Neg B \<in> C
[PROOF STEP]
unfolding subsumes_def
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> D
B \<in> Sel
Neg B \<in> D
D \<subseteq> C

goal (1 subgoal):
 1. Neg B \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg B \<in> C

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C = ( (P1 - { Pos A}) \<union> ( P2 - { Neg A }))\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg B \<in> C
C = P1 - {Pos A} \<union> (P2 - {Neg A})
[PROOF STEP]
have "Neg B \<in> (P1 \<union> P2)"
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> C
C = P1 - {Pos A} \<union> (P2 - {Neg A})

goal (1 subgoal):
 1. Neg B \<in> P1 \<union> P2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg B \<in> P1 \<union> P2

goal (1 subgoal):
 1. \<not> saturated_binary_rule ordered_resolvent (empty_selected_part Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>Neg B \<in> (P1 \<union> P2)\<close> and \<open>P1 \<in> empty_selected_part Sel S\<close>
      and \<open>P2 \<in> empty_selected_part Sel S\<close> and \<open>B \<in> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg B \<in> P1 \<union> P2
P1 \<in> empty_selected_part Sel S
P2 \<in> empty_selected_part Sel S
B \<in> Sel
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> P1 \<union> P2
P1 \<in> empty_selected_part Sel S
P2 \<in> empty_selected_part Sel S
B \<in> Sel

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding empty_selected_part_def selected_part_def
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> P1 \<union> P2
P1 \<in> {C \<in> S. {L \<in> C. \<exists>A\<in>Sel. L = Neg A} = {}}
P2 \<in> {C \<in> S. {L \<in> C. \<exists>A\<in>Sel. L = Neg A} = {}}
B \<in> Sel

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordered_sel_resolvent_upon_is_resolvent:
  assumes "ordered_sel_resolvent_upon Sel P1 P2 C A"
  shows "ordered_sel_resolvent Sel P1 P2 C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent_upon Sel P1 P2 C A

goal (1 subgoal):
 1. ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
unfolding ordered_sel_resolvent_upon_def and ordered_sel_resolvent_def
[PROOF STATE]
proof (prove)
using this:
C = P1 - {Pos A} \<union> (P2 - {Neg A}) \<and> strictly_maximal_literal P1 (Pos A) \<and> selected_part Sel P1 = {} \<and> (strictly_maximal_literal P2 (Neg A) \<and> selected_part Sel P2 = {} \<or> strictly_maximal_literal (selected_part Sel P2) (Neg A))

goal (1 subgoal):
 1. \<exists>A. C = P1 - {Pos A} \<union> (P2 - {Neg A}) \<and> strictly_maximal_literal P1 (Pos A) \<and> selected_part Sel P1 = {} \<and> (strictly_maximal_literal P2 (Neg A) \<and> selected_part Sel P2 = {} \<or> strictly_maximal_literal (selected_part Sel P2) (Neg A))
[PROOF STEP]
by auto


[STATEMENT]
lemma resolution_decreases_selected_part:
  assumes "ordered_sel_resolvent_upon Sel P1 P2 C A"
  assumes "Neg A \<in> P2"
  assumes "finite P1"
  assumes "finite P2"
  assumes "card (selected_part Sel P2) = Suc n"
  shows "card (selected_part Sel C) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>finite P2\<close>
[PROOF STATE]
proof (chain)
picking this:
finite P2
[PROOF STEP]
have "finite (selected_part Sel P2)"
[PROOF STATE]
proof (prove)
using this:
finite P2

goal (1 subgoal):
 1. finite (selected_part Sel P2)
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
finite P2

goal (1 subgoal):
 1. finite {L \<in> P2. \<exists>A\<in>Sel. L = Neg A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (selected_part Sel P2)

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>card (selected_part Sel P2) = (Suc n)\<close>
[PROOF STATE]
proof (chain)
picking this:
card (selected_part Sel P2) = Suc n
[PROOF STEP]
have "card (selected_part Sel P2) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel P2) = Suc n

goal (1 subgoal):
 1. card (selected_part Sel P2) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (selected_part Sel P2) \<noteq> 0

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this and \<open>finite (selected_part Sel P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
card (selected_part Sel P2) \<noteq> 0
finite (selected_part Sel P2)
[PROOF STEP]
have "selected_part Sel P2 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel P2) \<noteq> 0
finite (selected_part Sel P2)

goal (1 subgoal):
 1. selected_part Sel P2 \<noteq> {}
[PROOF STEP]
using card_0_eq
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel P2) \<noteq> 0
finite (selected_part Sel P2)
finite ?A \<Longrightarrow> (card ?A = 0) = (?A = {})

goal (1 subgoal):
 1. selected_part Sel P2 \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel P2 \<noteq> {}

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this and \<open>ordered_sel_resolvent_upon Sel P1 P2 C A\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part Sel P2 \<noteq> {}
ordered_sel_resolvent_upon Sel P1 P2 C A
[PROOF STEP]
have
    "C = (P1 - { Pos A}) \<union> ( P2 - { Neg A })"
      and "selected_part Sel P1 = {}" and  "strictly_maximal_literal (selected_part Sel P2) (Neg A)"
[PROOF STATE]
proof (prove)
using this:
selected_part Sel P2 \<noteq> {}
ordered_sel_resolvent_upon Sel P1 P2 C A

goal (1 subgoal):
 1. C = P1 - {Pos A} \<union> (P2 - {Neg A}) &&& selected_part Sel P1 = {} &&& strictly_maximal_literal (selected_part Sel P2) (Neg A)
[PROOF STEP]
unfolding ordered_sel_resolvent_upon_def
[PROOF STATE]
proof (prove)
using this:
selected_part Sel P2 \<noteq> {}
C = P1 - {Pos A} \<union> (P2 - {Neg A}) \<and> strictly_maximal_literal P1 (Pos A) \<and> selected_part Sel P1 = {} \<and> (strictly_maximal_literal P2 (Neg A) \<and> selected_part Sel P2 = {} \<or> strictly_maximal_literal (selected_part Sel P2) (Neg A))

goal (1 subgoal):
 1. C = P1 - {Pos A} \<union> (P2 - {Neg A}) &&& selected_part Sel P1 = {} &&& strictly_maximal_literal (selected_part Sel P2) (Neg A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
selected_part Sel P1 = {}
strictly_maximal_literal (selected_part Sel P2) (Neg A)

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>strictly_maximal_literal (selected_part Sel P2) (Neg A)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (selected_part Sel P2) (Neg A)
[PROOF STEP]
have "Neg A \<in> selected_part Sel P2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (selected_part Sel P2) (Neg A)

goal (1 subgoal):
 1. Neg A \<in> selected_part Sel P2
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> selected_part Sel P2 \<and> (\<forall>B. B \<in> selected_part Sel P2 \<and> Neg A \<noteq> B \<longrightarrow> literal_ordering B (Neg A))

goal (1 subgoal):
 1. Neg A \<in> selected_part Sel P2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg A \<in> selected_part Sel P2

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> selected_part Sel P2
[PROOF STEP]
have "A \<in> Sel"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> selected_part Sel P2

goal (1 subgoal):
 1. A \<in> Sel
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> {L \<in> P2. \<exists>A\<in>Sel. L = Neg A}

goal (1 subgoal):
 1. A \<in> Sel
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> Sel

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>selected_part Sel P1 = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part Sel P1 = {}
[PROOF STEP]
have "selected_part Sel (P1 - { Pos A}) = {}"
[PROOF STATE]
proof (prove)
using this:
selected_part Sel P1 = {}

goal (1 subgoal):
 1. selected_part Sel (P1 - {Pos A}) = {}
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
{L \<in> P1. \<exists>A\<in>Sel. L = Neg A} = {}

goal (1 subgoal):
 1. {L \<in> P1 - {Pos A}. \<exists>A\<in>Sel. L = Neg A} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel (P1 - {Pos A}) = {}

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>Neg A \<in> (selected_part Sel P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> selected_part Sel P2
[PROOF STEP]
have "selected_part Sel (P2 - { Neg A}) = (selected_part Sel P2) - { Neg A }"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> selected_part Sel P2

goal (1 subgoal):
 1. selected_part Sel (P2 - {Neg A}) = selected_part Sel P2 - {Neg A}
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> {L \<in> P2. \<exists>A\<in>Sel. L = Neg A}

goal (1 subgoal):
 1. {L \<in> P2 - {Neg A}. \<exists>A\<in>Sel. L = Neg A} = {L \<in> P2. \<exists>A\<in>Sel. L = Neg A} - {Neg A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel (P2 - {Neg A}) = selected_part Sel P2 - {Neg A}

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>C = ( (P1 - { Pos A}) \<union> ( P2 - { Neg A }))\<close>
[PROOF STATE]
proof (chain)
picking this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})
[PROOF STEP]
have
  "selected_part Sel C
    = (selected_part Sel (P1 - { Pos A})) \<union> (selected_part Sel (P2 - { Neg A}))"
[PROOF STATE]
proof (prove)
using this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})

goal (1 subgoal):
 1. selected_part Sel C = selected_part Sel (P1 - {Pos A}) \<union> selected_part Sel (P2 - {Neg A})
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
C = P1 - {Pos A} \<union> (P2 - {Neg A})

goal (1 subgoal):
 1. {L \<in> C. \<exists>A\<in>Sel. L = Neg A} = {L \<in> P1 - {Pos A}. \<exists>A\<in>Sel. L = Neg A} \<union> {L \<in> P2 - {Neg A}. \<exists>A\<in>Sel. L = Neg A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel C = selected_part Sel (P1 - {Pos A}) \<union> selected_part Sel (P2 - {Neg A})

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this and \<open>selected_part Sel (P1 - { Pos A}) = {}\<close>
    and \<open>selected_part Sel (P2 - { Neg A}) = selected_part Sel P2 - { Neg A }\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part Sel C = selected_part Sel (P1 - {Pos A}) \<union> selected_part Sel (P2 - {Neg A})
selected_part Sel (P1 - {Pos A}) = {}
selected_part Sel (P2 - {Neg A}) = selected_part Sel P2 - {Neg A}
[PROOF STEP]
have "selected_part Sel C = selected_part Sel P2 - { Neg A }"
[PROOF STATE]
proof (prove)
using this:
selected_part Sel C = selected_part Sel (P1 - {Pos A}) \<union> selected_part Sel (P2 - {Neg A})
selected_part Sel (P1 - {Pos A}) = {}
selected_part Sel (P2 - {Neg A}) = selected_part Sel P2 - {Neg A}

goal (1 subgoal):
 1. selected_part Sel C = selected_part Sel P2 - {Neg A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel C = selected_part Sel P2 - {Neg A}

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from \<open>Neg A \<in> P2\<close> and \<open>A \<in> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> P2
A \<in> Sel
[PROOF STEP]
have "Neg A \<in> selected_part Sel P2"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> P2
A \<in> Sel

goal (1 subgoal):
 1. Neg A \<in> selected_part Sel P2
[PROOF STEP]
unfolding selected_part_def
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> P2
A \<in> Sel

goal (1 subgoal):
 1. Neg A \<in> {L \<in> P2. \<exists>A\<in>Sel. L = Neg A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg A \<in> selected_part Sel P2

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this and \<open>selected_part Sel C = (selected_part Sel P2) - { Neg A }\<close>
    and \<open>finite (selected_part Sel P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> selected_part Sel P2
selected_part Sel C = selected_part Sel P2 - {Neg A}
finite (selected_part Sel P2)
[PROOF STEP]
have "card (selected_part Sel C) = card (selected_part Sel P2) - 1"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> selected_part Sel P2
selected_part Sel C = selected_part Sel P2 - {Neg A}
finite (selected_part Sel P2)

goal (1 subgoal):
 1. card (selected_part Sel C) = card (selected_part Sel P2) - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (selected_part Sel C) = card (selected_part Sel P2) - 1

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
from this and \<open>card (selected_part Sel P2) = Suc n\<close>
[PROOF STATE]
proof (chain)
picking this:
card (selected_part Sel C) = card (selected_part Sel P2) - 1
card (selected_part Sel P2) = Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel C) = card (selected_part Sel P2) - 1
card (selected_part Sel P2) = Suc n

goal (1 subgoal):
 1. card (selected_part Sel C) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (selected_part Sel C) = n

goal:
No subgoals!
[PROOF STEP]
qed