[STATEMENT]
lemma renaming_preserves_satisfiability:
  assumes "satisfiable S"
  shows "satisfiable (rename_formula Sel S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
satisfiable S
[PROOF STEP]
obtain I where "validate_formula I S"
[PROOF STATE]
proof (prove)
using this:
satisfiable S

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

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

goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
let ?J = "rename_interpretation Sel I"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
have "validate_formula ?J (rename_formula Sel S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_formula Sel S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> rename_interpretation Sel I \<Turnstile> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>validate_formula ?J (rename_formula Sel S)"
[PROOF STATE]
proof (state)
this:
\<not> rename_interpretation Sel I \<Turnstile> rename_formula Sel S

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

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

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

goal (1 subgoal):
 1. \<not> rename_interpretation Sel I \<Turnstile> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> S\<close> and \<open>validate_formula I S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
I \<Turnstile> S
[PROOF STEP]
obtain L where "L \<in> C"
      and "validate_literal I L"
[PROOF STATE]
proof (prove)
using this:
C \<in> S
I \<Turnstile> S

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

goal (1 subgoal):
 1. \<not> rename_interpretation Sel I \<Turnstile> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_literal I L\<close>
[PROOF STATE]
proof (chain)
picking this:
I \<Turnstile> L
[PROOF STEP]
have "validate_literal ?J (rename_literal Sel L)"
[PROOF STATE]
proof (prove)
using this:
I \<Turnstile> L

goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
using renaming_preserves_semantic
[PROOF STATE]
proof (prove)
using this:
I \<Turnstile> L
?I \<Turnstile> ?L \<Longrightarrow> rename_interpretation ?Sel ?I \<Turnstile> rename_literal ?Sel ?L

goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L

