[STATEMENT]
lemma orient_lit_semantics_replacement :
  assumes "fo_interpretation I"
  assumes "orient_lit_inst l u v polarity \<theta>"
  assumes "validate_ground_lit I (subst_lit l \<sigma>)"
  assumes "I (subst u \<sigma>) (subst u' \<sigma>)"
  shows "validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst l u v polarity \<theta>
[PROOF STEP]
obtain e where "l = Pos e \<or> l = Neg e" and "e = Eq u v \<or> e = Eq v u"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst l u v polarity \<theta>

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>l = Pos e \<or> l = Neg e; e = Eq u v \<or> e = Eq v u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(l = Pos (Eq u v) \<or> l = Pos (Eq v u)) \<and> (u \<lhd> \<theta>, v \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = pos \<or> (l = Neg (Eq u v) \<or> l = Neg (Eq v u)) \<and> (u \<lhd> \<theta>, v \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = neg

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>l = Pos e \<or> l = Neg e; e = Eq u v \<or> e = Eq v u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = Pos e \<or> l = Neg e
e = Eq u v \<or> e = Eq v u

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<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 blast
[PROOF STATE]
proof (state)
this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<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. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
 2. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
assume "polarity = pos"
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
 2. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and assms(1) and assms(2) and \<open>validate_ground_lit I (subst_lit l \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)
[PROOF STEP]
have
      "I (subst u \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)

goal (1 subgoal):
 1. I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
using orient_lit_semantics_pos
[PROOF STATE]
proof (prove)
using this:
polarity = pos
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)
\<lbrakk>fo_interpretation ?I; orient_lit_inst ?l ?u ?v pos ?\<eta>; validate_ground_lit ?I (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> ?I (?u \<lhd> ?\<sigma>) (?v \<lhd> ?\<sigma>)

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
 2. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and assms(1) and \<open>I (subst u \<sigma>) (subst u' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
fo_interpretation I
I (u \<lhd> \<sigma>) (u' \<lhd> \<sigma>)
[PROOF STEP]
have "I (subst u' \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
fo_interpretation I
I (u \<lhd> \<sigma>) (u' \<lhd> \<sigma>)

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

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 (2 subgoals):
 1. polarity = pos \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
 2. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and \<open>polarity = pos\<close>
[PROOF STATE]
proof (chain)
picking this:
I (u' \<lhd> \<sigma>) (v \<lhd> \<sigma>)
polarity = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I (u' \<lhd> \<sigma>) (v \<lhd> \<sigma>)
polarity = pos

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and assms(1) and assms(2) and \<open>validate_ground_lit I (subst_lit l \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)
[PROOF STEP]
have
      "\<not>I (subst u \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)

goal (1 subgoal):
 1. \<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
using orient_lit_semantics_neg
[PROOF STATE]
proof (prove)
using this:
polarity = neg
fo_interpretation I
orient_lit_inst l u v polarity \<theta>
validate_ground_lit I (subst_lit l \<sigma>)
\<lbrakk>fo_interpretation ?I; orient_lit_inst ?l ?u ?v neg ?\<theta>; validate_ground_lit ?I (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> \<not> ?I (?u \<lhd> ?\<sigma>) (?v \<lhd> ?\<sigma>)

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 (1 subgoal):
 1. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and assms(1) and \<open>I (subst u \<sigma>) (subst u' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
fo_interpretation I
I (u \<lhd> \<sigma>) (u' \<lhd> \<sigma>)
[PROOF STEP]
have "\<not>I (subst u' \<sigma>) (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
fo_interpretation I
I (u \<lhd> \<sigma>) (u' \<lhd> \<sigma>)

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 transitive_def
[PROOF STATE]
proof (prove)
using this:
\<not> I (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)
(reflexive I \<and> (\<forall>y z. I y z = I z y) \<and> (\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u)) \<and> compatible_with_structure I
I (u \<lhd> \<sigma>) (u' \<lhd> \<sigma>)

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 (1 subgoal):
 1. polarity = neg \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
from this and \<open>polarity = neg\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> I (u' \<lhd> \<sigma>) (v \<lhd> \<sigma>)
polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> I (u' \<lhd> \<sigma>) (v \<lhd> \<sigma>)
polarity = neg

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_ground_lit I (subst_lit (mk_lit polarity (Eq u' v)) \<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_factorization_is_sound :
  assumes "finite (cl_ecl C)"
  assumes "factorization 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]
assume "\<not> clause_entails_clause (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
          (subst_cl (cl_ecl D) \<theta>)"
[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 (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)" and
      "\<not> (validate_clause I (subst_cl (cl_ecl D) \<theta>))" and "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:
factorization C D \<sigma> k C'
[PROOF STEP]
obtain L1 L2 L' t s u v where
      "orient_lit_inst L1 t s pos \<sigma>" and "orient_lit_inst L2 u v pos \<sigma>" and "ck_unifier t u \<sigma> k"
      and "L' = Neg (Eq s v)"
      and "(?D =  (subst_cl ( (?C - { L2 }) \<union> { L' } )) \<sigma>)"
      and "L1 \<noteq> L2"
      and "L1 \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
factorization C D \<sigma> k C'

goal (1 subgoal):
 1. (\<And>L1 t s L2 u v L'. \<lbrakk>orient_lit_inst L1 t s pos \<sigma>; orient_lit_inst L2 u v pos \<sigma>; ck_unifier t u \<sigma> k; L' = Neg (Eq s v); cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>; L1 \<noteq> L2; L1 \<in> cl_ecl C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using factorization_def
[PROOF STATE]
proof (prove)
using this:
factorization C D \<sigma> k C'
factorization ?P ?C ?\<sigma> ?k ?C' = (\<exists>L1 L2 L' t s u v Cl_P Cl_C trms_C. eligible_literal L1 ?P ?\<sigma> \<and> L1 \<in> cl_ecl ?P \<and> L2 \<in> cl_ecl ?P - {L1} \<and> Cl_C = cl_ecl ?C \<and> Cl_P = cl_ecl ?P \<and> orient_lit_inst L1 t s pos ?\<sigma> \<and> orient_lit_inst L2 u v pos ?\<sigma> \<and> t \<lhd> ?\<sigma> \<noteq> s \<lhd> ?\<sigma> \<and> t \<lhd> ?\<sigma> \<noteq> v \<lhd> ?\<sigma> \<and> ck_unifier t u ?\<sigma> ?k \<and> L' = Neg (Eq s v) \<and> (?C = Ecl Cl_C trms_C \<and> trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl ?P \<union> proper_subterms_of t) ?\<sigma>)) ?k) \<and> Cl_C = subst_cl ?C' ?\<sigma> \<and> ?C' = Cl_P - {L2} \<union> {L'})

goal (1 subgoal):
 1. (\<And>L1 t s L2 u v L'. \<lbrakk>orient_lit_inst L1 t s pos \<sigma>; orient_lit_inst L2 u v pos \<sigma>; ck_unifier t u \<sigma> k; L' = Neg (Eq s v); cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>; L1 \<noteq> L2; L1 \<in> cl_ecl C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst L1 t s pos \<sigma>
orient_lit_inst L2 u v pos \<sigma>
ck_unifier t u \<sigma> k
L' = Neg (Eq s v)
cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>
L1 \<noteq> L2
L1 \<in> cl_ecl C

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]
from \<open>\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
have "\<not> validate_ground_clause I (subst_cl ?D \<theta>)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
using assms(3) substs_preserve_ground_clause validate_clause.elims(3)
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (subst_cl (cl_ecl D) \<theta>)
ground_clause (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. \<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> 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 \<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>\<not> validate_ground_clause I (subst_cl ?D \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
have "\<not> validate_ground_clause I (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl D) \<theta> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
\<not> validate_ground_clause I (subst_cl (cl_ecl D) \<theta>)

goal (1 subgoal):
 1. \<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> 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>(?D =  (subst_cl ( (?C - { L2 }) \<union> { L' } )) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>
[PROOF STEP]
have "(subst_lit L' \<sigma>) \<in> ?D"
[PROOF STATE]
proof (prove)
using this:
cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>

goal (1 subgoal):
 1. subst_lit L' \<sigma> \<in> cl_ecl D
[PROOF STEP]
by auto
[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]
then
[PROOF STATE]
proof (chain)
picking this:
subst_lit L' \<sigma> \<in> cl_ecl D
[PROOF STEP]
have
    "(subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta>)
      \<in> (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit L' \<sigma> \<in> cl_ecl D

goal (1 subgoal):
 1. subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<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>\<not> validate_ground_clause I (subst_cl (subst_cl ?D \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
[PROOF STEP]
have "\<not>validate_ground_lit I (subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)

goal (1 subgoal):
 1. \<not> validate_ground_lit I (subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_lit I (subst_lit (subst_lit (subst_lit L' \<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]
from this and \<open>L'= Neg (Eq s v)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_ground_lit I (subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta>)
L' = Neg (Eq s v)
[PROOF STEP]
have
    "I (subst (subst (subst s \<sigma>) \<theta>) \<eta>)
       (subst (subst (subst v \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_ground_lit I (subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta>)
L' = Neg (Eq s v)

goal (1 subgoal):
 1. I (s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>) (v \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I (s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>) (v \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<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
[PROOF STATE]
proof (chain)
picking this:
I (s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>) (v \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>)
[PROOF STEP]
have "I (subst s ?\<sigma>') (subst v ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>) (v \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>)

goal (1 subgoal):
 1. I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<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 - { L2 }) \<union> { L' } )) \<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 - {L2} \<union> {L'}) \<sigma>
l \<in> cl_ecl C
[PROOF STEP]
have "l = L2"
[PROOF STATE]
proof (prove)
using this:
subst_lit l \<sigma> \<notin> cl_ecl D
cl_ecl D = subst_cl (cl_ecl C - {L2} \<union> {L'}) \<sigma>
l \<in> cl_ecl C

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

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

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

goal (1 subgoal):
 1. t \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> = u \<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> = u \<lhd> \<sigma>
[PROOF STEP]
have "subst (subst (subst t \<sigma>) \<theta>) \<eta> =
      subst (subst (subst u \<sigma>) \<theta>) \<eta>"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u \<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> = u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
have "(subst t ?\<sigma>') = subst u ?\<sigma>'"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>

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

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

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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>fo_interpretation I\<close> and \<open>l = L2\<close> and \<open>orient_lit_inst L2 u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I
l = L2
orient_lit_inst L2 u v pos \<sigma>
[PROOF STEP]
have "I (subst u ?\<sigma>') (subst v ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I
l = L2
orient_lit_inst L2 u v pos \<sigma>

goal (1 subgoal):
 1. I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
using orient_lit_semantics_pos
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit I (subst_lit l (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
fo_interpretation I
l = L2
orient_lit_inst L2 u v pos \<sigma>
\<lbrakk>fo_interpretation ?I; orient_lit_inst ?l ?u ?v pos ?\<eta>; validate_ground_lit ?I (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> ?I (?u \<lhd> ?\<sigma>) (?v \<lhd> ?\<sigma>)

goal (1 subgoal):
 1. I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<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> and \<open>I (subst s ?\<sigma>') (subst v ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
fo_interpretation I
I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "I (subst u ?\<sigma>') (subst s ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
fo_interpretation I
I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

goal (1 subgoal):
 1. I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I (u \<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>(subst t ?\<sigma>') = subst u ?\<sigma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "I (subst t ?\<sigma>') (subst s ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I (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
[PROOF STATE]
proof (chain)
picking this:
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "validate_ground_eq I (subst_equation (Eq t s) ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
unfolding fo_interpretation_def congruence_def equivalence_relation_def
        symmetric_def
[PROOF STATE]
proof (prove)
using this:
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
(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 (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I (s \<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
[PROOF STATE]
proof (chain)
picking this:
I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "validate_ground_eq I (subst_equation (Eq s t) ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. subst_lit l \<sigma> \<notin> cl_ecl D \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_lit L1 \<sigma> \<in> cl_ecl D
[PROOF STEP]
have
      "(subst_lit (subst_lit (subst_lit L1 \<sigma>) \<theta>) \<eta>)
        \<in> (subst_cl (subst_cl ?D \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit L1 \<sigma> \<in> cl_ecl D

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

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

goal (1 subgoal):
 1. subst_lit L1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
using composition_of_substs_lit
[PROOF STATE]
proof (prove)
using this:
subst_lit (subst_lit (subst_lit L1 \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
subst_lit (subst_lit ?l ?\<sigma>) ?\<eta> = subst_lit ?l (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_lit L1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
subst_lit L1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>

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

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 this and \<open>\<not> validate_ground_clause I (subst_cl (subst_cl ?D \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma factorization_is_sound :
  assumes "finite (cl_ecl C)"
  assumes "factorization 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)
factorization 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)
factorization C D \<sigma> k C'

goal (1 subgoal):
 1. validate_clause I (subst_cl (cl_ecl D) \<theta>)
[PROOF STEP]
using ground_factorization_is_sound
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl C) \<sigma>) \<theta>)
finite (cl_ecl C)
factorization C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); factorization ?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)
factorization C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); factorization ?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)
factorization C D \<sigma> k C'
\<lbrakk>finite (cl_ecl ?C); factorization ?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