[STATEMENT]
lemma conclusion_is_smaller_than_premisses:
  assumes "derivable C P S \<sigma> Ground C'"
  assumes "\<forall>x \<in> S. (finite (cl_ecl x))"
  assumes "grounding_set P \<sigma>"
  shows "\<exists> D. (D \<in> P \<and> (( (mset_cl (C',\<sigma>)), (mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
assume hyp: "\<not> (\<exists> D. (D \<in> P \<and> (( (mset_cl (C',\<sigma>)), (mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord)))))"
[PROOF STATE]
proof (state)
this:
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
derivable C P S \<sigma> Ground C'
[PROOF STEP]
have "P \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
derivable C P S \<sigma> Ground C'

goal (1 subgoal):
 1. P \<subseteq> S
[PROOF STEP]
unfolding derivable_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> Ground C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> Ground C')

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

goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
have not_sup: "\<not> (\<exists>P1 P2. (P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1 P2. (P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'
[PROOF STEP]
obtain P1 P2 where "P1 \<in> P" "P2 \<in> P" "superposition P1 P2 C \<sigma> Ground C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>P1 P2. \<lbrakk>P1 \<in> P; P2 \<in> P; superposition P1 P2 C \<sigma> Ground C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P1 \<in> P
P2 \<in> P
superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>superposition P1 P2 C \<sigma> Ground C'\<close>
[PROOF STATE]
proof (chain)
picking this:
superposition P1 P2 C \<sigma> Ground C'
[PROOF STEP]
obtain L t s u v M  L' polarity u' p t' Cl_C NT where
      "M \<in> (cl_ecl P2)" "L \<in> (cl_ecl P1)"
      "orient_lit_inst M u v pos \<sigma>"
      "orient_lit_inst L t s polarity \<sigma>"
      "subterm t p u'"
      "ck_unifier u' u \<sigma> Ground"
      "replace_subterm t p v t'"
      "L' = mk_lit polarity (Eq t' s)"
      "(C = (Ecl Cl_C NT))"
      "(subst u \<sigma>) \<noteq> (subst v \<sigma>)"
      "( (subst_lit M \<sigma>),(subst_lit L \<sigma>))
            \<in> lit_ord"
      "strictly_maximal_literal P2 M \<sigma>"
      "Cl_C = (subst_cl (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } )) \<sigma>)"
      "C' = (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>M L u v t s polarity p u' t' L' Cl_C NT. \<lbrakk>M \<in> cl_ecl P2; L \<in> cl_ecl P1; orient_lit_inst M u v pos \<sigma>; orient_lit_inst L t s polarity \<sigma>; subterm t p u'; ck_unifier u' u \<sigma> Ground; replace_subterm t p v t'; L' = mk_lit polarity (Eq t' s); C = Ecl Cl_C NT; u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>; (subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord; strictly_maximal_literal P2 M \<sigma>; Cl_C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>; C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding superposition_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L t s u v M p Cl_P1 Cl_P2 Cl_C polarity t' u' L' trms_C. L \<in> Cl_P1 \<and> M \<in> Cl_P2 \<and> eligible_literal L P1 \<sigma> \<and> eligible_literal M P2 \<sigma> \<and> variable_disjoint P1 P2 \<and> Cl_P1 = cl_ecl P1 \<and> Cl_P2 = cl_ecl P2 \<and> \<not> is_a_variable u' \<and> allowed_redex u' P1 \<sigma> \<and> trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}) \<sigma>)) Ground \<and> C = Ecl Cl_C trms_C \<and> orient_lit_inst M u v pos \<sigma> \<and> orient_lit_inst L t s polarity \<sigma> \<and> u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma> \<and> subterm t p u' \<and> ck_unifier u' u \<sigma> Ground \<and> replace_subterm t p v t' \<and> (Ground = FirstOrder \<or> (subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord) \<and> (Ground = FirstOrder \<or> strictly_maximal_literal P2 M \<sigma>) \<and> L' = mk_lit polarity (Eq t' s) \<and> Cl_C = subst_cl C' \<sigma> \<and> C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})

goal (1 subgoal):
 1. (\<And>M L u v t s polarity p u' t' L' Cl_C NT. \<lbrakk>M \<in> cl_ecl P2; L \<in> cl_ecl P1; orient_lit_inst M u v pos \<sigma>; orient_lit_inst L t s polarity \<sigma>; subterm t p u'; ck_unifier u' u \<sigma> Ground; replace_subterm t p v t'; L' = mk_lit polarity (Eq t' s); C = Ecl Cl_C NT; u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>; (subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord; strictly_maximal_literal P2 M \<sigma>; Cl_C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>; C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M \<in> cl_ecl P2
L \<in> cl_ecl P1
orient_lit_inst M u v pos \<sigma>
orient_lit_inst L t s polarity \<sigma>
subterm t p u'
ck_unifier u' u \<sigma> Ground
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
C = Ecl Cl_C NT
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
(subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
strictly_maximal_literal P2 M \<sigma>
Cl_C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>P1 \<in> P\<close> and assms(2) and \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S
[PROOF STEP]
have "finite (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>P2 \<in> P\<close> and assms(2) and \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
P2 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S
[PROOF STEP]
have "finite (cl_ecl P2)"
[PROOF STATE]
proof (prove)
using this:
P2 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>P2 \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
grounding_set P \<sigma>
P2 \<in> P
[PROOF STEP]
have "ground_clause (subst_cl (cl_ecl P2) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
grounding_set P \<sigma>
P2 \<in> P

goal (1 subgoal):
 1. ground_clause (subst_cl (cl_ecl P2) \<sigma>)
[PROOF STEP]
unfolding grounding_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> ground_clause (subst_cl (cl_ecl x) \<sigma>)
P2 \<in> P

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl P2) \<sigma>)
[PROOF STEP]
have "vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl P2) \<sigma>)

goal (1 subgoal):
 1. vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> (cl_ecl P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> cl_ecl P2
[PROOF STEP]
have "(subst_lit M \<sigma>) \<in> (subst_cl (cl_ecl P2) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
M \<in> cl_ecl P2

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit M \<sigma> \<in> subst_cl (cl_ecl P2) \<sigma>
vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}
[PROOF STEP]
have "vars_of_lit (subst_lit M \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit M \<sigma> \<in> subst_cl (cl_ecl P2) \<sigma>
vars_of_cl (subst_cl (cl_ecl P2) \<sigma>) = {}

