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

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

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>saturated_binary_rule (ordered_model_resolvent Sel) S; {} \<notin> S; all_fulfill finite 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_model_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_model_resolvent Sel) S; {} \<notin> S; all_fulfill finite S; \<not> satisfiable S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
saturated_binary_rule (ordered_model_resolvent Sel) S
{} \<notin> S
all_fulfill finite S
\<not> satisfiable S

goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
let ?S' = "rename_formula Sel S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
have "{} \<notin> ?S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> rename_formula Sel S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<in> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
assume "{} \<in> ?S'"
[PROOF STATE]
proof (state)
this:
{} \<in> rename_formula Sel S

goal (1 subgoal):
 1. {} \<in> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<in> rename_formula Sel S
[PROOF STEP]
obtain V where "V \<in> S" and "rename_clause Sel V = {}"
[PROOF STATE]
proof (prove)
using this:
{} \<in> rename_formula Sel S

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<in> S; rename_clause Sel V = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rename_formula_def
[PROOF STATE]
proof (prove)
using this:
{} \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC}

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<in> S; rename_clause Sel V = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<in> S
rename_clause Sel V = {}

goal (1 subgoal):
 1. {} \<in> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
from \<open>rename_clause Sel V = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel V = {}
[PROOF STEP]
have "V = {}"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel V = {}

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

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

goal (1 subgoal):
 1. {} \<in> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>V \<in> S\<close>  and \<open>{} \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
V = {}
V \<in> S
{} \<notin> S
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
V = {}
V \<in> S
{} \<notin> S

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:
{} \<notin> rename_formula Sel S

goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[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 ?S'"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S

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

goal (1 subgoal):
 1. \<forall>C. C \<in> {C. \<exists>CC. CC \<in> S \<and> C = {L. \<exists>LL. LL \<in> CC \<and> L = rename_literal Sel LL}} \<longrightarrow> finite C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
have "saturated_binary_rule (ordered_sel_resolvent UNIV) ?S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(saturated_binary_rule (ordered_sel_resolvent UNIV) ?S')"
[PROOF STATE]
proof (state)
this:
\<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
[PROOF STEP]
obtain P1 and P2 and C where "P1 \<in> ?S'" and "P2 \<in> ?S'"
      and "ordered_sel_resolvent UNIV P1 P2 C" and "\<not>tautology C"
      and not_subsumed: "\<forall>D. (D \<in> ?S' \<longrightarrow> \<not>subsumes D C)"
[PROOF STATE]
proof (prove)
using this:
\<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>P1 \<in> rename_formula Sel S; P2 \<in> rename_formula Sel S; ordered_sel_resolvent UNIV P1 P2 C; \<not> tautology C; \<forall>D. D \<in> rename_formula Sel S \<longrightarrow> \<not> subsumes D C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding saturated_binary_rule_def redundant_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>P1 P2 C. P1 \<in> rename_formula Sel S \<and> P2 \<in> rename_formula Sel S \<and> ordered_sel_resolvent UNIV P1 P2 C \<longrightarrow> tautology C \<or> (\<exists>D. D \<in> rename_formula Sel S \<and> subsumes D C))

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>P1 \<in> rename_formula Sel S; P2 \<in> rename_formula Sel S; ordered_sel_resolvent UNIV P1 P2 C; \<not> tautology C; \<forall>D. D \<in> rename_formula Sel S \<longrightarrow> \<not> subsumes D C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P1 \<in> rename_formula Sel S
P2 \<in> rename_formula Sel S
ordered_sel_resolvent UNIV P1 P2 C
\<not> tautology C
\<forall>D. D \<in> rename_formula Sel S \<longrightarrow> \<not> subsumes D C

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>ordered_sel_resolvent UNIV P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_sel_resolvent UNIV P1 P2 C
[PROOF STEP]
have ord_ren: "ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2)
                        (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent UNIV P1 P2 C

goal (1 subgoal):
 1. ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
[PROOF STEP]
using ordered_res_with_selection_is_model_res
[PROOF STATE]
proof (prove)
using this:
ordered_sel_resolvent UNIV P1 P2 C
ordered_sel_resolvent UNIV ?P1.0 ?P2.0 ?C \<Longrightarrow> ordered_model_resolvent ?Sel (rename_clause ?Sel ?P1.0) (rename_clause ?Sel ?P2.0) (rename_clause ?Sel ?C)

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 (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
have "\<not>tautology (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> tautology (rename_clause Sel C)
[PROOF STEP]
using renaming_preserves_tautology inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
tautology ?C \<Longrightarrow> tautology (rename_clause ?Sel ?C)
rename_clause ?A (rename_clause ?A ?L) = ?L

goal (1 subgoal):
 1. \<not> tautology (rename_clause Sel C)
[PROOF STEP]
by (metis \<open>\<not> tautology C\<close> inverse_clause_renaming renaming_preserves_tautology)
[PROOF STATE]
proof (state)
this:
\<not> tautology (rename_clause Sel C)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>P1 \<in> ?S'\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> rename_formula Sel S
[PROOF STEP]
have "rename_clause Sel P1 \<in> rename_formula Sel ?S'"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> rename_formula Sel S

goal (1 subgoal):
 1. rename_clause Sel P1 \<in> rename_formula Sel (rename_formula Sel S)
[PROOF STEP]
unfolding rename_formula_def
[PROOF STATE]
proof (prove)
using this:
P1 \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC}

goal (1 subgoal):
 1. rename_clause Sel P1 \<in> {C. \<exists>CC. CC \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC} \<and> C = rename_clause Sel CC}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause Sel P1 \<in> rename_formula Sel (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
hence "rename_clause Sel P1 \<in> S"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel P1 \<in> rename_formula Sel (rename_formula Sel S)

goal (1 subgoal):
 1. rename_clause Sel P1 \<in> S
[PROOF STEP]
using inverse_formula_renaming
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel P1 \<in> rename_formula Sel (rename_formula Sel S)
rename_formula ?A (rename_formula ?A ?L) = ?L

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>P2 \<in> ?S'\<close>
[PROOF STATE]
proof (chain)
picking this:
P2 \<in> rename_formula Sel S
[PROOF STEP]
have "rename_clause Sel P2 \<in> rename_formula Sel ?S'"
[PROOF STATE]
proof (prove)
using this:
P2 \<in> rename_formula Sel S

goal (1 subgoal):
 1. rename_clause Sel P2 \<in> rename_formula Sel (rename_formula Sel S)
[PROOF STEP]
unfolding rename_formula_def
[PROOF STATE]
proof (prove)
using this:
P2 \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC}

