[STATEMENT]
lemma simplify_and_membership :
  assumes "all_fulfill finite S"
  assumes "T = simplify S"
  assumes "C \<in> S"
  shows "redundant C T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
have "\<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T" (is "?P n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>C. card C \<le> 0 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
 2. \<And>n. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T \<Longrightarrow> \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
show "?P 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. card C \<le> 0 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
proof ((rule allI),(rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
assume "card C \<le> 0" and "C \<in> S"
[PROOF STATE]
proof (state)
this:
card C \<le> 0
C \<in> S

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
from \<open>card C \<le> 0\<close> and \<open>C \<in> S\<close> and \<open>all_fulfill finite S\<close>
[PROOF STATE]
proof (chain)
picking this:
card C \<le> 0
C \<in> S
all_fulfill finite S
[PROOF STEP]
have "C = {}"
[PROOF STATE]
proof (prove)
using this:
card C \<le> 0
C \<in> S
all_fulfill finite S

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

goal (1 subgoal):
 1. C = {}
[PROOF STEP]
unfolding all_fulfill_def
[PROOF STATE]
proof (prove)
using this:
card C \<le> 0
C \<in> S
\<forall>C. C \<in> S \<longrightarrow> finite C
finite ?A \<Longrightarrow> (card ?A = 0) = (?A = {})

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

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = {}
[PROOF STEP]
have "\<not> strictly_redundant C S"
[PROOF STATE]
proof (prove)
using this:
C = {}

goal (1 subgoal):
 1. \<not> strictly_redundant C S
[PROOF STEP]
unfolding strictly_redundant_def tautology_def
[PROOF STATE]
proof (prove)
using this:
C = {}

goal (1 subgoal):
 1. \<not> ((\<exists>A. Pos A \<in> C \<and> Neg A \<in> C) \<or> (\<exists>D. D \<in> S \<and> D \<subset> C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> strictly_redundant C S

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
from this and \<open>C \<in> S\<close> and \<open>T = simplify S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> strictly_redundant C S
C \<in> S
T = simplify S
[PROOF STEP]
have "C \<in> T"
[PROOF STATE]
proof (prove)
using this:
\<not> strictly_redundant C S
C \<in> S
T = simplify S

goal (1 subgoal):
 1. C \<in> T
[PROOF STEP]
using simplify_def
[PROOF STATE]
proof (prove)
using this:
\<not> strictly_redundant C S
C \<in> S
T = simplify S
simplify ?S = {C \<in> ?S. \<not> strictly_redundant C ?S}

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

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> 0; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C \<in> T
[PROOF STEP]
show "redundant C T"
[PROOF STATE]
proof (prove)
using this:
C \<in> T

goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
C \<in> T

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> 0 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T

goal (1 subgoal):
 1. \<And>n. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T \<Longrightarrow> \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T \<Longrightarrow> \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T \<Longrightarrow> \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
assume "?P n"
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T

goal (1 subgoal):
 1. \<And>n. \<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T \<Longrightarrow> \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
show "?P (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
[PROOF STEP]
proof ((rule allI),(rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> Suc n; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> Suc n; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
assume "card C \<le> (Suc n)" and "C \<in> S"
[PROOF STATE]
proof (state)
this:
card C \<le> Suc n
C \<in> S

goal (1 subgoal):
 1. \<And>C. \<lbrakk>card C \<le> Suc n; C \<in> S\<rbrakk> \<Longrightarrow> redundant C T
[PROOF STEP]
show "redundant C T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
assume "\<not>redundant C T"
[PROOF STATE]
proof (state)
this:
\<not> redundant C T

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> redundant C T
[PROOF STEP]
have "C \<notin> T"
[PROOF STATE]
proof (prove)
using this:
\<not> redundant C T

goal (1 subgoal):
 1. C \<notin> T
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
\<not> (tautology C \<or> (\<exists>D. D \<in> T \<and> D \<subseteq> C))

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

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
from this and \<open>T = simplify S\<close> and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<notin> T
T = simplify S
C \<in> S
[PROOF STEP]
have "strictly_redundant C S"
[PROOF STATE]
proof (prove)
using this:
C \<notin> T
T = simplify S
C \<in> S

goal (1 subgoal):
 1. strictly_redundant C S
[PROOF STEP]
unfolding simplify_def strictly_redundant_def
[PROOF STATE]
proof (prove)
using this:
C \<notin> T
T = {C \<in> S. \<not> (tautology C \<or> (\<exists>D. D \<in> S \<and> D \<subset> C))}
C \<in> S

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

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>redundant C T\<close>
[PROOF STATE]
proof (chain)
picking this:
strictly_redundant C S
\<not> redundant C T
[PROOF STEP]
obtain D where "D \<in> S" and "D \<subset> C"
[PROOF STATE]
proof (prove)
using this:
strictly_redundant C S
\<not> redundant C T

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

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

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

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

goal (1 subgoal):
 1. card D < card C
[PROOF STEP]
using psubset_card_mono
[PROOF STATE]
proof (prove)
using this:
D \<subset> C
C \<in> S
\<forall>C. C \<in> S \<longrightarrow> finite C
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B

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

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
from this and \<open>card C \<le> (Suc n)\<close>
[PROOF STATE]
proof (chain)
picking this:
card D < card C
card C \<le> Suc n
[PROOF STEP]
have "card D \<le> n"
[PROOF STATE]
proof (prove)
using this:
card D < card C
card C \<le> Suc n

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

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
from this and  \<open>?P n\<close> and \<open>D \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
card D \<le> n
\<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
D \<in> S
[PROOF STEP]
have "redundant D T"
[PROOF STATE]
proof (prove)
using this:
card D \<le> n
\<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
D \<in> S

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

goal (1 subgoal):
 1. \<not> redundant C T \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume "tautology D"
[PROOF STATE]
proof (state)
this:
tautology D

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from this and  \<open>D \<subset> C\<close>
[PROOF STATE]
proof (chain)
picking this:
tautology D
D \<subset> C
[PROOF STEP]
have "tautology C"
[PROOF STATE]
proof (prove)
using this:
tautology D
D \<subset> C

goal (1 subgoal):
 1. tautology C
[PROOF STEP]
unfolding tautology_def
[PROOF STATE]
proof (prove)
using this:
\<exists>A. Pos A \<in> D \<and> Neg A \<in> D
D \<subset> C

goal (1 subgoal):
 1. \<exists>A. Pos A \<in> C \<and> Neg A \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tautology C

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tautology C
[PROOF STEP]
have "redundant C T"
[PROOF STATE]
proof (prove)
using this:
tautology C

goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
unfolding redundant_def
[PROOF STATE]
proof (prove)
using this:
tautology C

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>redundant C T\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant C T
\<not> redundant C T
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
redundant C T
\<not> redundant C T

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

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

goal (1 subgoal):
 1. \<not> tautology D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>redundant D T\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology D
redundant D T
[PROOF STEP]
obtain E where "E \<in> T" and "E \<subseteq> D"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology D
redundant D T

goal (1 subgoal):
 1. (\<And>E. \<lbrakk>E \<in> T; E \<subseteq> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
\<not> tautology D
tautology D \<or> (\<exists>Da. Da \<in> T \<and> Da \<subseteq> D)

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

goal (1 subgoal):
 1. \<not> tautology D \<Longrightarrow> False
[PROOF STEP]
from this and  \<open>D \<subset> C\<close>
[PROOF STATE]
proof (chain)
picking this:
E \<in> T
E \<subseteq> D
D \<subset> C
[PROOF STEP]
have "E \<subseteq> C"
[PROOF STATE]
proof (prove)
using this:
E \<in> T
E \<subseteq> D
D \<subset> C

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

goal (1 subgoal):
 1. \<not> tautology D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>E \<in> T\<close> and  \<open>\<not>redundant C T\<close>
[PROOF STATE]
proof (chain)
picking this:
E \<subseteq> C
E \<in> T
\<not> redundant C T
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> C
E \<in> T
\<not> redundant C T

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding redundant_def and subsumes_def
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> C
E \<in> T
\<not> (tautology C \<or> (\<exists>D. D \<in> T \<and> D \<subseteq> C))

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> Suc n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> n \<longrightarrow> C \<in> S \<longrightarrow> redundant C T

goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>C. card C \<le> ?n2 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T

goal (1 subgoal):
 1. redundant C T
[PROOF STEP]
from this and \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>C. card C \<le> ?n2 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
C \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>C. card C \<le> ?n2 \<longrightarrow> C \<in> S \<longrightarrow> redundant C T
C \<in> S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simplify_preserves_redundancy:
  assumes "all_fulfill finite S"
  assumes "redundant C S"
  shows "redundant C (simplify S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (simplify S)
[PROOF STEP]
by (meson assms redundant_def simplify_and_membership subsumption_preserves_redundancy)


[STATEMENT]
lemma simplify_preserves_strict_redundancy:
  assumes "all_fulfill finite S"
  assumes "strictly_redundant C S"
  shows "strictly_redundant C (simplify S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_redundant C (simplify S)
[PROOF STEP]
proof ((cases "tautology C"),(auto simp add: strictly_redundant_def)[1])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
assume "\<not>tautology C"
[PROOF STATE]
proof (state)
this:
\<not> tautology C

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology C
strictly_redundant C S
[PROOF STEP]
obtain D where "D \<subset> C" and "D \<in> S"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
strictly_redundant C S

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from \<open>D \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<in> S
[PROOF STEP]
have "redundant D S"
[PROOF STATE]
proof (prove)
using this:
D \<in> S

goal (1 subgoal):
 1. redundant D S
[PROOF STEP]
unfolding redundant_def subsumes_def
[PROOF STATE]
proof (prove)
using this:
D \<in> S

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from assms(1) this
[PROOF STATE]
proof (chain)
picking this:
all_fulfill finite S
redundant D S
[PROOF STEP]
have "redundant D (simplify S)"
[PROOF STATE]
proof (prove)
using this:
all_fulfill finite S
redundant D S

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from \<open>\<not>tautology C\<close> and \<open>D \<subset> C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> tautology C
D \<subset> C
[PROOF STEP]
have "\<not>tautology D"
[PROOF STATE]
proof (prove)
using this:
\<not> tautology C
D \<subset> C

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

goal (1 subgoal):
 1. \<nexists>A. Pos A \<in> D \<and> Neg A \<in> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> tautology D

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

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from \<open>subsumes E D\<close> and \<open>D \<subset> C\<close>
[PROOF STATE]
proof (chain)
picking this:
subsumes E D
D \<subset> C
[PROOF STEP]
have "E \<subset> C"
[PROOF STATE]
proof (prove)
using this:
subsumes E D
D \<subset> C

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

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

goal (1 subgoal):
 1. \<not> tautology C \<Longrightarrow> strictly_redundant C (simplify S)
[PROOF STEP]
from this and \<open>E \<in> simplify S\<close>
[PROOF STATE]
proof (chain)
picking this:
E \<subset> C
E \<in> simplify S
[PROOF STEP]
show "strictly_redundant C (simplify S)"
[PROOF STATE]
proof (prove)
using this:
E \<subset> C
E \<in> simplify S

goal (1 subgoal):
 1. strictly_redundant C (simplify S)
[PROOF STEP]
unfolding strictly_redundant_def
[PROOF STATE]
proof (prove)
using this:
E \<subset> C
E \<in> simplify S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simplify_preserves_semantic :
  assumes "T = simplify S"
  assumes "all_fulfill finite S"
  shows "validate_formula I S \<longleftrightarrow> validate_formula I T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile> S = I \<Turnstile> T
[PROOF STEP]
by (metis (mono_tags, lifting) assms mem_Collect_eq redundancy_and_semantics simplify_and_membership
    simplify_def validate_formula.simps)


[STATEMENT]
lemma simplify_preserves_equivalence :
  assumes "T = simplify S"
  assumes "all_fulfill finite S"
  shows "equivalent S T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalent S T
[PROOF STEP]
using assms equivalent_def simplify_preserves_semantic validity_implies_entailment
[PROOF STATE]
proof (prove)
using this:
T = simplify S
all_fulfill finite S
equivalent ?S1.0 ?S2.0 = (entails_formula ?S1.0 ?S2.0 \<and> entails_formula ?S2.0 ?S1.0)
\<lbrakk>?T = simplify ?S; all_fulfill finite ?S\<rbrakk> \<Longrightarrow> ?I \<Turnstile> ?S = ?I \<Turnstile> ?T
\<forall>I. I \<Turnstile> ?S1.0 \<longrightarrow> I \<Turnstile> ?S2.0 \<Longrightarrow> entails_formula ?S1.0 ?S2.0

goal (1 subgoal):
 1. equivalent S T
[PROOF STEP]
by auto


[STATEMENT]
lemma simplify_non_redundant:
  shows "non_redundant (simplify S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_redundant (simplify S)
[PROOF STEP]
by (simp add: non_redundant_def simplify_def strictly_redundant_def)


[STATEMENT]
lemma deducible_clause_preserve_redundancy:
  assumes "redundant C S"
  shows "redundant C (add_all_deducible_clauses R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R S)
[PROOF STEP]
using assms superset_preserves_redundancy
[PROOF STATE]
proof (prove)
using this:
redundant C S
\<lbrakk>redundant ?C ?S; ?S \<subseteq> ?S'\<rbrakk> \<Longrightarrow> redundant ?C ?S'

goal (1 subgoal):
 1. redundant C (add_all_deducible_clauses R S)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma inverse_clause_renaming : "(rename_clause A (rename_clause A L)) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause A (rename_clause A L) = L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_clause A (rename_clause A L) = L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause A (rename_clause A L) = L
[PROOF STEP]
using inverse_renaming
[PROOF STATE]
proof (prove)
using this:
rename_literal ?A (rename_literal ?A ?L) = ?L

goal (1 subgoal):
 1. rename_clause A (rename_clause A L) = L
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
rename_literal ?A (rename_literal ?A ?L) = ?L

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inverse_formula_renaming : "rename_formula A (rename_formula A L) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_formula A (rename_formula A L) = L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_formula A (rename_formula A L) = L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_formula A (rename_formula A L) = L
[PROOF STEP]
using inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
rename_clause ?A (rename_clause ?A ?L) = ?L

goal (1 subgoal):
 1. rename_formula A (rename_formula A L) = L
[PROOF STEP]
unfolding rename_formula_def
[PROOF STATE]
proof (prove)
using this:
rename_clause ?A (rename_clause ?A ?L) = ?L

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_preserves_cardinality :
  "card (rename_clause A C) = card C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (rename_clause A C) = card C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (rename_clause A C) = card C
[PROOF STEP]
have im: "rename_clause A C = (rename_literal A) ` C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause A C = rename_literal A ` C
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {L. \<exists>LL. LL \<in> C \<and> L = rename_literal A LL} = rename_literal A ` C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_clause A C = rename_literal A ` C

goal (1 subgoal):
 1. card (rename_clause A C) = card C
[PROOF STEP]
have "inj_on (rename_literal A) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (rename_literal A) C
[PROOF STEP]
by (metis inj_onI inverse_renaming)
[PROOF STATE]
proof (state)
this:
inj_on (rename_literal A) C

goal (1 subgoal):
 1. card (rename_clause A C) = card C
[PROOF STEP]
from this and im
[PROOF STATE]
proof (chain)
picking this:
inj_on (rename_literal A) C
rename_clause A C = rename_literal A ` C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (rename_literal A) C
rename_clause A C = rename_literal A ` C

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_preserves_literal_order :
  assumes "literal_ordering L1 L2"
  shows "literal_ordering (rename_literal A L1) (rename_literal A L2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literal_ordering (rename_literal A L1) (rename_literal A L2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. literal_ordering (rename_literal A L1) (rename_literal A L2)
[PROOF STEP]
obtain A1 where at1: "L1 = (Pos A1) \<or> L1 = (Neg A1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A1. L1 = Pos A1 \<or> L1 = Neg A1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of L1 ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. L1 = Pos x1 \<Longrightarrow> ?P; \<And>x2. L1 = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. literal_ordering (rename_literal A L1) (rename_literal A L2)
[PROOF STEP]
obtain A2 where at2: "L2 = (Pos A2) \<or> L2 = (Neg A2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A2. L2 = Pos A2 \<or> L2 = Neg A2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Literal.exhaust [of L2 ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. L2 = Pos x1 \<Longrightarrow> ?P; \<And>x2. L2 = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. literal_ordering (rename_literal A L1) (rename_literal A L2)
[PROOF STEP]
from assms and at1 and at2
[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. literal_ordering (rename_literal A L1) (rename_literal A L2)
[PROOF STEP]
unfolding rename_literal_def
[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. literal_ordering (if atom L1 \<in> A then complement L1 else L1) (if atom L2 \<in> A then complement L2 else L2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
literal_ordering (rename_literal A L1) (rename_literal A L2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inverse_renaming_preserves_literal_order :
  assumes  "literal_ordering (rename_literal A L1) (rename_literal A L2)"
  shows "literal_ordering L1 L2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. literal_ordering L1 L2
[PROOF STEP]
by (metis assms inverse_renaming renaming_preserves_literal_order)


[STATEMENT]
lemma renaming_is_injective:
  assumes "rename_literal A L1 = rename_literal A L2"
  shows "L1 = L2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L1 = L2
[PROOF STEP]
by (metis (no_types) assms inverse_renaming)


[STATEMENT]
lemma renaming_preserves_strictly_maximal_literal :
  assumes "strictly_maximal_literal C L"
  shows "strictly_maximal_literal (rename_clause A C) (rename_literal A L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause A C) (rename_literal A L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause A C) (rename_literal A L)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
strictly_maximal_literal C L
[PROOF STEP]
have "(L \<in> C)" and Lismax: "(\<forall>B. (B \<in> C \<and> L \<noteq> B)  \<longrightarrow> (literal_ordering B L))"
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_literal C L

goal (1 subgoal):
 1. L \<in> C &&& \<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:
L \<in> C \<and> (\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L)

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

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause A C) (rename_literal A L)
[PROOF STEP]
from \<open>L \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> C
[PROOF STEP]
have "(rename_literal A L) \<in> (rename_clause A C)"
[PROOF STATE]
proof (prove)
using this:
L \<in> C

goal (1 subgoal):
 1. rename_literal A L \<in> rename_clause A C
[PROOF STEP]
unfolding rename_literal_def and rename_clause_def
[PROOF STATE]
proof (prove)
using this:
L \<in> C

goal (1 subgoal):
 1. (if atom L \<in> A then complement L else L) \<in> {L. \<exists>LL. LL \<in> C \<and> L = (if atom LL \<in> A then complement LL else LL)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal A L \<in> rename_clause A C

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause A C) (rename_literal A L)
[PROOF STEP]
have
    "\<forall>B. (B \<in> rename_clause A C \<longrightarrow> rename_literal A L \<noteq> B
      \<longrightarrow> literal_ordering B (rename_literal A L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B. B \<in> rename_clause A C \<longrightarrow> rename_literal A L \<noteq> B \<longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
proof (rule)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
assume "B \<in> rename_clause A C" and "rename_literal A L \<noteq> B"
[PROOF STATE]
proof (state)
this:
B \<in> rename_clause A C
rename_literal A L \<noteq> B

goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
from \<open>B \<in> rename_clause A C\<close>
[PROOF STATE]
proof (chain)
picking this:
B \<in> rename_clause A C
[PROOF STEP]
obtain B' where "B' \<in> C" and "B = rename_literal A B'"
[PROOF STATE]
proof (prove)
using this:
B \<in> rename_clause A C

goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>B' \<in> C; B = rename_literal A B'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
B \<in> {L. \<exists>LL. LL \<in> C \<and> L = rename_literal A LL}

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

goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
from \<open>rename_literal A L \<noteq> B\<close> and \<open>B = rename_literal A B'\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_literal A L \<noteq> B
B = rename_literal A B'
[PROOF STEP]
have "rename_literal A L \<noteq> rename_literal A B'"
[PROOF STATE]
proof (prove)
using this:
rename_literal A L \<noteq> B
B = rename_literal A B'

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

goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
hence "L \<noteq> B'"
[PROOF STATE]
proof (prove)
using this:
rename_literal A L \<noteq> rename_literal A B'

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

goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
from this and \<open>B' \<in> C\<close> and Lismax
[PROOF STATE]
proof (chain)
picking this:
L \<noteq> B'
B' \<in> C
\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L
[PROOF STEP]
have "literal_ordering B' L"
[PROOF STATE]
proof (prove)
using this:
L \<noteq> B'
B' \<in> C
\<forall>B. B \<in> C \<and> L \<noteq> B \<longrightarrow> literal_ordering B L

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

goal (1 subgoal):
 1. \<And>B. \<lbrakk>B \<in> rename_clause A C; rename_literal A L \<noteq> B\<rbrakk> \<Longrightarrow> literal_ordering B (rename_literal A L)
[PROOF STEP]
from this and \<open>B = (rename_literal A B')\<close>
[PROOF STATE]
proof (chain)
picking this:
literal_ordering B' L
B = rename_literal A B'
[PROOF STEP]
show "literal_ordering B (rename_literal A L)"
[PROOF STATE]
proof (prove)
using this:
literal_ordering B' L
B = rename_literal A B'

goal (1 subgoal):
 1. literal_ordering B (rename_literal A L)
[PROOF STEP]
using renaming_preserves_literal_order
[PROOF STATE]
proof (prove)
using this:
literal_ordering B' L
B = rename_literal A B'
literal_ordering ?L1.0 ?L2.0 \<Longrightarrow> literal_ordering (rename_literal ?A ?L1.0) (rename_literal ?A ?L2.0)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>B. B \<in> rename_clause A C \<longrightarrow> rename_literal A L \<noteq> B \<longrightarrow> literal_ordering B (rename_literal A L)

goal (1 subgoal):
 1. strictly_maximal_literal (rename_clause A C) (rename_literal A L)
[PROOF STEP]
from this and \<open>(rename_literal A L) \<in> (rename_clause A C)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>B. B \<in> rename_clause A C \<longrightarrow> rename_literal A L \<noteq> B \<longrightarrow> literal_ordering B (rename_literal A L)
rename_literal A L \<in> rename_clause A C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>B. B \<in> rename_clause A C \<longrightarrow> rename_literal A L \<noteq> B \<longrightarrow> literal_ordering B (rename_literal A L)
rename_literal A L \<in> rename_clause A C

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_and_selected_part :
  "selected_part UNIV C = rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selected_part UNIV C = rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. selected_part UNIV C \<subseteq> rename_clause Sel (validated_part Sel (rename_clause Sel C))
 2. rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> selected_part UNIV C
[PROOF STEP]
show "selected_part UNIV C \<subseteq> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selected_part UNIV C \<subseteq> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> selected_part UNIV C \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> selected_part UNIV C \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
assume "x \<in> selected_part UNIV C"
[PROOF STATE]
proof (state)
this:
x \<in> selected_part UNIV C

goal (1 subgoal):
 1. \<And>x. x \<in> selected_part UNIV C \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
show "x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from \<open>x \<in> selected_part UNIV C\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> selected_part UNIV C
[PROOF STEP]
obtain A where "x = Neg A" and "x \<in> C"
[PROOF STATE]
proof (prove)
using this:
x \<in> selected_part UNIV C

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

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

goal (1 subgoal):
 1. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from \<open>x \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> C
[PROOF STEP]
have "rename_literal Sel x \<in> rename_clause Sel C"
[PROOF STATE]
proof (prove)
using this:
x \<in> C

goal (1 subgoal):
 1. rename_literal Sel x \<in> rename_clause Sel C
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
x \<in> C

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

goal (1 subgoal):
 1. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
show "x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
 2. \<not> ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
assume "A \<in> Sel"
[PROOF STATE]
proof (state)
this:
A \<in> Sel

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

goal (1 subgoal):
 1. rename_literal Sel x = Pos A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel
x = Neg A

goal (1 subgoal):
 1. (if atom x \<in> Sel then complement x else x) = Pos A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel x = Pos A

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
 2. \<not> ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from this and \<open>rename_literal Sel x \<in> rename_clause Sel C\<close>
[PROOF STATE]
proof (chain)
picking this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C
[PROOF STEP]
have "rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C

goal (1 subgoal):
 1. rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)
[PROOF STEP]
unfolding validated_part_def
[PROOF STATE]
proof (prove)
using this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C

goal (1 subgoal):
 1. rename_literal Sel x \<in> {L \<in> rename_clause Sel C. Sel \<Turnstile> L}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
 2. \<not> ?P \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
thus "x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)

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

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
assume "A \<notin> Sel"
[PROOF STATE]
proof (state)
this:
A \<notin> Sel

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from this and \<open>x = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> Sel
x = Neg A
[PROOF STEP]
have "rename_literal Sel x = Neg A"
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
x = Neg A

goal (1 subgoal):
 1. rename_literal Sel x = Neg A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
x = Neg A

goal (1 subgoal):
 1. (if atom x \<in> Sel then complement x else x) = Neg A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel x = Neg A

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from this and \<open>A \<notin> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_literal Sel x = Neg A
A \<notin> Sel
[PROOF STEP]
have "validate_literal Sel (rename_literal Sel x)"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel x = Neg A
A \<notin> Sel

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
from this and \<open>rename_literal Sel x \<in> rename_clause Sel C\<close>
[PROOF STATE]
proof (chain)
picking this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C
[PROOF STEP]
have "rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C

goal (1 subgoal):
 1. rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)
[PROOF STEP]
unfolding  validated_part_def
[PROOF STATE]
proof (prove)
using this:
Sel \<Turnstile> rename_literal Sel x
rename_literal Sel x \<in> rename_clause Sel C

goal (1 subgoal):
 1. rename_literal Sel x \<in> {L \<in> rename_clause Sel C. Sel \<Turnstile> L}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
thus "x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel x \<in> validated_part Sel (rename_clause Sel C)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
selected_part UNIV C \<subseteq> rename_clause Sel (validated_part Sel (rename_clause Sel C))

goal (1 subgoal):
 1. rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> selected_part UNIV C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> selected_part UNIV C
[PROOF STEP]
show "rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> (selected_part UNIV C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> selected_part UNIV C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
assume "x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))"
[PROOF STATE]
proof (state)
this:
x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))
[PROOF STEP]
obtain y where "y \<in> validated_part Sel (rename_clause Sel C)"
      and "x = rename_literal Sel y"
[PROOF STATE]
proof (prove)
using this:
x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> validated_part Sel (rename_clause Sel C); x = rename_literal Sel y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rename_clause_def validated_part_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {L. \<exists>LL. LL \<in> {L \<in> {L. \<exists>LL. LL \<in> C \<and> L = rename_literal Sel LL}. Sel \<Turnstile> L} \<and> L = rename_literal Sel LL}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> {L \<in> {L. \<exists>LL. LL \<in> C \<and> L = rename_literal Sel LL}. Sel \<Turnstile> L}; x = rename_literal Sel y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> validated_part Sel (rename_clause Sel C)
x = rename_literal Sel y

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from \<open>y \<in> validated_part Sel (rename_clause Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> validated_part Sel (rename_clause Sel C)
[PROOF STEP]
have
      "y \<in> rename_clause Sel C" and "validate_literal Sel y"
[PROOF STATE]
proof (prove)
using this:
y \<in> validated_part Sel (rename_clause Sel C)

goal (1 subgoal):
 1. y \<in> rename_clause Sel C &&& Sel \<Turnstile> y
[PROOF STEP]
unfolding validated_part_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {L \<in> rename_clause Sel C. Sel \<Turnstile> L}

goal (1 subgoal):
 1. y \<in> rename_clause Sel C &&& Sel \<Turnstile> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> rename_clause Sel C
Sel \<Turnstile> y

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from \<open>y \<in> rename_clause Sel C\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> rename_clause Sel C
[PROOF STEP]
obtain z where "z \<in> C" and "y = rename_literal Sel z"
[PROOF STATE]
proof (prove)
using this:
y \<in> rename_clause Sel C

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> C; y = rename_literal Sel z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {L. \<exists>LL. LL \<in> C \<and> L = rename_literal Sel LL}

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
show "x \<in> selected_part UNIV C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> selected_part UNIV C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> selected_part UNIV C
 2. \<not> ?P \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
assume "A \<in> Sel"
[PROOF STATE]
proof (state)
this:
A \<in> Sel

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> selected_part UNIV C
 2. \<not> ?P \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and zA and \<open>y = rename_literal Sel z\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z
[PROOF STEP]
have "y = complement z"
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z

goal (1 subgoal):
 1. y = complement z
[PROOF STEP]
using rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z
rename_literal ?A ?L = (if atom ?L \<in> ?A then complement ?L else ?L)

goal (1 subgoal):
 1. y = complement z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = complement z

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> selected_part UNIV C
 2. \<not> ?P \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and \<open>A \<in> Sel\<close> and zA and \<open>validate_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
y = complement z
A \<in> Sel
z = Pos A \<or> z = Neg A
Sel \<Turnstile> y
[PROOF STEP]
have "y = Pos A"
          and "z = Neg A"
[PROOF STATE]
proof (prove)
using this:
y = complement z
A \<in> Sel
z = Pos A \<or> z = Neg A
Sel \<Turnstile> y

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> selected_part UNIV C
 2. \<not> ?P \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and  \<open>A \<in> Sel\<close> and \<open>x = rename_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
y = Pos A
z = Neg A
A \<in> Sel
x = rename_literal Sel y
[PROOF STEP]
have "x = Neg A"
[PROOF STATE]
proof (prove)
using this:
y = Pos A
z = Neg A
A \<in> Sel
x = rename_literal Sel y

goal (1 subgoal):
 1. x = Neg A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
y = Pos A
z = Neg A
A \<in> Sel
x = (if atom y \<in> Sel then complement y else y)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x \<in> selected_part UNIV C
 2. \<not> ?P \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and \<open>z \<in> C\<close> and \<open>z = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
x = Neg A
z \<in> C
z = Neg A
[PROOF STEP]
show "x \<in> selected_part UNIV C"
[PROOF STATE]
proof (prove)
using this:
x = Neg A
z \<in> C
z = Neg A

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

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
assume "A \<notin> Sel"
[PROOF STATE]
proof (state)
this:
A \<notin> Sel

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and zA and \<open>y = rename_literal Sel z\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z
[PROOF STEP]
have "y = z"
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z

goal (1 subgoal):
 1. y = z
[PROOF STEP]
using rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
z = Pos A \<or> z = Neg A
y = rename_literal Sel z
rename_literal ?A ?L = (if atom ?L \<in> ?A then complement ?L else ?L)

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and \<open>A \<notin> Sel\<close> and zA and \<open>validate_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
y = z
A \<notin> Sel
z = Pos A \<or> z = Neg A
Sel \<Turnstile> y
[PROOF STEP]
have "y = Neg A"
          and "z = Neg A"
[PROOF STATE]
proof (prove)
using this:
y = z
A \<notin> Sel
z = Pos A \<or> z = Neg A
Sel \<Turnstile> y

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and  \<open>A \<notin> Sel\<close> and \<open>x = rename_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
y = Neg A
z = Neg A
A \<notin> Sel
x = rename_literal Sel y
[PROOF STEP]
have "x = Neg A"
[PROOF STATE]
proof (prove)
using this:
y = Neg A
z = Neg A
A \<notin> Sel
x = rename_literal Sel y

goal (1 subgoal):
 1. x = Neg A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
y = Neg A
z = Neg A
A \<notin> Sel
x = (if atom y \<in> Sel then complement y else y)

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> x \<in> selected_part UNIV C
[PROOF STEP]
from this and \<open>z \<in> C\<close> and \<open>z = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
x = Neg A
z \<in> C
z = Neg A
[PROOF STEP]
show "x \<in> selected_part UNIV C"
[PROOF STATE]
proof (prove)
using this:
x = Neg A
z \<in> C
z = Neg A

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rename_clause Sel (validated_part Sel (rename_clause Sel C)) \<subseteq> selected_part UNIV C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_preserves_tautology:
  assumes "tautology C"
  shows "tautology (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
tautology C
[PROOF STEP]
obtain A where "Pos A \<in> C" and "Neg A \<in> C"
[PROOF STATE]
proof (prove)
using this:
tautology C

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>Pos A \<in> C; Neg A \<in> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding tautology_def
[PROOF STATE]
proof (prove)
using this:
\<exists>A. Pos A \<in> C \<and> Neg A \<in> C

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

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

goal (1 subgoal):
 1. rename_literal Sel (Pos A) \<in> rename_clause Sel C
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
Pos A \<in> C

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

goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
from \<open>Neg A \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> C
[PROOF STEP]
have "rename_literal Sel (Neg A) \<in>  rename_clause Sel C"
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> C

goal (1 subgoal):
 1. rename_literal Sel (Neg A) \<in> rename_clause Sel C
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> C

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

goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> tautology (rename_clause Sel C)
 2. \<not> ?P \<Longrightarrow> tautology (rename_clause Sel C)
[PROOF STEP]
assume "A \<in> Sel"
[PROOF STATE]
proof (state)
this:
A \<in> Sel

goal (2 subgoals):
 1. ?P \<Longrightarrow> tautology (rename_clause Sel C)
 2. \<not> ?P \<Longrightarrow> tautology (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A \<in> Sel
[PROOF STEP]
have "rename_literal Sel (Pos A) = Neg A"
      and "rename_literal Sel (Neg A) = (Pos A)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel

goal (1 subgoal):
 1. rename_literal Sel (Pos A) = Neg A &&& rename_literal Sel (Neg A) = Pos A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel

goal (1 subgoal):
 1. (if atom (Pos A) \<in> Sel then complement (Pos A) else Pos A) = Neg A &&& (if atom (Neg A) \<in> Sel then complement (Neg A) else Neg A) = Pos A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel (Pos A) = Neg A
rename_literal Sel (Neg A) = Pos A

goal (2 subgoals):
 1. ?P \<Longrightarrow> tautology (rename_clause Sel C)
 2. \<not> ?P \<Longrightarrow> tautology (rename_clause Sel C)
[PROOF STEP]
from \<open>rename_literal Sel (Pos A) = (Neg A)\<close> and  \<open>rename_literal Sel (Neg A) = (Pos A)\<close>
      and \<open>rename_literal Sel (Pos A) \<in>  (rename_clause Sel C)\<close>
      and  \<open>rename_literal Sel (Neg A) \<in>  (rename_clause Sel C)\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_literal Sel (Pos A) = Neg A
rename_literal Sel (Neg A) = Pos A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C
[PROOF STEP]
show "tautology (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Pos A) = Neg A
rename_literal Sel (Neg A) = Pos A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C

goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
unfolding tautology_def
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Pos A) = Neg A
rename_literal Sel (Neg A) = Pos A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C

goal (1 subgoal):
 1. \<exists>A. Pos A \<in> rename_clause Sel C \<and> Neg A \<in> rename_clause Sel C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tautology (rename_clause Sel C)

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> tautology (rename_clause Sel C)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A \<notin> Sel
[PROOF STEP]
have "rename_literal Sel (Pos A) = Pos A" and "rename_literal Sel (Neg A) = (Neg A)"
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel

goal (1 subgoal):
 1. rename_literal Sel (Pos A) = Pos A &&& rename_literal Sel (Neg A) = Neg A
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel

goal (1 subgoal):
 1. (if atom (Pos A) \<in> Sel then complement (Pos A) else Pos A) = Pos A &&& (if atom (Neg A) \<in> Sel then complement (Neg A) else Neg A) = Neg A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel (Pos A) = Pos A
rename_literal Sel (Neg A) = Neg A

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> tautology (rename_clause Sel C)
[PROOF STEP]
from \<open>rename_literal Sel (Pos A) = Pos A\<close> and \<open>rename_literal Sel (Neg A) = (Neg A)\<close>
      and \<open>rename_literal Sel (Pos A) \<in>  rename_clause Sel C\<close>
      and  \<open>rename_literal Sel (Neg A) \<in>  rename_clause Sel C\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_literal Sel (Pos A) = Pos A
rename_literal Sel (Neg A) = Neg A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C
[PROOF STEP]
show "tautology (rename_clause Sel C)"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Pos A) = Pos A
rename_literal Sel (Neg A) = Neg A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C

goal (1 subgoal):
 1. tautology (rename_clause Sel C)
[PROOF STEP]
unfolding tautology_def
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel (Pos A) = Pos A
rename_literal Sel (Neg A) = Neg A
rename_literal Sel (Pos A) \<in> rename_clause Sel C
rename_literal Sel (Neg A) \<in> rename_clause Sel C

goal (1 subgoal):
 1. \<exists>A. Pos A \<in> rename_clause Sel C \<and> Neg A \<in> rename_clause Sel C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tautology (rename_clause Sel C)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
tautology (rename_clause Sel C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rename_union : "rename_clause Sel (C \<union> D) = rename_clause Sel C \<union> rename_clause Sel D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (C \<union> D) = rename_clause Sel C \<union> rename_clause Sel D
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {L. \<exists>LL. LL \<in> C \<union> D \<and> L = rename_literal Sel LL} = {L. \<exists>LL. LL \<in> C \<and> L = rename_literal Sel LL} \<union> {L. \<exists>LL. LL \<in> D \<and> L = rename_literal Sel LL}
[PROOF STEP]
by auto


[STATEMENT]
lemma renaming_set_minus_subset :
  "rename_clause Sel (C - { L }) \<subseteq> rename_clause Sel C - {rename_literal Sel L }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (C - {L}) \<subseteq> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
assume "x \<in> rename_clause Sel (C - { L })"
[PROOF STATE]
proof (state)
this:
x \<in> rename_clause Sel (C - {L})

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> rename_clause Sel (C - {L})
[PROOF STEP]
obtain y where "y \<in> C - { L }" and "x = rename_literal Sel y"
[PROOF STATE]
proof (prove)
using this:
x \<in> rename_clause Sel (C - {L})

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> C - {L}; x = rename_literal Sel y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {La. \<exists>LL. LL \<in> C - {L} \<and> La = rename_literal Sel LL}

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

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
from \<open>y \<in> C - { L }\<close> and \<open>x = rename_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> C - {L}
x = rename_literal Sel y
[PROOF STEP]
have "x \<in> rename_clause Sel C"
[PROOF STATE]
proof (prove)
using this:
y \<in> C - {L}
x = rename_literal Sel y

goal (1 subgoal):
 1. x \<in> rename_clause Sel C
[PROOF STEP]
unfolding rename_clause_def
[PROOF STATE]
proof (prove)
using this:
y \<in> C - {L}
x = rename_literal Sel y

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

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
have "x \<noteq> rename_literal Sel L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> rename_literal Sel L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = rename_literal Sel L \<Longrightarrow> False
[PROOF STEP]
assume "x = rename_literal Sel L"
[PROOF STATE]
proof (state)
this:
x = rename_literal Sel L

goal (1 subgoal):
 1. x = rename_literal Sel L \<Longrightarrow> False
[PROOF STEP]
hence "rename_literal Sel x = L"
[PROOF STATE]
proof (prove)
using this:
x = rename_literal Sel L

goal (1 subgoal):
 1. rename_literal Sel x = L
[PROOF STEP]
using inverse_renaming
[PROOF STATE]
proof (prove)
using this:
x = rename_literal Sel L
rename_literal ?A (rename_literal ?A ?L) = ?L

goal (1 subgoal):
 1. rename_literal Sel x = L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel x = L

goal (1 subgoal):
 1. x = rename_literal Sel L \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x = rename_literal Sel y\<close>
[PROOF STATE]
proof (chain)
picking this:
rename_literal Sel x = L
x = rename_literal Sel y
[PROOF STEP]
have "y = L"
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel x = L
x = rename_literal Sel y

goal (1 subgoal):
 1. y = L
[PROOF STEP]
using inverse_renaming
[PROOF STATE]
proof (prove)
using this:
rename_literal Sel x = L
x = rename_literal Sel y
rename_literal ?A (rename_literal ?A ?L) = ?L

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

goal (1 subgoal):
 1. x = rename_literal Sel L \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> C - { L }\<close>
[PROOF STATE]
proof (chain)
picking this:
y = L
y \<in> C - {L}
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
y = L
y \<in> C - {L}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<noteq> rename_literal Sel L

goal (1 subgoal):
 1. \<And>x. x \<in> rename_clause Sel (C - {L}) \<Longrightarrow> x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
from \<open>x \<noteq> rename_literal Sel L\<close> and \<open>x \<in> rename_clause Sel C\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> rename_literal Sel L
x \<in> rename_clause Sel C
[PROOF STEP]
show "x \<in> (rename_clause Sel C) - {rename_literal Sel L }"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> rename_literal Sel L
x \<in> rename_clause Sel C

goal (1 subgoal):
 1. x \<in> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> rename_clause Sel C - {rename_literal Sel L}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_set_minus : "rename_clause Sel (C - { L })
  = (rename_clause Sel C) - {rename_literal Sel L }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (C - {L}) = rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rename_clause Sel (C - {L}) \<subseteq> rename_clause Sel C - {rename_literal Sel L}
 2. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
show "rename_clause Sel (C - { L }) \<subseteq>  (rename_clause Sel C) - {rename_literal Sel L }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (C - {L}) \<subseteq> rename_clause Sel C - {rename_literal Sel L}
[PROOF STEP]
using renaming_set_minus_subset
[PROOF STATE]
proof (prove)
using this:
rename_clause ?Sel (?C - {?L}) \<subseteq> rename_clause ?Sel ?C - {rename_literal ?Sel ?L}

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

goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
show "(rename_clause Sel C) - {rename_literal Sel L } \<subseteq> rename_clause Sel (C - { L })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
have "rename_clause Sel ( (rename_clause Sel C) - { (rename_literal Sel L) })
      \<subseteq>  (rename_clause Sel (rename_clause Sel C)) - {rename_literal Sel (rename_literal Sel L) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> rename_clause Sel (rename_clause Sel C) - {rename_literal Sel (rename_literal Sel L)}
[PROOF STEP]
using renaming_set_minus_subset
[PROOF STATE]
proof (prove)
using this:
rename_clause ?Sel (?C - {?L}) \<subseteq> rename_clause ?Sel ?C - {rename_literal ?Sel ?L}

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

goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> rename_clause Sel (rename_clause Sel C) - {rename_literal Sel (rename_literal Sel L)}
[PROOF STEP]
have "rename_clause Sel ( (rename_clause Sel C) - { (rename_literal Sel L) }) \<subseteq>  (C - {L })"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> rename_clause Sel (rename_clause Sel C) - {rename_literal Sel (rename_literal Sel L)}

goal (1 subgoal):
 1. rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> C - {L}
[PROOF STEP]
using inverse_renaming inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> rename_clause Sel (rename_clause Sel C) - {rename_literal Sel (rename_literal Sel L)}
rename_literal ?A (rename_literal ?A ?L) = ?L
rename_clause ?A (rename_clause ?A ?L) = ?L

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

goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> C - {L}
[PROOF STEP]
have "rename_clause Sel (rename_clause Sel ( (rename_clause Sel C) - { (rename_literal Sel L) }))
            \<subseteq>  (rename_clause Sel (C - {L }))"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> C - {L}

goal (1 subgoal):
 1. rename_clause Sel (rename_clause Sel (rename_clause Sel C - {rename_literal Sel L})) \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
using rename_clause_def
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel C - {rename_literal Sel L}) \<subseteq> C - {L}
rename_clause ?A ?C = {L. \<exists>LL. LL \<in> ?C \<and> L = rename_literal ?A LL}

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

goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
rename_clause Sel (rename_clause Sel (rename_clause Sel C - {rename_literal Sel L})) \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
show "(rename_clause Sel C) - { (rename_literal Sel L) } \<subseteq>  rename_clause Sel (C - {L })"
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel (rename_clause Sel C - {rename_literal Sel L})) \<subseteq> rename_clause Sel (C - {L})

goal (1 subgoal):
 1. rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})
[PROOF STEP]
using inverse_renaming inverse_clause_renaming
[PROOF STATE]
proof (prove)
using this:
rename_clause Sel (rename_clause Sel (rename_clause Sel C - {rename_literal Sel L})) \<subseteq> rename_clause Sel (C - {L})
rename_literal ?A (rename_literal ?A ?L) = ?L
rename_clause ?A (rename_clause ?A ?L) = ?L

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rename_clause Sel C - {rename_literal Sel L} \<subseteq> rename_clause Sel (C - {L})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renaming_preserves_semantic :
  assumes "validate_literal I L"
  shows "validate_literal (rename_interpretation Sel I) (rename_literal Sel L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
let ?J = "rename_interpretation Sel I"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[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. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from \<open>L = Pos A \<or> L = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos A \<or> L = Neg A
[PROOF STEP]
have "atom L = A"
[PROOF STATE]
proof (prove)
using this:
L = Pos A \<or> L = Neg A

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

goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
assume "A \<in> Sel"
[PROOF STATE]
proof (state)
this:
A \<in> Sel

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>atom L = A\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> Sel
atom L = A
[PROOF STEP]
have "rename_literal Sel L = complement L"
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel
atom L = A

goal (1 subgoal):
 1. rename_literal Sel L = complement L
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<in> Sel
atom L = A

goal (1 subgoal):
 1. (if atom L \<in> Sel then complement L else L) = complement L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel L = complement L

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
assume "L = Pos A"
[PROOF STATE]
proof (state)
this:
L = Pos A

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>validate_literal I L\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos A
I \<Turnstile> L
[PROOF STEP]
have "A \<in> I"
[PROOF STATE]
proof (prove)
using this:
L = Pos A
I \<Turnstile> L

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>A \<in> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> I
A \<in> Sel
[PROOF STEP]
have "A \<notin> ?J"
[PROOF STATE]
proof (prove)
using this:
A \<in> I
A \<in> Sel

goal (1 subgoal):
 1. A \<notin> rename_interpretation Sel I
[PROOF STEP]
unfolding rename_interpretation_def
[PROOF STATE]
proof (prove)
using this:
A \<in> I
A \<in> Sel

goal (1 subgoal):
 1. A \<notin> {A \<in> I. A \<notin> Sel} \<union> {A. A \<notin> I \<and> A \<in> Sel}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<notin> rename_interpretation Sel I

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Pos A\<close> and \<open>rename_literal Sel L = complement L\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> rename_interpretation Sel I
L = Pos A
rename_literal Sel L = complement L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<notin> rename_interpretation Sel I
L = Pos A
rename_literal Sel L = complement 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. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
assume "L \<noteq> Pos A"
[PROOF STATE]
proof (state)
this:
L \<noteq> Pos A

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Pos A \<or> L = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<noteq> Pos A
L = Pos A \<or> L = Neg A
[PROOF STEP]
have "L = Neg A"
[PROOF STATE]
proof (prove)
using this:
L \<noteq> Pos A
L = Pos A \<or> L = Neg A

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

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>validate_literal I L\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Neg A
I \<Turnstile> L
[PROOF STEP]
have "A \<notin> I"
[PROOF STATE]
proof (prove)
using this:
L = Neg A
I \<Turnstile> L

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

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>A \<in> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> I
A \<in> Sel
[PROOF STEP]
have "A \<in> ?J"
[PROOF STATE]
proof (prove)
using this:
A \<notin> I
A \<in> Sel

goal (1 subgoal):
 1. A \<in> rename_interpretation Sel I
[PROOF STEP]
unfolding rename_interpretation_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> I
A \<in> Sel

goal (1 subgoal):
 1. A \<in> {A \<in> I. A \<notin> Sel} \<union> {A. A \<notin> I \<and> A \<in> Sel}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<in> rename_interpretation Sel I

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Neg A\<close> and \<open>rename_literal Sel L = complement L\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> rename_interpretation Sel I
L = Neg A
rename_literal Sel L = complement L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> rename_interpretation Sel I
L = Neg A
rename_literal Sel L = complement 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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L

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

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>atom L = A\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> Sel
atom L = A
[PROOF STEP]
have "rename_literal Sel L = L"
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
atom L = A

goal (1 subgoal):
 1. rename_literal Sel L = L
[PROOF STEP]
unfolding rename_literal_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> Sel
atom L = A

goal (1 subgoal):
 1. (if atom L \<in> Sel then complement L else L) = L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rename_literal Sel L = L

goal (1 subgoal):
 1. A \<notin> Sel \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
assume "L = Pos A"
[PROOF STATE]
proof (state)
this:
L = Pos A

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>validate_literal I L\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos A
I \<Turnstile> L
[PROOF STEP]
have "A \<in> I"
[PROOF STATE]
proof (prove)
using this:
L = Pos A
I \<Turnstile> L

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>A \<notin> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> I
A \<notin> Sel
[PROOF STEP]
have "A \<in> ?J"
[PROOF STATE]
proof (prove)
using this:
A \<in> I
A \<notin> Sel

goal (1 subgoal):
 1. A \<in> rename_interpretation Sel I
[PROOF STEP]
unfolding rename_interpretation_def
[PROOF STATE]
proof (prove)
using this:
A \<in> I
A \<notin> Sel

goal (1 subgoal):
 1. A \<in> {A \<in> I. A \<notin> Sel} \<union> {A. A \<notin> I \<and> A \<in> Sel}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<in> rename_interpretation Sel I

goal (2 subgoals):
 1. ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
 2. \<not> ?P \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Pos A\<close> and \<open>rename_literal Sel L = L\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> rename_interpretation Sel I
L = Pos A
rename_literal Sel L = L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> rename_interpretation Sel I
L = Pos A
rename_literal Sel L = 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. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
assume "L \<noteq> Pos A"
[PROOF STATE]
proof (state)
this:
L \<noteq> Pos A

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Pos A \<or> L = Neg A\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<noteq> Pos A
L = Pos A \<or> L = Neg A
[PROOF STEP]
have "L = Neg A"
[PROOF STATE]
proof (prove)
using this:
L \<noteq> Pos A
L = Pos A \<or> L = Neg A

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

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>validate_literal I L\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Neg A
I \<Turnstile> L
[PROOF STEP]
have "A \<notin> I"
[PROOF STATE]
proof (prove)
using this:
L = Neg A
I \<Turnstile> L

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

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>A \<notin> Sel\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> I
A \<notin> Sel
[PROOF STEP]
have "A \<notin> ?J"
[PROOF STATE]
proof (prove)
using this:
A \<notin> I
A \<notin> Sel

goal (1 subgoal):
 1. A \<notin> rename_interpretation Sel I
[PROOF STEP]
unfolding rename_interpretation_def
[PROOF STATE]
proof (prove)
using this:
A \<notin> I
A \<notin> Sel

goal (1 subgoal):
 1. A \<notin> {A \<in> I. A \<notin> Sel} \<union> {A. A \<notin> I \<and> A \<in> Sel}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<notin> rename_interpretation Sel I

goal (1 subgoal):
 1. L \<noteq> Pos A \<Longrightarrow> rename_interpretation Sel I \<Turnstile> rename_literal Sel L
[PROOF STEP]
from this and \<open>L = Neg A\<close> and \<open>rename_literal Sel L = L\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<notin> rename_interpretation Sel I
L = Neg A
rename_literal Sel L = L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<notin> rename_interpretation Sel I
L = Neg A
rename_literal Sel L = 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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rename_interpretation Sel I \<Turnstile> rename_literal Sel L

goal:
No subgoals!
[PROOF STEP]
qed