goal (1 subgoal):
 1. vars_of_lit (subst_lit M \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit (subst_lit M \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst M u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst M u v pos \<sigma>
[PROOF STEP]
have
      "orient_lit (subst_lit M \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M u v pos \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M u v pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit (subst_lit M \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst u \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit M \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos\<close>
      and \<open>vars_of_lit (subst_lit M \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst v \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit M \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (v \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit M \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
[PROOF STEP]
have "((subst u \<sigma>),(subst v \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit M \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit M \<sigma> = Pos (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> subst_lit M \<sigma> = Pos (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (subst_lit M \<sigma> = Neg (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> subst_lit M \<sigma> = Neg (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = neg

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst u \<sigma>) \<noteq> (subst v \<sigma>)\<close>
      and \<open>vars_of (subst u \<sigma>) = {}\<close> \<open>vars_of (subst v \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
have "((subst v \<sigma>),(subst u \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
\<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. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
\<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. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>P1 \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
grounding_set P \<sigma>
P1 \<in> P
[PROOF STEP]
have "ground_clause (subst_cl (cl_ecl P1) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
grounding_set P \<sigma>
P1 \<in> P

goal (1 subgoal):
 1. ground_clause (subst_cl (cl_ecl P1) \<sigma>)
[PROOF STEP]
unfolding grounding_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> ground_clause (subst_cl (cl_ecl x) \<sigma>)
P1 \<in> P

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl P1) \<sigma>)
[PROOF STEP]
have "vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl P1) \<sigma>)

goal (1 subgoal):
 1. vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in> (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> cl_ecl P1
[PROOF STEP]
have "(subst_lit L \<sigma>) \<in> (subst_cl (cl_ecl P1) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> cl_ecl P1

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}
[PROOF STEP]
have "vars_of_lit (subst_lit L \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}

goal (1 subgoal):
 1. vars_of_lit (subst_lit L \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit (subst_lit L \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst L t s polarity \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have
      "orient_lit (subst_lit L \<sigma>) (subst t \<sigma>) (subst s \<sigma>) polarity"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s polarity \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s polarity \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit (subst_lit L \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst t \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (t \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit L \<sigma>) (subst t \<sigma>) (subst s \<sigma>) polarity\<close>
       and \<open>vars_of_lit (subst_lit L \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst s \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (s \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC1 = "mset_ecl (P1, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC2 = "mset_ecl (C, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in> (cl_ecl P1)\<close> \<open>finite (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> cl_ecl P1
finite (cl_ecl P1)
[PROOF STEP]
have "mset_set (cl_ecl P1) = mset_set ((cl_ecl P1)-{ L }) + mset_set { L }"
[PROOF STATE]
proof (prove)
using this:
L \<in> cl_ecl P1
finite (cl_ecl P1)

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}
[PROOF STEP]
using split_mset_set [of "cl_ecl P1" "cl_ecl P1 - { L }" "{ L }"]
[PROOF STATE]
proof (prove)
using this:
L \<in> cl_ecl P1
finite (cl_ecl P1)
\<lbrakk>cl_ecl P1 = cl_ecl P1 - {L} \<union> {L}; (cl_ecl P1 - {L}) \<inter> {L} = {}; finite (cl_ecl P1 - {L}); finite {L}\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}
[PROOF STEP]
have  d1: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set (cl_ecl P1)) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L }) #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L}) + mset_set {L}
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C = "(((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } ))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close> \<open>finite (cl_ecl P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
finite (cl_ecl P2)
[PROOF STEP]
have "finite ?C"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P2)

goal (1 subgoal):
 1. finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C' = "?C - ( (cl_ecl P1) - { L })"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))
[PROOF STEP]
have "finite ?C'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))

goal (1 subgoal):
 1. finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "?C = ( (cl_ecl P1) - { L }) \<union> ?C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) = cl_ecl P1 - {L} \<union> (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) = cl_ecl P1 - {L} \<union> (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close> \<open>finite ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
have "mset_set ?C = mset_set ((cl_ecl P1)-{ L }) + mset_set ?C'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
using split_mset_set [of "?C" "cl_ecl P1 - { L }" "?C'"]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
\<lbrakk>cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) = cl_ecl P1 - {L} \<union> (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})); (cl_ecl P1 - {L}) \<inter> (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})) = {}; finite (cl_ecl P1 - {L}); finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
have  d2: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) = mset_set (cl_ecl P1 - {L}) + mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L }) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#} \<noteq> {#}

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?K = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?J = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L }) #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "(\<forall>k \<in> set_mset ?K. \<exists>j \<in> set_mset ?J. (k, j) \<in> (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
assume "k \<in> set_mset ?K"
[PROOF STATE]
proof (state)
this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
have "k \<in># ?K"
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
obtain M' where "M' \<in># (mset_set ?C')" and "k = (mset_lit (subst_lit M' \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>M' \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})); k = mset_lit (subst_lit M' \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using image_mset_thm [of "?K"  "\<lambda>x. (mset_lit (subst_lit x \<sigma>))" "(mset_set ?C')"]
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
\<lbrakk>{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}; ?x \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}\<rbrakk> \<Longrightarrow> \<exists>y. y \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})) \<and> ?x = mset_lit (subst_lit y \<sigma>)

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>M' \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})); k = mset_lit (subst_lit M' \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
M' \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
k = mset_lit (subst_lit M' \<sigma>)

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>M' \<in># (mset_set ?C')\<close>and \<open>finite ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
[PROOF STEP]
have "M' \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
M' \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))

goal (1 subgoal):
 1. M' \<in> cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M' \<in> cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "L \<in># (mset_set { L })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<in># mset_set {L}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in># mset_set {L}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L \<in># mset_set {L}
[PROOF STEP]
have "(mset_lit (subst_lit L \<sigma>) \<in># ?J)"
[PROOF STATE]
proof (prove)
using this:
L \<in># mset_set {L}

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
[PROOF STEP]
have "(mset_lit (subst_lit L \<sigma>) \<in> set_mset ?J)"
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L }) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#} \<noteq> {#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
show "\<exists>j \<in> set_mset ?J. (k, j) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
 2. \<not> ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
assume "M' \<in> (cl_ecl P2) - { M }"
[PROOF STATE]
proof (state)
this:
M' \<in> cl_ecl P2 - {M}

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
 2. \<not> ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this and \<open>strictly_maximal_literal P2 M \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<in> cl_ecl P2 - {M}
strictly_maximal_literal P2 M \<sigma>
[PROOF STEP]
have "((subst_lit M' \<sigma>),(subst_lit M \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
M' \<in> cl_ecl P2 - {M}
strictly_maximal_literal P2 M \<sigma>