goal (1 subgoal):
 1. rename_clause Sel P2 \<in> {C. \<exists>CC. CC \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC} \<and> C = rename_clause Sel CC}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause Sel P2 \<in> rename_formula Sel (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
hence "rename_clause Sel P2 \<in> S"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel P2 \<in> rename_formula Sel (rename_formula Sel S)

goal (1 subgoal):
 1. rename_clause Sel P2 \<in> S
[PROOF STEP]
using inverse_formula_renaming
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel P2 \<in> rename_formula Sel (rename_formula Sel S)
rename_formula ?A (rename_formula ?A ?L) = ?L

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>tautology (rename_clause Sel C)\<close> and ord_ren
      and \<open>saturated_binary_rule (ordered_model_resolvent Sel) S\<close>
      and \<open>rename_clause Sel P1 \<in> S\<close> and \<open>rename_clause Sel P2 \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology (rename_clause Sel C)
ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
saturated_binary_rule (ordered_model_resolvent Sel) S
rename_clause Sel P1 \<in> S
rename_clause Sel P2 \<in> S
[PROOF STEP]
obtain D' where "D' \<in> S" and "subsumes D' (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology (rename_clause Sel C)
ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
saturated_binary_rule (ordered_model_resolvent Sel) S
rename_clause Sel P1 \<in> S
rename_clause Sel P2 \<in> S

goal (1 subgoal):
 1. (\<And>D'. \<lbrakk>D' \<in> S; subsumes D' (rename_clause Sel C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding saturated_binary_rule_def redundant_def
[PROOF STATE]
proof (prove)
using this:
\<not> tautology (rename_clause Sel C)
ordered_model_resolvent Sel (rename_clause Sel P1) (rename_clause Sel P2) (rename_clause Sel C)
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> ordered_model_resolvent Sel P1 P2 C \<longrightarrow> tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
rename_clause Sel P1 \<in> S
rename_clause Sel P2 \<in> S

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>subsumes D' (rename_clause Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes D' (rename_clause Sel C)
[PROOF STEP]
have "subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
using this:
subsumes D' (rename_clause Sel C)

goal (1 subgoal):
 1. subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))
[PROOF STEP]
using renaming_preserves_subsumption
[PROOF STATE]
proof (prove)
using this:
subsumes D' (rename_clause Sel C)
subsumes ?C ?D \<Longrightarrow> subsumes (rename_clause ?Sel ?C) (rename_clause ?Sel ?D)

goal (1 subgoal):
 1. subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
hence "subsumes (rename_clause Sel D') C"
[PROOF STATE]
proof (prove)
using this:
subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))