goal (1 subgoal):
 1. \<not> rename_interpretation Sel I \<Turnstile> rename_formula Sel S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L \<in> C\<close> and \<open>\<not>validate_clause ?J (rename_clause Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L
L \<in> C
\<not> rename_interpretation Sel I \<Turnstile> rename_clause Sel C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L
L \<in> C
\<not> rename_interpretation Sel I \<Turnstile> rename_clause Sel C

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

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:
rename_interpretation Sel I \<Turnstile> rename_formula Sel S

goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
rename_interpretation Sel I \<Turnstile> rename_formula Sel S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rename_interpretation Sel I \<Turnstile> rename_formula Sel S

goal (1 subgoal):
 1. satisfiable (rename_formula Sel S)
[PROOF STEP]
unfolding satisfiable_def
[PROOF STATE]
proof (prove)
using this:
rename_interpretation Sel I \<Turnstile> rename_formula Sel S

goal (1 subgoal):
 1. \<exists>I. I \<Turnstile> rename_formula Sel S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfiable (rename_formula Sel S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_preserves_subsumption:
  assumes "subsumes C D"
  shows "subsumes (rename_clause Sel C) (rename_clause Sel D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subsumes (rename_clause Sel C) (rename_clause Sel D)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subsumes C D

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

goal (1 subgoal):
 1. {L. \<exists>LL. LL \<in> C \<and> L = rename_literal Sel LL} \<subseteq> {L. \<exists>LL. LL \<in> D \<and> L = rename_literal Sel LL}
[PROOF STEP]
by auto


[STATEMENT]
lemma soundness_and_entailment :
  assumes "Sound Rule"
  assumes "Rule P1 P2 C"
  assumes "P1 \<in> S"
  assumes "P2 \<in> S"
  shows "entails S C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails S C
[PROOF STEP]
using Sound_def assms entails_def
[PROOF STATE]
proof (prove)
using this:
Sound ?Rule \<equiv> \<forall>I P1 P2 C. ?Rule P1 P2 C \<longrightarrow> I \<Turnstile> P1 \<longrightarrow> I \<Turnstile> P2 \<longrightarrow> I \<Turnstile> C
Sound Rule
Rule P1 P2 C
P1 \<in> S
P2 \<in> S
entails ?S ?C \<equiv> \<forall>I. I \<Turnstile> ?S \<longrightarrow> I \<Turnstile> ?C

goal (1 subgoal):
 1. entails S C
[PROOF STEP]
by auto


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

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

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

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

goal (1 subgoal):
 1. \<not> entails_formula S (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]
obtain P1 P2 where "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. (\<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> entails_formula S (all_deducible_clauses R S) \<Longrightarrow> False
[PROOF STEP]
from \<open>R P1 P2 C\<close>and assms(1) and \<open>P1 \<in> S\<close> and \<open>P2 \<in> S\<close> and \<open>\<not> entails S C\<close>
[PROOF STATE]
proof (chain)
picking this:
R P1 P2 C
Sound R
P1 \<in> S
P2 \<in> S
\<not> entails S C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
R P1 P2 C
Sound R
P1 \<in> S
P2 \<in> S
\<not> entails S C

goal (1 subgoal):
 1. False
[PROOF STEP]
using soundness_and_entailment
[PROOF STATE]
proof (prove)
using this:
R P1 P2 C
Sound R
P1 \<in> S
P2 \<in> S
\<not> entails S C
\<lbrakk>Sound ?Rule; ?Rule ?P1.0 ?P2.0 ?C; ?P1.0 \<in> ?S; ?P2.0 \<in> ?S\<rbrakk> \<Longrightarrow> entails ?S ?C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_all_deducible_sound:
  assumes "Sound R"
  shows "entails_formula S (add_all_deducible_clauses R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S (add_all_deducible_clauses R S)
[PROOF STEP]
by (metis UnE add_all_deducible_clauses.simps all_deducible_sound assms
      entails_formula_def entails_member)


[STATEMENT]
lemma less_restrictive_correct:
  assumes "less_restrictive R1 R2"
  assumes "Sound R1"
  shows "Sound R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sound R2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
less_restrictive R1 R2
Sound R1

goal (1 subgoal):
 1. Sound R2
[PROOF STEP]
unfolding less_restrictive_def Sound_def
[PROOF STATE]
proof (prove)
using this:
\<forall>P1 P2 C. R2 P1 P2 C \<longrightarrow> R1 P1 P2 C \<or> R1 P2 P1 C
\<forall>I P1 P2 C. R1 P1 P2 C \<longrightarrow> I \<Turnstile> P1 \<longrightarrow> I \<Turnstile> P2 \<longrightarrow> I \<Turnstile> C

goal (1 subgoal):
 1. \<forall>I P1 P2 C. R2 P1 P2 C \<longrightarrow> I \<Turnstile> P1 \<longrightarrow> I \<Turnstile> P2 \<longrightarrow> I \<Turnstile> C
[PROOF STEP]
by blast


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

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

goal (1 subgoal):
 1. (\<And>P1 P2 C I. \<lbrakk>resolvent P1 P2 C; I \<Turnstile> P1; I \<Turnstile> P2; \<not> I \<Turnstile> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding  Sound_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I P1 P2 C. resolvent P1 P2 C \<longrightarrow> I \<Turnstile> P1 \<longrightarrow> I \<Turnstile> P2 \<longrightarrow> I \<Turnstile> C)

goal (1 subgoal):
 1. (\<And>P1 P2 C I. \<lbrakk>resolvent P1 P2 C; I \<Turnstile> P1; I \<Turnstile> P2; \<not> I \<Turnstile> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
resolvent P1 P2 C
I \<Turnstile> P1
I \<Turnstile> P2
\<not> I \<Turnstile> C

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

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

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

goal (1 subgoal):
 1. \<not> Sound resolvent \<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 "A \<in> I"
[PROOF STATE]
proof (state)
this:
A \<in> I

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
hence "\<not>validate_literal I (Neg A)"
[PROOF STATE]
proof (prove)
using this:
A \<in> I

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>validate_literal I (Neg A)\<close> and \<open>validate_clause I P2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I \<Turnstile> Neg A
I \<Turnstile> P2
[PROOF STEP]
have "validate_clause I (P2 - { Neg A })"
[PROOF STATE]
proof (prove)
using this:
\<not> I \<Turnstile> Neg A
I \<Turnstile> P2

goal (1 subgoal):
 1. I \<Turnstile> (P2 - {Neg A})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<Turnstile> (P2 - {Neg A})

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_clause I (P2 - { Neg A })\<close> and \<open>C = ( (P1 - { Pos A}) \<union> (P2 - { Neg A }))\<close>
          and \<open>\<not>validate_clause I C\<close>
[PROOF STATE]
proof (chain)
picking this:
I \<Turnstile> (P2 - {Neg A})
C = P1 - {Pos A} \<union> (P2 - {Neg A})
\<not> I \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
I \<Turnstile> (P2 - {Neg A})
C = P1 - {Pos A} \<union> (P2 - {Neg A})
\<not> I \<Turnstile> C

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

goal (1 subgoal):
 1. A \<notin> I \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<notin> I \<Longrightarrow> False
[PROOF STEP]
assume "A \<notin> I"
[PROOF STATE]
proof (state)
this:
A \<notin> I

goal (1 subgoal):
 1. A \<notin> I \<Longrightarrow> False
[PROOF STEP]
hence "\<not>validate_literal I (Pos A)"
[PROOF STATE]
proof (prove)
using this:
A \<notin> I

goal (1 subgoal):
 1. \<not> I \<Turnstile> Pos A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> I \<Turnstile> Pos A

goal (1 subgoal):
 1. A \<notin> I \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>validate_literal I (Pos A)\<close> and \<open>validate_clause I P1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I \<Turnstile> Pos A
I \<Turnstile> P1
[PROOF STEP]
have "validate_clause I (P1 - { Pos A })"
[PROOF STATE]
proof (prove)
using this:
\<not> I \<Turnstile> Pos A
I \<Turnstile> P1

goal (1 subgoal):
 1. I \<Turnstile> (P1 - {Pos A})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<Turnstile> (P1 - {Pos A})

goal (1 subgoal):
 1. A \<notin> I \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_clause I (P1 - { Pos A })\<close> and \<open>C = ( (P1 - { Pos A}) \<union> (P2 - { Neg A }))\<close>
          and \<open>\<not>validate_clause I C\<close>
[PROOF STATE]
proof (chain)
picking this:
I \<Turnstile> (P1 - {Pos A})
C = P1 - {Pos A} \<union> (P2 - {Neg A})
\<not> I \<Turnstile> C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
I \<Turnstile> (P1 - {Pos A})
C = P1 - {Pos A} \<union> (P2 - {Neg A})
\<not> I \<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


[STATEMENT]
theorem ordered_resolution_correct : "Sound ordered_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sound ordered_resolvent
[PROOF STEP]
using resolution_is_correct and ordered_resolvent_is_resolvent  less_restrictive_correct
[PROOF STATE]
proof (prove)
using this:
Sound resolvent
less_restrictive resolvent ordered_resolvent
\<lbrakk>less_restrictive ?R1.0 ?R2.0; Sound ?R1.0\<rbrakk> \<Longrightarrow> Sound ?R2.0

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


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

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


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

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


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

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


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

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


[STATEMENT]
lemma less_restrictive_saturated:
  assumes "less_restrictive R1 R2"
  assumes "saturated_binary_rule R1 S"
  shows "saturated_binary_rule R2 S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated_binary_rule R2 S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
less_restrictive R1 R2
saturated_binary_rule R1 S

goal (1 subgoal):
 1. saturated_binary_rule R2 S
[PROOF STEP]
unfolding less_restrictive_def Complete_def saturated_binary_rule_def
[PROOF STATE]
proof (prove)
using this:
\<forall>P1 P2 C. R2 P1 P2 C \<longrightarrow> R1 P1 P2 C \<or> R1 P2 P1 C
\<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> R1 P1 P2 C \<longrightarrow> redundant C S

goal (1 subgoal):
 1. \<forall>P1 P2 C. P1 \<in> S \<and> P2 \<in> S \<and> R2 P1 P2 C \<longrightarrow> redundant C S
[PROOF STEP]
by blast


[STATEMENT]
lemma less_restrictive_complete:
  assumes "less_restrictive R1 R2"
  assumes "Complete R2"
  shows "Complete R1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete R1
[PROOF STEP]
using assms less_restrictive_saturated Complete_def
[PROOF STATE]
proof (prove)
using this:
less_restrictive R1 R2
Complete R2
\<lbrakk>less_restrictive ?R1.0 ?R2.0; saturated_binary_rule ?R1.0 ?S\<rbrakk> \<Longrightarrow> saturated_binary_rule ?R2.0 ?S
Complete ?Rule = (\<forall>S. saturated_binary_rule ?Rule S \<longrightarrow> all_fulfill finite S \<longrightarrow> {} \<notin> S \<longrightarrow> satisfiable S)

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


[STATEMENT]
lemma int_validate_cl_with_pos_max :
  assumes "strictly_maximal_literal C (Pos A)"
  assumes "C \<in> S"
  shows "validate_clause (canonic_int_ordered S) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume c1: "(\<forall> B. ( Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                  \<longrightarrow> (\<not>(canonic_int_fun_ordered B) S)))"
[PROOF STATE]
proof (state)
this:
\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S

goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume c2: "( \<forall> B. ( Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                    \<longrightarrow> ((canonic_int_fun_ordered B) S)))"
[PROOF STATE]
proof (state)
this:
\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S

goal (2 subgoals):
 1. ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
 2. \<not> ?P \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
have "((canonic_int_fun_ordered A) S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonic_int_fun_ordered A S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> canonic_int_fun_ordered A S \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ((canonic_int_fun_ordered A) S)"
[PROOF STATE]
proof (state)
this:
\<not> canonic_int_fun_ordered A S

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

goal (1 subgoal):
 1. \<nexists>C. C \<in> 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 S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)
[PROOF STEP]
by ((simp only:canonic_int_fun_ordered.simps[of A]), blast)
[PROOF STATE]
proof (state)
this:
\<nexists>C. C \<in> 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 S) \<and> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume not_c2: "\<not>( \<forall> B. ( Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                        \<longrightarrow> ((canonic_int_fun_ordered B) S)))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)

goal (1 subgoal):
 1. \<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from not_c2
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)
[PROOF STEP]
obtain B where "Neg B \<in> C" and "\<not>((canonic_int_fun_ordered B) S)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S)

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>B. Neg B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
with \<open>Neg B \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg B \<in> C
B \<notin> canonic_int_ordered S
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
Neg B \<in> C
B \<notin> canonic_int_ordered S

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

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

