[STATEMENT]
lemma trm_rep_preserves_lit_semantics:
  assumes "fo_interpretation I"
  assumes "(I (subst t1 \<sigma>) (subst t2 \<sigma>))"
  assumes "orient_lit_inst L t1 s polarity \<sigma>'"
  assumes "\<not>(validate_ground_lit I (subst_lit L \<sigma>))"
  shows "\<not>validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
[PROOF STEP]
have "transitive I" and "symmetric I"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I

goal (1 subgoal):
 1. transitive I &&& symmetric I
[PROOF STEP]
unfolding
    fo_interpretation_def congruence_def equivalence_relation_def
[PROOF STATE]
proof (prove)
using this:
(reflexive I \<and> symmetric I \<and> transitive I) \<and> compatible_with_structure I

goal (1 subgoal):
 1. transitive I &&& symmetric I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
transitive I
symmetric I

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
have "polarity = pos \<or> polarity = neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polarity = pos \<or> polarity = neg
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. polarity = pos \<or> polarity = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "polarity = pos"
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
[PROOF STEP]
have mk: "(mk_lit polarity (Eq t2 s)) = (Pos (Eq t2 s))"
[PROOF STATE]
proof (prove)
using this:
polarity = pos

goal (1 subgoal):
 1. mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from \<open>polarity = pos\<close> and assms(3)
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L t1 s polarity \<sigma>'
[PROOF STEP]
have "L = (Pos (Eq t1 s)) \<or> L = (Pos (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L t1 s polarity \<sigma>'

goal (1 subgoal):
 1. L = Pos (Eq t1 s) \<or> L = Pos (Eq s t1)
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
polarity = pos
(L = Pos (Eq t1 s) \<or> L = Pos (Eq s t1)) \<and> (t1 \<lhd> \<sigma>', s \<lhd> \<sigma>') \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t1 s) \<or> L = Neg (Eq s t1)) \<and> (t1 \<lhd> \<sigma>', s \<lhd> \<sigma>') \<notin> trm_ord \<and> polarity = neg

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t1 s) \<or> L = Pos (Eq s t1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t1 s) \<or> L = Pos (Eq s t1)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Pos (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "L = (Pos (Eq t1 s))"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t1 s)

goal (2 subgoals):
 1. L = Pos (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(4)
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t1 s)
\<not> validate_ground_lit I (subst_lit L \<sigma>)
[PROOF STEP]
have "\<not>I (subst t1 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t1 s)
\<not> validate_ground_lit I (subst_lit L \<sigma>)

goal (1 subgoal):
 1. \<not> I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (2 subgoals):
 1. L = Pos (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(2) and \<open>transitive I\<close> and \<open>symmetric I\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I
[PROOF STEP]
have "\<not>I (subst t2 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<not> I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I

goal (1 subgoal):
 1. \<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
unfolding transitive_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
\<not> I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u
\<forall>y z. I y z = I z y

goal (1 subgoal):
 1. \<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (2 subgoals):
 1. L = Pos (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and mk
[PROOF STATE]
proof (chain)
picking this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal (1 subgoal):
 1. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "L = (Pos (Eq s t1))"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq s t1)

goal (1 subgoal):
 1. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(4)
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq s t1)
\<not> validate_ground_lit I (subst_lit L \<sigma>)
[PROOF STEP]
have "\<not>I (subst s \<sigma>) (subst t1 \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq s t1)
\<not> validate_ground_lit I (subst_lit L \<sigma>)

goal (1 subgoal):
 1. \<not> I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)

goal (1 subgoal):
 1. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(2) and \<open>transitive I\<close> and \<open>symmetric I\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I
[PROOF STEP]
have "\<not>I (subst t2 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<not> I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I

goal (1 subgoal):
 1. \<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
unfolding transitive_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
\<not> I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u
\<forall>y z. I y z = I z y

goal (1 subgoal):
 1. \<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. L = Pos (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and mk
[PROOF STATE]
proof (chain)
picking this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Pos (Eq t2 s)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "polarity = neg"
[PROOF STATE]
proof (state)
this:
polarity = neg

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
[PROOF STEP]
have mk: "(mk_lit polarity (Eq t2 s)) = (Neg (Eq t2 s))"
[PROOF STATE]
proof (prove)
using this:
polarity = neg

goal (1 subgoal):
 1. mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from \<open>polarity = neg\<close> and assms(3)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L t1 s polarity \<sigma>'
[PROOF STEP]
have "L = (Neg (Eq t1 s)) \<or> L = (Neg (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L t1 s polarity \<sigma>'

goal (1 subgoal):
 1. L = Neg (Eq t1 s) \<or> L = Neg (Eq s t1)
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
polarity = neg
(L = Pos (Eq t1 s) \<or> L = Pos (Eq s t1)) \<and> (t1 \<lhd> \<sigma>', s \<lhd> \<sigma>') \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t1 s) \<or> L = Neg (Eq s t1)) \<and> (t1 \<lhd> \<sigma>', s \<lhd> \<sigma>') \<notin> trm_ord \<and> polarity = neg

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t1 s) \<or> L = Neg (Eq s t1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t1 s) \<or> L = Neg (Eq s t1)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Neg (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "L = (Neg (Eq t1 s))"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t1 s)

goal (2 subgoals):
 1. L = Neg (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(4)
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t1 s)
\<not> validate_ground_lit I (subst_lit L \<sigma>)
[PROOF STEP]
have "I (subst t1 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t1 s)
\<not> validate_ground_lit I (subst_lit L \<sigma>)