goal (1 subgoal):
 1. subsumes (rename_clause Sel D') C
[PROOF STEP]
using inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
subsumes (rename_clause Sel D') (rename_clause Sel (rename_clause Sel C))
rename_clause ?A (rename_clause ?A ?L) = ?L

goal (1 subgoal):
 1. subsumes (rename_clause Sel D') C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subsumes (rename_clause Sel D') C

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from \<open>D' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
D' \<in> S
[PROOF STEP]
have "rename_clause Sel D' \<in> ?S'"
[PROOF STATE]
proof (prove)
using this:
D' \<in> S

goal (1 subgoal):
 1. rename_clause Sel D' \<in> rename_formula Sel S
[PROOF STEP]
unfolding rename_formula_def
[PROOF STATE]
proof (prove)
using this:
D' \<in> S

goal (1 subgoal):
 1. rename_clause Sel D' \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause Sel CC}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause Sel D' \<in> rename_formula Sel S

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S) \<Longrightarrow> False
[PROOF STEP]
from this and not_subsumed and  \<open>subsumes (rename_clause Sel D') C\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel D' \<in> rename_formula Sel S
\<forall>D. D \<in> rename_formula Sel S \<longrightarrow> \<not> subsumes D C
subsumes (rename_clause Sel D') C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel D' \<in> rename_formula Sel S
\<forall>D. D \<in> rename_formula Sel S \<longrightarrow> \<not> subsumes D C
subsumes (rename_clause Sel D') 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:
saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>{} \<notin> ?S'\<close> and \<open>all_fulfill finite ?S'\<close>
[PROOF STATE]
proof (chain)
picking this:
saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
{} \<notin> rename_formula Sel S
all_fulfill finite (rename_formula Sel S)
[PROOF STEP]
have "satisfiable ?S'"
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
{} \<notin> rename_formula Sel S
all_fulfill finite (rename_formula Sel S)

goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
using ordered_resolution_is_complete_ordered_sel
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
{} \<notin> rename_formula Sel S
all_fulfill finite (rename_formula Sel S)
Complete (ordered_sel_resolvent ?Sel)

goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
unfolding Complete_def
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_sel_resolvent UNIV) (rename_formula Sel S)
{} \<notin> rename_formula Sel S
all_fulfill finite (rename_formula Sel S)
\<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. satisfiable (rename_formula Sel S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfiable (rename_formula Sel S)

goal (1 subgoal):
 1. \<not> Complete (ordered_model_resolvent Sel) \<Longrightarrow> False
[PROOF STEP]
hence "satisfiable (rename_formula Sel ?S')"
[PROOF STATE]
proof (prove)
using this:
satisfiable (rename_formula Sel S)

goal (1 subgoal):
 1. satisfiable (rename_formula Sel (rename_formula Sel S))
[PROOF STEP]
using renaming_preserves_satisfiability
[PROOF STATE]
proof (prove)
using this:
satisfiable (rename_formula Sel S)
satisfiable ?S \<Longrightarrow> satisfiable (rename_formula ?Sel ?S)

goal (1 subgoal):
 1. satisfiable (rename_formula Sel (rename_formula Sel S))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfiable (rename_formula Sel (rename_formula Sel S))

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using inverse_formula_renaming
[PROOF STATE]
proof (prove)
using this:
satisfiable (rename_formula Sel (rename_formula Sel S))
\<not> satisfiable S
rename_formula ?A (rename_formula ?A ?L) = ?L

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_interpretation_validate :
  "validate_literal {} L = (\<exists>A. (L = Neg A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<Turnstile> L = (\<exists>A. L = Neg A)
[PROOF STEP]
by (meson empty_iff validate_literal.elims(2) validate_literal.simps(2))


[STATEMENT]
lemma universal_interpretation_validate :
  "validate_literal UNIV L = (\<exists>A. (L = Pos A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<Turnstile> L = (\<exists>A. L = Pos A)
[PROOF STEP]
by (meson UNIV_I validate_literal.elims(2) validate_literal.simps(1))


[STATEMENT]
lemma negative_part_lemma:
  "(negative_part C) = (validated_part {} C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. negative_part C = validated_part {} C
[PROOF STEP]
unfolding negative_part_def validated_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {L. (\<exists>A. L = Neg A) \<and> L \<in> C} = {L \<in> C. {} \<Turnstile> L}
[PROOF STEP]
using empty_interpretation_validate
[PROOF STATE]
proof (prove)
using this:
{} \<Turnstile> ?L = (\<exists>A. ?L = Neg A)

goal (1 subgoal):
 1. {L. (\<exists>A. L = Neg A) \<and> L \<in> C} = {L \<in> C. {} \<Turnstile> L}
[PROOF STEP]
by blast


[STATEMENT]
lemma positive_part_lemma:
  "(positive_part C) = (validated_part UNIV C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive_part C = validated_part UNIV C
[PROOF STEP]
unfolding positive_part_def validated_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {L. (\<exists>A. L = Pos A) \<and> L \<in> C} = {L \<in> C. UNIV \<Turnstile> L}
[PROOF STEP]
using universal_interpretation_validate
[PROOF STATE]
proof (prove)
using this:
UNIV \<Turnstile> ?L = (\<exists>A. ?L = Pos A)

goal (1 subgoal):
 1. {L. (\<exists>A. L = Pos A) \<and> L \<in> C} = {L \<in> C. UNIV \<Turnstile> L}
[PROOF STEP]
by blast


[STATEMENT]
lemma negative_resolvent_is_model_res:
  "less_restrictive ordered_negative_resolvent (ordered_model_resolvent UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_restrictive ordered_negative_resolvent (ordered_model_resolvent UNIV)
[PROOF STEP]
unfolding ordered_negative_resolvent_def ordered_model_resolvent_def  less_restrictive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P1 P2 C. (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (validated_part UNIV P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (validated_part UNIV P2) (complement L)) \<longrightarrow> (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (positive_part P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (positive_part P2) (complement L)) \<or> (\<exists>L. C = P2 - {L} \<union> (P1 - {complement L}) \<and> (positive_part P2 = {} \<and> strictly_maximal_literal P2 L) \<and> strictly_maximal_literal (positive_part P1) (complement L))
[PROOF STEP]
using positive_part_lemma
[PROOF STATE]
proof (prove)
using this:
positive_part ?C = validated_part UNIV ?C

goal (1 subgoal):
 1. \<forall>P1 P2 C. (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (validated_part UNIV P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (validated_part UNIV P2) (complement L)) \<longrightarrow> (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (positive_part P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (positive_part P2) (complement L)) \<or> (\<exists>L. C = P2 - {L} \<union> (P1 - {complement L}) \<and> (positive_part P2 = {} \<and> strictly_maximal_literal P2 L) \<and> strictly_maximal_literal (positive_part P1) (complement L))
[PROOF STEP]
by auto


[STATEMENT]
lemma positive_resolvent_is_model_res:
  "less_restrictive ordered_positive_resolvent (ordered_model_resolvent {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_restrictive ordered_positive_resolvent (ordered_model_resolvent {})
[PROOF STEP]
unfolding ordered_positive_resolvent_def ordered_model_resolvent_def less_restrictive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P1 P2 C. (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (validated_part {} P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (validated_part {} P2) (complement L)) \<longrightarrow> (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (negative_part P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (negative_part P2) (complement L)) \<or> (\<exists>L. C = P2 - {L} \<union> (P1 - {complement L}) \<and> (negative_part P2 = {} \<and> strictly_maximal_literal P2 L) \<and> strictly_maximal_literal (negative_part P1) (complement L))
[PROOF STEP]
using negative_part_lemma
[PROOF STATE]
proof (prove)
using this:
negative_part ?C = validated_part {} ?C

goal (1 subgoal):
 1. \<forall>P1 P2 C. (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (validated_part {} P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (validated_part {} P2) (complement L)) \<longrightarrow> (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> (negative_part P1 = {} \<and> strictly_maximal_literal P1 L) \<and> strictly_maximal_literal (negative_part P2) (complement L)) \<or> (\<exists>L. C = P2 - {L} \<union> (P1 - {complement L}) \<and> (negative_part P2 = {} \<and> strictly_maximal_literal P2 L) \<and> strictly_maximal_literal (negative_part P1) (complement L))
[PROOF STEP]
by auto


[STATEMENT]
theorem ordered_positive_resolvent_is_complete : "Complete ordered_positive_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete ordered_positive_resolvent
[PROOF STEP]
using ordered_resolution_is_complete_model_resolution less_restrictive_complete positive_resolvent_is_model_res
[PROOF STATE]
proof (prove)
using this:
Complete (ordered_model_resolvent ?Sel)
\<lbrakk>less_restrictive ?R1.0 ?R2.0; Complete ?R2.0\<rbrakk> \<Longrightarrow> Complete ?R1.0
less_restrictive ordered_positive_resolvent (ordered_model_resolvent {})

goal (1 subgoal):
 1. Complete ordered_positive_resolvent
[PROOF STEP]
by auto


[STATEMENT]
theorem ordered_negative_resolvent_is_complete: "Complete ordered_negative_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete ordered_negative_resolvent
[PROOF STEP]
using ordered_resolution_is_complete_model_resolution less_restrictive_complete negative_resolvent_is_model_res
[PROOF STATE]
proof (prove)
using this:
Complete (ordered_model_resolvent ?Sel)
\<lbrakk>less_restrictive ?R1.0 ?R2.0; Complete ?R2.0\<rbrakk> \<Longrightarrow> Complete ?R1.0
less_restrictive ordered_negative_resolvent (ordered_model_resolvent UNIV)

goal (1 subgoal):
 1. Complete ordered_negative_resolvent
[PROOF STEP]
by auto


[STATEMENT]
theorem unit_resolvent_complete_for_Horn_renamable_set:
  assumes "saturated_binary_rule unit_resolvent S"
  assumes "all_fulfill finite S"
  assumes "{} \<notin> S"
  assumes "Horn_renamable_formula S"
  shows "satisfiable S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
from \<open>Horn_renamable_formula S\<close>
[PROOF STATE]
proof (chain)
picking this:
Horn_renamable_formula S
[PROOF STEP]
obtain I where "all_fulfill Horn (rename_formula I S)"
[PROOF STATE]
proof (prove)
using this:
Horn_renamable_formula S

goal (1 subgoal):
 1. (\<And>I. all_fulfill Horn (rename_formula I S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Horn_renamable_formula_def
[PROOF STATE]
proof (prove)
using this:
\<exists>I. all_fulfill Horn (rename_formula I S)

goal (1 subgoal):
 1. (\<And>I. all_fulfill Horn (rename_formula I S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill Horn (rename_formula I S)

goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
have "saturated_binary_rule (ordered_model_resolvent I) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule (ordered_model_resolvent I) S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>saturated_binary_rule (ordered_model_resolvent I) S"
[PROOF STATE]
proof (state)
this:
\<not> saturated_binary_rule (ordered_model_resolvent I) S

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

goal (1 subgoal):
 1. (\<And>P1 P2 C. \<lbrakk>ordered_model_resolvent I P1 P2 C; P1 \<in> S; P2 \<in> S; \<not> redundant C 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> S \<and> P2 \<in> S \<and> ordered_model_resolvent I P1 P2 C \<longrightarrow> redundant C S)

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from \<open>ordered_model_resolvent I P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
ordered_model_resolvent I P1 P2 C
[PROOF STEP]
obtain L
      where def_c: "C = ( (P1 - { L }) \<union> ( P2 - { (complement L) }))"
      and "strictly_maximal_literal P1 L" and "validated_part I P1 = {}"
      and "strictly_maximal_literal (validated_part I P2) (complement L)"
[PROOF STATE]
proof (prove)
using this:
ordered_model_resolvent I P1 P2 C

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal P1 L\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal P1 L
[PROOF STEP]
have "L \<in> P1"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P1 L

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal (validated_part I P2) (complement L)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (validated_part I P2) (complement L)
[PROOF STEP]
have "complement L \<in> P2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (validated_part I P2) (complement L)

goal (1 subgoal):
 1. complement L \<in> P2
[PROOF STEP]
unfolding strictly_maximal_literal_def validated_part_def
[PROOF STATE]
proof (prove)
using this:
complement L \<in> {L \<in> P2. I \<Turnstile> L} \<and> (\<forall>B. B \<in> {L \<in> P2. I \<Turnstile> L} \<and> complement L \<noteq> B \<longrightarrow> literal_ordering B (complement L))

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
have "selected_part UNIV (rename_clause I P1)
      =  rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))
[PROOF STEP]
using renaming_and_selected_part [of "rename_clause I P1" I]
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))

goal (1 subgoal):
 1. selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))
[PROOF STEP]
have "selected_part UNIV (rename_clause I P1) =  rename_clause I (validated_part I P1)"
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))

goal (1 subgoal):
 1. selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I P1)
[PROOF STEP]
using inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I (rename_clause I (rename_clause I P1)))
rename_clause ?A (rename_clause ?A ?L) = ?L

goal (1 subgoal):
 1. selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I P1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I P1)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validated_part I P1 = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I P1)
validated_part I P1 = {}
[PROOF STEP]
have "selected_part UNIV (rename_clause I P1) = {}"
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV (rename_clause I P1) = rename_clause I (validated_part I P1)
validated_part I P1 = {}

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selected_part UNIV (rename_clause I P1) = {}
[PROOF STEP]
have "negative_part (rename_clause I P1) = {}"
[PROOF STATE]
proof (prove)
using this:
selected_part UNIV (rename_clause I P1) = {}

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

goal (1 subgoal):
 1. {L. (\<exists>A. L = Neg A) \<and> L \<in> rename_clause I P1} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
negative_part (rename_clause I P1) = {}

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from \<open>all_fulfill Horn (rename_formula I S)\<close> and \<open>P1 \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill Horn (rename_formula I S)
P1 \<in> S
[PROOF STEP]
have "Horn (rename_clause I P1)"
[PROOF STATE]
proof (prove)
using this:
all_fulfill Horn (rename_formula I S)
P1 \<in> S

goal (1 subgoal):
 1. Horn (rename_clause I P1)
[PROOF STEP]
unfolding all_fulfill_def and rename_formula_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C. C \<in> {C. \<exists>CC. CC \<in> S \<and> C = rename_clause I CC} \<longrightarrow> Horn C
P1 \<in> S

goal (1 subgoal):
 1. Horn (rename_clause I P1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Horn (rename_clause I P1)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Horn (rename_clause I P1)
[PROOF STEP]
have "card (positive_part (rename_clause I P1)) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
Horn (rename_clause I P1)

goal (1 subgoal):
 1. card (positive_part (rename_clause I P1)) \<le> 1
[PROOF STEP]
unfolding Horn_def
[PROOF STATE]
proof (prove)
using this:
card (positive_part (rename_clause I P1)) \<le> 1

goal (1 subgoal):
 1. card (positive_part (rename_clause I P1)) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (positive_part (rename_clause I P1)) \<le> 1

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from  \<open>negative_part (rename_clause I P1) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
negative_part (rename_clause I P1) = {}
[PROOF STEP]
have "rename_clause I P1 = (positive_part (rename_clause I P1))"
[PROOF STATE]
proof (prove)
using this:
negative_part (rename_clause I P1) = {}

goal (1 subgoal):
 1. rename_clause I P1 = positive_part (rename_clause I P1)
[PROOF STEP]
using decomposition_clause_pos_neg
[PROOF STATE]
proof (prove)
using this:
negative_part (rename_clause I P1) = {}
?C = negative_part ?C \<union> positive_part ?C

goal (1 subgoal):
 1. rename_clause I P1 = positive_part (rename_clause I P1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause I P1 = positive_part (rename_clause I P1)

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>card (positive_part (rename_clause I P1)) \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_clause I P1 = positive_part (rename_clause I P1)
card (positive_part (rename_clause I P1)) \<le> 1
[PROOF STEP]
have "card (rename_clause I P1) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
rename_clause I P1 = positive_part (rename_clause I P1)
card (positive_part (rename_clause I P1)) \<le> 1

goal (1 subgoal):
 1. card (rename_clause I P1) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (rename_clause I P1) \<le> 1

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal P1 L\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal P1 L
[PROOF STEP]
have "P1 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P1 L

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P1 \<noteq> {}
[PROOF STEP]
have "rename_clause I P1 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
P1 \<noteq> {}

goal (1 subgoal):
 1. rename_clause I P1 \<noteq> {}
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
P1 \<noteq> {}

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

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

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite P1
[PROOF STEP]
have "finite (rename_clause I P1)"
[PROOF STATE]
proof (prove)
using this:
finite P1

goal (1 subgoal):
 1. finite (rename_clause I P1)
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
finite P1

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>rename_clause I P1 \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (rename_clause I P1)
rename_clause I P1 \<noteq> {}
[PROOF STEP]
have "card(rename_clause I P1) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite (rename_clause I P1)
rename_clause I P1 \<noteq> {}

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

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>card (rename_clause I P1) \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
card (rename_clause I P1) \<noteq> 0
card (rename_clause I P1) \<le> 1
[PROOF STEP]
have "card (rename_clause I P1) = 1"
[PROOF STATE]
proof (prove)
using this:
card (rename_clause I P1) \<noteq> 0
card (rename_clause I P1) \<le> 1

goal (1 subgoal):
 1. card (rename_clause I P1) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (rename_clause I P1) = 1

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (rename_clause I P1) = 1
[PROOF STEP]
have "card P1 = 1"
[PROOF STATE]
proof (prove)
using this:
card (rename_clause I P1) = 1

goal (1 subgoal):
 1. card P1 = 1
[PROOF STEP]
using renaming_preserves_cardinality
[PROOF STATE]
proof (prove)
using this:
card (rename_clause I P1) = 1
card (rename_clause ?A ?C) = card ?C

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

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card P1 = 1
[PROOF STEP]
have "Unit P1"
[PROOF STATE]
proof (prove)
using this:
card P1 = 1

goal (1 subgoal):
 1. Unit P1
[PROOF STEP]
unfolding Unit_def
[PROOF STATE]
proof (prove)
using this:
card P1 = 1

goal (1 subgoal):
 1. card P1 = 1
[PROOF STEP]
using card_image
[PROOF STATE]
proof (prove)
using this:
card P1 = 1
inj_on ?f ?A \<Longrightarrow> card (?f ` ?A) = card ?A

goal (1 subgoal):
 1. card P1 = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Unit P1

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L \<in> P1\<close> and \<open>complement L \<in> P2\<close> and def_c
[PROOF STATE]
proof (chain)
picking this:
Unit P1
L \<in> P1
complement L \<in> P2
C = P1 - {L} \<union> (P2 - {complement L})
[PROOF STEP]
have "unit_resolvent P1 P2 C"
[PROOF STATE]
proof (prove)
using this:
Unit P1
L \<in> P1
complement L \<in> P2
C = P1 - {L} \<union> (P2 - {complement L})

goal (1 subgoal):
 1. unit_resolvent P1 P2 C
[PROOF STEP]
unfolding unit_resolvent_def
[PROOF STATE]
proof (prove)
using this:
Unit P1
L \<in> P1
complement L \<in> P2
C = P1 - {L} \<union> (P2 - {complement L})

goal (1 subgoal):
 1. (\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> L \<in> P1 \<and> complement L \<in> P2) \<and> Unit P1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_resolvent P1 P2 C

goal (1 subgoal):
 1. \<not> saturated_binary_rule (ordered_model_resolvent I) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>(redundant C S)\<close> and \<open>P1 \<in> S\<close> and \<open>P2 \<in> S\<close>
      and \<open>saturated_binary_rule unit_resolvent S\<close>
[PROOF STATE]
proof (chain)
picking this:
unit_resolvent P1 P2 C
\<not> redundant C S
P1 \<in> S
P2 \<in> S
saturated_binary_rule unit_resolvent S
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
unit_resolvent P1 P2 C
\<not> redundant C S
P1 \<in> S
P2 \<in> S
saturated_binary_rule unit_resolvent S

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

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_model_resolvent I) S

goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
from this and \<open>all_fulfill finite S\<close> and \<open>{} \<notin> S\<close>
[PROOF STATE]
proof (chain)
picking this:
saturated_binary_rule (ordered_model_resolvent I) S
all_fulfill finite S
{} \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_model_resolvent I) S
all_fulfill finite S
{} \<notin> S

goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
using ordered_resolution_is_complete_model_resolution
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_model_resolvent I) S
all_fulfill finite S
{} \<notin> S
Complete (ordered_model_resolvent ?Sel)

goal (1 subgoal):
 1. satisfiable S
[PROOF STEP]
unfolding Complete_def
[PROOF STATE]
proof (prove)
using this:
saturated_binary_rule (ordered_model_resolvent I) S
all_fulfill finite S
{} \<notin> S
\<forall>S. saturated_binary_rule (ordered_model_resolvent ?Sel) S \<longrightarrow> all_fulfill finite S \<longrightarrow> {} \<notin> S \<longrightarrow> satisfiable S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ordered_resolvent_is_finite : "derived_clauses_are_finite ordered_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite ordered_resolvent
[PROOF STEP]
using less_restrictive_and_finite ordered_resolvent_is_resolvent resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_restrictive ?R1.0 ?R2.0; derived_clauses_are_finite ?R1.0\<rbrakk> \<Longrightarrow> derived_clauses_are_finite ?R2.0
less_restrictive resolvent ordered_resolvent
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. derived_clauses_are_finite ordered_resolvent
[PROOF STEP]
by auto


[STATEMENT]
theorem model_resolvent_is_finite : "derived_clauses_are_finite (ordered_model_resolvent I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite (ordered_model_resolvent I)
[PROOF STEP]
using less_restrictive_and_finite ordered_model_resolvent_is_resolvent resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_restrictive ?R1.0 ?R2.0; derived_clauses_are_finite ?R1.0\<rbrakk> \<Longrightarrow> derived_clauses_are_finite ?R2.0
less_restrictive resolvent (ordered_model_resolvent ?I)
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. derived_clauses_are_finite (ordered_model_resolvent I)
[PROOF STEP]
by auto


[STATEMENT]
theorem positive_resolvent_is_finite : "derived_clauses_are_finite ordered_positive_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite ordered_positive_resolvent
[PROOF STEP]
using less_restrictive_and_finite positive_resolvent_is_resolvent resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_restrictive ?R1.0 ?R2.0; derived_clauses_are_finite ?R1.0\<rbrakk> \<Longrightarrow> derived_clauses_are_finite ?R2.0
less_restrictive resolvent ordered_positive_resolvent
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. derived_clauses_are_finite ordered_positive_resolvent
[PROOF STEP]
by auto


[STATEMENT]
theorem negative_resolvent_is_finite : "derived_clauses_are_finite ordered_negative_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite ordered_negative_resolvent
[PROOF STEP]
using less_restrictive_and_finite negative_resolvent_is_resolvent resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_restrictive ?R1.0 ?R2.0; derived_clauses_are_finite ?R1.0\<rbrakk> \<Longrightarrow> derived_clauses_are_finite ?R2.0
less_restrictive resolvent ordered_negative_resolvent
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. derived_clauses_are_finite ordered_negative_resolvent
[PROOF STEP]
by auto


[STATEMENT]
theorem unit_resolvent_is_finite : "derived_clauses_are_finite unit_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite unit_resolvent
[PROOF STEP]
using less_restrictive_and_finite unit_resolvent_is_resolvent resolvent_is_finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_restrictive ?R1.0 ?R2.0; derived_clauses_are_finite ?R1.0\<rbrakk> \<Longrightarrow> derived_clauses_are_finite ?R2.0
less_restrictive resolvent unit_resolvent
derived_clauses_are_finite resolvent

goal (1 subgoal):
 1. derived_clauses_are_finite unit_resolvent
[PROOF STEP]
by auto


[STATEMENT]
lemma all_deducible_clauses_are_finite:
  assumes "derived_clauses_are_finite R"
  assumes "all_fulfill finite S"
  shows "all_fulfill finite (all_deducible_clauses R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_fulfill finite (all_deducible_clauses R S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> all_fulfill finite (all_deducible_clauses R S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>all_fulfill finite (all_deducible_clauses R S)"
[PROOF STATE]
proof (state)
this:
\<not> all_fulfill finite (all_deducible_clauses R S)

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

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> all_deducible_clauses R S; infinite C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C. C \<in> all_deducible_clauses R S \<longrightarrow> finite C)

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. R P1 P2 C \<and> P1 \<in> S \<and> P2 \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2. R P1 P2 C \<and> P1 \<in> S \<and> P2 \<in> S

goal (1 subgoal):
 1. \<not> all_fulfill finite (all_deducible_clauses R S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1 P2. R P1 P2 C \<and> P1 \<in> S \<and> P2 \<in> S
[PROOF STEP]
obtain P1 P2 where "R P1 P2 C" and "P1 \<in> S" and "P2 \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1 P2. R P1 P2 C \<and> P1 \<in> S \<and> P2 \<in> S

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> all_fulfill finite (all_deducible_clauses R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>finite P1\<close> and \<open>finite P2\<close> and \<open>derived_clauses_are_finite R\<close> and \<open>R P1 P2 C\<close> and \<open>\<not>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
finite P1
finite P2
derived_clauses_are_finite R
R P1 P2 C
infinite C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
finite P1
finite P2
derived_clauses_are_finite R
R P1 P2 C
infinite C

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_inferred_clause_sets_are_finite:
  assumes "derived_clauses_are_finite R"
  assumes "all_fulfill finite S"
  shows "all_fulfill finite (inferred_clause_sets R S N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S N)
[PROOF STEP]
proof (induction N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. all_fulfill finite (inferred_clause_sets R S 0)
 2. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
derived_clauses_are_finite R
all_fulfill finite S
[PROOF STEP]
show "all_fulfill finite (inferred_clause_sets R S 0)"
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S 0)
[PROOF STEP]
using simplify_finite
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
all_fulfill finite ?S \<Longrightarrow> all_fulfill finite (simplify ?S)

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (inferred_clause_sets R S 0)

goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
fix N
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
assume "all_fulfill finite (inferred_clause_sets R S N)"
[PROOF STATE]
proof (state)
this:
all_fulfill finite (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (inferred_clause_sets R S N)
[PROOF STEP]
have "all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (inferred_clause_sets R S N)

goal (1 subgoal):
 1. all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
using assms(1) all_deducible_clauses_are_finite [of R "inferred_clause_sets R S N"]
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (inferred_clause_sets R S N)
derived_clauses_are_finite R
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
from this and \<open>all_fulfill finite (inferred_clause_sets R S N)\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
all_fulfill finite (inferred_clause_sets R S N)
[PROOF STEP]
have "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
all_fulfill finite (inferred_clause_sets R S N)

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

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. \<And>N. all_fulfill finite (inferred_clause_sets R S N) \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
show "all_fulfill finite (inferred_clause_sets R S (Suc N))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
using simplify_finite
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
all_fulfill finite ?S \<Longrightarrow> all_fulfill finite (simplify ?S)

goal (1 subgoal):
 1. all_fulfill finite (inferred_clause_sets R S (Suc N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (inferred_clause_sets R S (Suc N))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_all_deducible_clauses_finite:
  assumes "derived_clauses_are_finite R"
  assumes "all_fulfill finite S"
  shows "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
derived_clauses_are_finite R
all_fulfill finite S
[PROOF STEP]
have "all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S

goal (1 subgoal):
 1. all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
using all_deducible_clauses_are_finite [of R "inferred_clause_sets R S N"]
    all_inferred_clause_sets_are_finite [of R S N]
[PROOF STATE]
proof (prove)
using this:
derived_clauses_are_finite R
all_fulfill finite S
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite S\<rbrakk> \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S N)

goal (1 subgoal):
 1. all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
show "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
using assms all_fulfill_def all_inferred_clause_sets_are_finite [of R S "N"]
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (all_deducible_clauses R (inferred_clause_sets R S N))
derived_clauses_are_finite R
all_fulfill finite S
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite S\<rbrakk> \<Longrightarrow> all_fulfill finite (inferred_clause_sets R S N)

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S N))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sequence_of_inferred_clause_sets_is_monotonous:
 assumes "derived_clauses_are_finite R"
 assumes "all_fulfill finite S"
 shows "\<forall>C. redundant C (inferred_clause_sets R S N)
  \<longrightarrow> redundant C (inferred_clause_sets R S (N+M::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))
[PROOF STEP]
proof ((induction M), auto simp del: inferred_clause_sets.simps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
fix M C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
assume ind_hyp: "\<forall>C. redundant C (inferred_clause_sets R S N)
    \<longrightarrow> redundant C (inferred_clause_sets R S (N+M::nat))"
[PROOF STATE]
proof (state)
this:
\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
assume "redundant C (inferred_clause_sets R S N)"
[PROOF STATE]
proof (state)
this:
redundant C (inferred_clause_sets R S N)

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
from this and ind_hyp
[PROOF STATE]
proof (chain)
picking this:
redundant C (inferred_clause_sets R S N)
\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))
[PROOF STEP]
have "redundant C (inferred_clause_sets R S (N+M))"
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S N)
\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))

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

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
redundant C (inferred_clause_sets R S (N + M))
[PROOF STEP]
have "redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))"
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S (N + M))

goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
using deducible_clause_preserve_redundancy
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S (N + M))
redundant ?C ?S \<Longrightarrow> redundant ?C (add_all_deducible_clauses ?R ?S)

goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
have "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))"
[PROOF STATE]
proof (prove)
using this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
using assms  add_all_deducible_clauses_finite [of R S "N+M"]
[PROOF STATE]
proof (prove)
using this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
derived_clauses_are_finite R
all_fulfill finite S
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite S\<rbrakk> \<Longrightarrow> all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
from  \<open>redundant C (inferred_clause_sets R S N)\<close> and ind_hyp
[PROOF STATE]
proof (chain)
picking this:
redundant C (inferred_clause_sets R S N)
\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))
[PROOF STEP]
have "redundant C (inferred_clause_sets R S (N+M))"
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S N)
\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M))

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

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
from  \<open>redundant C (inferred_clause_sets R S (N+M))\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant C (inferred_clause_sets R S (N + M))
[PROOF STEP]
have "redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))"
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S (N + M))

goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
using deducible_clause_preserve_redundancy
[PROOF STATE]
proof (prove)
using this:
redundant C (inferred_clause_sets R S (N + M))
redundant ?C ?S \<Longrightarrow> redundant ?C (add_all_deducible_clauses ?R ?S)

goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
from this and \<open>all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
have "redundant C (simplify (add_all_deducible_clauses R (inferred_clause_sets R S (N+M))))"
[PROOF STATE]
proof (prove)
using this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. redundant C (simplify (add_all_deducible_clauses R (inferred_clause_sets R S (N + M))))
[PROOF STEP]
using simplify_preserves_redundancy
[PROOF STATE]
proof (prove)
using this:
redundant C (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
\<lbrakk>all_fulfill finite ?S; redundant ?C ?S\<rbrakk> \<Longrightarrow> redundant ?C (simplify ?S)

goal (1 subgoal):
 1. redundant C (simplify (add_all_deducible_clauses R (inferred_clause_sets R S (N + M))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (simplify (add_all_deducible_clauses R (inferred_clause_sets R S (N + M))))

goal (1 subgoal):
 1. \<And>M C. \<lbrakk>\<forall>C. redundant C (inferred_clause_sets R S N) \<longrightarrow> redundant C (inferred_clause_sets R S (N + M)); redundant C (inferred_clause_sets R S N)\<rbrakk> \<Longrightarrow> redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
thus "redundant C (inferred_clause_sets R S (Suc (N + M)))"
[PROOF STATE]
proof (prove)
using this:
redundant C (simplify (add_all_deducible_clauses R (inferred_clause_sets R S (N + M))))

goal (1 subgoal):
 1. redundant C (inferred_clause_sets R S (Suc (N + M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant C (inferred_clause_sets R S (Suc (N + M)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_persistent_clauses_are_redundant:
  assumes "D \<in> inferred_clause_sets R S N"
  assumes "D \<notin> saturation R S"
  assumes "all_fulfill finite S"
  assumes "derived_clauses_are_finite R"
  shows "\<exists>M. strictly_redundant D (inferred_clause_sets R S M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. strictly_redundant D (inferred_clause_sets R S M)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
assume hyp: "\<not>(\<exists>M. strictly_redundant D (inferred_clause_sets R S M))"
[PROOF STATE]
proof (state)
this:
\<nexists>M. strictly_redundant D (inferred_clause_sets R S M)

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<nexists>M. strictly_redundant D (inferred_clause_sets R S M)

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
have "D \<in> (inferred_clause_sets R S (N+M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<in> inferred_clause_sets R S (N + M)
[PROOF STEP]
proof (induction M)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D \<in> inferred_clause_sets R S (N + 0)
 2. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
show "D \<in> inferred_clause_sets R S (N+0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<in> inferred_clause_sets R S (N + 0)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
D \<in> inferred_clause_sets R S N

goal (1 subgoal):
 1. D \<in> inferred_clause_sets R S (N + 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<in> inferred_clause_sets R S (N + 0)

goal (1 subgoal):
 1. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
assume "D \<in> inferred_clause_sets R S (N+M)"
[PROOF STATE]
proof (state)
this:
D \<in> inferred_clause_sets R S (N + M)

goal (1 subgoal):
 1. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
D \<in> inferred_clause_sets R S (N + M)
[PROOF STEP]
have "D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N+M))"
[PROOF STATE]
proof (prove)
using this:
D \<in> inferred_clause_sets R S (N + M)

goal (1 subgoal):
 1. D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N + M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N + M))

goal (1 subgoal):
 1. \<And>M. D \<in> inferred_clause_sets R S (N + M) \<Longrightarrow> D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
show "D \<in> (inferred_clause_sets R S (N+(Suc M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<in> inferred_clause_sets R S (N + Suc M)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D \<notin> inferred_clause_sets R S (N + Suc M) \<Longrightarrow> False
[PROOF STEP]
assume "D \<notin> (inferred_clause_sets R S (N+(Suc M)))"
[PROOF STATE]
proof (state)
this:
D \<notin> inferred_clause_sets R S (N + Suc M)

goal (1 subgoal):
 1. D \<notin> inferred_clause_sets R S (N + Suc M) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N+M))\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<notin> inferred_clause_sets R S (N + Suc M)
D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N + M))
[PROOF STEP]
have "strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))"
[PROOF STATE]
proof (prove)
using this:
D \<notin> inferred_clause_sets R S (N + Suc M)
D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N + M))

goal (1 subgoal):
 1. strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
using simplify_def
[PROOF STATE]
proof (prove)
using this:
D \<notin> inferred_clause_sets R S (N + Suc M)
D \<in> add_all_deducible_clauses R (inferred_clause_sets R S (N + M))
simplify ?S = {C \<in> ?S. \<not> strictly_redundant C ?S}

goal (1 subgoal):
 1. strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. D \<notin> inferred_clause_sets R S (N + Suc M) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
have "all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))"
[PROOF STATE]
proof (prove)
using this:
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
using assms(4) assms(3)  add_all_deducible_clauses_finite [of R S "N+M"]
[PROOF STATE]
proof (prove)
using this:
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
derived_clauses_are_finite R
all_fulfill finite S
\<lbrakk>derived_clauses_are_finite R; all_fulfill finite S\<rbrakk> \<Longrightarrow> all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. D \<notin> inferred_clause_sets R S (N + Suc M) \<Longrightarrow> False
[PROOF STEP]
from this
          and \<open>strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N+M)))\<close>
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
[PROOF STEP]
have "strictly_redundant D (inferred_clause_sets R S (N+(Suc M)))"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))

goal (1 subgoal):
 1. strictly_redundant D (inferred_clause_sets R S (N + Suc M))
[PROOF STEP]
using simplify_preserves_strict_redundancy
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
strictly_redundant D (add_all_deducible_clauses R (inferred_clause_sets R S (N + M)))
\<lbrakk>all_fulfill finite ?S; strictly_redundant ?C ?S\<rbrakk> \<Longrightarrow> strictly_redundant ?C (simplify ?S)

goal (1 subgoal):
 1. strictly_redundant D (inferred_clause_sets R S (N + Suc M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_redundant D (inferred_clause_sets R S (N + Suc M))

goal (1 subgoal):
 1. D \<notin> inferred_clause_sets R S (N + Suc M) \<Longrightarrow> False
[PROOF STEP]
from this and hyp
[PROOF STATE]
proof (chain)
picking this:
strictly_redundant D (inferred_clause_sets R S (N + Suc M))
\<nexists>M. strictly_redundant D (inferred_clause_sets R S M)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
strictly_redundant D (inferred_clause_sets R S (N + Suc M))
\<nexists>M. strictly_redundant D (inferred_clause_sets R S M)

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:
D \<in> inferred_clause_sets R S (N + Suc M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
D \<in> inferred_clause_sets R S (N + M)

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
D \<in> inferred_clause_sets R S (N + ?M2)

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
from assms(2) and assms(1)
[PROOF STATE]
proof (chain)
picking this:
D \<notin> saturation R S
D \<in> inferred_clause_sets R S N
[PROOF STEP]
have "\<not>(\<forall>M'. (M' \<ge> N \<longrightarrow> D \<in> inferred_clause_sets R S M'))"
[PROOF STATE]
proof (prove)
using this:
D \<notin> saturation R S
D \<in> inferred_clause_sets R S N

goal (1 subgoal):
 1. \<not> (\<forall>M'\<ge>N. D \<in> inferred_clause_sets R S M')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>M'\<ge>N. D \<in> inferred_clause_sets R S M')

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>M'\<ge>N. D \<in> inferred_clause_sets R S M')
[PROOF STEP]
obtain M' where "M' \<ge> N" and "D \<notin> inferred_clause_sets R S M'"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>M'\<ge>N. D \<in> inferred_clause_sets R S M')

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>N \<le> M'; D \<notin> inferred_clause_sets R S M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N \<le> M'
D \<notin> inferred_clause_sets R S M'

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
from \<open>M' \<ge> N\<close>
[PROOF STATE]
proof (chain)
picking this:
N \<le> M'
[PROOF STEP]
obtain N':: nat where "N' = M' - N"
[PROOF STATE]
proof (prove)
using this:
N \<le> M'

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

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
have "D \<in> inferred_clause_sets R S (N+(M'-N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<in> inferred_clause_sets R S (N + (M' - N))
[PROOF STEP]
by (simp add: \<open>\<And>M. D \<in> inferred_clause_sets R S (N + M)\<close>)
[PROOF STATE]
proof (state)
this:
D \<in> inferred_clause_sets R S (N + (M' - N))

goal (1 subgoal):
 1. \<nexists>M. strictly_redundant D (inferred_clause_sets R S M) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>D \<notin> inferred_clause_sets R S M'\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<in> inferred_clause_sets R S (N + (M' - N))
D \<notin> inferred_clause_sets R S M'
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
D \<in> inferred_clause_sets R S (N + (M' - N))
D \<notin> inferred_clause_sets R S M'

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: \<open>N \<le> M'\<close>)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed