[STATEMENT]
lemma cl_in_altdef:
  assumes "X \<subseteq> \<E>"
  shows "cl_in \<E> X = \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_in \<E> X = \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.cl X = \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
proof (safe, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
 2. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
case (LTR x)
[PROOF STATE]
proof (state)
this:
x \<in> \<E>.cl X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
 2. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E>.cl X
[PROOF STEP]
have "x \<in> \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>.cl X

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
using \<E>.cl_altdef[OF assms]
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>.cl X
\<E>.cl X = \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
 2. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
obtain Y where Y: "x \<in> Y" "Y \<in> Pow \<E>" "X \<subseteq> Y" "\<E>.rank_of Y = \<E>.rank_of X"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>x \<in> Y; Y \<in> Pow \<E>; X \<subseteq> Y; \<E>.rank_of Y = \<E>.rank_of X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> Y
Y \<in> Pow \<E>
X \<subseteq> Y
\<E>.rank_of Y = \<E>.rank_of X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl X \<Longrightarrow> x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
 2. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Y
Y \<in> Pow \<E>
X \<subseteq> Y
\<E>.rank_of Y = \<E>.rank_of X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<in> Pow \<E>
X \<subseteq> Y
\<E>.rank_of Y = \<E>.rank_of X

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
using rank_of_sub_cong[OF *]
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<in> Pow \<E>
X \<subseteq> Y
\<E>.rank_of Y = \<E>.rank_of X
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> rank_of Y = rank_of X}

goal (1 subgoal):
 1. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
case (RTL x Y)
[PROOF STATE]
proof (state)
this:
x \<in> Y
Y \<subseteq> \<E>
X \<subseteq> Y
rank_of Y = rank_of X

goal (1 subgoal):
 1. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Y
Y \<subseteq> \<E>
X \<subseteq> Y
rank_of Y = rank_of X
[PROOF STEP]
have "x \<in> \<Union>{Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}"
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<subseteq> \<E>
X \<subseteq> Y
rank_of Y = rank_of X

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
using rank_of_sub_cong[OF *, of X] rank_of_sub_cong[OF *, of Y]
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
Y \<subseteq> \<E>
X \<subseteq> Y
rank_of Y = rank_of X
X \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of X = rank_of X
Y \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of Y = rank_of Y

goal (1 subgoal):
 1. x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

goal (1 subgoal):
 1. \<And>x Xa. \<lbrakk>x \<in> Xa; Xa \<subseteq> \<E>; X \<subseteq> Xa; rank_of Xa = rank_of X\<rbrakk> \<Longrightarrow> x \<in> \<E>.cl X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

goal (1 subgoal):
 1. x \<in> \<E>.cl X
[PROOF STEP]
using \<E>.cl_altdef[OF assms]
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}
\<E>.cl X = \<Union> {Y \<in> Pow \<E>. X \<subseteq> Y \<and> \<E>.rank_of Y = \<E>.rank_of X}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_in_subset_carrier: "cl_in \<E> X \<subseteq> \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_in \<E> X \<subseteq> \<E>
[PROOF STEP]
using \<E>.cl_subset_carrier
[PROOF STATE]
proof (prove)
using this:
\<E>.cl ?X \<subseteq> \<E>

goal (1 subgoal):
 1. cl_in \<E> X \<subseteq> \<E>
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.cl ?X \<subseteq> \<E>

goal (1 subgoal):
 1. \<E>.cl X \<subseteq> \<E>
[PROOF STEP]
.


[STATEMENT]
lemma cl_in_rank_of:
  assumes "X \<subseteq> \<E>"
  assumes "x \<in> cl_in \<E> X"
  shows "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "\<E>.rank_of (insert x X) = \<E>.rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = \<E>.rank_of X
[PROOF STEP]
using assms \<E>.cl_rank_of
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> cl_in \<E> X
?x \<in> \<E>.cl ?X \<Longrightarrow> \<E>.rank_of (insert ?x ?X) = \<E>.rank_of ?X

goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = \<E>.rank_of X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> \<E>.cl X
?x \<in> \<E>.cl ?X \<Longrightarrow> \<E>.rank_of (insert ?x ?X) = \<E>.rank_of ?X

goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = \<E>.rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = \<E>.rank_of X

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = \<E>.rank_of X

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
using assms rank_of_sub_cong[OF *, of "insert x X"] cl_in_subset_carrier
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> cl_in \<E> X
insert x X \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of (insert x X) = rank_of (insert x X)
cl_in \<E> ?X \<subseteq> \<E>

goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
have "\<E>.rank_of X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
using assms rank_of_sub_cong[OF *]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> cl_in \<E> X
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'

goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. rank_of (insert x X) = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rank_of (insert x X) = rank_of X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_in_subset:
  assumes "X \<subseteq> \<E>"
  shows "X \<subseteq> cl_in \<E> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> cl_in \<E> X
[PROOF STEP]
using \<E>.cl_subset[OF assms]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>.cl X

goal (1 subgoal):
 1. X \<subseteq> cl_in \<E> X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>.cl X

goal (1 subgoal):
 1. X \<subseteq> \<E>.cl X
[PROOF STEP]
.


[STATEMENT]
lemma cl_in_mono:
  assumes "X \<subseteq> Y"
  assumes "Y \<subseteq> \<E>"
  shows "cl_in \<E> X \<subseteq> cl_in \<E> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_in \<E> X \<subseteq> cl_in \<E> Y