goal (1 subgoal):
 1. \<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
assume not_c1: "\<not>(\<forall> B. ( Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering
                      \<longrightarrow> (\<not>(canonic_int_fun_ordered B) S)))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S)

goal (1 subgoal):
 1. \<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
from not_c1
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S)
[PROOF STEP]
obtain B where "Pos B \<in> C" and "((canonic_int_fun_ordered B) S)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S)

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>Pos B \<in> C; canonic_int_fun_ordered B S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pos B \<in> C
canonic_int_fun_ordered B S

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>B. Pos B \<in> C \<longrightarrow> (B, A) \<in> atom_ordering \<longrightarrow> \<not> canonic_int_fun_ordered B S) \<Longrightarrow> canonic_int_ordered S \<Turnstile> C
[PROOF STEP]
with \<open>Pos B \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
Pos B \<in> C
B \<in> canonic_int_ordered S
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
Pos B \<in> C
B \<in> canonic_int_ordered S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strictly_maximal_literal_exists :

  "\<forall>C. (((finite C) \<and> (card C) = n \<and> n \<noteq> 0 \<and> (\<not> (tautology C))))
    \<longrightarrow> (\<exists>A. (strictly_maximal_literal C A))" (is "?P n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>C. finite C \<and> card C = 0 \<and> 0 \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
 2. \<And>n. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A) \<Longrightarrow> \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
