[STATEMENT]
lemma canonic_int_validates_all_clauses_sel :
  assumes "saturated_binary_rule (ordered_sel_resolvent Sel) S"
  assumes "all_fulfill finite S"
  assumes "{} \<notin> S"
  assumes "C \<in> S"
  shows "validate_clause (canonic_int_ordered (empty_selected_part Sel S)) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
let ?nat_order = "{ (x::nat,y::nat). x < y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
let ?SE = "empty_selected_part Sel S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
let ?I = "canonic_int_ordered ?SE"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
obtain n where "n = card (selected_part Sel C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n = card (selected_part Sel C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = card (selected_part Sel C)

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
have "\<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> validate_clause ?I C" (is "?P n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
proof ((rule wf_induct [of ?nat_order ?P n]), (simp add:wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = y \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C) \<Longrightarrow> \<forall>C. card (selected_part Sel C) = x \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = y \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C) \<Longrightarrow> \<forall>C. card (selected_part Sel C) = x \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = y \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C) \<Longrightarrow> \<forall>C. card (selected_part Sel C) = x \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
assume ind_hyp: "\<forall>m. (m,n) \<in> ?nat_order \<longrightarrow> (?P m)"
[PROOF STATE]
proof (state)
this:
\<forall>m. (m, n) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = m \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C)

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = y \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C) \<Longrightarrow> \<forall>C. card (selected_part Sel C) = x \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "(?P n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
proof (rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card (selected_part Sel C) = n; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card (selected_part Sel C) = n; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
assume "card (selected_part Sel C) = n" and "C \<in> S"
[PROOF STATE]
proof (state)
this:
card (selected_part Sel C) = n
C \<in> S

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card (selected_part Sel C) = n; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel 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]
unfolding all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C. C \<in> S \<longrightarrow> finite C
C \<in> S

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

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card (selected_part Sel C) = n; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
have "finite (selected_part Sel C)"
[PROOF STATE]
proof (prove)
using this:
finite C

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

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

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card (selected_part Sel C) = n; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "validate_clause ?I  C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
proof (rule nat.exhaust [of "n"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
assume "n = 0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from this and \<open>card (selected_part Sel C) = n\<close> and \<open>finite (selected_part Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
n = 0
card (selected_part Sel C) = n
finite (selected_part Sel C)
[PROOF STEP]
have "selected_part Sel C = {}"
[PROOF STATE]
proof (prove)
using this:
n = 0
card (selected_part Sel C) = n
finite (selected_part Sel C)

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[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 "saturated_binary_rule ordered_resolvent ?SE"
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent Sel) S

goal (1 subgoal):
 1. saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
using saturated_ordered_sel_res_empty_sel
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent Sel) S
saturated_binary_rule (ordered_sel_resolvent ?Sel) ?S \<Longrightarrow> saturated_binary_rule ordered_resolvent (empty_selected_part ?Sel ?S)

goal (1 subgoal):
 1. saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from \<open>{} \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
{} \<notin> S
[PROOF STEP]
have "{} \<notin> ?SE"
[PROOF STATE]
proof (prove)
using this:
{} \<notin> S

goal (1 subgoal):
 1. {} \<notin> empty_selected_part Sel S
[PROOF STEP]
unfolding empty_selected_part_def
[PROOF STATE]
proof (prove)
using this:
{} \<notin> S

goal (1 subgoal):
 1. {} \<notin> {C \<in> S. selected_part Sel C = {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<notin> empty_selected_part Sel S

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from \<open>selected_part Sel C = {}\<close> \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part Sel C = {}
C \<in> S
[PROOF STEP]
have "C \<in> ?SE"
[PROOF STATE]
proof (prove)
using this:
selected_part Sel C = {}
C \<in> S

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

goal (1 subgoal):
 1. C \<in> {C \<in> S. selected_part Sel C = {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> empty_selected_part Sel S

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from \<open>all_fulfill finite S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
[PROOF STEP]
have "all_fulfill finite ?SE"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S

goal (1 subgoal):
 1. all_fulfill finite (empty_selected_part Sel S)
[PROOF STEP]
unfolding empty_selected_part_def all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C. C \<in> S \<longrightarrow> finite C

goal (1 subgoal):
 1. \<forall>C. C \<in> {C \<in> S. selected_part Sel C = {}} \<longrightarrow> finite C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (empty_selected_part Sel S)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
 2. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from this  and \<open>saturated_binary_rule ordered_resolvent ?SE\<close> and \<open>{} \<notin> ?SE\<close> and \<open>C \<in> ?SE\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (empty_selected_part Sel S)
saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
{} \<notin> empty_selected_part Sel S
C \<in> empty_selected_part Sel S
[PROOF STEP]
show "validate_clause ?I C"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (empty_selected_part Sel S)
saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
{} \<notin> empty_selected_part Sel S
C \<in> empty_selected_part Sel S

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
using canonic_int_validates_all_clauses
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (empty_selected_part Sel S)
saturated_binary_rule ordered_resolvent (empty_selected_part Sel S)
{} \<notin> empty_selected_part Sel S
C \<in> empty_selected_part Sel S
\<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. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

goal (1 subgoal):
 1. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
assume "n = Suc m"
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (1 subgoal):
 1. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from this and \<open>card (selected_part Sel C) = n\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
card (selected_part Sel C) = n
[PROOF STEP]
have "selected_part Sel C \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
n = Suc m
card (selected_part Sel C) = n

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

goal (1 subgoal):
 1. \<And>x2. n = Suc x2 \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "validate_clause ?I C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C \<Longrightarrow> False
[PROOF STEP]
assume "\<not>validate_clause ?I C"
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C \<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 "tautology C"
[PROOF STATE]
proof (state)
this:
tautology C

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>tautology C\<close> and \<open>\<not>validate_clause ?I C\<close>
[PROOF STATE]
proof (chain)
picking this:
tautology C
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
tautology C
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

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

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
hence "\<not>(tautology (selected_part Sel C))"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C

goal (1 subgoal):
 1. \<not> tautology (selected_part Sel C)
[PROOF STEP]
unfolding selected_part_def tautology_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>A. Pos A \<in> C \<and> Neg A \<in> C

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal (selected_part Sel C) L\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (selected_part Sel C) L
[PROOF STEP]
have "L \<in> (selected_part Sel C)"
              and "L \<in> C"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (selected_part Sel C) L

goal (1 subgoal):
 1. L \<in> selected_part Sel C &&& L \<in> C
[PROOF STEP]
unfolding strictly_maximal_literal_def selected_part_def
[PROOF STATE]
proof (prove)
using this:
L \<in> {L \<in> C. \<exists>A\<in>Sel. L = Neg A} \<and> (\<forall>B. B \<in> {L \<in> C. \<exists>A\<in>Sel. L = Neg A} \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>validate_clause ?I C\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> selected_part Sel C
L \<in> C
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
have "\<not>(validate_literal ?I L)"
[PROOF STATE]
proof (prove)
using this:
L \<in> selected_part Sel C
L \<in> C
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in> (selected_part Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> selected_part Sel C
[PROOF STEP]
obtain A where "L = (Neg A)" and "A \<in> Sel"
[PROOF STATE]
proof (prove)
using this:
L \<in> selected_part Sel C

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>(validate_literal ?I L)\<close> and \<open>L = (Neg A)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L
L = Neg A
[PROOF STEP]
have "A \<in> ?I"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L
L = Neg A

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A \<in> canonic_int_ordered (empty_selected_part Sel S)
[PROOF STEP]
have "((canonic_int_fun_ordered A) ?SE)"
[PROOF STATE]
proof (prove)
using this:
A \<in> canonic_int_ordered (empty_selected_part Sel S)

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
have "((\<exists> C. (C \<in> ?SE) \<and> (strictly_maximal_literal C (Pos A) )
                \<and> ( \<forall> B. ( Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                  \<longrightarrow> (\<not>(canonic_int_fun_ordered B) ?SE)))
                \<and> ( \<forall> B. ( Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                  \<longrightarrow> ((canonic_int_fun_ordered B) ?SE)))))" (is ?exp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?exp"
[PROOF STATE]
proof (state)
this:
\<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))

goal (1 subgoal):
 1. \<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))
[PROOF STEP]
have "\<not>((canonic_int_fun_ordered A) ?SE)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))

goal (1 subgoal):
 1. \<not> canonic_int_fun_ordered A (empty_selected_part Sel S)
[PROOF STEP]
by ((simp only:canonic_int_fun_ordered.simps [of A]), blast)
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_fun_ordered A (empty_selected_part Sel S)

goal (1 subgoal):
 1. \<nexists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(canonic_int_fun_ordered A) ?SE\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_fun_ordered A (empty_selected_part Sel S)
canonic_int_fun_ordered A (empty_selected_part Sel S)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_fun_ordered A (empty_selected_part Sel S)
canonic_int_fun_ordered A (empty_selected_part Sel 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:
\<exists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))
[PROOF STEP]
obtain D where
                "D \<in> ?SE" and "strictly_maximal_literal D (Pos A)"
                and c1: "( \<forall> B. ( Pos B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering
                  \<longrightarrow> (\<not>(canonic_int_fun_ordered B) ?SE)))"
                and c2: "( \<forall> B. ( Neg B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering
                  \<longrightarrow> ((canonic_int_fun_ordered B) ?SE)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. C \<in> empty_selected_part Sel S \<and> strictly_maximal_literal C (Pos A) \<and> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S))

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

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

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

goal (1 subgoal):
 1. selected_part Sel D = {} &&& D \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part Sel D = {}
D \<in> S

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

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
let ?R = "(D - { Pos A }) \<union> (C - { Neg A })"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal D (Pos A)\<close>
                and \<open>strictly_maximal_literal (selected_part Sel C) L\<close>
                and \<open>L = (Neg A)\<close> and \<open>(selected_part Sel D) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal D (Pos A)
strictly_maximal_literal (selected_part Sel C) L
L = Neg A
selected_part Sel D = {}
[PROOF STEP]
have "(ordered_sel_resolvent_upon Sel D C ?R A)"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal D (Pos A)
strictly_maximal_literal (selected_part Sel C) L
L = Neg A
selected_part Sel D = {}

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ordered_sel_resolvent_upon Sel D C (D - {Pos A} \<union> (C - {Neg A})) A
[PROOF STEP]
have "ordered_sel_resolvent Sel D C ?R"
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent_upon Sel D C (D - {Pos A} \<union> (C - {Neg A})) A

goal (1 subgoal):
 1. ordered_sel_resolvent Sel D C (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
by (rule ordered_sel_resolvent_upon_is_resolvent)
[PROOF STATE]
proof (state)
this:
ordered_sel_resolvent Sel D C (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>(ordered_sel_resolvent_upon Sel D C ?R A)\<close> \<open>(card (selected_part Sel C)) = n\<close>
                and \<open>n = Suc m\<close> and \<open>L \<in> C\<close> and \<open>L = (Neg A)\<close> and \<open>finite D\<close> and \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_sel_resolvent_upon Sel D C (D - {Pos A} \<union> (C - {Neg A})) A
card (selected_part Sel C) = n
n = Suc m
L \<in> C
L = Neg A
finite D
finite C
[PROOF STEP]
have "card (selected_part Sel ?R) = m"
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent_upon Sel D C (D - {Pos A} \<union> (C - {Neg A})) A
card (selected_part Sel C) = n
n = Suc m
L \<in> C
L = Neg A
finite D
finite C

goal (1 subgoal):
 1. card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))) = m