goal (1 subgoal):
 1. (subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
unfolding strictly_maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
M' \<in> cl_ecl P2 - {M}
\<forall>x\<in>cl_ecl P2 - {M}. (subst_lit x \<sigma>, subst_lit M \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
 2. \<not> ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this and \<open>( (subst_lit M \<sigma>),(subst_lit L \<sigma>)) \<in> lit_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
(subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "((subst_lit M' \<sigma>),(subst_lit L \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
(subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit M' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
using lit_ord_trans
[PROOF STATE]
proof (prove)
using this:
(subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
(subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
trans lit_ord

goal (1 subgoal):
 1. (subst_lit M' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit M' \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
(subst_lit M \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
\<forall>x y z. (x, y) \<in> lit_ord \<longrightarrow> (y, z) \<in> lit_ord \<longrightarrow> (x, z) \<in> lit_ord

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
 2. \<not> ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(subst_lit M' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "((mset_lit (subst_lit M' \<sigma>)),
                (mset_lit (subst_lit L \<sigma>))) \<in>  (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(subst_lit M' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit M' \<sigma>, subst_lit L \<sigma>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

goal (1 subgoal):
 1. (mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
 2. \<not> ?P \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>(mset_lit (subst_lit L \<sigma>) \<in> set_mset ?J)\<close> this \<open>((mset_lit (subst_lit M' \<sigma>)),
                (mset_lit (subst_lit L \<sigma>))) \<in>  (mult trm_ord)\<close>
       and \<open>k = (mset_lit (subst_lit M' \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
(mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
(mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
k = mset_lit (subst_lit M' \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
(mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
(mset_lit (subst_lit M' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
k = mset_lit (subst_lit M' \<sigma>)

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
assume "M' \<notin> (cl_ecl P2) - { M }"
[PROOF STATE]
proof (state)
this:
M' \<notin> cl_ecl P2 - {M}

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this and \<open>M' \<in> ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<notin> cl_ecl P2 - {M}
M' \<in> cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})
[PROOF STEP]
have "M' = L'"
[PROOF STATE]
proof (prove)
using this:
M' \<notin> cl_ecl P2 - {M}
M' \<in> cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L})

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

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>subterm t p u'\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t p u'
[PROOF STEP]
have "subterm (subst t \<sigma>) p  (subst u' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subterm t p u'

goal (1 subgoal):
 1. subterm (t \<lhd> \<sigma>) p (u' \<lhd> \<sigma>)
[PROOF STEP]
using substs_preserve_subterms
[PROOF STATE]
proof (prove)
using this:
subterm t p u'
subterm ?t ?p ?s \<Longrightarrow> subterm (?t \<lhd> ?\<sigma>) ?p (?s \<lhd> ?\<sigma>)

goal (1 subgoal):
 1. subterm (t \<lhd> \<sigma>) p (u' \<lhd> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subterm (t \<lhd> \<sigma>) p (u' \<lhd> \<sigma>)

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>ck_unifier u' u \<sigma> Ground\<close>
[PROOF STATE]
proof (chain)
picking this:
ck_unifier u' u \<sigma> Ground
[PROOF STEP]
have
      "(subst u \<sigma>) = (subst u' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
ck_unifier u' u \<sigma> Ground

goal (1 subgoal):
 1. u \<lhd> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
unfolding ck_unifier_def Unifier_def
[PROOF STATE]
proof (prove)
using this:
if Ground = FirstOrder then min_IMGU \<sigma> u' u else u' \<lhd> \<sigma> = u \<lhd> \<sigma>

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

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this and \<open>((subst v \<sigma>),(subst u \<sigma>)) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<lhd> \<sigma> = u' \<lhd> \<sigma>
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "((subst v \<sigma>),(subst u' \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<sigma> = u' \<lhd> \<sigma>
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

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

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this \<open>subterm t p u'\<close> \<open>replace_subterm t p v t'\<close>
[PROOF STATE]
proof (chain)
picking this:
(v \<lhd> \<sigma>, u' \<lhd> \<sigma>) \<in> trm_ord
subterm t p u'
replace_subterm t p v t'
[PROOF STEP]
have "((subst t' \<sigma>),(subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u' \<lhd> \<sigma>) \<in> trm_ord
subterm t p u'
replace_subterm t p v t'

goal (1 subgoal):
 1. (t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using replacement_monotonic
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u' \<lhd> \<sigma>) \<in> trm_ord
subterm t p u'
replace_subterm t p v t'
\<lbrakk>(?v \<lhd> ?\<sigma>, ?u \<lhd> ?\<sigma>) \<in> trm_ord; subterm ?t ?p ?u; replace_subterm ?t ?p ?v ?s\<rbrakk> \<Longrightarrow> (?s \<lhd> ?\<sigma>, ?t \<lhd> ?\<sigma>) \<in> trm_ord

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

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[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. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
have "((subst_lit L' \<sigma>),(subst_lit L \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
assume "polarity = pos"
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit_inst L t s polarity \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have i: "(mset_lit (subst_lit L \<sigma>)) = {# (subst s \<sigma>) #} + {# (subst t \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L t s polarity \<sigma>

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

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>#}
[PROOF STEP]
using add.commute
[PROOF STATE]
proof (prove)
using this:
polarity = pos
(L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>#}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>#}

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from  \<open>L' = mk_lit polarity (Eq t' s)\<close> \<open>polarity = pos\<close>
[PROOF STATE]
proof (chain)
picking this:
L' = mk_lit polarity (Eq t' s)
polarity = pos
[PROOF STEP]
have ii: "(mset_lit (subst_lit L' \<sigma>)) = {# (subst s \<sigma>) #}
          + {# (subst t' \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
L' = mk_lit polarity (Eq t' s)
polarity = pos

goal (1 subgoal):
 1. mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>#}
[PROOF STEP]
using add.commute
[PROOF STATE]
proof (prove)
using this:
L' = mk_lit polarity (Eq t' s)
polarity = pos
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>#}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>#}

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "{# (subst t \<sigma>) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#t \<lhd> \<sigma>#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#t \<lhd> \<sigma>#} \<noteq> {#}

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "(\<forall>k' \<in> set_mset {# (subst t' \<sigma>) #}. \<exists>j' \<in> set_mset {# (subst t \<sigma>) #}. (k', j') \<in> (trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k'\<in>#{#t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
fix k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
assume "k' \<in>set_mset {# (subst t' \<sigma>) #}"
[PROOF STATE]
proof (state)
this:
k' \<in># {#t' \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k' \<in># {#t' \<lhd> \<sigma>#}
[PROOF STEP]
have "k' = (subst t' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
k' \<in># {#t' \<lhd> \<sigma>#}

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

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
have "(subst t \<sigma>) \<in> set_mset {# (subst t \<sigma>) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this \<open>k' = (subst t' \<sigma>)\<close>
            and \<open>((subst t' \<sigma>),(subst t \<sigma>)) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>#}
k' = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
show "\<exists>j' \<in> set_mset {# (subst t \<sigma>) #}. (k', j') \<in> (trm_ord)"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>#}
k' = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k'\<in>#{#t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from i ii
          \<open>((subst t' \<sigma>),(subst t \<sigma>)) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>#}
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "(mset_lit (subst_lit L' \<sigma>),(mset_lit (subst_lit L \<sigma>)))
            \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>#}
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
by (metis one_step_implies_mult empty_iff insert_iff set_mset_add_mset_insert set_mset_empty)
[PROOF STATE]
proof (state)
this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
assume "polarity = neg"
[PROOF STATE]
proof (state)
this:
polarity = neg

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit_inst L t s polarity \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have i: "(mset_lit (subst_lit L \<sigma>)) = {# (subst s \<sigma>), (subst s \<sigma>) #}
          + {# (subst t \<sigma>), (subst t \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L t s polarity \<sigma>

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

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from  \<open>L' = mk_lit polarity (Eq t' s)\<close> \<open>polarity = neg\<close>
[PROOF STATE]
proof (chain)
picking this:
L' = mk_lit polarity (Eq t' s)
polarity = neg
[PROOF STEP]
have
          "subst_lit L' \<sigma> = (Neg (Eq (subst t' \<sigma>) (subst s \<sigma>)))"
[PROOF STATE]
proof (prove)
using this:
L' = mk_lit polarity (Eq t' s)
polarity = neg

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit L' \<sigma> = Neg (Eq (t' \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
have "(mset_lit (subst_lit L' \<sigma>))
          = {# (subst t' \<sigma>), (subst t' \<sigma>), (subst s \<sigma>), (subst s \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L' \<sigma> = Neg (Eq (t' \<lhd> \<sigma>) (s \<lhd> \<sigma>))

goal (1 subgoal):
 1. mset_lit (subst_lit L' \<sigma>) = {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>, s \<lhd> \<sigma>, s \<lhd> \<sigma>#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L' \<sigma>) = {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>, s \<lhd> \<sigma>, s \<lhd> \<sigma>#}

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_lit (subst_lit L' \<sigma>) = {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>, s \<lhd> \<sigma>, s \<lhd> \<sigma>#}
[PROOF STEP]
have ii: "(mset_lit (subst_lit L' \<sigma>))
          = {# (subst s \<sigma>), (subst s \<sigma>) #} + {# (subst t' \<sigma>), (subst t' \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit L' \<sigma>) = {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>, s \<lhd> \<sigma>, s \<lhd> \<sigma>#}

goal (1 subgoal):
 1. mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}
[PROOF STEP]
by (simp add: add.commute add.left_commute)
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "{# (subst t \<sigma>), (subst t \<sigma>) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "(\<forall>k' \<in> set_mset {# (subst t' \<sigma>),(subst t' \<sigma>) #}.
          \<exists>j' \<in> set_mset {# (subst t \<sigma>),(subst t \<sigma>) #}. (k', j') \<in> (trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k'\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
fix k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
assume "k' \<in>set_mset {# (subst t' \<sigma>),(subst t' \<sigma>) #}"
[PROOF STATE]
proof (state)
this:
k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}
[PROOF STEP]
have "k' = (subst t' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}

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

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
have "(subst t \<sigma>) \<in> set_mset {# (subst t \<sigma>),(subst t \<sigma>) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this \<open>k' = (subst t' \<sigma>)\<close>
            and \<open>((subst t' \<sigma>),(subst t \<sigma>)) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
k' = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
show "\<exists>j' \<in> set_mset {# (subst t \<sigma>),(subst t \<sigma>) #}. (k', j') \<in> (trm_ord)"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<in># {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
k' = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k'\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this i ii \<open>{# (subst t \<sigma>), (subst t \<sigma>) #} \<noteq> {#}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>k'\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}
{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}
[PROOF STEP]
have "(mset_lit (subst_lit L' \<sigma>),
            (mset_lit (subst_lit L \<sigma>))) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k'\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}
{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}

goal (1 subgoal):
 1. (mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
using one_step_implies_mult  [of "{# (subst t \<sigma>), (subst t \<sigma>) #}"
               "{# (subst t' \<sigma>),(subst t' \<sigma>) #}" trm_ord
               "{# (subst s \<sigma>),(subst s \<sigma>) #}"]
             trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
\<forall>k'\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j'\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}
{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}
\<lbrakk>{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#} \<noteq> {#}; \<forall>k\<in>#{#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}. \<exists>j\<in>#{#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}. (k, j) \<in> trm_ord\<rbrakk> \<Longrightarrow> ({#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t' \<lhd> \<sigma>, t' \<lhd> \<sigma>#}, {#s \<lhd> \<sigma>, s \<lhd> \<sigma>#} + {#t \<lhd> \<sigma>, t \<lhd> \<sigma>#}) \<in> mult trm_ord
trans trm_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. M' \<notin> cl_ecl P2 - {M} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this and
      \<open>(mset_lit (subst_lit L \<sigma>) \<in> set_mset ?J)\<close>
      \<open>k = (mset_lit (subst_lit M' \<sigma>))\<close>
      \<open>M' = L'\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
k = mset_lit (subst_lit M' \<sigma>)
M' = L'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
k = mset_lit (subst_lit M' \<sigma>)
M' = L'

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
mset_lit (subst_lit L \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
k = mset_lit (subst_lit M' \<sigma>)
M' = L'

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this d1 d2
[PROOF STATE]
proof (chain)
picking this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
[PROOF STEP]
have o: "
      ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set ?C #},
      {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#})
     \<in> mult (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
using  mult_trm_ord_trans one_step_implies_mult [of "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L }) #}"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"  "mult trm_ord"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L })) #} " ]
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}
trans (mult trm_ord)
\<lbrakk>{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#} \<noteq> {#}; \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}. (k, j) \<in> mult trm_ord\<rbrakk> \<Longrightarrow> ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}) - (cl_ecl P1 - {L}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L}#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>C' = (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } ))\<close> and \<open>P1 \<in> P\<close>
    and hyp
[PROOF STATE]
proof (chain)
picking this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

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:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
have not_ref: "\<not> (\<exists>P1. (P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. (P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'
[PROOF STEP]
obtain P1 where "P1 \<in> P" "reflexion P1 C \<sigma> Ground C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>P1. \<lbrakk>P1 \<in> P; reflexion P1 C \<sigma> Ground C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P1 \<in> P
reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>reflexion P1 C \<sigma> Ground C'\<close>
[PROOF STATE]
proof (chain)
picking this:
reflexion P1 C \<sigma> Ground C'
[PROOF STEP]
obtain L1 t s Cl_C Cl_P where
      "(eligible_literal L1 P1 \<sigma>)"
      "(L1 \<in> (cl_ecl P1))"  "(Cl_C = (cl_ecl C))" "(Cl_P = (cl_ecl P1))"
      "(orient_lit_inst L1 t s neg \<sigma>)"
      "(ck_unifier t s \<sigma> Ground)"
      "(Cl_C = (subst_cl ((Cl_P - { L1 }) )) \<sigma>)"
      "(C' = ((Cl_P - { L1 }) ))"
[PROOF STATE]
proof (prove)
using this:
reflexion P1 C \<sigma> Ground C'

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

goal (1 subgoal):
 1. (\<And>L1 Cl_C Cl_P t s. \<lbrakk>eligible_literal L1 P1 \<sigma>; L1 \<in> cl_ecl P1; Cl_C = cl_ecl C; Cl_P = cl_ecl P1; orient_lit_inst L1 t s neg \<sigma>; ck_unifier t s \<sigma> Ground; Cl_C = subst_cl (Cl_P - {L1}) \<sigma>; C' = Cl_P - {L1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eligible_literal L1 P1 \<sigma>
L1 \<in> cl_ecl P1
Cl_C = cl_ecl C
Cl_P = cl_ecl P1
orient_lit_inst L1 t s neg \<sigma>
ck_unifier t s \<sigma> Ground
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>
C' = Cl_P - {L1}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>P1 \<in> P\<close> and assms(2) and \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S
[PROOF STEP]
have "finite (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC1 = "mset_ecl (P1, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC2 = "mset_ecl (C, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L1 \<in> (cl_ecl P1)\<close> \<open>finite (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L1 \<in> cl_ecl P1
finite (cl_ecl P1)
[PROOF STEP]
have "mset_set (cl_ecl P1) = mset_set ((cl_ecl P1)-{ L1 }) + mset_set { L1 }"
[PROOF STATE]
proof (prove)
using this:
L1 \<in> cl_ecl P1
finite (cl_ecl P1)

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}
[PROOF STEP]
using split_mset_set [of "cl_ecl P1" "cl_ecl P1 - { L1 }" "{ L1 }"]
[PROOF STATE]
proof (prove)
using this:
L1 \<in> cl_ecl P1
finite (cl_ecl P1)
\<lbrakk>cl_ecl P1 = cl_ecl P1 - {L1} \<union> {L1}; (cl_ecl P1 - {L1}) \<inter> {L1} = {}; finite (cl_ecl P1 - {L1}); finite {L1}\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}
[PROOF STEP]
have  d1: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set (cl_ecl P1)) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L1 })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L1 }) #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L1}) + mset_set {L1}
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C = "((cl_ecl P1) - { L1 })"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
[PROOF STEP]
have "finite ?C"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C' = "{}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "finite ?C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "?C = ( (cl_ecl P1) - { L1 }) \<union> ?C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_ecl P1 - {L1} = cl_ecl P1 - {L1} \<union> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl P1 - {L1} = cl_ecl P1 - {L1} \<union> {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close> \<open>finite ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
finite {}
[PROOF STEP]
have "mset_set ?C = mset_set ((cl_ecl P1)-{ L1 }) + mset_set ?C'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite {}

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}
[PROOF STEP]
using split_mset_set [of "?C" "cl_ecl P1 - { L1 }" "?C'"]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite {}
\<lbrakk>cl_ecl P1 - {L1} = cl_ecl P1 - {L1} \<union> {}; (cl_ecl P1 - {L1}) \<inter> {} = {}; finite (cl_ecl P1 - {L1}); finite {}\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}
[PROOF STEP]
have  d2: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L1 })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L1}) = mset_set (cl_ecl P1 - {L1}) + mset_set {}
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L1 }) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?K = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?J = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L1 }) #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "(\<forall>k \<in> set_mset ?K. \<exists>j \<in> set_mset ?J. (k, j) \<in> (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this d1 d2  \<open>{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L1 }) #} \<noteq> {#}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}
[PROOF STEP]
have o: "
      ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set ?C #},
      {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#})
     \<in> mult (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
using  mult_trm_ord_trans one_step_implies_mult [of
    "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L1 }) #}"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"  "mult trm_ord"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L1 })) #} " ]
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}
trans (mult trm_ord)
\<lbrakk>{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#} \<noteq> {#}; \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}. (k, j) \<in> mult trm_ord\<rbrakk> \<Longrightarrow> ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {}#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L1}#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>Cl_P = (cl_ecl P1)\<close> \<open>C' = ((Cl_P - { L1 }) )\<close> and \<open>P1 \<in> P\<close>
    and hyp
[PROOF STATE]
proof (chain)
picking this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
Cl_P = cl_ecl P1
C' = Cl_P - {L1}
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L1})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
Cl_P = cl_ecl P1
C' = Cl_P - {L1}
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

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:
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
have not_fact: "\<not> (\<exists>P1. (P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. (P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'
[PROOF STEP]
obtain P1 where "P1 \<in> P" "factorization  P1 C \<sigma> Ground C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>P1. \<lbrakk>P1 \<in> P; factorization P1 C \<sigma> Ground C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P1 \<in> P
factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>factorization P1 C \<sigma> Ground C'\<close>
[PROOF STATE]
proof (chain)
picking this:
factorization P1 C \<sigma> Ground C'
[PROOF STEP]
obtain L1 L2 L' t s u v Cl_P Cl_C  where
      "(eligible_literal L1 P1 \<sigma>)"
      "(L1 \<in> (cl_ecl P1))" "(L2 \<in> (cl_ecl P1) - { L1 })" "(Cl_C = (cl_ecl C))" "(Cl_P = (cl_ecl P1))"
      "(orient_lit_inst L1 t s pos \<sigma>)"
      "(orient_lit_inst L2 u v pos \<sigma>)"
      "((subst t \<sigma>) \<noteq> (subst s \<sigma>))"
      "((subst t \<sigma>) \<noteq> (subst v \<sigma>))"
      "(ck_unifier t u \<sigma> Ground)"
      "(L' = Neg (Eq s v))"
      "(Cl_C = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } )) \<sigma>)"
      "(C' = ( (Cl_P - { L2 }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>L1 L2 Cl_C Cl_P t s u v L'. \<lbrakk>eligible_literal L1 P1 \<sigma>; L1 \<in> cl_ecl P1; L2 \<in> cl_ecl P1 - {L1}; Cl_C = cl_ecl C; Cl_P = cl_ecl P1; orient_lit_inst L1 t s pos \<sigma>; orient_lit_inst L2 u v pos \<sigma>; t \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>; t \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>; ck_unifier t u \<sigma> Ground; L' = Neg (Eq s v); Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>; C' = Cl_P - {L2} \<union> {L'}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding factorization_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L1 L2 L' t s u v Cl_P Cl_C trms_C. eligible_literal L1 P1 \<sigma> \<and> L1 \<in> cl_ecl P1 \<and> L2 \<in> cl_ecl P1 - {L1} \<and> Cl_C = cl_ecl C \<and> Cl_P = cl_ecl P1 \<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> Ground \<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 P1 \<union> proper_subterms_of t) \<sigma>)) Ground) \<and> Cl_C = subst_cl C' \<sigma> \<and> C' = Cl_P - {L2} \<union> {L'}

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>P1 \<in> P\<close> and assms(2) and \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S
[PROOF STEP]
have "finite (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
\<forall>x\<in>S. finite (cl_ecl x)
P \<subseteq> S

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>P1 \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
grounding_set P \<sigma>
P1 \<in> P
[PROOF STEP]
have "ground_clause (subst_cl (cl_ecl P1) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
grounding_set P \<sigma>
P1 \<in> P

goal (1 subgoal):
 1. ground_clause (subst_cl (cl_ecl P1) \<sigma>)
[PROOF STEP]
unfolding grounding_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> ground_clause (subst_cl (cl_ecl x) \<sigma>)
P1 \<in> P

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl P1) \<sigma>)
[PROOF STEP]
have "vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl P1) \<sigma>)

goal (1 subgoal):
 1. vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L1 \<in> (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L1 \<in> cl_ecl P1
[PROOF STEP]
have "(subst_lit L1 \<sigma>) \<in> (subst_cl (cl_ecl P1) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L1 \<in> cl_ecl P1

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L1 \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}
[PROOF STEP]
have "vars_of_lit (subst_lit L1 \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L1 \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}

goal (1 subgoal):
 1. vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<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
      "orient_lit (subst_lit L1 \<sigma>) (subst t \<sigma>) (subst s \<sigma>) pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L1 t s pos \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L1 t s pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst t \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (t \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit L1 \<sigma>) (subst t \<sigma>) (subst s \<sigma>) pos\<close>
       and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst s \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (s \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(L2 \<in> (cl_ecl P1) - { L1 })\<close>
[PROOF STATE]
proof (chain)
picking this:
L2 \<in> cl_ecl P1 - {L1}
[PROOF STEP]
have "L2 \<in> (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
L2 \<in> cl_ecl P1 - {L1}

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L2 \<in> (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L2 \<in> cl_ecl P1
[PROOF STEP]
have "(subst_lit L2 \<sigma>) \<in> (subst_cl (cl_ecl P1) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L2 \<in> cl_ecl P1

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L2 \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}
[PROOF STEP]
have "vars_of_lit (subst_lit L2 \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L2 \<sigma> \<in> subst_cl (cl_ecl P1) \<sigma>
vars_of_cl (subst_cl (cl_ecl P1) \<sigma>) = {}

goal (1 subgoal):
 1. vars_of_lit (subst_lit L2 \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit (subst_lit L2 \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst L2 u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L2 u v pos \<sigma>
[PROOF STEP]
have
      "orient_lit (subst_lit L2 \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L2 u v pos \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L2 u v pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of_lit (subst_lit L2 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst u \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit L2 \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos\<close>
       and \<open>vars_of_lit (subst_lit L2 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst v \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L2 \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (v \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>ck_unifier t u \<sigma> Ground\<close>
[PROOF STATE]
proof (chain)
picking this:
ck_unifier t u \<sigma> Ground
[PROOF STEP]
have "(subst t \<sigma>) = (subst u \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
ck_unifier t u \<sigma> Ground

goal (1 subgoal):
 1. t \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
unfolding ck_unifier_def Unifier_def
[PROOF STATE]
proof (prove)
using this:
if Ground = FirstOrder then min_IMGU \<sigma> t u else t \<lhd> \<sigma> = u \<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. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit L1 \<sigma>) (subst t \<sigma>) (subst s \<sigma>) pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
have "((subst t \<sigma>),(subst s \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst t \<sigma>) \<noteq> (subst s \<sigma>)\<close>
      and \<open>vars_of (subst t \<sigma>) = {}\<close> \<open>vars_of (subst s \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
vars_of (t \<lhd> \<sigma>) = {}
vars_of (s \<lhd> \<sigma>) = {}
[PROOF STEP]
have "((subst s \<sigma>),(subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
vars_of (t \<lhd> \<sigma>) = {}
vars_of (s \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
vars_of (t \<lhd> \<sigma>) = {}
vars_of (s \<lhd> \<sigma>) = {}
\<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. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
vars_of (t \<lhd> \<sigma>) = {}
vars_of (s \<lhd> \<sigma>) = {}
\<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. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst t \<sigma>) = (subst u \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
t \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
have
      "((subst s \<sigma>),(subst u \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
t \<lhd> \<sigma> = u \<lhd> \<sigma>

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit (subst_lit L2 \<sigma>) (subst u \<sigma>) (subst v \<sigma>) pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos
[PROOF STEP]
have "((subst u \<sigma>),(subst v \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L2 \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit L2 \<sigma> = Pos (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> subst_lit L2 \<sigma> = Pos (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (subst_lit L2 \<sigma> = Neg (Eq (u \<lhd> \<sigma>) (v \<lhd> \<sigma>)) \<or> subst_lit L2 \<sigma> = Neg (Eq (v \<lhd> \<sigma>) (u \<lhd> \<sigma>))) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = neg

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst t \<sigma>) \<noteq> (subst v \<sigma>)\<close>
      and \<open>(subst t \<sigma>) = (subst u \<sigma>)\<close>
      and \<open>vars_of (subst u \<sigma>) = {}\<close> \<open>vars_of (subst v \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
t \<lhd> \<sigma> = u \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
have "((subst v \<sigma>),(subst u \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
t \<lhd> \<sigma> = u \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
t \<lhd> \<sigma> = u \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
\<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. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
t \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
t \<lhd> \<sigma> = u \<lhd> \<sigma>
vars_of (u \<lhd> \<sigma>) = {}
vars_of (v \<lhd> \<sigma>) = {}
\<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. (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC1 = "mset_ecl (P1, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?mC2 = "mset_ecl (C, \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L2 \<in> (cl_ecl P1)\<close> \<open>finite (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
L2 \<in> cl_ecl P1
finite (cl_ecl P1)
[PROOF STEP]
have "mset_set (cl_ecl P1) = mset_set ((cl_ecl P1)-{ L2 }) + mset_set { L2 }"
[PROOF STATE]
proof (prove)
using this:
L2 \<in> cl_ecl P1
finite (cl_ecl P1)

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}
[PROOF STEP]
using split_mset_set [of "cl_ecl P1" "cl_ecl P1 - { L2 }" "{ L2 }"]
[PROOF STATE]
proof (prove)
using this:
L2 \<in> cl_ecl P1
finite (cl_ecl P1)
\<lbrakk>cl_ecl P1 = cl_ecl P1 - {L2} \<union> {L2}; (cl_ecl P1 - {L2}) \<inter> {L2} = {}; finite (cl_ecl P1 - {L2}); finite {L2}\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}

goal (1 subgoal):
 1. mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}
[PROOF STEP]
have  d1: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set (cl_ecl P1)) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L2 })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1) = mset_set (cl_ecl P1 - {L2}) + mset_set {L2}
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C = "(((cl_ecl P1) - { L2 }) \<union> { L' } )"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
[PROOF STEP]
have "finite ?C"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)

goal (1 subgoal):
 1. finite (cl_ecl P1 - {L2} \<union> {L'})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (cl_ecl P1 - {L2} \<union> {L'})

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?C' = "?C - ( (cl_ecl P1) - { L2 })"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1 - {L2} \<union> {L'})
[PROOF STEP]
have "finite ?C'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L2} \<union> {L'})

goal (1 subgoal):
 1. finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "?C = ( (cl_ecl P1) - { L2 }) \<union> ?C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_ecl P1 - {L2} \<union> {L'} = cl_ecl P1 - {L2} \<union> (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl P1 - {L2} \<union> {L'} = cl_ecl P1 - {L2} \<union> (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (cl_ecl P1)\<close> \<open>finite ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
have "mset_set ?C = mset_set ((cl_ecl P1)-{ L2 }) + mset_set ?C'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
using split_mset_set [of "?C" "cl_ecl P1 - { L2 }" "?C'"]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
\<lbrakk>cl_ecl P1 - {L2} \<union> {L'} = cl_ecl P1 - {L2} \<union> (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})); (cl_ecl P1 - {L2}) \<inter> (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})) = {}; finite (cl_ecl P1 - {L2}); finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))\<rbrakk> \<Longrightarrow> mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
have  d2: "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C) #}
      = {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L2 })) #}
        + {# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
[PROOF STEP]
using split_image_mset
[PROOF STATE]
proof (prove)
using this:
mset_set (cl_ecl P1 - {L2} \<union> {L'}) = mset_set (cl_ecl P1 - {L2}) + mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
?M = ?M1.0 + ?M2.0 \<Longrightarrow> image_mset ?f ?M = image_mset ?f ?M1.0 + image_mset ?f ?M2.0

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?K = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?J = "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have "(\<forall>k \<in> set_mset ?K. \<exists>j \<in> set_mset ?J. (k, j) \<in> (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
assume "k \<in> set_mset ?K"
[PROOF STATE]
proof (state)
this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
[PROOF STEP]
have "k \<in># ?K"
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}

goal (1 subgoal):
 1. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
[PROOF STEP]
obtain M' where "M' \<in># (mset_set ?C')" and "k = (mset_lit (subst_lit M' \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>M' \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})); k = mset_lit (subst_lit M' \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using image_mset_thm [of "?K"  "\<lambda>x. (mset_lit (subst_lit x \<sigma>))" "(mset_set ?C')"]
[PROOF STATE]
proof (prove)
using this:
k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
\<lbrakk>{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}; ?x \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}\<rbrakk> \<Longrightarrow> \<exists>y. y \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})) \<and> ?x = mset_lit (subst_lit y \<sigma>)

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>M' \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})); k = mset_lit (subst_lit M' \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
M' \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
k = mset_lit (subst_lit M' \<sigma>)

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>M' \<in># (mset_set ?C')\<close>and \<open>finite ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
[PROOF STEP]
have "M' \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
M' \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))
finite (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))

goal (1 subgoal):
 1. M' \<in> cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M' \<in> cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "L2 \<in># (mset_set { L2 })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2 \<in># mset_set {L2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L2 \<in># mset_set {L2}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L2 \<in># mset_set {L2}
[PROOF STEP]
have "(mset_lit (subst_lit L2 \<sigma>) \<in># ?J)"
[PROOF STATE]
proof (prove)
using this:
L2 \<in># mset_set {L2}

goal (1 subgoal):
 1. mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
[PROOF STEP]
have "(mset_lit (subst_lit L2 \<sigma>) \<in> set_mset ?J)"
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}

goal (1 subgoal):
 1. mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L2 \<sigma>) \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}

goal (1 subgoal):
 1. \<And>k. k \<in># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#} \<Longrightarrow> \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
show "\<exists>j \<in> set_mset ?J. (k, j) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from \<open>M' \<in> ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<in> cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})
[PROOF STEP]
have "M' = L'"
[PROOF STATE]
proof (prove)
using this:
M' \<in> cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2})

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

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from  \<open>orient_lit_inst L2 u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L2 u v pos \<sigma>
[PROOF STEP]
have i: "(mset_lit (subst_lit L2 \<sigma>))
          = {#} + {# (subst u \<sigma>), (subst v \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L2 u v pos \<sigma>

goal (1 subgoal):
 1. mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(L2 = Pos (Eq u v) \<or> L2 = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (L2 = Neg (Eq u v) \<or> L2 = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
using add.commute
[PROOF STATE]
proof (prove)
using this:
(L2 = Pos (Eq u v) \<or> L2 = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (L2 = Neg (Eq u v) \<or> L2 = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = neg
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from  \<open>L' = Neg (Eq s v)\<close>
[PROOF STATE]
proof (chain)
picking this:
L' = Neg (Eq s v)
[PROOF STEP]
have ii: "(mset_lit (subst_lit L' \<sigma>)) =
          {#} + {# (subst s \<sigma>), (subst s \<sigma>), (subst v \<sigma>), (subst v \<sigma>) #}"
[PROOF STATE]
proof (prove)
using this:
L' = Neg (Eq s v)

goal (1 subgoal):
 1. mset_lit (subst_lit L' \<sigma>) = {#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L' \<sigma>) = {#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "{# (subst u \<sigma>), (subst v \<sigma>) #} \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
have "(\<forall>k' \<in> set_mset {# (subst s \<sigma>), (subst s \<sigma>), (subst v \<sigma>), (subst v \<sigma>) #}.
          \<exists>j' \<in> set_mset {# (subst u \<sigma>), (subst v \<sigma>) #}. (k', j') \<in> (trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k'\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
fix k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
assume nh: "k' \<in>set_mset {# (subst s \<sigma>), (subst s \<sigma>), (subst v \<sigma>), (subst v \<sigma>) #}"
[PROOF STATE]
proof (state)
this:
k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
have "(subst u \<sigma>) \<in> set_mset {# (subst u \<sigma>), (subst v \<sigma>) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from nh
[PROOF STATE]
proof (chain)
picking this:
k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
have "k' = (subst s \<sigma>) \<or> k' = (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}

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

goal (1 subgoal):
 1. \<And>k'. k' \<in># {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' = s \<lhd> \<sigma> \<or> k' = v \<lhd> \<sigma>
[PROOF STEP]
show "\<exists>j' \<in> set_mset {# (subst u \<sigma>), (subst v \<sigma>) #}. (k', j') \<in> (trm_ord)"
[PROOF STATE]
proof (prove)
using this:
k' = s \<lhd> \<sigma> \<or> k' = v \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k' = s \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
 2. k' = v \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
assume "k' = (subst s \<sigma>)"
[PROOF STATE]
proof (state)
this:
k' = s \<lhd> \<sigma>

goal (2 subgoals):
 1. k' = s \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
 2. k' = v \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this and \<open>((subst s \<sigma>),(subst u \<sigma>)) \<in> trm_ord\<close>
              and \<open>(subst u \<sigma>) \<in> set_mset {# (subst u \<sigma>), (subst v \<sigma>) #}\<close>
[PROOF STATE]
proof (chain)
picking this:
k' = s \<lhd> \<sigma>
(s \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k' = s \<lhd> \<sigma>
(s \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal (1 subgoal):
 1. k' = v \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k' = v \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
assume "k' = (subst v \<sigma>)"
[PROOF STATE]
proof (state)
this:
k' = v \<lhd> \<sigma>

goal (1 subgoal):
 1. k' = v \<lhd> \<sigma> \<Longrightarrow> \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
from this and \<open>((subst v \<sigma>),(subst u \<sigma>)) \<in> trm_ord\<close>
              and \<open>(subst u \<sigma>) \<in> set_mset {# (subst u \<sigma>), (subst v \<sigma>) #}\<close>
[PROOF STATE]
proof (chain)
picking this:
k' = v \<lhd> \<sigma>
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k' = v \<lhd> \<sigma>
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> \<in># {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}

goal (1 subgoal):
 1. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k'\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this i ii \<open>{# (subst u \<sigma>), (subst v \<sigma>) #} \<noteq> {#}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>k'\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}
{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}
[PROOF STEP]
have "(mset_lit (subst_lit L' \<sigma>),
            (mset_lit (subst_lit L2 \<sigma>))) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k'\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}
{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}

goal (1 subgoal):
 1. (mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L2 \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
using one_step_implies_mult  [of "{# (subst u \<sigma>), (subst v \<sigma>) #}"
               "{#  (subst s \<sigma>),(subst s \<sigma>), (subst v \<sigma>),(subst v \<sigma>) #}"
               trm_ord "{#}"]
             trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
\<forall>k'\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j'\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k', j') \<in> trm_ord
mset_lit (subst_lit L2 \<sigma>) = {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}
mset_lit (subst_lit L' \<sigma>) = {#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}
{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}
\<lbrakk>{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#} \<noteq> {#}; \<forall>k\<in>#{#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}. \<exists>j\<in>#{#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}. (k, j) \<in> trm_ord\<rbrakk> \<Longrightarrow> ({#} + {#s \<lhd> \<sigma>, s \<lhd> \<sigma>, v \<lhd> \<sigma>, v \<lhd> \<sigma>#}, {#} + {#u \<lhd> \<sigma>, v \<lhd> \<sigma>#}) \<in> mult trm_ord
trans trm_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L2 \<sigma>)) \<in> mult trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L2 \<sigma>)) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
from this \<open>M' = L'\<close> \<open>k = (mset_lit (subst_lit M' \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L2 \<sigma>)) \<in> mult trm_ord
M' = L'
k = mset_lit (subst_lit M' \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L' \<sigma>), mset_lit (subst_lit L2 \<sigma>)) \<in> mult trm_ord
M' = L'
k = mset_lit (subst_lit M' \<sigma>)

goal (1 subgoal):
 1. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this d1 d2 \<open>{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #} \<noteq> {#}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}
[PROOF STEP]
have o: "
      ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set ?C #},
      {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#})
     \<in> mult (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
using  mult_trm_ord_trans one_step_implies_mult [of
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set { L2 }) #}"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ?C') #}"  "mult trm_ord"
      "{# (mset_lit (subst_lit x \<sigma>)). x \<in># (mset_set ((cl_ecl P1) - { L2 })) #} " ]
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}
{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}
trans (mult trm_ord)
\<lbrakk>{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#} \<noteq> {#}; \<forall>k\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}. \<exists>j\<in>#{#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}. (k, j) \<in> mult trm_ord\<rbrakk> \<Longrightarrow> ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'} - (cl_ecl P1 - {L2}))#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2})#} + {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set {L2}#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>(Cl_P = (cl_ecl P1))\<close> \<open>C' = ( (Cl_P - { L2 }) \<union> { L' } )\<close> and \<open>P1 \<in> P\<close>
    and hyp
[PROOF STATE]
proof (chain)
picking this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
Cl_P = cl_ecl P1
C' = Cl_P - {L2} \<union> {L'}
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
({#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1 - {L2} \<union> {L'})#}, {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl P1)#}) \<in> mult (mult trm_ord)
Cl_P = cl_ecl P1
C' = Cl_P - {L2} \<union> {L'}
P1 \<in> P
\<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

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:
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D. D \<in> P \<and> (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> False
[PROOF STEP]
from not_sup not_ref not_fact and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'
derivable C P S \<sigma> Ground C'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'
derivable C P S \<sigma> Ground C'

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding derivable_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> Ground C'
(\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> Ground C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> Ground C')

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

goal:
No subgoals!
[PROOF STEP]
qed