show "(?P 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. finite C \<and> card C = 0 \<and> 0 \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>C. finite C \<and> card C = 0 \<and> 0 \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal (1 subgoal):
 1. \<And>n. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A) \<Longrightarrow> \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A) \<Longrightarrow> \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A) \<Longrightarrow> \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
assume "?P n"
[PROOF STATE]
proof (state)
this:
\<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal (1 subgoal):
 1. \<And>n. \<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A) \<Longrightarrow> \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
show "?P (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
show "(finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> (tautology C))
              \<longrightarrow> (\<exists>A. (strictly_maximal_literal C A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
assume "finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not>(tautology C)"
[PROOF STATE]
proof (state)
this:
finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
hence "(finite C)" and "(card C) = (Suc n)" and "(\<not> (tautology C))"
[PROOF STATE]
proof (prove)
using this:
finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C

goal (1 subgoal):
 1. finite C &&& card C = Suc n &&& \<not> tautology C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite C
card C = Suc n
\<not> tautology C

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
have "C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C = {} \<Longrightarrow> False
[PROOF STEP]
assume "C = {}"
[PROOF STATE]
proof (state)
this:
C = {}

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

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

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

goal (1 subgoal):
 1. C = {} \<Longrightarrow> False
[PROOF STEP]
from \<open>card C = 0\<close> and \<open>card C = Suc n\<close>
[PROOF STATE]
proof (chain)
picking this:
card C = 0
card C = Suc n
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
card C = 0
card C = Suc n

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:
C \<noteq> {}

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> {}
[PROOF STEP]
obtain L where "L \<in> C"
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {}

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

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from \<open>\<not>tautology C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology C
[PROOF STEP]
have "\<not>tautology (C - { L })"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C

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

goal (1 subgoal):
 1. \<not> tautology (C - {L})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> tautology (C - {L})

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from \<open>L \<in> C\<close> and  \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> C
finite C
[PROOF STEP]
have "Suc (card (C - { L })) = card C"
[PROOF STATE]
proof (prove)
using this:
L \<in> C
finite C

goal (1 subgoal):
 1. Suc (card (C - {L})) = card C
[PROOF STEP]
using card_Suc_Diff1
[PROOF STATE]
proof (prove)
using this:
L \<in> C
finite C
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> Suc (card (?A - {?x})) = card ?A

goal (1 subgoal):
 1. Suc (card (C - {L})) = card C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Suc (card (C - {L})) = card C

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
with \<open>card C = Suc n\<close>
[PROOF STATE]
proof (chain)
picking this:
card C = Suc n
Suc (card (C - {L})) = card C
[PROOF STEP]
have "card (C - { L }) = n"
[PROOF STATE]
proof (prove)
using this:
card C = Suc n
Suc (card (C - {L})) = card C

goal (1 subgoal):
 1. card (C - {L}) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (C - {L}) = n

goal (1 subgoal):
 1. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
show "\<exists>A. (strictly_maximal_literal C A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
 2. \<not> ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
assume "card C = 1"
[PROOF STATE]
proof (state)
this:
card C = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
 2. \<not> ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from this and  \<open>card C = Suc n\<close>
[PROOF STATE]
proof (chain)
picking this:
card C = 1
card C = Suc n
[PROOF STEP]
have "n = 0"
[PROOF STATE]
proof (prove)
using this:
card C = 1
card C = Suc n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
 2. \<not> ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from this and \<open>finite C\<close> and \<open>card (C - { L }) = n\<close>
[PROOF STATE]
proof (chain)
picking this:
n = 0
finite C
card (C - {L}) = n
[PROOF STEP]
have "C - { L } = {}"
[PROOF STATE]
proof (prove)
using this:
n = 0
finite C
card (C - {L}) = n

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
 2. \<not> ?P \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from this and \<open>L \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
C - {L} = {}
L \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C - {L} = {}
L \<in> C

goal (1 subgoal):
 1. \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
C - {L} = {}
L \<in> C

goal (1 subgoal):
 1. \<exists>A. A \<in> C \<and> (\<forall>B. B \<in> C \<and> A \<noteq> B \<longrightarrow> literal_ordering B A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A. strictly_maximal_literal C A

goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
assume "card C \<noteq> 1"
[PROOF STATE]
proof (state)
this:
card C \<noteq> 1

goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from \<open>finite C\<close>
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
have "finite (C - { L })"
[PROOF STATE]
proof (prove)
using this:
finite C

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

goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from  \<open>Suc (card (C - { L })) = card C\<close> and \<open>card C \<noteq> 1\<close>
                    and \<open>(card (C - { L })) = n\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc (card (C - {L})) = card C
card C \<noteq> 1
card (C - {L}) = n
[PROOF STEP]
have "n \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
Suc (card (C - {L})) = card C
card C \<noteq> 1
card (C - {L}) = n

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

goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
from this and \<open>finite (C - { L })\<close> and \<open>card (C - { L }) = n\<close>
                    and \<open>\<not>tautology (C - { L })\<close> and \<open>?P n\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
finite (C - {L})
card (C - {L}) = n
\<not> tautology (C - {L})
\<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)
[PROOF STEP]
obtain A where "strictly_maximal_literal (C - { L }) A"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
finite (C - {L})
card (C - {L}) = n
\<not> tautology (C - {L})
\<forall>C. finite C \<and> card C = n \<and> n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

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

goal (1 subgoal):
 1. card C \<noteq> 1 \<Longrightarrow> \<exists>A. strictly_maximal_literal C A
[PROOF STEP]
show "\<exists>M. strictly_maximal_literal C M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
 2. \<not> ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
assume "(atom L, atom A) \<in> atom_ordering"
[PROOF STATE]
proof (state)
this:
(atom L, atom A) \<in> atom_ordering

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
 2. \<not> ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(atom L, atom A) \<in> atom_ordering
[PROOF STEP]
have "literal_ordering L A"
[PROOF STATE]
proof (prove)
using this:
(atom L, atom A) \<in> atom_ordering

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
 2. \<not> ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
from this and \<open>strictly_maximal_literal (C - { L }) A\<close>
[PROOF STATE]
proof (chain)
picking this:
literal_ordering L A
strictly_maximal_literal (C - {L}) A
[PROOF STEP]
have "strictly_maximal_literal C A"
[PROOF STATE]
proof (prove)
using this:
literal_ordering L A
strictly_maximal_literal (C - {L}) A

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

goal (1 subgoal):
 1. A \<in> C \<and> (\<forall>B. B \<in> C \<and> A \<noteq> B \<longrightarrow> literal_ordering B A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal C A

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
 2. \<not> ?P \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal C A

goal (1 subgoal):
 1. \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>M. strictly_maximal_literal C M

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
assume "(atom L, atom A) \<notin> atom_ordering"
[PROOF STATE]
proof (state)
this:
(atom L, atom A) \<notin> atom_ordering

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
have l_cases: "L = (Pos (atom L)) \<or> L = (Neg (atom L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = Pos (atom L) \<or> L = Neg (atom L)
[PROOF STEP]
by ((rule atom_property [of "(atom L)"]), auto)
[PROOF STATE]
proof (state)
this:
L = Pos (atom L) \<or> L = Neg (atom L)

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
have a_cases: "A = (Pos (atom A)) \<or> A = (Neg (atom A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = Pos (atom A) \<or> A = Neg (atom A)
[PROOF STEP]
by ((rule atom_property [of "(atom A)"]), auto)
[PROOF STATE]
proof (state)
this:
A = Pos (atom A) \<or> A = Neg (atom A)

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
from l_cases and a_cases and\<open>(strictly_maximal_literal (C - { L }) A)\<close>
                        and \<open>\<not> (tautology C)\<close> and \<open>L \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos (atom L) \<or> L = Neg (atom L)
A = Pos (atom A) \<or> A = Neg (atom A)
strictly_maximal_literal (C - {L}) A
\<not> tautology C
L \<in> C
[PROOF STEP]
have "atom L \<noteq> atom A"
[PROOF STATE]
proof (prove)
using this:
L = Pos (atom L) \<or> L = Neg (atom L)
A = Pos (atom A) \<or> A = Neg (atom A)
strictly_maximal_literal (C - {L}) A
\<not> tautology C
L \<in> C

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

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

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
from this and \<open>(atom L, atom A) \<notin> atom_ordering\<close> and atom_ordering_total
[PROOF STATE]
proof (chain)
picking this:
atom L \<noteq> atom A
(atom L, atom A) \<notin> atom_ordering
\<forall>x y. x \<noteq> y \<longrightarrow> (x, y) \<in> atom_ordering \<or> (y, x) \<in> atom_ordering
[PROOF STEP]
have "(atom A,atom L) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
atom L \<noteq> atom A
(atom L, atom A) \<notin> atom_ordering
\<forall>x y. x \<noteq> y \<longrightarrow> (x, y) \<in> atom_ordering \<or> (y, x) \<in> atom_ordering

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

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
hence "literal_ordering A L"
[PROOF STATE]
proof (prove)
using this:
(atom A, atom L) \<in> atom_ordering

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

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
from this and \<open>L \<in> C\<close> and \<open>strictly_maximal_literal (C - { L }) A\<close>
                        and literal_ordering_trans
[PROOF STATE]
proof (chain)
picking this:
literal_ordering A L
L \<in> C
strictly_maximal_literal (C - {L}) A
\<lbrakk>literal_ordering ?A ?B; literal_ordering ?B ?C\<rbrakk> \<Longrightarrow> literal_ordering ?A ?C
[PROOF STEP]
have "strictly_maximal_literal C L"
[PROOF STATE]
proof (prove)
using this:
literal_ordering A L
L \<in> C
strictly_maximal_literal (C - {L}) A
\<lbrakk>literal_ordering ?A ?B; literal_ordering ?B ?C\<rbrakk> \<Longrightarrow> literal_ordering ?A ?C

goal (1 subgoal):
 1. strictly_maximal_literal C L
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
literal_ordering A L
L \<in> C
A \<in> C - {L} \<and> (\<forall>B. B \<in> C - {L} \<and> A \<noteq> B \<longrightarrow> literal_ordering B A)
\<lbrakk>literal_ordering ?A ?B; literal_ordering ?B ?C\<rbrakk> \<Longrightarrow> literal_ordering ?A ?C

goal (1 subgoal):
 1. L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
literal_ordering A L
L \<in> C
A \<in> C - {L} \<and> (\<forall>B. B \<in> C - {L} \<and> A \<noteq> B \<longrightarrow> literal_ordering B A)
\<lbrakk>literal_ordering ?A ?B; literal_ordering ?B ?C\<rbrakk> \<Longrightarrow> literal_ordering ?A ?C

goal (1 subgoal):
 1. L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal C L

goal (1 subgoal):
 1. (atom L, atom A) \<notin> atom_ordering \<Longrightarrow> \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal C L

goal (1 subgoal):
 1. \<exists>M. strictly_maximal_literal C M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>M. strictly_maximal_literal C M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>M. strictly_maximal_literal C M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>A. strictly_maximal_literal C A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. finite C \<and> card C = Suc n \<and> Suc n \<noteq> 0 \<and> \<not> tautology C \<longrightarrow> (\<exists>A. strictly_maximal_literal C A)

goal:
No subgoals!
[PROOF STEP]
qed