[PROOF STEP]
using \<E>.cl_mono[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<E>.cl X \<subseteq> \<E>.cl Y

goal (1 subgoal):
 1. cl_in \<E> X \<subseteq> cl_in \<E> Y
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
\<E>.cl X \<subseteq> \<E>.cl Y

goal (1 subgoal):
 1. \<E>.cl X \<subseteq> \<E>.cl Y
[PROOF STEP]
.


[STATEMENT]
lemma cl_in_insert_absorb:
  assumes "X \<subseteq> \<E>"
  assumes "x \<in> cl_in \<E> X"
  shows "cl_in \<E> (insert x X) = cl_in \<E> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_in \<E> (insert x X) = cl_in \<E> X
[PROOF STEP]
using assms \<E>.cl_insert_absorb
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> cl_in \<E> X
\<lbrakk>?X \<subseteq> \<E>; ?x \<in> \<E>.cl ?X\<rbrakk> \<Longrightarrow> \<E>.cl (insert ?x ?X) = \<E>.cl ?X

goal (1 subgoal):
 1. cl_in \<E> (insert x X) = cl_in \<E> X
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> \<E>.cl X
\<lbrakk>?X \<subseteq> \<E>; ?x \<in> \<E>.cl ?X\<rbrakk> \<Longrightarrow> \<E>.cl (insert ?x ?X) = \<E>.cl ?X

goal (1 subgoal):
 1. \<E>.cl (insert x X) = \<E>.cl X
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_in_augment:
  assumes "X \<subseteq> \<E>"
  assumes "x \<in> \<E>"
  assumes "y \<in> cl_in \<E> (insert x X) - cl_in \<E> X"
  shows "x \<in> cl_in \<E> (insert y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cl_in \<E> (insert y X)
[PROOF STEP]
using assms \<E>.cl_augment
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> \<E>
y \<in> cl_in \<E> (insert x X) - cl_in \<E> X
\<lbrakk>?X \<subseteq> \<E>; ?x \<in> \<E>; ?y \<in> \<E>.cl (insert ?x ?X) - \<E>.cl ?X\<rbrakk> \<Longrightarrow> ?x \<in> \<E>.cl (insert ?y ?X)

goal (1 subgoal):
 1. x \<in> cl_in \<E> (insert y X)
[PROOF STEP]
unfolding cl_in_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>
x \<in> \<E>
y \<in> \<E>.cl (insert x X) - \<E>.cl X
\<lbrakk>?X \<subseteq> \<E>; ?x \<in> \<E>; ?y \<in> \<E>.cl (insert ?x ?X) - \<E>.cl ?X\<rbrakk> \<Longrightarrow> ?x \<in> \<E>.cl (insert ?y ?X)

goal (1 subgoal):
 1. x \<in> \<E>.cl (insert y X)
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_in_subI:
  assumes "X \<subseteq> \<E>'" "\<E>' \<subseteq> \<E>" "\<E> \<subseteq> carrier"
  shows "cl_in \<E>' X \<subseteq> cl_in \<E> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_in \<E>' X \<subseteq> cl_in \<E> X
[PROOF STEP]
proof (safe, goal_cases elem)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E> X
[PROOF STEP]
case (elem x)
[PROOF STATE]
proof (state)
this:
x \<in> cl_in \<E>' X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl_in \<E>' X
[PROOF STEP]
have "x \<in> \<E>'" "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
x \<in> cl_in \<E>' X

goal (1 subgoal):
 1. x \<in> \<E>' &&& rank_of (insert x X) = rank_of X
[PROOF STEP]
using assms cl_inD[where \<E> = \<E>' and X = X]
[PROOF STATE]
proof (prove)
using this:
x \<in> cl_in \<E>' X
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
\<E> \<subseteq> carrier
\<lbrakk>\<E>' \<subseteq> carrier; X \<subseteq> \<E>'; ?x \<in> cl_in \<E>' X\<rbrakk> \<Longrightarrow> rank_of (insert ?x X) = rank_of X
\<E>' \<subseteq> carrier \<Longrightarrow> cl_in \<E>' X \<subseteq> \<E>'

goal (1 subgoal):
 1. x \<in> \<E>' &&& rank_of (insert x X) = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X
[PROOF STEP]
show "x \<in> cl_in \<E> X"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
\<E> \<subseteq> carrier

goal (1 subgoal):
 1. x \<in> cl_in \<E> X
[PROOF STEP]
by (auto intro: cl_inI)
[PROOF STATE]
proof (state)
this:
x \<in> cl_in \<E> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cl_in_sub_cong:
  assumes "X \<subseteq> \<E>'" "\<E>' \<subseteq> \<E>"
  shows "\<E>.cl_in \<E>' X = cl_in \<E>' X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.cl_in \<E>' X = cl_in \<E>' X
[PROOF STEP]
proof (safe, goal_cases LTR RTL)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
case (LTR x)
[PROOF STATE]
proof (state)
this:
x \<in> \<E>.cl_in \<E>' X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
have "x \<in> \<E>'" "\<E>.rank_of (insert x X) = \<E>.rank_of X"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>.cl_in \<E>' X

goal (1 subgoal):
 1. x \<in> \<E>' &&& \<E>.rank_of (insert x X) = \<E>.rank_of X
[PROOF STEP]
using assms
      \<E>.cl_in_rank_of[where \<E> = \<E>' and X = X and x = x]
      \<E>.cl_in_subset_carrier[where \<E> = \<E>']
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>.cl_in \<E>' X
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
\<lbrakk>\<E>' \<subseteq> \<E>; X \<subseteq> \<E>'; x \<in> \<E>.cl_in \<E>' X\<rbrakk> \<Longrightarrow> \<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.cl_in \<E>' ?X \<subseteq> \<E>'

goal (1 subgoal):
 1. x \<in> \<E>' &&& \<E>.rank_of (insert x X) = \<E>.rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<E>'
\<E>.rank_of (insert x X) = \<E>.rank_of X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> \<E>'
\<E>.rank_of (insert x X) = \<E>.rank_of X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
have "\<E>.rank_of X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
using assms rank_of_sub_cong[OF *]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'

goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of X = rank_of X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<E>.rank_of X = rank_of X

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
using assms rank_of_sub_cong[OF *, of "insert x X"] \<open>x \<in> \<E>'\<close>
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
insert x X \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of (insert x X) = rank_of (insert x X)
x \<in> \<E>'

goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (2 subgoals):
 1. \<And>x. x \<in> \<E>.cl_in \<E>' X \<Longrightarrow> x \<in> cl_in \<E>' X
 2. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E>'
\<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
\<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (1 subgoal):
 1. x \<in> cl_in \<E>' X
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
\<E>.rank_of (insert x X) = \<E>.rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
\<E> \<subseteq> carrier

goal (1 subgoal):
 1. x \<in> cl_in \<E>' X
[PROOF STEP]
by (auto intro: cl_inI)
[PROOF STATE]
proof (state)
this:
x \<in> cl_in \<E>' X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
case (RTL x)
[PROOF STATE]
proof (state)
this:
x \<in> cl_in \<E>' X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl_in \<E>' X
[PROOF STEP]
have "x \<in> \<E>'" "rank_of (insert x X) = rank_of X"
[PROOF STATE]
proof (prove)
using this:
x \<in> cl_in \<E>' X

goal (1 subgoal):
 1. x \<in> \<E>' &&& rank_of (insert x X) = rank_of X
[PROOF STEP]
using * assms cl_inD[where \<E> = \<E>' and X = X]
[PROOF STATE]
proof (prove)
using this:
x \<in> cl_in \<E>' X
\<E> \<subseteq> carrier
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
\<lbrakk>\<E>' \<subseteq> carrier; X \<subseteq> \<E>'; ?x \<in> cl_in \<E>' X\<rbrakk> \<Longrightarrow> rank_of (insert ?x X) = rank_of X
\<E>' \<subseteq> carrier \<Longrightarrow> cl_in \<E>' X \<subseteq> \<E>'

goal (1 subgoal):
 1. x \<in> \<E>' &&& rank_of (insert x X) = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
have "\<E>.rank_of X = rank_of X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
using assms rank_of_sub_cong[OF *]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
?\<E>' \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of ?\<E>' = rank_of ?\<E>'

goal (1 subgoal):
 1. \<E>.rank_of X = rank_of X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<E>.rank_of X = rank_of X

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
have "\<E>.rank_of (insert x X) = rank_of (insert x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
using assms rank_of_sub_cong[OF *, of "insert x X"] \<open>x \<in> \<E>'\<close>
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>
insert x X \<subseteq> \<E> \<Longrightarrow> \<E>.rank_of (insert x X) = rank_of (insert x X)
x \<in> \<E>'

goal (1 subgoal):
 1. \<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (1 subgoal):
 1. \<And>x. x \<in> cl_in \<E>' X \<Longrightarrow> x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)

goal (1 subgoal):
 1. x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E>'
rank_of (insert x X) = rank_of X
\<E>.rank_of X = rank_of X
\<E>.rank_of (insert x X) = rank_of (insert x X)
X \<subseteq> \<E>'
\<E>' \<subseteq> \<E>

goal (1 subgoal):
 1. x \<in> \<E>.cl_in \<E>' X
[PROOF STEP]
by (auto intro: \<E>.cl_inI)
[PROOF STATE]
proof (state)
this:
x \<in> \<E>.cl_in \<E>' X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atom_property : "A = (atom L) \<Longrightarrow> (L = (Pos A) \<or> L = (Neg A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = atom L \<Longrightarrow> L = Pos A \<or> L = Neg A
[PROOF STEP]
by (metis atom.elims)


[STATEMENT]
lemma atoms_formula_subset: "S1 \<subseteq> S2 \<Longrightarrow> atoms_formula S1 \<subseteq> atoms_formula S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S1 \<subseteq> S2 \<Longrightarrow> atoms_formula S1 \<subseteq> atoms_formula S2
[PROOF STEP]
by auto


[STATEMENT]
lemma atoms_formula_union: "atoms_formula (S1 \<union> S2) = atoms_formula S1 \<union> atoms_formula S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_formula (S1 \<union> S2) = atoms_formula S1 \<union> atoms_formula S2
[PROOF STEP]
by auto


[STATEMENT]
lemma literal_ordering_trans :
  assumes "literal_ordering A B"
  assumes "literal_ordering B C"
  shows "literal_ordering A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literal_ordering A C
[PROOF STEP]
using assms(1) assms(2) atom_ordering_trans literal_ordering.simps
[PROOF STATE]
proof (prove)
using this:
literal_ordering A B
literal_ordering B C
\<forall>x y z. (x, y) \<in> atom_ordering \<longrightarrow> (y, z) \<in> atom_ordering \<longrightarrow> (x, z) \<in> atom_ordering
literal_ordering ?L1.0 ?L2.0 = ((atom ?L1.0, atom ?L2.0) \<in> atom_ordering)

goal (1 subgoal):
 1. literal_ordering A C
[PROOF STEP]
by blast


[STATEMENT]
lemma entails_member:
  assumes "C \<in> S"
  shows "entails S C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails S C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. entails S C
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. \<forall>I. I \<Turnstile> S \<longrightarrow> I \<Turnstile> C
[PROOF STEP]
by simp


[STATEMENT]
lemma equivalent_symmetric: "equivalent S1 S2 \<Longrightarrow> equivalent S2 S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalent S1 S2 \<Longrightarrow> equivalent S2 S1
[PROOF STEP]
by (simp add: equivalent_def)


[STATEMENT]
lemma entailment_implies_validity:
  assumes "entails_formula S1 S2"
  assumes "validate_formula I S1"
  shows "validate_formula I S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile> S2
[PROOF STEP]
using assms entails_def entails_formula_def
[PROOF STATE]
proof (prove)
using this:
entails_formula S1 S2
I \<Turnstile> S1
entails ?S ?C \<equiv> \<forall>I. I \<Turnstile> ?S \<longrightarrow> I \<Turnstile> ?C
entails_formula ?S1.0 ?S2.0 = (\<forall>C\<in>?S2.0. entails ?S1.0 C)

goal (1 subgoal):
 1. I \<Turnstile> S2
[PROOF STEP]
by auto


[STATEMENT]
lemma validity_implies_entailment:
  assumes "\<forall>I. validate_formula I S1 \<longrightarrow> validate_formula I S2"
  shows "entails_formula S1 S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S1 S2
[PROOF STEP]
by (meson assms entails_def entails_formula_def validate_formula.elims(2))


[STATEMENT]
lemma entails_transitive:
  assumes "entails_formula S1 S2"
  assumes "entails_formula S2 S3"
  shows "entails_formula S1 S3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S1 S3
[PROOF STEP]
by (meson assms entailment_implies_validity validity_implies_entailment)


[STATEMENT]
lemma equivalent_transitive:
  assumes "equivalent S1 S2"
  assumes "equivalent S2 S3"
  shows "equivalent S1 S3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalent S1 S3
[PROOF STEP]
using assms entails_transitive equivalent_def
[PROOF STATE]
proof (prove)
using this:
equivalent S1 S2
equivalent S2 S3
\<lbrakk>entails_formula ?S1.0 ?S2.0; entails_formula ?S2.0 ?S3.0\<rbrakk> \<Longrightarrow> entails_formula ?S1.0 ?S3.0
equivalent ?S1.0 ?S2.0 = (entails_formula ?S1.0 ?S2.0 \<and> entails_formula ?S2.0 ?S1.0)

goal (1 subgoal):
 1. equivalent S1 S3
[PROOF STEP]
by auto


[STATEMENT]
lemma entailment_subset :
  assumes "S2 \<subseteq> S1"
  shows "entails_formula S1 S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails_formula S1 S2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. entails_formula S1 S2
[PROOF STEP]
have "\<forall>L La. L \<notin> La \<or> entails La L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>L La. L \<notin> La \<or> entails La L
[PROOF STEP]
by (meson entails_member)
[PROOF STATE]
proof (state)
this:
\<forall>L La. L \<notin> La \<or> entails La L

goal (1 subgoal):
 1. entails_formula S1 S2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>L La. L \<notin> La \<or> entails La L

goal (1 subgoal):
 1. entails_formula S1 S2
[PROOF STEP]
by (meson assms entails_formula_def rev_subsetD)
[PROOF STATE]
proof (state)
this:
entails_formula S1 S2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma entailed_formula_entails_implicates:
  assumes "entails_formula S1 S2"
  assumes "entails S2 C"
  shows "entails S1 C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails S1 C
[PROOF STEP]
using assms entailment_implies_validity entails_def
[PROOF STATE]
proof (prove)
using this:
entails_formula S1 S2
entails S2 C
\<lbrakk>entails_formula ?S1.0 ?S2.0; ?I \<Turnstile> ?S1.0\<rbrakk> \<Longrightarrow> ?I \<Turnstile> ?S2.0
entails ?S ?C \<equiv> \<forall>I. I \<Turnstile> ?S \<longrightarrow> I \<Turnstile> ?C

goal (1 subgoal):
 1. entails S1 C
[PROOF STEP]
by blast


[STATEMENT]
lemma less_restrictive_and_finite :
  assumes "less_restrictive R1 R2"
  assumes "derived_clauses_are_finite R1"
  shows "derived_clauses_are_finite R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derived_clauses_are_finite R2
[PROOF STEP]
by (metis assms derived_clauses_are_finite_def less_restrictive_def)


[STATEMENT]
lemma resolvent_upon_is_resolvent :
  assumes "Pos A \<in> P1"
  assumes "Neg A \<in> P2"
  shows "resolvent P1 P2 (resolvent_upon P1 P2 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolvent P1 P2 (resolvent_upon P1 P2 A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Pos A \<in> P1
Neg A \<in> P2

goal (1 subgoal):
 1. resolvent P1 P2 (resolvent_upon P1 P2 A)
[PROOF STEP]
unfolding resolvent_def
[PROOF STATE]
proof (prove)
using this:
Pos A \<in> P1
Neg A \<in> P2

goal (1 subgoal):
 1. \<exists>Aa. Pos Aa \<in> P1 \<and> Neg Aa \<in> P2 \<and> resolvent_upon P1 P2 A = P1 - {Pos Aa} \<union> (P2 - {Neg Aa})
[PROOF STEP]
by auto


[STATEMENT]
lemma resolvent_is_resolvent_upon :
  assumes "resolvent P1 P2 C"
  shows "\<exists>A. C = resolvent_upon P1 P2 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. C = resolvent_upon P1 P2 A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
resolvent P1 P2 C

goal (1 subgoal):
 1. \<exists>A. C = resolvent_upon P1 P2 A
[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. \<exists>A. C = resolvent_upon P1 P2 A
[PROOF STEP]
by auto


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

goal (1 subgoal):
 1. \<not> derived_clauses_are_finite resolvent \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> derived_clauses_are_finite resolvent
[PROOF STEP]
have "\<exists>P1 P2 C. \<not>(resolvent P1 P2 C \<longrightarrow> finite P1 \<longrightarrow> finite P2 \<longrightarrow> finite C)"
[PROOF STATE]
proof (prove)
using this:
\<not> derived_clauses_are_finite resolvent

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

goal (1 subgoal):
 1. \<exists>P1 P2 C. \<not> (resolvent P1 P2 C \<longrightarrow> finite P1 \<longrightarrow> finite P2 \<longrightarrow> finite C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2 C. \<not> (resolvent P1 P2 C \<longrightarrow> finite P1 \<longrightarrow> finite P2 \<longrightarrow> finite C)

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

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

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

goal (1 subgoal):
 1. False
[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})
finite P1
finite P2
infinite C

goal (1 subgoal):
 1. False
[PROOF STEP]
using finite_Diff and finite_Union
[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})
finite P1
finite P2
infinite C
finite ?A \<Longrightarrow> finite (?A - ?B)
\<lbrakk>finite ?A; \<And>M. M \<in> ?A \<Longrightarrow> finite M\<rbrakk> \<Longrightarrow> finite (\<Union> ?A)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resolution_and_max_literal :
  assumes "R = resolvent_upon P1 P2 A"
  assumes "strictly_maximal_literal P1 (Pos A)"
  assumes "strictly_maximal_literal P2 (Neg A)"
  assumes "strictly_maximal_literal R M"
  shows "(atom M, A) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
obtain MA where "M = (Pos MA) \<or> M = (Neg MA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>MA. M = Pos MA \<or> M = Neg MA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of M]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. M = Pos x1 \<Longrightarrow> ?P; \<And>x2. M = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
hence "MA = (atom M)"
[PROOF STATE]
proof (prove)
using this:
M = Pos MA \<or> M = Neg MA

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

goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
from \<open>strictly_maximal_literal R M\<close> and \<open>R = resolvent_upon P1 P2 A\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal R M
R = resolvent_upon P1 P2 A
[PROOF STEP]
have "M \<in> P1 - { Pos A } \<or> M \<in> P2 - { Neg A }"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal R M
R = resolvent_upon P1 P2 A

goal (1 subgoal):
 1. M \<in> P1 - {Pos A} \<or> M \<in> P2 - {Neg A}
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
M \<in> R \<and> (\<forall>B. B \<in> R \<and> M \<noteq> B \<longrightarrow> literal_ordering B M)
R = resolvent_upon P1 P2 A

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

goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
hence "(MA,A) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
M \<in> P1 - {Pos A} \<or> M \<in> P2 - {Neg A}

goal (1 subgoal):
 1. (MA, A) \<in> atom_ordering
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M \<in> P1 - {Pos A} \<Longrightarrow> (MA, A) \<in> atom_ordering
 2. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
assume "M \<in> P1 - { Pos A }"
[PROOF STATE]
proof (state)
this:
M \<in> P1 - {Pos A}

goal (2 subgoals):
 1. M \<in> P1 - {Pos A} \<Longrightarrow> (MA, A) \<in> atom_ordering
 2. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
from \<open>M \<in> P1 - { Pos A }\<close> and \<open>strictly_maximal_literal P1 (Pos A)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> P1 - {Pos A}
strictly_maximal_literal P1 (Pos A)
[PROOF STEP]
have "literal_ordering M (Pos A)"
[PROOF STATE]
proof (prove)
using this:
M \<in> P1 - {Pos A}
strictly_maximal_literal P1 (Pos A)

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

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

goal (2 subgoals):
 1. M \<in> P1 - {Pos A} \<Longrightarrow> (MA, A) \<in> atom_ordering
 2. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
from \<open>M = Pos MA \<or> M = Neg MA\<close> and \<open>literal_ordering M (Pos A)\<close>
[PROOF STATE]
proof (chain)
picking this:
M = Pos MA \<or> M = Neg MA
literal_ordering M (Pos A)
[PROOF STEP]
show "(MA,A) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
M = Pos MA \<or> M = Neg MA
literal_ordering M (Pos A)

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

goal (1 subgoal):
 1. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
assume "M \<in> P2 - { Neg A }"
[PROOF STATE]
proof (state)
this:
M \<in> P2 - {Neg A}

goal (1 subgoal):
 1. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
from \<open>M \<in> P2 - { Neg A }\<close> and \<open>strictly_maximal_literal P2 (Neg A)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> P2 - {Neg A}
strictly_maximal_literal P2 (Neg A)
[PROOF STEP]
have "literal_ordering M (Neg A)"
[PROOF STATE]
proof (prove)
using this:
M \<in> P2 - {Neg A}
strictly_maximal_literal P2 (Neg A)

goal (1 subgoal):
 1. literal_ordering M (Neg A)
[PROOF STEP]
by (auto simp only: strictly_maximal_literal_def)
[PROOF STATE]
proof (state)
this:
literal_ordering M (Neg A)

goal (1 subgoal):
 1. M \<in> P2 - {Neg A} \<Longrightarrow> (MA, A) \<in> atom_ordering
[PROOF STEP]
from \<open>M = Pos MA \<or> M = Neg MA\<close> and \<open>literal_ordering M (Neg A)\<close>
[PROOF STATE]
proof (chain)
picking this:
M = Pos MA \<or> M = Neg MA
literal_ordering M (Neg A)
[PROOF STEP]
show "(MA,A) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
using this:
M = Pos MA \<or> M = Neg MA
literal_ordering M (Neg A)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(MA, A) \<in> atom_ordering

goal (1 subgoal):
 1. (atom M, A) \<in> atom_ordering
[PROOF STEP]
from this and \<open>MA = atom M\<close>
[PROOF STATE]
proof (chain)
picking this:
(MA, A) \<in> atom_ordering
MA = atom M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(MA, A) \<in> atom_ordering
MA = atom M

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordered_resolvent_is_resolvent : "less_restrictive resolvent ordered_resolvent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_restrictive resolvent ordered_resolvent
[PROOF STEP]
using less_restrictive_def ordered_resolvent_def resolvent_upon_is_resolvent strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
less_restrictive ?R1.0 ?R2.0 = (\<forall>P1 P2 C. ?R2.0 P1 P2 C \<longrightarrow> ?R1.0 P1 P2 C \<or> ?R1.0 P2 P1 C)
ordered_resolvent ?P1.0 ?P2.0 ?C \<equiv> \<exists>A. ?C = ?P1.0 - {Pos A} \<union> (?P2.0 - {Neg A}) \<and> strictly_maximal_literal ?P1.0 (Pos A) \<and> strictly_maximal_literal ?P2.0 (Neg A)
\<lbrakk>Pos ?A \<in> ?P1.0; Neg ?A \<in> ?P2.0\<rbrakk> \<Longrightarrow> resolvent ?P1.0 ?P2.0 (resolvent_upon ?P1.0 ?P2.0 ?A)
strictly_maximal_literal ?S ?A \<equiv> ?A \<in> ?S \<and> (\<forall>B. B \<in> ?S \<and> ?A \<noteq> B \<longrightarrow> literal_ordering B ?A)

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


[STATEMENT]
lemma ordered_sel_resolvent_is_ordered_resolvent :
 assumes "ordered_resolvent P1 P2 C"
 assumes "selected_part Sel P1 = {}"
 assumes "selected_part Sel P2 = {}"
 shows "ordered_sel_resolvent Sel P1 P2 C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
using assms ordered_resolvent_def ordered_sel_resolvent_def
[PROOF STATE]
proof (prove)
using this:
ordered_resolvent P1 P2 C
selected_part Sel P1 = {}
selected_part Sel P2 = {}
ordered_resolvent ?P1.0 ?P2.0 ?C \<equiv> \<exists>A. ?C = ?P1.0 - {Pos A} \<union> (?P2.0 - {Neg A}) \<and> strictly_maximal_literal ?P1.0 (Pos A) \<and> strictly_maximal_literal ?P2.0 (Neg A)
ordered_sel_resolvent ?Sel ?P1.0 ?P2.0 ?C \<equiv> \<exists>A. ?C = ?P1.0 - {Pos A} \<union> (?P2.0 - {Neg A}) \<and> strictly_maximal_literal ?P1.0 (Pos A) \<and> selected_part ?Sel ?P1.0 = {} \<and> (strictly_maximal_literal ?P2.0 (Neg A) \<and> selected_part ?Sel ?P2.0 = {} \<or> strictly_maximal_literal (selected_part ?Sel ?P2.0) (Neg A))

goal (1 subgoal):
 1. ordered_sel_resolvent Sel P1 P2 C
[PROOF STEP]
by auto


[STATEMENT]
lemma ordered_resolvent_upon_is_resolvent :
  assumes "strictly_maximal_literal P1 (Pos A)"
  assumes "strictly_maximal_literal P2 (Neg A)"
  shows "ordered_resolvent P1 P2 (resolvent_upon P1 P2 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordered_resolvent P1 P2 (resolvent_upon P1 P2 A)
[PROOF STEP]
using assms ordered_resolvent_def
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal P1 (Pos A)
strictly_maximal_literal P2 (Neg A)
ordered_resolvent ?P1.0 ?P2.0 ?C \<equiv> \<exists>A. ?C = ?P1.0 - {Pos A} \<union> (?P2.0 - {Neg A}) \<and> strictly_maximal_literal ?P1.0 (Pos A) \<and> strictly_maximal_literal ?P2.0 (Neg A)

goal (1 subgoal):
 1. ordered_resolvent P1 P2 (resolvent_upon P1 P2 A)
[PROOF STEP]
by auto


[STATEMENT]
lemma ordered_model_resolvent_is_resolvent : "less_restrictive resolvent (ordered_model_resolvent I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_restrictive resolvent (ordered_model_resolvent I)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> less_restrictive resolvent (ordered_model_resolvent I) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> less_restrictive resolvent (ordered_model_resolvent I)"
[PROOF STATE]
proof (state)
this:
\<not> less_restrictive resolvent (ordered_model_resolvent I)

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

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

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent (ordered_model_resolvent I) \<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 "strictly_maximal_literal P1 L"
    and "strictly_maximal_literal (validated_part I P2) (complement L)"
    and "C = (P1 - { L }) \<union> (P2 - { complement L })"
[PROOF STATE]
proof (prove)
using this:
ordered_model_resolvent I P1 P2 C

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>strictly_maximal_literal P1 L; strictly_maximal_literal (validated_part I P2) (complement L); C = P1 - {L} \<union> (P2 - {complement L})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ordered_model_resolvent_def [of I P1 P2 C]
[PROOF STATE]
proof (prove)
using this:
ordered_model_resolvent I P1 P2 C
ordered_model_resolvent I P1 P2 C = (\<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>strictly_maximal_literal P1 L; strictly_maximal_literal (validated_part I P2) (complement L); C = P1 - {L} \<union> (P2 - {complement L})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_literal P1 L
strictly_maximal_literal (validated_part I P2) (complement L)
C = P1 - {L} \<union> (P2 - {complement L})

goal (1 subgoal):
 1. \<not> less_restrictive resolvent (ordered_model_resolvent I) \<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]
by (simp only: strictly_maximal_literal_def)
[PROOF STATE]
proof (state)
this:
L \<in> P1

goal (1 subgoal):
 1. \<not> less_restrictive resolvent (ordered_model_resolvent I) \<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]
by (auto simp only: strictly_maximal_literal_def validated_part_def)
[PROOF STATE]
proof (state)
this:
complement L \<in> P2

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

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

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

goal (1 subgoal):
 1. resolvent P1 P2 C \<or> resolvent P2 P1 C
[PROOF STEP]
unfolding resolvent_def
[PROOF STATE]
proof (prove)
using this:
L = Pos A \<or> L = Neg A
C = P1 - {L} \<union> (P2 - {complement L})
L \<in> P1
complement L \<in> P2

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in> P1; complement L \<in> P2; C = P1 - {L} \<union> (P2 - {complement L})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using unit_resolvent_def [of P1 P2 C]
[PROOF STATE]
proof (prove)
using this:
unit_resolvent P1 P2 C
unit_resolvent P1 P2 C = ((\<exists>L. C = P1 - {L} \<union> (P2 - {complement L}) \<and> L \<in> P1 \<and> complement L \<in> P2) \<and> Unit P1)

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

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

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

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

goal (1 subgoal):
 1. resolvent P1 P2 C \<or> resolvent P2 P1 C
[PROOF STEP]
unfolding resolvent_def
[PROOF STATE]
proof (prove)
using this:
L = Pos A \<or> L = Neg A
C = P1 - {L} \<union> (P2 - {complement L})
L \<in> P1
complement L \<in> P2

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent unit_resolvent \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>resolvent P2 P1 C\<close> and \<open>\<not>resolvent P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decomposition_clause_pos_neg :
  "C = (negative_part C) \<union> (positive_part C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = negative_part C \<union> positive_part C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<subseteq> negative_part C \<union> positive_part C
 2. negative_part C \<union> positive_part C \<subseteq> C
[PROOF STEP]
show "C \<subseteq> (negative_part C) \<union> (positive_part C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> negative_part C \<union> positive_part C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
assume "x \<in> C"
[PROOF STATE]
proof (state)
this:
x \<in> C

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
obtain A where "x = Pos A \<or> x = Neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. x = Pos A \<or> x = Neg A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. x = Pos x1 \<Longrightarrow> ?P; \<And>x2. x = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
show "x \<in> (negative_part C) \<union> (positive_part C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
 2. \<not> ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
assume "x = Pos A"
[PROOF STATE]
proof (state)
this:
x = Pos A

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
 2. \<not> ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
from this and \<open>x \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
x = Pos A
x \<in> C
[PROOF STEP]
have "x \<in> positive_part C"
[PROOF STATE]
proof (prove)
using this:
x = Pos A
x \<in> C

goal (1 subgoal):
 1. x \<in> positive_part C
[PROOF STEP]
unfolding positive_part_def
[PROOF STATE]
proof (prove)
using this:
x = Pos A
x \<in> C

goal (1 subgoal):
 1. x \<in> {L. (\<exists>A. L = Pos A) \<and> L \<in> C}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> positive_part C

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
 2. \<not> ?P \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> positive_part C
[PROOF STEP]
show "x \<in> (negative_part C) \<union> (positive_part C)"
[PROOF STATE]
proof (prove)
using this:
x \<in> positive_part C

goal (1 subgoal):
 1. x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> negative_part C \<union> positive_part C

goal (1 subgoal):
 1. x \<noteq> Pos A \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> Pos A \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
assume "x \<noteq> Pos A"
[PROOF STATE]
proof (state)
this:
x \<noteq> Pos A

goal (1 subgoal):
 1. x \<noteq> Pos A \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
from this and \<open>x = Pos A \<or> x = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> Pos A
x = Pos A \<or> x = Neg A
[PROOF STEP]
have "x = Neg A"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> Pos A
x = Pos A \<or> x = Neg A

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

goal (1 subgoal):
 1. x \<noteq> Pos A \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
from this and \<open>x \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
x = Neg A
x \<in> C
[PROOF STEP]
have "x \<in> negative_part C"
[PROOF STATE]
proof (prove)
using this:
x = Neg A
x \<in> C

goal (1 subgoal):
 1. x \<in> negative_part C
[PROOF STEP]
unfolding negative_part_def
[PROOF STATE]
proof (prove)
using this:
x = Neg A
x \<in> C

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

goal (1 subgoal):
 1. x \<noteq> Pos A \<Longrightarrow> x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> negative_part C
[PROOF STEP]
show "x \<in> (negative_part C) \<union> (positive_part C)"
[PROOF STATE]
proof (prove)
using this:
x \<in> negative_part C

goal (1 subgoal):
 1. x \<in> negative_part C \<union> positive_part C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> negative_part C \<union> positive_part C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> negative_part C \<union> positive_part C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C \<subseteq> negative_part C \<union> positive_part C

goal (1 subgoal):
 1. negative_part C \<union> positive_part C \<subseteq> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. negative_part C \<union> positive_part C \<subseteq> C
[PROOF STEP]
show "(negative_part C) \<union> (positive_part C) \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. negative_part C \<union> positive_part C \<subseteq> C
[PROOF STEP]
unfolding negative_part_def
  and positive_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {L. (\<exists>A. L = Neg A) \<and> L \<in> C} \<union> {L. (\<exists>A. L = Pos A) \<and> L \<in> C} \<subseteq> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
negative_part C \<union> positive_part C \<subseteq> C

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>strictly_maximal_literal P1 L; strictly_maximal_literal (negative_part P2) (complement L); C = P1 - {L} \<union> (P2 - {complement L})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ordered_positive_resolvent_def [of P1 P2 C]
[PROOF STATE]
proof (prove)
using this:
ordered_positive_resolvent P1 P2 C
ordered_positive_resolvent P1 P2 C = (\<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))

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent ordered_positive_resolvent \<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> less_restrictive resolvent ordered_positive_resolvent \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal (negative_part P2) (complement L)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (negative_part P2) (complement L)
[PROOF STEP]
have "(complement L) \<in> P2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (negative_part P2) (complement L)

goal (1 subgoal):
 1. complement L \<in> P2
[PROOF STEP]
unfolding strictly_maximal_literal_def negative_part_def
[PROOF STATE]
proof (prove)
using this:
complement L \<in> {L. (\<exists>A. L = Neg A) \<and> L \<in> P2} \<and> (\<forall>B. B \<in> {L. (\<exists>A. L = Neg A) \<and> L \<in> P2} \<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> less_restrictive resolvent ordered_positive_resolvent \<Longrightarrow> False
[PROOF STEP]
obtain A where "L = Pos A \<or> L = Neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. L = Pos A \<or> L = Neg A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of L]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. L = Pos x1 \<Longrightarrow> ?P; \<And>x2. L = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

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

goal (1 subgoal):
 1. resolvent P1 P2 C \<or> resolvent P2 P1 C
[PROOF STEP]
unfolding resolvent_def
[PROOF STATE]
proof (prove)
using this:
L = Pos A \<or> L = Neg A
C = P1 - {L} \<union> (P2 - {complement L})
L \<in> P1
complement L \<in> P2

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent ordered_positive_resolvent \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>(resolvent P2 P1 C)\<close> and \<open>\<not>(resolvent P1 P2 C)\<close>
[PROOF STATE]
proof (chain)
picking this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>strictly_maximal_literal P1 L; strictly_maximal_literal (positive_part P2) (complement L); C = P1 - {L} \<union> (P2 - {complement L})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ordered_negative_resolvent_def [of P1 P2 C]
[PROOF STATE]
proof (prove)
using this:
ordered_negative_resolvent P1 P2 C
ordered_negative_resolvent P1 P2 C = (\<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))

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent ordered_negative_resolvent \<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> less_restrictive resolvent ordered_negative_resolvent \<Longrightarrow> False
[PROOF STEP]
from \<open>strictly_maximal_literal (positive_part P2) (complement L)\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal (positive_part P2) (complement L)
[PROOF STEP]
have "(complement L) \<in> P2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal (positive_part P2) (complement L)

goal (1 subgoal):
 1. complement L \<in> P2
[PROOF STEP]
unfolding strictly_maximal_literal_def positive_part_def
[PROOF STATE]
proof (prove)
using this:
complement L \<in> {L. (\<exists>A. L = Pos A) \<and> L \<in> P2} \<and> (\<forall>B. B \<in> {L. (\<exists>A. L = Pos A) \<and> L \<in> P2} \<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> less_restrictive resolvent ordered_negative_resolvent \<Longrightarrow> False
[PROOF STEP]
obtain A where "L = Pos A \<or> L = Neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. L = Pos A \<or> L = Neg A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of L]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. L = Pos x1 \<Longrightarrow> ?P; \<And>x2. L = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

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

goal (1 subgoal):
 1. resolvent P1 P2 C \<or> resolvent P2 P1 C
[PROOF STEP]
unfolding resolvent_def
[PROOF STATE]
proof (prove)
using this:
L = Pos A \<or> L = Neg A
C = P1 - {L} \<union> (P2 - {complement L})
L \<in> P1
complement L \<in> P2

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

goal (1 subgoal):
 1. \<not> less_restrictive resolvent ordered_negative_resolvent \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>resolvent P2 P1 C\<close> and \<open>\<not>resolvent P1 P2 C\<close>
[PROOF STATE]
proof (chain)
picking this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
resolvent P1 P2 C \<or> resolvent P2 P1 C
\<not> resolvent P2 P1 C
\<not> resolvent P1 P2 C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tautology_monotonous : "(tautology C) \<Longrightarrow> (C \<subseteq> D) \<Longrightarrow> (tautology D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tautology C; C \<subseteq> D\<rbrakk> \<Longrightarrow> tautology D
[PROOF STEP]
unfolding tautology_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>A. Pos A \<in> C \<and> Neg A \<in> C; C \<subseteq> D\<rbrakk> \<Longrightarrow> \<exists>A. Pos A \<in> D \<and> Neg A \<in> D
[PROOF STEP]
by auto


[STATEMENT]
lemma simplify_involutive:
  shows "simplify (simplify S) = (simplify S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplify (simplify S) = simplify S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simplify (simplify S) = simplify S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplify (simplify S) = simplify S
[PROOF STEP]
unfolding simplify_def strictly_redundant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C \<in> {C \<in> S. \<not> (tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subset> C))}. \<not> (tautology C \<or> (\<exists>D. D \<in> {C \<in> S. \<not> (tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subset> C))} \<and> D \<subset> C))} = {C \<in> S. \<not> (tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subset> C))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
simplify (simplify S) = simplify S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simplify_finite:
  assumes "all_fulfill finite S"
  shows "all_fulfill finite (simplify S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_fulfill finite (simplify S)
[PROOF STEP]
using assms all_fulfill_def simplify_def
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
all_fulfill ?P ?S = (\<forall>C. C \<in> ?S \<longrightarrow> ?P C)
simplify ?S = {C \<in> ?S. \<not> strictly_redundant C ?S}

goal (1 subgoal):
 1. all_fulfill finite (simplify S)
[PROOF STEP]
by auto


[STATEMENT]
lemma atoms_formula_simplify:
  shows "atoms_formula (simplify S) \<subseteq> atoms_formula S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_formula (simplify S) \<subseteq> atoms_formula S
[PROOF STEP]
unfolding simplify_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_formula {C \<in> S. \<not> strictly_redundant C S} \<subseteq> atoms_formula S
[PROOF STEP]
using atoms_formula_subset
[PROOF STATE]
proof (prove)
using this:
?S1.0 \<subseteq> ?S2.0 \<Longrightarrow> atoms_formula ?S1.0 \<subseteq> atoms_formula ?S2.0

goal (1 subgoal):
 1. atoms_formula {C \<in> S. \<not> strictly_redundant C S} \<subseteq> atoms_formula S
[PROOF STEP]
by auto


[STATEMENT]
lemma subsumption_preserves_redundancy :
  assumes "redundant C S"
  assumes "subsumes C D"
  shows "redundant D S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant D S
[PROOF STEP]
using assms tautology_monotonous
[PROOF STATE]
proof (prove)
using this:
redundant C S
subsumes C D
\<lbrakk>tautology ?C; ?C \<subseteq> ?D\<rbrakk> \<Longrightarrow> tautology ?D

goal (1 subgoal):
 1. redundant D S
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subseteq> C)
C \<subseteq> D
\<lbrakk>tautology ?C; ?C \<subseteq> ?D\<rbrakk> \<Longrightarrow> tautology ?D

goal (1 subgoal):
 1. tautology D \<or> (\<exists>Da. Da \<in> S \<and> Da \<subseteq> D)
[PROOF STEP]
by blast


[STATEMENT]
lemma subsumption_and_max_literal :
  assumes "subsumes C1 C2"
  assumes "strictly_maximal_literal C1 L1"
  assumes "strictly_maximal_literal C2 L2"
  assumes "A1 = atom L1"
  assumes "A2 = atom L2"
  shows "(A1 = A2) \<or> (A1,A2) \<in> atom_ordering"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>A1 = atom L1\<close>
[PROOF STATE]
proof (chain)
picking this:
A1 = atom L1
[PROOF STEP]
have "L1 = (Pos A1) \<or> L1 = (Neg A1)"
[PROOF STATE]
proof (prove)
using this:
A1 = atom L1

goal (1 subgoal):
 1. L1 = Pos A1 \<or> L1 = Neg A1
[PROOF STEP]
by (rule atom_property)
[PROOF STATE]
proof (state)
this:
L1 = Pos A1 \<or> L1 = Neg A1

goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>A2 = atom L2\<close>
[PROOF STATE]
proof (chain)
picking this:
A2 = atom L2
[PROOF STEP]
have "L2 = (Pos A2) \<or> L2 = (Neg A2)"
[PROOF STATE]
proof (prove)
using this:
A2 = atom L2