[PROOF STEP]
using resolution_decreases_selected_part
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent_upon Sel D C (D - {Pos A} \<union> (C - {Neg A})) A
card (selected_part Sel C) = n
n = Suc m
L \<in> C
L = Neg A
finite D
finite C
\<lbrakk>ordered_sel_resolvent_upon ?Sel ?P1.0 ?P2.0 ?C ?A; Neg ?A \<in> ?P2.0; finite ?P1.0; finite ?P2.0; card (selected_part ?Sel ?P2.0) = Suc ?n\<rbrakk> \<Longrightarrow> card (selected_part ?Sel ?C) = ?n

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from \<open>ordered_sel_resolvent Sel D C ?R\<close> and \<open>D \<in> S\<close>and \<open>C \<in> S\<close>
                and \<open>saturated_binary_rule (ordered_sel_resolvent Sel) S\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_sel_resolvent Sel D C (D - {Pos A} \<union> (C - {Neg A}))
D \<in> S
C \<in> S
saturated_binary_rule (ordered_sel_resolvent Sel) S
[PROOF STEP]
have "redundant ?R S"
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent Sel D C (D - {Pos A} \<union> (C - {Neg A}))
D \<in> S
C \<in> S
saturated_binary_rule (ordered_sel_resolvent Sel) S

goal (1 subgoal):
 1. redundant (D - {Pos A} \<union> (C - {Neg A})) S
[PROOF STEP]
unfolding saturated_binary_rule_def
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent Sel D C (D - {Pos A} \<union> (C - {Neg A}))
D \<in> S
C \<in> S
\<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. redundant (D - {Pos A} \<union> (C - {Neg A})) S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant (D - {Pos A} \<union> (C - {Neg A})) S

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
hence "tautology ?R \<or> (\<exists>RR. (RR \<in> S \<and> (subsumes RR ?R)))"
[PROOF STATE]
proof (prove)
using this:
redundant (D - {Pos A} \<union> (C - {Neg A})) S

goal (1 subgoal):
 1. tautology (D - {Pos A} \<union> (C - {Neg A})) \<or> (\<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})))
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology (D - {Pos A} \<union> (C - {Neg A})) \<or> (\<exists>Da. Da \<in> S \<and> subsumes Da (D - {Pos A} \<union> (C - {Neg A})))