goal (1 subgoal):
 1. I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (2 subgoals):
 1. L = Neg (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(2) and \<open>transitive I\<close> and \<open>symmetric I\<close>
[PROOF STATE]
proof (chain)
picking this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I
[PROOF STEP]
have "I (subst t2 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
unfolding transitive_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u
\<forall>y z. I y z = I z y

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (2 subgoals):
 1. L = Neg (Eq t1 s) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
 2. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and mk
[PROOF STATE]
proof (chain)
picking this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal (1 subgoal):
 1. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
assume "L = (Neg (Eq s t1))"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq s t1)

goal (1 subgoal):
 1. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(4)
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq s t1)
\<not> validate_ground_lit I (subst_lit L \<sigma>)
[PROOF STEP]
have "I (subst s \<sigma>) (subst t1 \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq s t1)
\<not> validate_ground_lit I (subst_lit L \<sigma>)

goal (1 subgoal):
 1. I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)

goal (1 subgoal):
 1. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and assms(2) and \<open>transitive I\<close> and \<open>symmetric I\<close>
[PROOF STATE]
proof (chain)
picking this:
I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I
[PROOF STEP]
have "I (subst t2 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
unfolding transitive_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma>) (t1 \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u
\<forall>y z. I y z = I z y

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. L = Neg (Eq s t1) \<Longrightarrow> \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
from this and mk
[PROOF STATE]
proof (chain)
picking this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
mk_lit polarity (Eq t2 s) = Neg (Eq t2 s)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t2 s)) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterms_dominated :
  assumes "maximal_literal L C"
  assumes "orient_lit L t s p"
  assumes "u \<in> subterms_of_cl C"
  assumes "vars_of_lit L = {}"
  assumes "vars_of_cl C = {}"
  shows "u = t \<or> (u,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = t \<or> (u, t) \<in> trm_ord
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
assume neg_h: "\<not>(u = t \<or> (u,t) \<in> trm_ord)"
[PROOF STATE]
proof (state)
this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from assms(5) and assms(3)
[PROOF STATE]
proof (chain)
picking this:
vars_of_cl C = {}
u \<in> subterms_of_cl C
[PROOF STEP]
have "vars_of u = {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_cl C = {}
u \<in> subterms_of_cl C

goal (1 subgoal):
 1. vars_of u = {}
[PROOF STEP]
using subterm_vars
[PROOF STATE]
proof (prove)
using this:
vars_of_cl C = {}
u \<in> subterms_of_cl C
?u \<in> subterms_of_cl ?C \<Longrightarrow> vars_of ?u \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of u = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of u = {}

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from \<open>vars_of_lit L = {}\<close> and \<open>orient_lit L t s p\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = {}
orient_lit L t s p
[PROOF STEP]
have "vars_of s = {}" and "vars_of t = {}"
    and "\<not>(t,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = {}
orient_lit L t s p

goal (1 subgoal):
 1. vars_of s = {} &&& vars_of t = {} &&& (t, s) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = {}
(L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t, s) \<notin> trm_ord \<and> p = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t, s) \<notin> trm_ord \<and> p = neg

goal (1 subgoal):
 1. vars_of s = {} &&& vars_of t = {} &&& (t, s) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of s = {}
vars_of t = {}
(t, s) \<notin> trm_ord

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of_cl C
[PROOF STEP]
obtain L' where "u \<in> subterms_of_lit L'" and "L' \<in> C"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of_cl C

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

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from assms(5) and \<open>L' \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_cl C = {}
L' \<in> C
[PROOF STEP]
have "vars_of_lit L' = {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_cl C = {}
L' \<in> C

goal (1 subgoal):
 1. vars_of_lit L' = {}
[PROOF STEP]
using vars_of_cl.simps
[PROOF STATE]
proof (prove)
using this:
vars_of_cl C = {}
L' \<in> C
vars_of_cl ?C = {x. \<exists>L. x \<in> vars_of_lit L \<and> L \<in> ?C}

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

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from \<open>u \<in> subterms_of_lit L'\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of_lit L'
[PROOF STEP]
obtain t' s' p' where "orient_lit L' t' s' p'"
    and "u \<in> subterms_of t' \<union> subterms_of s'"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of_lit L'

goal (1 subgoal):
 1. (\<And>t' s' p'. \<lbrakk>orient_lit L' t' s' p'; u \<in> subterms_of t' \<union> subterms_of s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of_lit L'

goal (1 subgoal):
 1. (\<And>t' s' p'. \<lbrakk>(L' = Pos (Eq t' s') \<or> L' = Pos (Eq s' t')) \<and> (t', s') \<notin> trm_ord \<and> p' = pos \<or> (L' = Neg (Eq t' s') \<or> L' = Neg (Eq s' t')) \<and> (t', s') \<notin> trm_ord \<and> p' = neg; u \<in> subterms_of t' \<union> subterms_of s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Un_commute mset_lit.cases subterms_of_eq.simps subterms_of_lit.simps(1)
          subterms_of_lit.simps(2) trm_ord_wf wf_asym)
[PROOF STATE]
proof (state)
this:
orient_lit L' t' s' p'
u \<in> subterms_of t' \<union> subterms_of s'

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
from \<open>u \<in> subterms_of t' \<union> subterms_of s'\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of t' \<union> subterms_of s'
[PROOF STEP]
have "u \<in> subterms_of t' \<or> u \<in> subterms_of s'"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of t' \<union> subterms_of s'

goal (1 subgoal):
 1. u \<in> subterms_of t' \<or> u \<in> subterms_of s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of t' \<or> u \<in> subterms_of s'

goal (1 subgoal):
 1. \<not> (u = t \<or> (u, t) \<in> trm_ord) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of t' \<or> u \<in> subterms_of s'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of t' \<or> u \<in> subterms_of s'

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
assume "u \<in> subterms_of t'"
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of t'

goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of t'
[PROOF STEP]
have "u = t' \<or> (u,t') \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of t'

goal (1 subgoal):
 1. u = t' \<or> (u, t') \<in> trm_ord