goal (1 subgoal):
 1. L2 = Pos A2 \<or> L2 = Neg A2
[PROOF STEP]
by (rule atom_property)
[PROOF STATE]
proof (state)
this:
L2 = Pos A2 \<or> L2 = Neg A2

goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>subsumes C1 C2\<close> and \<open>strictly_maximal_literal C1 L1\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes C1 C2
strictly_maximal_literal C1 L1
[PROOF STEP]
have "L1 \<in> C2"
[PROOF STATE]
proof (prove)
using this:
subsumes C1 C2
strictly_maximal_literal C1 L1

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

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

goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>strictly_maximal_literal C2 L2\<close> and \<open>L1 \<in> C2\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal C2 L2
L1 \<in> C2
[PROOF STEP]
have "L1 = L2 \<or> literal_ordering L1 L2"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal C2 L2
L1 \<in> C2

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

goal (1 subgoal):
 1. L1 = L2 \<or> literal_ordering L1 L2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L1 = L2 \<or> literal_ordering L1 L2

goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
L1 = L2 \<or> literal_ordering L1 L2

goal (1 subgoal):
 1. A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L1 = L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
 2. literal_ordering L1 L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
assume "L1 = L2"
[PROOF STATE]
proof (state)
this:
L1 = L2

goal (2 subgoals):
 1. L1 = L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
 2. literal_ordering L1 L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>L1 = L2\<close> and \<open>A1 = atom L1\<close> and \<open>A2 = atom L2\<close>