goal (1 subgoal):
 1. tautology (D - {Pos A} \<union> (C - {Neg A})) \<or> (\<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tautology (D - {Pos A} \<union> (C - {Neg A})) \<or> (\<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})))

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
hence "validate_clause ?I ?R"
[PROOF STATE]
proof (prove)
using this:
tautology (D - {Pos A} \<union> (C - {Neg A})) \<or> (\<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})))

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tautology (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
 2. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
assume "tautology ?R"
[PROOF STATE]
proof (state)
this:
tautology (D - {Pos A} \<union> (C - {Neg A}))

goal (2 subgoals):
 1. tautology (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
 2. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
thus "validate_clause ?I ?R"
[PROOF STATE]
proof (prove)
using this:
tautology (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
by (rule tautologies_are_valid)
[PROOF STATE]
proof (state)
this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
assume "\<exists>R'. R' \<in> S \<and> (subsumes R' ?R)"
[PROOF STATE]
proof (state)
this:
\<exists>R'. R' \<in> S \<and> subsumes R' (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>R'. R' \<in> S \<and> subsumes R' (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
obtain R' where "R' \<in> S" and "subsumes R' ?R"
[PROOF STATE]
proof (prove)
using this:
\<exists>R'. R' \<in> S \<and> subsumes R' (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R' \<in> S; subsumes R' (D - {Pos A} \<union> (C - {Neg A}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<in> S
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from \<open>finite C\<close>and \<open>finite D\<close>
[PROOF STATE]
proof (chain)
picking this:
finite C
finite D
[PROOF STEP]
have "finite ?R"
[PROOF STATE]
proof (prove)
using this:
finite C
finite D

goal (1 subgoal):
 1. finite (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
finite (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
have "finite (selected_part Sel ?R)"
[PROOF STATE]
proof (prove)
using this:
finite (D - {Pos A} \<union> (C - {Neg A}))

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

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

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from \<open>subsumes R' ?R\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
have "selected_part Sel R' \<subseteq> selected_part Sel ?R"
[PROOF STATE]
proof (prove)
using this:
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. selected_part Sel R' \<subseteq> selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
unfolding selected_part_def and subsumes_def
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> D - {Pos A} \<union> (C - {Neg A})

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

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from this and \<open>finite (selected_part Sel ?R)\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part Sel R' \<subseteq> selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))
finite (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
[PROOF STEP]
have "card (selected_part Sel R') \<le> card (selected_part Sel ?R)"
[PROOF STATE]
proof (prove)
using this:
selected_part Sel R' \<subseteq> selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))
finite (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))

goal (1 subgoal):
 1. card (selected_part Sel R') \<le> card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
[PROOF STEP]
using card_mono
[PROOF STATE]
proof (prove)
using this:
selected_part Sel R' \<subseteq> selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))
finite (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. card (selected_part Sel R') \<le> card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (selected_part Sel R') \<le> card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from this and \<open>card (selected_part Sel ?R) = m\<close> and \<open>n = Suc m\<close>
[PROOF STATE]
proof (chain)
picking this:
card (selected_part Sel R') \<le> card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))) = m
n = Suc m
[PROOF STEP]
have "card (selected_part Sel R') < n"
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel R') \<le> card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A})))
card (selected_part Sel (D - {Pos A} \<union> (C - {Neg A}))) = m
n = Suc m

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

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from this and ind_hyp and \<open>R' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
card (selected_part Sel R') < n
\<forall>m. (m, n) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = m \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C)
R' \<in> S
[PROOF STEP]
have "validate_clause ?I R'"
[PROOF STATE]
proof (prove)
using this:
card (selected_part Sel R') < n
\<forall>m. (m, n) \<in> {(x, y). x < y} \<longrightarrow> (\<forall>C. card (selected_part Sel C) = m \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C)
R' \<in> S

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

goal (1 subgoal):
 1. \<exists>RR. RR \<in> S \<and> subsumes RR (D - {Pos A} \<union> (C - {Neg A})) \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
from this and \<open>subsumes R' ?R\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> R'
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
show "validate_clause ?I ?R"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> R'
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
using subsumption_and_semantics [of R' ?R ?I]
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> R'
subsumes R' (D - {Pos A} \<union> (C - {Neg A}))
\<lbrakk>subsumes R' (D - {Pos A} \<union> (C - {Neg A})); canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> R'\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))
[PROOF STEP]
obtain L' where "L' \<in> ?R" and "validate_literal ?I L'"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> (D - {Pos A} \<union> (C - {Neg A}))

goal (1 subgoal):
 1. (\<And>L'. \<lbrakk>L' \<in> D - {Pos A} \<union> (C - {Neg A}); canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L' \<in> D - {Pos A} \<union> (C - {Neg A})
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
have "L' \<notin> D - { Pos A }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L' \<notin> D - {Pos A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L' \<in> D - {Pos A} \<Longrightarrow> False
[PROOF STEP]
assume "L' \<in> D - { Pos A }"
[PROOF STATE]
proof (state)
this:
L' \<in> D - {Pos A}

goal (1 subgoal):
 1. L' \<in> D - {Pos A} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L' \<in> D - {Pos A}
[PROOF STEP]
have "L' \<in> D"
[PROOF STATE]
proof (prove)
using this:
L' \<in> D - {Pos A}

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

goal (1 subgoal):
 1. L' \<in> D - {Pos A} \<Longrightarrow> False
[PROOF STEP]
let ?A' = "atom L'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L' \<in> D - {Pos A} \<Longrightarrow> False
[PROOF STEP]
have "L' = (Pos ?A') \<or> L' = (Neg ?A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L' = Pos (atom L') \<or> L' = Neg (atom L')
[PROOF STEP]
using atom_property [of ?A' L']
[PROOF STATE]
proof (prove)
using this:
atom L' = atom L' \<Longrightarrow> L' = Pos (atom L') \<or> L' = Neg (atom L')

goal (1 subgoal):
 1. L' = Pos (atom L') \<or> L' = Neg (atom L')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L' = Pos (atom L') \<or> L' = Neg (atom L')

goal (1 subgoal):
 1. L' \<in> D - {Pos A} \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
L' = Pos (atom L') \<or> L' = Neg (atom L')

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
assume "L' = (Pos ?A')"
[PROOF STATE]
proof (state)
this:
L' = Pos (atom L')

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

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

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

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from c1
[PROOF STATE]
proof (chain)
picking this:
\<forall>B. Pos B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)
[PROOF STEP]
have c1': "Pos ?A' \<in> D \<longrightarrow> (?A', A) \<in> atom_ordering
                                \<longrightarrow> (\<not>(canonic_int_fun_ordered ?A') ?SE)"
[PROOF STATE]
proof (prove)
using this:
\<forall>B. Pos B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B (empty_selected_part Sel S)

goal (1 subgoal):
 1. Pos (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pos (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from \<open>L' \<in> D\<close> and \<open>L' = Pos ?A'\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> D
L' = Pos (atom L')
[PROOF STEP]
have "Pos ?A' \<in> D"
[PROOF STATE]
proof (prove)
using this:
L' \<in> D
L' = Pos (atom L')

goal (1 subgoal):
 1. Pos (atom L') \<in> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pos (atom L') \<in> D

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from c1' and \<open>Pos ?A' \<in> D\<close> and \<open>(?A',A) \<in> atom_ordering\<close>
[PROOF STATE]
proof (chain)
picking this:
Pos (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
Pos (atom L') \<in> D
(atom L', A) \<in> atom_ordering
[PROOF STEP]
have "\<not>(canonic_int_fun_ordered ?A') ?SE"
[PROOF STATE]
proof (prove)
using this:
Pos (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
Pos (atom L') \<in> D
(atom L', A) \<in> atom_ordering

goal (1 subgoal):
 1. \<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
have "?A' \<notin> ?I"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

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

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

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
atom L' \<notin> canonic_int_ordered (empty_selected_part Sel S)
[PROOF STEP]
have "\<not>(validate_literal ?I (Pos ?A'))"
[PROOF STATE]
proof (prove)
using this:
atom L' \<notin> canonic_int_ordered (empty_selected_part Sel S)

goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Pos (atom L')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Pos (atom L')

goal (2 subgoals):
 1. L' = Pos (atom L') \<Longrightarrow> False
 2. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L' = Pos ?A'\<close> and \<open>validate_literal ?I L'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Pos (atom L')
L' = Pos (atom L')
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Pos (atom L')
L' = Pos (atom L')
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'

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

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
assume "L' = Neg ?A'"
[PROOF STATE]
proof (state)
this:
L' = Neg (atom L')

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

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

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

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from c2
[PROOF STATE]
proof (chain)
picking this:
\<forall>B. Neg B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S)
[PROOF STEP]
have c2': "Neg ?A' \<in> D \<longrightarrow> (?A', A) \<in> atom_ordering
                      \<longrightarrow> (canonic_int_fun_ordered ?A') ?SE"
[PROOF STATE]
proof (prove)
using this:
\<forall>B. Neg B \<in> D \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B (empty_selected_part Sel S)

goal (1 subgoal):
 1. Neg (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from \<open>L' \<in> D\<close> and \<open>L' = (Neg ?A')\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> D
L' = Neg (atom L')
[PROOF STEP]
have "Neg ?A' \<in> D"
[PROOF STATE]
proof (prove)
using this:
L' \<in> D
L' = Neg (atom L')

goal (1 subgoal):
 1. Neg (atom L') \<in> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg (atom L') \<in> D

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from c2' and \<open>Neg ?A' \<in> D\<close> and \<open>(?A',A) \<in> atom_ordering\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
Neg (atom L') \<in> D
(atom L', A) \<in> atom_ordering
[PROOF STEP]
have "(canonic_int_fun_ordered ?A') ?SE"
[PROOF STATE]
proof (prove)
using this:
Neg (atom L') \<in> D \<longrightarrow> (atom L', A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
Neg (atom L') \<in> D
(atom L', A) \<in> atom_ordering

goal (1 subgoal):
 1. canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)
[PROOF STEP]
have "?A' \<in> ?I"
[PROOF STATE]
proof (prove)
using this:
canonic_int_fun_ordered (atom L') (empty_selected_part Sel S)

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

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

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
atom L' \<in> canonic_int_ordered (empty_selected_part Sel S)
[PROOF STEP]
have "\<not>validate_literal ?I (Neg ?A')"
[PROOF STATE]
proof (prove)
using this:
atom L' \<in> canonic_int_ordered (empty_selected_part Sel S)

goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Neg (atom L')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Neg (atom L')

goal (1 subgoal):
 1. L' = Neg (atom L') \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L' = Neg ?A'\<close> and \<open>validate_literal ?I L'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Neg (atom L')
L' = Neg (atom L')
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> Neg (atom L')
L' = Neg (atom L')
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'

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:
L' \<notin> D - {Pos A}

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L' \<in> ?R\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<notin> D - {Pos A}
L' \<in> D - {Pos A} \<union> (C - {Neg A})
[PROOF STEP]
have "L' \<in> C"
[PROOF STATE]
proof (prove)
using this:
L' \<notin> D - {Pos A}
L' \<in> D - {Pos A} \<union> (C - {Neg A})

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validate_literal ?I L'\<close> and \<open>\<not>validate_clause ?I C\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> L'
\<not> canonic_int_ordered (empty_selected_part Sel 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:
False

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
from \<open>?P n\<close> and \<open>n = card (selected_part Sel C)\<close> and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
n = card (selected_part Sel C)
C \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>C. card (selected_part Sel C) = n \<longrightarrow> C \<in> S \<longrightarrow> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
n = card (selected_part Sel C)
C \<in> S

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>saturated_binary_rule (ordered_sel_resolvent Sel) 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_sel_resolvent Sel) S \<longrightarrow> all_fulfill finite S \<longrightarrow> {} \<notin> S \<longrightarrow> satisfiable S)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>saturated_binary_rule (ordered_sel_resolvent Sel) 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_sel_resolvent Sel) S
all_fulfill finite S
{} \<notin> S
\<not> satisfiable S

goal (1 subgoal):
 1. \<not> Complete (ordered_sel_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
let ?SE = "empty_selected_part Sel S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Complete (ordered_sel_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
let ?I = "canonic_int_ordered ?SE"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Complete (ordered_sel_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
have "validate_formula ?I S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(validate_formula ?I S)"
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> S

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

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

goal (1 subgoal):
 1. \<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> S \<Longrightarrow> False
[PROOF STEP]
from \<open>saturated_binary_rule (ordered_sel_resolvent Sel) 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 ?I C)\<close>
[PROOF STATE]
proof (chain)
picking this:
saturated_binary_rule (ordered_sel_resolvent Sel) S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent Sel) S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C

goal (1 subgoal):
 1. False
[PROOF STEP]
using canonic_int_validates_all_clauses_sel [of Sel S C]
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent Sel) S
all_fulfill finite S
{} \<notin> S
C \<in> S
\<not> canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> C
\<lbrakk>saturated_binary_rule (ordered_sel_resolvent Sel) S; all_fulfill finite S; {} \<notin> S; C \<in> S\<rbrakk> \<Longrightarrow> canonic_int_ordered (empty_selected_part Sel 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 (empty_selected_part Sel S) \<Turnstile> S

goal (1 subgoal):
 1. \<not> Complete (ordered_sel_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
from \<open>(validate_formula ?I S)\<close> and \<open>\<not>(satisfiable S)\<close>
[PROOF STATE]
proof (chain)
picking this:
canonic_int_ordered (empty_selected_part Sel S) \<Turnstile> S
\<not> satisfiable S
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
canonic_int_ordered (empty_selected_part Sel 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 (empty_selected_part Sel 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 ordered_res_with_selection_is_model_res :
  assumes "ordered_sel_resolvent UNIV P1 P2 C"
  shows "ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2)
            (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
ordered_sel_resolvent UNIV P1 P2 C
[PROOF STEP]
obtain A
  where c_def: "C = ((P1 - { Pos A }) \<union> (P2 - { Neg A }))"
    and "selected_part UNIV P1 = {}"
    and "strictly_maximal_literal P1 (Pos A)"
    and disj: "((strictly_maximal_literal P2 (Neg A)) \<and> (selected_part UNIV P2) = {})
      \<or> strictly_maximal_literal (selected_part UNIV P2) (Neg A)"
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent UNIV P1 P2 C

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>C = P1 - {Pos A} \<union> (P2 - {Neg A}); selected_part UNIV P1 = {}; strictly_maximal_literal P1 (Pos A); strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<or> strictly_maximal_literal (selected_part UNIV P2) (Neg A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ordered_sel_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> selected_part UNIV P1 = {} \<and> (strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<or> strictly_maximal_literal (selected_part UNIV P2) (Neg A))

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

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
have "rename_clause Sel ((P1 - { Pos A }) \<union> (P2 - { Neg A }))
    =  (rename_clause Sel (P1 - { Pos A })) \<union> rename_clause Sel (P2 - { (Neg A) })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (P1 - {Pos A} \<union> (P2 - {Neg A})) = rename_clause Sel (P1 - {Pos A}) \<union> rename_clause Sel (P2 - {Neg A})
[PROOF STEP]
using rename_union [of Sel "P1 - { Pos A }" "P2 - { Neg A }"]
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (P1 - {Pos A} \<union> (P2 - {Neg A})) = rename_clause Sel (P1 - {Pos A}) \<union> rename_clause Sel (P2 - {Neg A})

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

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

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

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
have m1: "(rename_clause Sel (P1 - { Pos A })) = (rename_clause Sel P1)
              - { rename_literal Sel (Pos A) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (P1 - {Pos A}) = rename_clause Sel P1 - {rename_literal Sel (Pos A)}
[PROOF STEP]
using renaming_set_minus
[PROOF STATE]
proof (prove)
using this:
rename_clause ?Sel (?C - {?L}) = rename_clause ?Sel ?C - {rename_literal ?Sel ?L}

goal (1 subgoal):
 1. rename_clause Sel (P1 - {Pos A}) = rename_clause Sel P1 - {rename_literal Sel (Pos A)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause Sel (P1 - {Pos A}) = rename_clause Sel P1 - {rename_literal Sel (Pos A)}

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
have m2: "rename_clause Sel (P2 - { Neg A }) = (rename_clause Sel P2)
              - { rename_literal Sel (Neg A) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (P2 - {Neg A}) = rename_clause Sel P2 - {rename_literal Sel (Neg A)}
[PROOF STEP]
using renaming_set_minus
[PROOF STATE]
proof (prove)
using this:
rename_clause ?Sel (?C - {?L}) = rename_clause ?Sel ?C - {rename_literal ?Sel ?L}

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

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from m1 and m2 and ren_c
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel (P1 - {Pos A}) = rename_clause Sel P1 - {rename_literal Sel (Pos A)}
rename_clause Sel (P2 - {Neg A}) = rename_clause Sel P2 - {rename_literal Sel (Neg A)}
rename_clause Sel C = rename_clause Sel (P1 - {Pos A}) \<union> rename_clause Sel (P2 - {Neg A})
[PROOF STEP]
have
  rc_def: "(rename_clause Sel C) =
    ((rename_clause Sel P1) - { rename_literal Sel (Pos A) })
    \<union> ((rename_clause Sel P2) - { rename_literal Sel (Neg A)  })"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (P1 - {Pos A}) = rename_clause Sel P1 - {rename_literal Sel (Pos A)}
rename_clause Sel (P2 - {Neg A}) = rename_clause Sel P2 - {rename_literal Sel (Neg A)}
rename_clause Sel C = rename_clause Sel (P1 - {Pos A}) \<union> rename_clause Sel (P2 - {Neg A})

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

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
have "\<not>((strictly_maximal_literal P2 (Neg A)) \<and> (selected_part UNIV P2) = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<Longrightarrow> False
[PROOF STEP]
assume "(strictly_maximal_literal P2 (Neg A)) \<and> (selected_part UNIV P2) = {}"
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {}

goal (1 subgoal):
 1. strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {}
[PROOF STEP]
have "strictly_maximal_literal P2 (Neg A)" and "selected_part UNIV P2 = {}"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {}

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

goal (1 subgoal):
 1. strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal P2 (Neg A)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal P2 (Neg A)
[PROOF STEP]
have "Neg A \<in> P2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P2 (Neg A)

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

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

goal (1 subgoal):
 1. strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<Longrightarrow> False
[PROOF STEP]
from this and \<open>selected_part UNIV P2 = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> P2
selected_part UNIV P2 = {}
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> P2
selected_part UNIV P2 = {}

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

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:
\<not> (strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {})

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from this and disj
[PROOF STATE]
proof (chain)
picking this:
\<not> (strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {})
strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<or> strictly_maximal_literal (selected_part UNIV P2) (Neg A)
[PROOF STEP]
have "strictly_maximal_literal (selected_part UNIV P2) (Neg A)"
[PROOF STATE]
proof (prove)
using this:
\<not> (strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {})
strictly_maximal_literal P2 (Neg A) \<and> selected_part UNIV P2 = {} \<or> strictly_maximal_literal (selected_part UNIV P2) (Neg A)

goal (1 subgoal):
 1. strictly_maximal_literal (selected_part UNIV P2) (Neg A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal (selected_part UNIV P2) (Neg A)

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (selected_part UNIV P2) (Neg A)
[PROOF STEP]
have "strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (selected_part UNIV P2) (Neg A)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)
[PROOF STEP]
using renaming_and_selected_part
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (selected_part UNIV P2) (Neg A)
selected_part UNIV ?C = rename_clause ?Sel (validated_part ?Sel (rename_clause ?Sel ?C))

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)
[PROOF STEP]
have
    "strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2))))
        (rename_literal Sel (Neg A))"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))
[PROOF STEP]
using renaming_preserves_strictly_maximal_literal
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (rename_clause Sel (validated_part Sel (rename_clause Sel P2))) (Neg A)
strictly_maximal_literal ?C ?L \<Longrightarrow> strictly_maximal_literal (rename_clause ?A ?C) (rename_literal ?A ?L)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))
[PROOF STEP]
have
    p1: "strictly_maximal_literal (validated_part Sel (rename_clause Sel P2))
      (rename_literal Sel (Neg A))"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))

goal (1 subgoal):
 1. strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))
[PROOF STEP]
using inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (rename_clause Sel (rename_clause Sel (validated_part Sel (rename_clause Sel P2)))) (rename_literal Sel (Neg A))
rename_clause ?A (rename_clause ?A ?L) = ?L

goal (1 subgoal):
 1. strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from \<open>strictly_maximal_literal P1 (Pos A)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal P1 (Pos A)
[PROOF STEP]
have p2: "strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P1 (Pos A)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))
[PROOF STEP]
using renaming_preserves_strictly_maximal_literal
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal ?C ?L \<Longrightarrow> strictly_maximal_literal (rename_clause ?A ?C) (rename_literal ?A ?L)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from \<open>(selected_part UNIV P1) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part UNIV P1 = {}
[PROOF STEP]
have
    "rename_clause Sel (validated_part Sel (rename_clause Sel P1)) = {}"
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV P1 = {}

goal (1 subgoal):
 1. rename_clause Sel (validated_part Sel (rename_clause Sel P1)) = {}
[PROOF STEP]
using renaming_and_selected_part
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV P1 = {}
selected_part UNIV ?C = rename_clause ?Sel (validated_part ?Sel (rename_clause ?Sel ?C))

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

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel (validated_part Sel (rename_clause Sel P1)) = {}
[PROOF STEP]
have q: "validated_part Sel (rename_clause Sel P1) = {}"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (validated_part Sel (rename_clause Sel P1)) = {}

goal (1 subgoal):
 1. validated_part Sel (rename_clause Sel P1) = {}
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
{L. \<exists>LL. LL \<in> validated_part Sel {L. \<exists>LL. LL \<in> P1 \<and> L = rename_literal Sel LL} \<and> L = rename_literal Sel LL} = {}

goal (1 subgoal):
 1. validated_part Sel {L. \<exists>LL. LL \<in> P1 \<and> L = rename_literal Sel LL} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validated_part Sel (rename_clause Sel P1) = {}

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
have r: "rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if atom (Neg A) \<in> Sel then complement (Neg A) else Neg A) = complement (if atom (Pos A) \<in> Sel then complement (Pos A) else Pos A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
from r and q and p1 and p2 and rc_def
[PROOF STATE]
proof (chain)
picking this:
rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))
validated_part Sel (rename_clause Sel P1) = {}
strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))
strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))
rename_clause Sel C = rename_clause Sel P1 - {rename_literal Sel (Pos A)} \<union> (rename_clause Sel P2 - {rename_literal Sel (Neg A)})
[PROOF STEP]
show
    "ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2)(rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))
validated_part Sel (rename_clause Sel P1) = {}
strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))
strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))
rename_clause Sel C = rename_clause Sel P1 - {rename_literal Sel (Pos A)} \<union> (rename_clause Sel P2 - {rename_literal Sel (Neg A)})

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
using ordered_model_resolvent_def [of Sel "rename_clause Sel P1" "rename_clause Sel P2"
      "rename_clause Sel C"]
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Neg A) = complement (rename_literal Sel (Pos A))
validated_part Sel (rename_clause Sel P1) = {}
strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (rename_literal Sel (Neg A))
strictly_maximal_literal (rename_clause Sel P1) (rename_literal Sel (Pos A))
rename_clause Sel C = rename_clause Sel P1 - {rename_literal Sel (Pos A)} \<union> (rename_clause Sel P2 - {rename_literal Sel (Neg A)})
ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C) = (\<exists>L. rename_clause Sel C = rename_clause Sel P1 - {L} \<union> (rename_clause Sel P2 - {complement L}) \<and> (validated_part Sel (rename_clause Sel P1) = {} \<and> strictly_maximal_literal (rename_clause Sel P1) L) \<and> strictly_maximal_literal (validated_part Sel (rename_clause Sel P2)) (complement L))

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)

goal:
No subgoals!
[PROOF STEP]
qed