[PROOF STEP]
using subterms_of_trm_ord_eq [of u t']
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of t'
u \<in> subterms_of t' \<Longrightarrow> u = t' \<or> (u, t') \<in> trm_ord

goal (1 subgoal):
 1. u = t' \<or> (u, t') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = t' \<or> (u, t') \<in> trm_ord

goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from neg_h and \<open>vars_of u = {}\<close> and  \<open>vars_of t = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
[PROOF STEP]
have "(t,u) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t, u) \<in> trm_ord

goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>u = t' \<or> (u,t') \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t, u) \<in> trm_ord
u = t' \<or> (u, t') \<in> trm_ord
[PROOF STEP]
have "(t,t') \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = t' \<or> (u, t') \<in> trm_ord

goal (1 subgoal):
 1. (t, t') \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = t' \<or> (u, t') \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (t, t') \<in> trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = t' \<or> (u, t') \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

goal (1 subgoal):
 1. (t, t') \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(t, t') \<in> trm_ord

goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit L' = {}\<close>  and assms(4) and
        \<open>orient_lit L t s p\<close> and \<open>orient_lit L' t' s' p'\<close>
[PROOF STATE]
proof (chain)
picking this:
(t, t') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'
[PROOF STEP]
have "(L,L') \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(t, t') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'

goal (1 subgoal):
 1. (L, L') \<in> lit_ord
[PROOF STEP]
using lit_ord_dominating_term
[PROOF STATE]
proof (prove)
using this:
(t, t') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'
\<lbrakk>(?s1.0, ?s2.0) \<in> trm_ord \<or> (?s1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s1.0 ?t1.0 ?p1.0; orient_lit ?x2.0 ?s2.0 ?t2.0 ?p2.0; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

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

goal (2 subgoals):
 1. u \<in> subterms_of t' \<Longrightarrow> False
 2. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and assms(1) and \<open>L' \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
(L, L') \<in> lit_ord
maximal_literal L C
L' \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(L, L') \<in> lit_ord
maximal_literal L C
L' \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
(L, L') \<in> lit_ord
\<forall>x. x \<in> C \<longrightarrow> (L, x) \<notin> lit_ord
L' \<in> C

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

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
assume "u \<in> subterms_of s'"
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of s'

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of s'
[PROOF STEP]
have "u = s' \<or> (u,s') \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of s'

goal (1 subgoal):
 1. u = s' \<or> (u, s') \<in> trm_ord
[PROOF STEP]
using subterms_of_trm_ord_eq [of u s']
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of s'
u \<in> subterms_of s' \<Longrightarrow> u = s' \<or> (u, s') \<in> trm_ord

goal (1 subgoal):
 1. u = s' \<or> (u, s') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = s' \<or> (u, s') \<in> trm_ord

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from neg_h and \<open>vars_of u = {}\<close> and  \<open>vars_of t = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
[PROOF STEP]
have "(t,u) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
\<not> (u = t \<or> (u, t) \<in> trm_ord)
vars_of u = {}
vars_of t = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (t, u) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t, u) \<in> trm_ord

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>u = s' \<or> (u,s') \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t, u) \<in> trm_ord
u = s' \<or> (u, s') \<in> trm_ord
[PROOF STEP]
have "(t,s') \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = s' \<or> (u, s') \<in> trm_ord

goal (1 subgoal):
 1. (t, s') \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = s' \<or> (u, s') \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (t, s') \<in> trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(t, u) \<in> trm_ord
u = s' \<or> (u, s') \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

goal (1 subgoal):
 1. (t, s') \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(t, s') \<in> trm_ord

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit L' = {}\<close>  and assms(4) and
        \<open>orient_lit L t s p\<close> and \<open>orient_lit L' t' s' p'\<close>