[PROOF STATE]
proof (chain)
picking this:
L1 = L2
A1 = atom L1
A2 = atom L2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L1 = L2
A1 = atom L1
A2 = atom L2

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

goal (1 subgoal):
 1. literal_ordering L1 L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. literal_ordering L1 L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
assume "literal_ordering L1 L2"
[PROOF STATE]
proof (state)
this:
literal_ordering L1 L2

goal (1 subgoal):
 1. literal_ordering L1 L2 \<Longrightarrow> A1 = A2 \<or> (A1, A2) \<in> atom_ordering
[PROOF STEP]
from \<open>literal_ordering L1 L2\<close> and \<open>L1 = (Pos A1) \<or> L1 = (Neg A1)\<close>
      and \<open>L2 = (Pos A2) \<or> L2 = (Neg A2)\<close>
[PROOF STATE]
proof (chain)
picking this:
literal_ordering L1 L2
L1 = Pos A1 \<or> L1 = Neg A1
L2 = Pos A2 \<or> L2 = Neg A2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
literal_ordering L1 L2
L1 = Pos A1 \<or> L1 = Neg A1
L2 = Pos A2 \<or> L2 = Neg A2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A1 = A2 \<or> (A1, A2) \<in> atom_ordering

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma superset_preserves_redundancy:
  assumes "redundant C S"
  assumes "S \<subseteq> S'"
  shows "redundant C S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C S'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
redundant C S
S \<subseteq> S'

goal (1 subgoal):
 1. redundant C S'
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology C \<or> (\<exists>D. D \<in> S \<and> subsumes D C)
S \<subseteq> S'

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> S' \<and> subsumes D C)
[PROOF STEP]
by blast


[STATEMENT]
lemma superset_preserves_strict_redundancy:
  assumes "strictly_redundant C S"
  assumes "S \<subseteq> SS"
  shows "strictly_redundant C SS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_redundant C SS
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
strictly_redundant C S
S \<subseteq> SS

goal (1 subgoal):
 1. strictly_redundant C SS
[PROOF STEP]
unfolding strictly_redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subset> C)
S \<subseteq> SS

goal (1 subgoal):
 1. tautology C \<or> (\<exists>D. D \<in> SS \<and> D \<subset> C)
[PROOF STEP]
by blast


[STATEMENT]
lemma tautologies_are_valid :
  assumes "tautology C"
  shows "validate_clause I C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile> C
[PROOF STEP]
by (meson assms tautology_def validate_clause.simps validate_literal.simps(1)
    validate_literal.simps(2))


[STATEMENT]
lemma subsumption_and_semantics :
  assumes "subsumes C D"
  assumes "validate_clause I C"
  shows "validate_clause I D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile> D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subsumes C D
I \<Turnstile> C

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

goal (1 subgoal):
 1. I \<Turnstile> D
[PROOF STEP]
by auto


[STATEMENT]
lemma redundancy_and_semantics :
  assumes "redundant C S"
  assumes "validate_formula I S"
  shows "validate_clause I C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile> C
[PROOF STEP]
by
(meson assms redundant_def subsumption_and_semantics tautologies_are_valid validate_formula.elims)


[STATEMENT]
lemma redundancy_implies_entailment:
  assumes "redundant C S"
  shows "entails S C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entails S C
[PROOF STEP]
using assms entails_def redundancy_and_semantics
[PROOF STATE]
proof (prove)
using this:
redundant C S
entails ?S ?C \<equiv> \<forall>I. I \<Turnstile> ?S \<longrightarrow> I \<Turnstile> ?C
\<lbrakk>redundant ?C ?S; ?I \<Turnstile> ?S\<rbrakk> \<Longrightarrow> ?I \<Turnstile> ?C

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