[PROOF STATE]
proof (chain)
picking this:
(t, s') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'
[PROOF STEP]
have "(L,L') \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(t, s') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'

goal (1 subgoal):
 1. (L, L') \<in> lit_ord
[PROOF STEP]
using lit_ord_dominating_term
[PROOF STATE]
proof (prove)
using this:
(t, s') \<in> trm_ord
vars_of_lit L' = {}
vars_of_lit L = {}
orient_lit L t s p
orient_lit L' t' s' p'
\<lbrakk>(?s1.0, ?s2.0) \<in> trm_ord \<or> (?s1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s1.0 ?t1.0 ?p1.0; orient_lit ?x2.0 ?s2.0 ?t2.0 ?p2.0; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

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

goal (1 subgoal):
 1. u \<in> subterms_of s' \<Longrightarrow> False
[PROOF STEP]
from this and assms(1) and \<open>L' \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
(L, L') \<in> lit_ord
maximal_literal L C
L' \<in> C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(L, L') \<in> lit_ord
maximal_literal L C
L' \<in> C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
(L, L') \<in> lit_ord
\<forall>x. x \<in> C \<longrightarrow> (L, x) \<notin> lit_ord
L' \<in> C

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ck_unifier_thm:
  assumes "ck_unifier t s \<sigma> k"
  shows "(subst t \<sigma>) = (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
by (metis assms min_IMGU_def IMGU_iff_Idem_and_MGU MGU_is_Unifier ck_unifier_def Unifier_def)


[STATEMENT]
lemma subst_preserve_ck_unifier:
  assumes "ck_unifier t s \<sigma> k"
  shows "ck_unifier t s (comp \<sigma> \<eta>) Ground"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
let ?\<sigma>' = "(comp \<sigma> \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
ck_unifier t s \<sigma> k
[PROOF STEP]
have "(subst t \<sigma>) = (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
ck_unifier t s \<sigma> k

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
using ck_unifier_thm
[PROOF STATE]
proof (prove)
using this:
ck_unifier t s \<sigma> k
ck_unifier ?t ?s ?\<sigma> ?k \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?s \<lhd> ?\<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
have "(subst t ?\<sigma>') = (subst s ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>

goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>

goal (1 subgoal):
 1. ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground
[PROOF STEP]
unfolding ck_unifier_def Unifier_def
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>

goal (1 subgoal):
 1. if Ground = FirstOrder then min_IMGU (\<sigma> \<lozenge> \<eta>) t s else t \<lhd> \<sigma> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ck_unifier t s (\<sigma> \<lozenge> \<eta>) Ground

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_trm_lemma:
  assumes "dom_trm t C"
  shows "\<exists> u. (u \<in> (subterms_of_cl C) \<and> (u = t \<or> (t,u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
from   assms(1)
[PROOF STATE]
proof (chain)
picking this:
dom_trm t C
[PROOF STEP]
obtain L u v p where
    "L \<in> C" "decompose_literal L u v p" "(u = t \<or> (t,u) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
dom_trm t C

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> C; decompose_literal L u v p; u = t \<or> (t, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> C \<and> decompose_literal L u v p \<and> (p = neg \<and> t = u \<or> (t, u) \<in> trm_ord)

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> C; decompose_literal L u v p; u = t \<or> (t, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L \<in> C
decompose_literal L u v p
u = t \<or> (t, u) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
from \<open>decompose_literal L u v p\<close>
[PROOF STATE]
proof (chain)
picking this:
decompose_literal L u v p
[PROOF STEP]
have "u \<in> subterms_of_lit L"
[PROOF STATE]
proof (prove)
using this:
decompose_literal L u v p

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
unfolding decompose_literal_def decompose_equation_def
[PROOF STATE]
proof (prove)
using this:
\<exists>e. p = pos \<and> L = Pos e \<and> (e = Eq u v \<or> e = Eq v u) \<or> p = neg \<and> L = Neg e \<and> (e = Eq u v \<or> e = Eq v u)

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
using root_subterm
[PROOF STATE]
proof (prove)
using this:
\<exists>e. p = pos \<and> L = Pos e \<and> (e = Eq u v \<or> e = Eq v u) \<or> p = neg \<and> L = Neg e \<and> (e = Eq u v \<or> e = Eq v u)
?t \<in> subterms_of ?t

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

goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
from this and \<open>L \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of_lit L
L \<in> C
[PROOF STEP]
have "u \<in> (subterms_of_cl C)"
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of_lit L
L \<in> C

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

goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
from this and \<open>(u = t \<or> (t,u) \<in> trm_ord)\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> subterms_of_cl C
u = t \<or> (t, u) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> subterms_of_cl C
u = t \<or> (t, u) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in> subterms_of_cl C \<and> (u = t \<or> (t, u) \<in> trm_ord)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_trms_subset:
  shows "(dom_trms C E ) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_trms C E \<subseteq> E
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> E. dom_trm x C} \<subseteq> E
[PROOF STEP]
by auto


[STATEMENT]
lemma dom_trm_vars:
  assumes "dom_trm t C"
  shows "vars_of t \<subseteq> vars_of_cl C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dom_trm t C
[PROOF STEP]
obtain L u v p where "L \<in> C" "decompose_literal L u v p" "t = u \<or> (t,u) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
dom_trm t C

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> C; decompose_literal L u v p; t = u \<or> (t, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> C \<and> decompose_literal L u v p \<and> (p = neg \<and> t = u \<or> (t, u) \<in> trm_ord)

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> C; decompose_literal L u v p; t = u \<or> (t, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> C
decompose_literal L u v p
t = u \<or> (t, u) \<in> trm_ord

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
from \<open>t = u \<or> (t,u) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t = u \<or> (t, u) \<in> trm_ord
[PROOF STEP]
have "vars_of t \<subseteq> vars_of u"
[PROOF STATE]
proof (prove)
using this:
t = u \<or> (t, u) \<in> trm_ord

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of u
[PROOF STEP]
using trm_ord_vars
[PROOF STATE]
proof (prove)
using this:
t = u \<or> (t, u) \<in> trm_ord
(?t, ?s) \<in> trm_ord \<Longrightarrow> vars_of ?t \<subseteq> vars_of ?s

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of u

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
from this and \<open>decompose_literal L u v p\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of u
decompose_literal L u v p
[PROOF STEP]
have "vars_of t \<subseteq> vars_of_lit L"
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of u
decompose_literal L u v p

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L
[PROOF STEP]
using decompose_literal_vars
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of u
decompose_literal L u v p
decompose_literal ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl C
[PROOF STEP]
using \<open>L \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L
L \<in> C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derivable_premisses:
  assumes "derivable C P S \<sigma> k C'"
  shows "P \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> S
[PROOF STEP]
using assms derivable_def
[PROOF STATE]
proof (prove)
using this:
derivable C P S \<sigma> k C'
derivable ?C ?P ?S ?\<sigma> ?k ?C' = ((\<exists>P1 P2. P1 \<in> ?S \<and> P2 \<in> ?S \<and> ?P = {P1, P2} \<and> superposition P1 P2 ?C ?\<sigma> ?k ?C') \<or> (\<exists>P1. P1 \<in> ?S \<and> ?P = {P1} \<and> factorization P1 ?C ?\<sigma> ?k ?C') \<or> (\<exists>P1. P1 \<in> ?S \<and> ?P = {P1} \<and> reflexion P1 ?C ?\<sigma> ?k ?C'))

goal (1 subgoal):
 1. P \<subseteq> S
[PROOF STEP]
by auto


[STATEMENT]
lemma cannot_validate_contradictary_literals :
  assumes "l = Neg (Eq t t)"
  assumes "fo_interpretation I"
  shows "\<not> (validate_ground_lit I l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> validate_ground_lit I l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> validate_ground_lit I l
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
[PROOF STEP]
have "congruence I"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I

goal (1 subgoal):
 1. congruence I
[PROOF STEP]
unfolding fo_interpretation_def
[PROOF STATE]
proof (prove)
using this:
congruence I

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

goal (1 subgoal):
 1. \<not> validate_ground_lit I l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
congruence I
[PROOF STEP]
have "I t t"
[PROOF STATE]
proof (prove)
using this:
congruence I

goal (1 subgoal):
 1. I t t
[PROOF STEP]
unfolding congruence_def reflexive_def equivalence_relation_def
[PROOF STATE]
proof (prove)
using this:
((\<forall>y. I y y) \<and> symmetric I \<and> transitive I) \<and> compatible_with_structure I

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

goal (1 subgoal):
 1. \<not> validate_ground_lit I l
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
I t t
l = Neg (Eq t t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I t t
l = Neg (Eq t t)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_reflexion_is_sound :
  assumes "finite (cl_ecl C)"
  assumes "reflexion C D \<sigma> k C'"
  assumes "(ground_clause (subst_cl (cl_ecl D) \<theta>))"
  shows "clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
          (subst_cl (cl_ecl D) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?C = "(cl_ecl C)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?D = "(cl_ecl D)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?C' = "(subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?D' = "(subst_cl (cl_ecl D) \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (clause_entails_clause ?C' ?D')"
[PROOF STATE]
proof (state)
this:
\<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
obtain I where "validate_clause I ?C'" and "\<not> (validate_clause I ?D')" "fo_interpretation I"
[PROOF STATE]
proof (prove)
using this:
\<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>); \<not> validate_clause I (subst_cl (cl_ecl D) \<theta>); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding clause_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<longrightarrow> validate_clause I (subst_cl (cl_ecl D) \<theta>))

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>); \<not> validate_clause I (subst_cl (cl_ecl D) \<theta>); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)
fo_interpretation I

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
reflexion C D \<sigma> k C'
[PROOF STEP]
obtain L1 t s where
    "?D = (subst_cl (?C - { L1 }) \<sigma>)"
    and "orient_lit_inst L1 t s neg \<sigma>" and "ck_unifier t s \<sigma> k"
[PROOF STATE]
proof (prove)
using this:
reflexion C D \<sigma> k C'

goal (1 subgoal):
 1. (\<And>L1 t s. \<lbrakk>cl_ecl D = subst_cl (cl_ecl C - {L1}) \<sigma>; orient_lit_inst L1 t s neg \<sigma>; ck_unifier t s \<sigma> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reflexion_def [of C D \<sigma> k]
[PROOF STATE]
proof (prove)
using this:
reflexion C D \<sigma> k C'
reflexion C D \<sigma> k ?C' = (\<exists>L1 t s Cl_P Cl_C trms_C. eligible_literal L1 C \<sigma> \<and> L1 \<in> cl_ecl C \<and> Cl_C = cl_ecl D \<and> Cl_P = cl_ecl C \<and> orient_lit_inst L1 t s neg \<sigma> \<and> ck_unifier t s \<sigma> k \<and> D = Ecl Cl_C trms_C \<and> trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl C \<union> {t}) \<sigma>)) k \<and> Cl_C = subst_cl ?C' \<sigma> \<and> ?C' = Cl_P - {L1})

goal (1 subgoal):
 1. (\<And>L1 t s. \<lbrakk>cl_ecl D = subst_cl (cl_ecl C - {L1}) \<sigma>; orient_lit_inst L1 t s neg \<sigma>; ck_unifier t s \<sigma> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl D = subst_cl (cl_ecl C - {L1}) \<sigma>
orient_lit_inst L1 t s neg \<sigma>
ck_unifier t s \<sigma> k

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl C)
[PROOF STEP]
have "finite (subst_cl (subst_cl ?C \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl C)

goal (1 subgoal):
 1. finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
[PROOF STEP]
obtain \<eta> where i: "ground_clause (subst_cl
        (subst_cl (subst_cl ?C \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)

goal (1 subgoal):
 1. (\<And>\<eta>. ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ground_instance_exists [of "(subst_cl (subst_cl ?C \<sigma>) \<theta>)"]
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<Longrightarrow> \<exists>\<sigma>'. ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<sigma>')

goal (1 subgoal):
 1. (\<And>\<eta>. ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?CC = "(subst_cl (subst_cl (subst_cl ?C \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?\<sigma>'' = "comp \<sigma> \<theta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?\<sigma>' = "comp ?\<sigma>'' \<eta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
have "?CC = (subst_cl (subst_cl ?C ?\<sigma>'') \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>
[PROOF STEP]
using composition_of_substs_cl [of ?C]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (cl_ecl C) ?\<sigma>) ?\<eta> = subst_cl (cl_ecl C) (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>
[PROOF STEP]
have "?CC = (subst_cl ?C ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>

goal (1 subgoal):
 1. subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
using composition_of_substs_cl [of ?C]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta>)) \<eta>
subst_cl (subst_cl (cl_ecl C) ?\<sigma>) ?\<eta> = subst_cl (cl_ecl C) (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
[PROOF STEP]
have "validate_ground_clause I ?CC"
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)

goal (1 subgoal):
 1. validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
using i validate_clause.simps
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)
validate_clause ?I ?C = (\<forall>s. ground_clause (subst_cl ?C s) \<longrightarrow> validate_ground_clause ?I (subst_cl ?C s))

goal (1 subgoal):
 1. validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
obtain l' where "l' \<in> ?CC" and "validate_ground_lit I l'"
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>)

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<in> subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>; validate_ground_lit I l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<in> subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>
validate_ground_lit I l'

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>l' \<in> ?CC\<close> and \<open>?CC = (subst_cl ?C ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
l' \<in> subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
obtain l where
    "l \<in> ?C" and "l' = (subst_lit l ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
l' \<in> subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<in> cl_ecl C; l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subst_cl.simps
[PROOF STATE]
proof (prove)
using this:
l' \<in> subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl C) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
subst_cl ?C ?s = {L. \<exists>L'. L' \<in> ?C \<and> L = subst_lit L' ?s}

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<in> cl_ecl C; l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> cl_ecl C
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
have "subst_lit l \<sigma> \<in> ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_lit l \<sigma> \<in> cl_ecl D
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
assume "subst_lit l \<sigma> \<notin> ?D"
[PROOF STATE]
proof (state)
this:
subst_lit l \<sigma> \<notin> cl_ecl D

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>?D = (subst_cl (?C - { L1 }) \<sigma>)\<close> and \<open>l \<in> ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit l \<sigma> \<notin> cl_ecl D
cl_ecl D = subst_cl (cl_ecl C - {L1}) \<sigma>
l \<in> cl_ecl C
[PROOF STEP]
have "l = L1"
[PROOF STATE]
proof (prove)
using this:
subst_lit l \<sigma> \<notin> cl_ecl D
cl_ecl D = subst_cl (cl_ecl C - {L1}) \<sigma>
l \<in> cl_ecl C

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

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>orient_lit_inst L1 t s neg \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
l = L1
orient_lit_inst L1 t s neg \<sigma>
[PROOF STEP]
have "l = (Neg (Eq t s)) \<or> l = (Neg (Eq s t))"
[PROOF STATE]
proof (prove)
using this:
l = L1
orient_lit_inst L1 t s neg \<sigma>

goal (1 subgoal):
 1. l = Neg (Eq t s) \<or> l = Neg (Eq s t)
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
l = L1
(L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> neg = pos \<or> (L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> neg = neg

goal (1 subgoal):
 1. l = Neg (Eq t s) \<or> l = Neg (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Neg (Eq t s) \<or> l = Neg (Eq s t)

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from \<open>ck_unifier t s \<sigma> k\<close>
[PROOF STATE]
proof (chain)
picking this:
ck_unifier t s \<sigma> k
[PROOF STEP]
have "subst t \<sigma> = subst s \<sigma>"
[PROOF STATE]
proof (prove)
using this:
ck_unifier t s \<sigma> k

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
using ck_unifier_thm
[PROOF STATE]
proof (prove)
using this:
ck_unifier t s \<sigma> k
ck_unifier ?t ?s ?\<sigma> ?k \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?s \<lhd> ?\<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
have "subst (subst (subst t \<sigma>) \<theta>) \<eta> =
      subst (subst (subst s \<sigma>) \<theta>) \<eta>"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
have "(subst t ?\<sigma>') = subst s ?\<sigma>'"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>l = (Neg (Eq t s)) \<or> l = (Neg (Eq s t))\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
l = Neg (Eq t s) \<or> l = Neg (Eq s t)
[PROOF STEP]
have "(subst_lit l ?\<sigma>') = (Neg (Eq (subst t ?\<sigma>') (subst t ?\<sigma>')))"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
l = Neg (Eq t s) \<or> l = Neg (Eq s t)

goal (1 subgoal):
 1. subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>fo_interpretation I\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I
[PROOF STEP]
have "\<not> (validate_ground_lit I (subst_lit l ?\<sigma>'))"
[PROOF STATE]
proof (prove)
using this:
subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
[PROOF STEP]
using cannot_validate_contradictary_literals [of "(subst_lit l ?\<sigma>')" "(subst t ?\<sigma>')" I]
[PROOF STATE]
proof (prove)
using this:
subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I
\<lbrakk>subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) = Neg (Eq (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)); fo_interpretation I\<rbrakk> \<Longrightarrow> \<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
from this and \<open>l' = subst_lit l ?\<sigma>'\<close> and \<open>validate_ground_lit I l'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
validate_ground_lit I l'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
validate_ground_lit I 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:
subst_lit l \<sigma> \<in> cl_ecl D

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>subst_lit l \<sigma> \<in> ?D\<close> and \<open>l' = subst_lit l ?\<sigma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit l \<sigma> \<in> cl_ecl D
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "l' \<in> (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit l \<sigma> \<in> cl_ecl D
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. l' \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
using subst_cl.simps composition_of_substs_lit mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
subst_lit l \<sigma> \<in> cl_ecl D
l' = subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
subst_cl ?C ?s = {L. \<exists>L'. L' \<in> ?C \<and> L = subst_lit L' ?s}
subst_lit (subst_lit ?l ?\<sigma>) ?\<eta> = subst_lit ?l (?\<sigma> \<lozenge> ?\<eta>)
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. l' \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
l' \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validate_ground_lit I l'\<close>
[PROOF STATE]
proof (chain)
picking this:
l' \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
validate_ground_lit I l'
[PROOF STEP]
have
    "validate_ground_clause I (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
l' \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
validate_ground_lit I l'

goal (1 subgoal):
 1. validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_clause (subst_cl ?D \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
have
    "(subst_cl ?D \<theta>) = (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
using substs_preserve_ground_clause [of "(subst_cl ?D \<theta>)"  \<eta>]
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl D) \<theta>)
ground_clause (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta> = subst_cl (cl_ecl D) \<theta>

goal (1 subgoal):
 1. subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validate_ground_clause I (subst_cl (subst_cl ?D \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
[PROOF STEP]
have "validate_ground_clause I (subst_cl ?D \<theta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)

goal (1 subgoal):
 1. validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>) (subst_cl (cl_ecl D) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) and \<open>\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause (subst_cl (cl_ecl D) \<theta>)
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause (subst_cl (cl_ecl D) \<theta>)
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. False
[PROOF STEP]
using substs_preserve_ground_clause validate_clause.elims(3)
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause (subst_cl (cl_ecl D) \<theta>)
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause ?C \<Longrightarrow> subst_cl ?C ?\<sigma> = ?C
\<lbrakk>\<not> validate_clause ?x ?xa; \<And>I C. \<lbrakk>?x = I; ?xa = C; \<not> (\<forall>s. ground_clause (subst_cl C s) \<longrightarrow> validate_ground_clause I (subst_cl C s))\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflexion_is_sound :
  assumes "finite (cl_ecl C)"
  assumes "reflexion C D \<sigma> k C'"
  shows "clause_entails_clause (cl_ecl C) (cl_ecl D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clause_entails_clause (cl_ecl C) (cl_ecl D)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
let ?C = "(cl_ecl C)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
let ?D = "(cl_ecl D)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (clause_entails_clause ?C ?D)"
[PROOF STATE]
proof (state)
this:
\<not> clause_entails_clause (cl_ecl C) (cl_ecl D)

goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> clause_entails_clause (cl_ecl C) (cl_ecl D)
[PROOF STEP]
obtain I where "validate_clause I ?C" and "\<not> (validate_clause I ?D)" "fo_interpretation I"
[PROOF STATE]
proof (prove)
using this:
\<not> clause_entails_clause (cl_ecl C) (cl_ecl D)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (cl_ecl C); \<not> validate_clause I (cl_ecl D); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding clause_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (cl_ecl C) \<longrightarrow> validate_clause I (cl_ecl D))

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (cl_ecl C); \<not> validate_clause I (cl_ecl D); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl D)
fo_interpretation I

goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not> (validate_clause I ?D)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause I (cl_ecl D)
[PROOF STEP]
obtain \<theta>
    where D_false: "\<not> (validate_ground_clause I (subst_cl ?D \<theta>))"
      and "(ground_clause (subst_cl ?D \<theta>))"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (cl_ecl D)

goal (1 subgoal):
 1. (\<And>\<theta>. \<lbrakk>\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>); ground_clause (subst_cl (cl_ecl D) \<theta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
have  "validate_clause I (subst_cl (subst_cl ?C \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
[PROOF STEP]
using \<open>validate_clause I (cl_ecl C)\<close> instances_are_entailed
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
validate_clause ?I ?C \<Longrightarrow> validate_clause ?I (subst_cl ?C ?\<sigma>)

goal (1 subgoal):
 1. validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from this and assms(1) and assms(2)
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
reflexion C D \<sigma> k C'
[PROOF STEP]
have "validate_clause I (subst_cl ?D \<theta>)"
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
reflexion C D \<sigma> k C'

goal (1 subgoal):
 1. validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
using ground_reflexion_is_sound
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
reflexion C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); reflexion ?C ?D ?\<sigma> ?k ?C'; ground_clause (subst_cl (cl_ecl ?D) ?\<theta>)\<rbrakk> \<Longrightarrow> clause_entails_clause (subst_cl (subst_cl (cl_ecl ?C) ?\<sigma>) ?\<theta>) (subst_cl (cl_ecl ?D) ?\<theta>)

goal (1 subgoal):
 1. validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
unfolding clause_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
reflexion C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); reflexion ?C ?D ?\<sigma> ?k ?C'; ground_clause (subst_cl (cl_ecl ?D) ?\<theta>)\<rbrakk> \<Longrightarrow> \<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (subst_cl (subst_cl (cl_ecl ?C) ?\<sigma>) ?\<theta>) \<longrightarrow> validate_clause I (subst_cl (cl_ecl ?D) ?\<theta>)

goal (1 subgoal):
 1. validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
using \<open>fo_interpretation I\<close> \<open>ground_clause (subst_cl (cl_ecl D) \<theta>)\<close>
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
reflexion C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); reflexion ?C ?D ?\<sigma> ?k ?C'; ground_clause (subst_cl (cl_ecl ?D) ?\<theta>)\<rbrakk> \<Longrightarrow> \<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (subst_cl (subst_cl (cl_ecl ?C) ?\<sigma>) ?\<theta>) \<longrightarrow> validate_clause I (subst_cl (cl_ecl ?D) ?\<theta>)
fo_interpretation I
ground_clause (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
validate_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> clause_entails_clause (cl_ecl C) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from this and D_false
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (subst_cl (cl_ecl D) \<theta>)
\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (cl_ecl D) \<theta>)
\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>ground_clause (subst_cl (cl_ecl D) \<theta>)\<close>
    substs_preserve_ground_clause validate_clause.elims(1))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orient_lit_semantics_pos :
  assumes "fo_interpretation I"
  assumes "orient_lit_inst l u v pos \<eta>"
  assumes "validate_ground_lit I (subst_lit l \<sigma>)"
  shows "I (subst u \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
let ?u = "subst u \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
let ?v = "subst v \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst l u v pos \<eta>
[PROOF STEP]
have "l = (Pos (Eq u v)) \<or> l = (Pos (Eq v u))"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst l u v pos \<eta>

goal (1 subgoal):
 1. l = Pos (Eq u v) \<or> l = Pos (Eq v u)
[PROOF STEP]
using orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst l u v pos \<eta>
orient_lit_inst ?L ?u ?v ?s ?\<sigma> = ((?L = Pos (Eq ?u ?v) \<or> ?L = Pos (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = pos \<or> (?L = Neg (Eq ?u ?v) \<or> ?L = Neg (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = neg)

goal (1 subgoal):
 1. l = Pos (Eq u v) \<or> l = Pos (Eq v u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Pos (Eq u v) \<or> l = Pos (Eq v u)

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
l = Pos (Eq u v) \<or> l = Pos (Eq v u)
validate_ground_lit I (subst_lit l \<sigma>)
[PROOF STEP]
have "validate_ground_eq I (Eq ?u ?v) \<or> validate_ground_eq I (Eq ?v ?u)"
[PROOF STATE]
proof (prove)
using this:
l = Pos (Eq u v) \<or> l = Pos (Eq v u)
validate_ground_lit I (subst_lit l \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))
[PROOF STEP]
have "I ?u ?v \<or> I ?v ?u"
[PROOF STATE]
proof (prove)
using this:
validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from this and \<open>fo_interpretation I\<close>
[PROOF STATE]
proof (chain)
picking this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
fo_interpretation I
[PROOF STEP]
show "I ?u ?v"
[PROOF STATE]
proof (prove)
using this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
fo_interpretation I

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
unfolding fo_interpretation_def congruence_def equivalence_relation_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
(reflexive I \<and> (\<forall>y z. I y z = I z y) \<and> transitive I) \<and> compatible_with_structure I

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orient_lit_semantics_neg :
  assumes "fo_interpretation I"
  assumes "orient_lit_inst l u v neg \<theta>"
  assumes "validate_ground_lit I (subst_lit l \<sigma>)"
  shows "\<not>I (subst u \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
let ?u = "subst u \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
let ?v = "subst v \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst l u v neg \<theta>
[PROOF STEP]
have "l = (Neg (Eq u v)) \<or> l = (Neg (Eq v u))"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst l u v neg \<theta>

goal (1 subgoal):
 1. l = Neg (Eq u v) \<or> l = Neg (Eq v u)
[PROOF STEP]
using orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst l u v neg \<theta>
orient_lit_inst ?L ?u ?v ?s ?\<sigma> = ((?L = Pos (Eq ?u ?v) \<or> ?L = Pos (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = pos \<or> (?L = Neg (Eq ?u ?v) \<or> ?L = Neg (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = neg)

goal (1 subgoal):
 1. l = Neg (Eq u v) \<or> l = Neg (Eq v u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Neg (Eq u v) \<or> l = Neg (Eq v u)

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
l = Neg (Eq u v) \<or> l = Neg (Eq v u)
validate_ground_lit I (subst_lit l \<sigma>)
[PROOF STEP]
have "\<not>validate_ground_eq I (Eq ?u ?v) \<or> \<not>validate_ground_eq I (Eq ?v ?u)"
[PROOF STATE]
proof (prove)
using this:
l = Neg (Eq u v) \<or> l = Neg (Eq v u)
validate_ground_lit I (subst_lit l \<sigma>)

goal (1 subgoal):
 1. \<not> validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> \<not> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> \<not> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> \<not> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))
[PROOF STEP]
have "\<not>I ?u ?v \<or> \<not>I ?v ?u"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_ground_eq I (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> \<not> validate_ground_eq I (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> \<not> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> \<not> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
from this and \<open>fo_interpretation I\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> \<not> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
fo_interpretation I
[PROOF STEP]
show "\<not>I ?u ?v"
[PROOF STATE]
proof (prove)
using this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> \<not> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
fo_interpretation I

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
unfolding fo_interpretation_def congruence_def equivalence_relation_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) \<or> \<not> I (v \<lhd> \<sigma>) (u \<lhd> \<sigma>)
(reflexive I \<and> (\<forall>y z. I y z = I z y) \<and> transitive I) \<and> compatible_with_structure I

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed