[STATEMENT]
lemma lifting_lemma:
  assumes "derivable C P S \<sigma> Ground C'"
  shows "\<exists> D \<theta> \<eta>. ((derivable D P S \<theta> FirstOrder C') \<and> (\<sigma> \<doteq> \<theta> \<lozenge> \<eta>) \<and> (trms_subsumes D C \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<Longrightarrow> False
[PROOF STEP]
assume hyp: "\<not> (\<exists> D \<theta> \<eta>. ((derivable D P S \<theta> FirstOrder C') \<and> (\<sigma> \<doteq> \<theta> \<lozenge> \<eta>)
                \<and> (trms_subsumes D C \<eta>)))"
[PROOF STATE]
proof (state)
this:
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>

goal (1 subgoal):
 1. \<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<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 \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<Longrightarrow> False
[PROOF STEP]
have not_sup: "\<not> (\<exists>P1 P2. (P = { P1, P2 } \<and> superposition P1 P2 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1 P2. (P = { P1, P2 } \<and> superposition P1 P2 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = {P1, P2}
superposition P1 P2 C \<sigma> Ground C'
[PROOF STEP]
obtain L t s u v M p Cl_P1 Cl_P2 Cl_C polarity t' u' L' trms_C
      where "L \<in> Cl_P1" "(M \<in> Cl_P2)" "(eligible_literal L P1 \<sigma>)" "(eligible_literal M P2 \<sigma>)"
      "(variable_disjoint P1 P2)"
      "(Cl_P1 = (cl_ecl P1))" "(Cl_P2 = (cl_ecl P2))"
      "(\<not> is_a_variable u')"
      "(allowed_redex u' P1 \<sigma>)"
      "(C = (Ecl Cl_C trms_C))"
      "(orient_lit_inst M u v pos \<sigma>)"
      "(orient_lit_inst L t s polarity \<sigma>)"
      "((subst u \<sigma>) \<noteq> (subst v \<sigma>))"
      "(subterm t p u')"
      "(ck_unifier u' u \<sigma> Ground)"
      "(replace_subterm t p v t')"
      "(L' = mk_lit polarity (Eq t' s))"
      "(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)"
      "(Cl_C = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<sigma>))"
      "(C' = (Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
P = {P1, P2}
superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>L Cl_P1 M Cl_P2 u' Cl_C trms_C u v t s polarity p t' L'. \<lbrakk>L \<in> Cl_P1; M \<in> Cl_P2; eligible_literal L P1 \<sigma>; eligible_literal M P2 \<sigma>; variable_disjoint P1 P2; Cl_P1 = cl_ecl P1; Cl_P2 = cl_ecl P2; \<not> is_a_variable u'; allowed_redex u' P1 \<sigma>; C = Ecl Cl_C trms_C; orient_lit_inst M u v pos \<sigma>; orient_lit_inst L t s polarity \<sigma>; u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>; subterm t p u'; ck_unifier u' u \<sigma> Ground; replace_subterm t p v t'; L' = mk_lit polarity (Eq t' s); 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; Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>; C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding superposition_def get_trms_def
[PROOF STATE]
proof (prove)
using this:
P = {P1, P2}
\<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 = (if Ground = FirstOrder then filter_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>)) else 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>)) \<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>L Cl_P1 M Cl_P2 u' Cl_C trms_C u v t s polarity p t' L'. \<lbrakk>L \<in> Cl_P1; M \<in> Cl_P2; eligible_literal L P1 \<sigma>; eligible_literal M P2 \<sigma>; variable_disjoint P1 P2; Cl_P1 = cl_ecl P1; Cl_P2 = cl_ecl P2; \<not> is_a_variable u'; allowed_redex u' P1 \<sigma>; C = Ecl Cl_C trms_C; orient_lit_inst M u v pos \<sigma>; orient_lit_inst L t s polarity \<sigma>; u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>; subterm t p u'; ck_unifier u' u \<sigma> Ground; replace_subterm t p v t'; L' = mk_lit polarity (Eq t' s); trms_C = (if Ground = FirstOrder then filter_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>)) else 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>)); Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>; C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> Cl_P1
M \<in> Cl_P2
eligible_literal L P1 \<sigma>
eligible_literal M P2 \<sigma>
variable_disjoint P1 P2
Cl_P1 = cl_ecl P1
Cl_P2 = cl_ecl P2
\<not> is_a_variable u'
allowed_redex u' P1 \<sigma>
C = Ecl Cl_C trms_C
orient_lit_inst M u v pos \<sigma>
orient_lit_inst L t s polarity \<sigma>
u \<lhd> \<sigma> \<noteq> v \<lhd> \<sigma>
subterm t p u'
ck_unifier u' u \<sigma> Ground
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
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
Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[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 " Unifier \<sigma> u' u"
[PROOF STATE]
proof (prove)
using this:
ck_unifier u' u \<sigma> Ground

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

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

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

goal (1 subgoal):
 1. u' \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
unfolding Unifier_def
[PROOF STATE]
proof (prove)
using this:
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. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u' \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
have "unify u' u \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
u' \<lhd> \<sigma> = u \<lhd> \<sigma>

goal (1 subgoal):
 1. unify u' u \<noteq> None
[PROOF STEP]
using MGU_exists
[PROOF STATE]
proof (prove)
using this:
u' \<lhd> \<sigma> = u \<lhd> \<sigma>
\<forall>\<sigma>. ?t \<lhd> \<sigma> = ?s \<lhd> \<sigma> \<longrightarrow> unify ?t ?s \<noteq> None

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
unify u' u \<noteq> None
[PROOF STEP]
obtain \<theta> where "unify u' u = Some \<theta>"
[PROOF STATE]
proof (prove)
using this:
unify u' u \<noteq> None

goal (1 subgoal):
 1. (\<And>\<theta>. unify u' u = Some \<theta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unify u' u = Some \<theta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
hence "min_IMGU \<theta> u' u"
[PROOF STATE]
proof (prove)
using this:
unify u' u = Some \<theta>

goal (1 subgoal):
 1. min_IMGU \<theta> u' u
[PROOF STEP]
by (rule unify_computes_min_IMGU)
[PROOF STATE]
proof (state)
this:
min_IMGU \<theta> u' u

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
with \<open>Unifier \<sigma> u' u\<close>
[PROOF STATE]
proof (chain)
picking this:
Unifier \<sigma> u' u
min_IMGU \<theta> u' u
[PROOF STEP]
obtain \<eta> where "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> u' u
min_IMGU \<theta> u' u

goal (1 subgoal):
 1. (\<And>\<eta>. \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_IMGU_def IMGU_iff_Idem_and_MGU MGU_def
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> u' u
(Idem \<theta> \<and> Unifier \<theta> u' u \<and> (\<forall>\<theta>'. Unifier \<theta>' u' u \<longrightarrow> (\<exists>\<gamma>. \<theta>' \<doteq> \<theta> \<lozenge> \<gamma>))) \<and> fst ` set \<theta> \<subseteq> vars_of u' \<union> vars_of u \<and> range_vars \<theta> \<subseteq> vars_of u' \<union> vars_of u

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and \<open>(eligible_literal L P1 \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L P1 \<sigma>
[PROOF STEP]
have "eligible_literal L P1 \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L P1 \<sigma>

goal (1 subgoal):
 1. eligible_literal L P1 \<theta>
[PROOF STEP]
using lift_eligible_literal
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L P1 \<sigma>
\<lbrakk>eligible_literal ?L ?C ?\<sigma>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> eligible_literal ?L ?C ?\<theta>

goal (1 subgoal):
 1. eligible_literal L P1 \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eligible_literal L P1 \<theta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and \<open>(eligible_literal M P2 \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal M P2 \<sigma>
[PROOF STEP]
have "eligible_literal M P2 \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal M P2 \<sigma>

goal (1 subgoal):
 1. eligible_literal M P2 \<theta>
[PROOF STEP]
using lift_eligible_literal
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal M P2 \<sigma>
\<lbrakk>eligible_literal ?L ?C ?\<sigma>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> eligible_literal ?L ?C ?\<theta>

goal (1 subgoal):
 1. eligible_literal M P2 \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eligible_literal M P2 \<theta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>min_IMGU \<theta> u' u\<close>
[PROOF STATE]
proof (chain)
picking this:
min_IMGU \<theta> u' u
[PROOF STEP]
have "ck_unifier u' u \<theta> FirstOrder"
[PROOF STATE]
proof (prove)
using this:
min_IMGU \<theta> u' u

goal (1 subgoal):
 1. ck_unifier u' u \<theta> FirstOrder
[PROOF STEP]
unfolding ck_unifier_def
[PROOF STATE]
proof (prove)
using this:
min_IMGU \<theta> u' u

goal (1 subgoal):
 1. if FirstOrder = FirstOrder then min_IMGU \<theta> u' u else Unifier \<theta> u' u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ck_unifier u' u \<theta> FirstOrder

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>(allowed_redex u' P1 \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
allowed_redex u' P1 \<sigma>
[PROOF STEP]
have "(allowed_redex u' P1 \<theta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
allowed_redex u' P1 \<sigma>

goal (1 subgoal):
 1. allowed_redex u' P1 \<theta>
[PROOF STEP]
using lift_allowed_redex [of \<sigma> \<theta> \<eta> ]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
allowed_redex u' P1 \<sigma>
\<lbrakk>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>; allowed_redex ?u ?C \<sigma>\<rbrakk> \<Longrightarrow> allowed_redex ?u ?C \<theta>

goal (1 subgoal):
 1. allowed_redex u' P1 \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
allowed_redex u' P1 \<theta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>orient_lit_inst M u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst M u v pos \<sigma>
[PROOF STEP]
have "orient_lit_inst M u v pos \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst M u v pos \<sigma>

goal (1 subgoal):
 1. orient_lit_inst M u v pos \<theta>
[PROOF STEP]
using lift_orient_lit_inst
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst M u v pos \<sigma>
\<lbrakk>orient_lit_inst ?L ?t ?s ?polarity ?\<theta>; ?\<theta> \<doteq> ?\<sigma> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> orient_lit_inst ?L ?t ?s ?polarity ?\<sigma>

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>orient_lit_inst L t s polarity \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have "orient_lit_inst L t s polarity \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L t s polarity \<sigma>

goal (1 subgoal):
 1. orient_lit_inst L t s polarity \<theta>
[PROOF STEP]
using lift_orient_lit_inst
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L t s polarity \<sigma>
\<lbrakk>orient_lit_inst ?L ?t ?s ?polarity ?\<theta>; ?\<theta> \<doteq> ?\<sigma> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> orient_lit_inst ?L ?t ?s ?polarity ?\<sigma>

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

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain E where "E = ((trms_ecl P1) \<union> (trms_ecl P2) \<union>
          { r. \<exists> q. (q,p) \<in> (pos_ord P1 t) \<and> (subterm t q r) })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E. E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(Cl_C = (subst_cl C' \<sigma>))\<close>
      \<open>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)\<close>
[PROOF STATE]
proof (chain)
picking this:
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}
Cl_C = subst_cl C' \<sigma>
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
[PROOF STEP]
have "trms_C = (get_trms Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        E  \<sigma>)) Ground)"
[PROOF STATE]
proof (prove)
using this:
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}
Cl_C = subst_cl C' \<sigma>
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

goal (1 subgoal):
 1. trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set E \<sigma>)) Ground
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set E \<sigma>)) Ground

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?Cl_C' = "(subst_cl C' \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from  \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>trms_C = (get_trms Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        E  \<sigma>)) Ground)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set E \<sigma>)) Ground
[PROOF STEP]
obtain "\<exists>T'. ( (subst_set T' \<eta>) \<subseteq> trms_C \<and> T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set E \<sigma>)) Ground

goal (1 subgoal):
 1. (\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lift_irreducible_terms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set E \<sigma>)) Ground
\<lbrakk>?T = get_trms ?C (dom_trms (subst_cl ?D ?\<sigma>) (subst_set ?E ?\<sigma>)) Ground; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> \<exists>T'. subst_set T' ?\<eta> \<subseteq> ?T \<and> T' = get_trms ?C' (dom_trms (subst_cl ?D ?\<theta>) (subst_set ?E ?\<theta>)) FirstOrder

goal (1 subgoal):
 1. (\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
obtain T' where "(subst_set T' \<eta>) \<subseteq> trms_C"
      and "T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder"
[PROOF STATE]
proof (prove)
using this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>subst_set T' \<eta> \<subseteq> trms_C; T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_set T' \<eta> \<subseteq> trms_C
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain C_fo where "C_fo = (Ecl ?Cl_C' T')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C_fo. C_fo = Ecl (subst_cl C' \<theta>) T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in> Cl_P1\<close> \<open>(M \<in> Cl_P2)\<close> \<open>(eligible_literal L P1 \<theta>)\<close> \<open>(eligible_literal M P2 \<theta>)\<close>
      \<open>(variable_disjoint P1 P2)\<close>
      \<open>(Cl_P1 = (cl_ecl P1))\<close> \<open>(Cl_P2 = (cl_ecl P2))\<close>
      \<open>(\<not> is_a_variable u')\<close>
      \<open>(allowed_redex u' P1 \<theta>)\<close>
      \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
      \<open>(orient_lit_inst M u v pos \<theta>)\<close>
      \<open>(orient_lit_inst L t s polarity \<theta>)\<close>
      \<open>((subst u \<theta>) \<noteq> (subst v \<theta>))\<close>
      \<open>(subterm t p u')\<close>
      \<open>(ck_unifier u' u \<theta> FirstOrder)\<close>
      \<open>(replace_subterm t p v t')\<close>
      \<open>(L' = mk_lit polarity (Eq t' s))\<close>
      \<open>T' = (get_trms ?Cl_C' (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder)\<close>
      \<open>(?Cl_C' = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<theta>))\<close>
      \<open>(C' = (Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } ))\<close>
      \<open>E = ((trms_ecl P1) \<union> (trms_ecl P2) \<union>
          { r. \<exists> q. (q,p) \<in> (pos_ord P1 t) \<and> (subterm t q r) })\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> Cl_P1
M \<in> Cl_P2
eligible_literal L P1 \<theta>
eligible_literal M P2 \<theta>
variable_disjoint P1 P2
Cl_P1 = cl_ecl P1
Cl_P2 = cl_ecl P2
\<not> is_a_variable u'
allowed_redex u' P1 \<theta>
C_fo = Ecl (subst_cl C' \<theta>) T'
orient_lit_inst M u v pos \<theta>
orient_lit_inst L t s polarity \<theta>
u \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
subterm t p u'
ck_unifier u' u \<theta> FirstOrder
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}
[PROOF STEP]
have "superposition P1 P2 C_fo \<theta> FirstOrder C'"
[PROOF STATE]
proof (prove)
using this:
L \<in> Cl_P1
M \<in> Cl_P2
eligible_literal L P1 \<theta>
eligible_literal M P2 \<theta>
variable_disjoint P1 P2
Cl_P1 = cl_ecl P1
Cl_P2 = cl_ecl P2
\<not> is_a_variable u'
allowed_redex u' P1 \<theta>
C_fo = Ecl (subst_cl C' \<theta>) T'
orient_lit_inst M u v pos \<theta>
orient_lit_inst L t s polarity \<theta>
u \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
subterm t p u'
ck_unifier u' u \<theta> FirstOrder
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}

goal (1 subgoal):
 1. superposition P1 P2 C_fo \<theta> FirstOrder C'
[PROOF STEP]
unfolding superposition_def
[PROOF STATE]
proof (prove)
using this:
L \<in> Cl_P1
M \<in> Cl_P2
eligible_literal L P1 \<theta>
eligible_literal M P2 \<theta>
variable_disjoint P1 P2
Cl_P1 = cl_ecl P1
Cl_P2 = cl_ecl P2
\<not> is_a_variable u'
allowed_redex u' P1 \<theta>
C_fo = Ecl (subst_cl C' \<theta>) T'
orient_lit_inst M u v pos \<theta>
orient_lit_inst L t s polarity \<theta>
u \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
subterm t p u'
ck_unifier u' u \<theta> FirstOrder
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set E \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
E = trms_ecl P1 \<union> trms_ecl P2 \<union> {r. \<exists>q. (q, p) \<in> pos_ord P1 t \<and> subterm t q r}

goal (1 subgoal):
 1. \<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 \<theta> \<and> eligible_literal M P2 \<theta> \<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 \<theta> \<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}) \<theta>)) FirstOrder \<and> C_fo = Ecl Cl_C trms_C \<and> orient_lit_inst M u v pos \<theta> \<and> orient_lit_inst L t s polarity \<theta> \<and> u \<lhd> \<theta> \<noteq> v \<lhd> \<theta> \<and> subterm t p u' \<and> ck_unifier u' u \<theta> FirstOrder \<and> replace_subterm t p v t' \<and> (FirstOrder = FirstOrder \<or> (subst_lit M \<theta>, subst_lit L \<theta>) \<in> lit_ord) \<and> (FirstOrder = FirstOrder \<or> strictly_maximal_literal P2 M \<theta>) \<and> L' = mk_lit polarity (Eq t' s) \<and> Cl_C = subst_cl C' \<theta> \<and> C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
superposition P1 P2 C_fo \<theta> FirstOrder C'

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>P = { P1, P2 }\<close>  \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
superposition P1 P2 C_fo \<theta> FirstOrder C'
P = {P1, P2}
P \<subseteq> S
[PROOF STEP]
have "(derivable C_fo P S \<theta> FirstOrder C')"
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C_fo \<theta> FirstOrder C'
P = {P1, P2}
P \<subseteq> S

goal (1 subgoal):
 1. derivable C_fo P S \<theta> FirstOrder C'
[PROOF STEP]
unfolding derivable_def
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C_fo \<theta> FirstOrder C'
P = {P1, P2}
P \<subseteq> S

goal (1 subgoal):
 1. (\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C_fo \<theta> FirstOrder C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derivable C_fo P S \<theta> FirstOrder C'

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(?Cl_C' = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<theta>))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>
[PROOF STEP]
have
      i: "(subst_cl ?Cl_C' \<eta>) =
      (subst_cl (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<theta>)) \<eta>"
[PROOF STATE]
proof (prove)
using this:
subst_cl C' \<theta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have ii: "(subst_cl (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<theta>) \<eta>)
      =  (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using composition_of_substs_cl [of "((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } ))" ]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) ?\<sigma>) ?\<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<sigma>)
      = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_cl [of \<sigma> "\<theta> \<lozenge> \<eta>" "((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } ))" ]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and i ii  \<open>Cl_C = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>
[PROOF STEP]
have "(subst_cl ?Cl_C' \<eta>) = Cl_C"
[PROOF STATE]
proof (prove)
using this:
subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<theta>) \<eta> = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_set T' \<eta>) \<subseteq> trms_C\<close>
      and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)\<close> \<open>(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
have "(trms_subsumes C_fo C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. trms_subsumes C_fo C \<eta>
[PROOF STEP]
unfolding trms_subsumes_def
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C \<and> subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_subsumes C_fo C \<eta>

goal (1 subgoal):
 1. \<exists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(derivable C_fo P S \<theta> FirstOrder C')\<close> and \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and hyp
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<Longrightarrow> False
[PROOF STEP]
have not_fact: "\<not> (\<exists>P1. ({ P1 } =  P \<and> factorization P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. ({ P1 } = P \<and> factorization P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C'

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = {P1}
factorization P1 C \<sigma> Ground C'
[PROOF STEP]
obtain L1 L2 L' t s u v Cl_P Cl_C trms_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))"
      "C = (Ecl Cl_C trms_C)"
      "trms_C  = (get_trms Cl_C
          (dom_trms Cl_C (subst_set ( (trms_ecl P1) \<union> (proper_subterms_of t) ) \<sigma>))) Ground"
      "(Cl_C = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } )) \<sigma>)"
      "(C' = ( (Cl_P - { L2 }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
P = {P1}
factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>L1 L2 Cl_C Cl_P t s u v L' trms_C. \<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); C = Ecl Cl_C trms_C; trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) Ground; 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 get_trms_def
[PROOF STATE]
proof (prove)
using this:
P = {P1}
\<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 = (if Ground = FirstOrder then filter_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) else dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>))) \<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' trms_C. \<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); C = Ecl Cl_C trms_C; trms_C = (if Ground = FirstOrder then filter_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) else dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)); Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>; C' = Cl_P - {L2} \<union> {L'}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[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)
C = Ecl Cl_C trms_C
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) Ground
Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>
C' = Cl_P - {L2} \<union> {L'}

goal (1 subgoal):
 1. \<exists>P1. {P1} = 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 " Unifier \<sigma> t u"
[PROOF STATE]
proof (prove)
using this:
ck_unifier t u \<sigma> Ground

goal (1 subgoal):
 1. Unifier \<sigma> t u
[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:
Unifier \<sigma> t u

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

goal (1 subgoal):
 1. t \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
unfolding Unifier_def
[PROOF STATE]
proof (prove)
using this:
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} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>
[PROOF STEP]
have "unify t u \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>

goal (1 subgoal):
 1. unify t u \<noteq> None
[PROOF STEP]
using MGU_exists
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>
\<forall>\<sigma>. ?t \<lhd> \<sigma> = ?s \<lhd> \<sigma> \<longrightarrow> unify ?t ?s \<noteq> None

goal (1 subgoal):
 1. unify t u \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unify t u \<noteq> None

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
unify t u \<noteq> None
[PROOF STEP]
obtain \<theta> where "unify t u = Some \<theta>"
[PROOF STATE]
proof (prove)
using this:
unify t u \<noteq> None

goal (1 subgoal):
 1. (\<And>\<theta>. unify t u = Some \<theta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unify t u = Some \<theta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
hence "min_IMGU \<theta> t u"
[PROOF STATE]
proof (prove)
using this:
unify t u = Some \<theta>

goal (1 subgoal):
 1. min_IMGU \<theta> t u
[PROOF STEP]
by (rule unify_computes_min_IMGU)
[PROOF STATE]
proof (state)
this:
min_IMGU \<theta> t u

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
with \<open>Unifier \<sigma> t u\<close>
[PROOF STATE]
proof (chain)
picking this:
Unifier \<sigma> t u
min_IMGU \<theta> t u
[PROOF STEP]
obtain \<eta> where "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> t u
min_IMGU \<theta> t u

goal (1 subgoal):
 1. (\<And>\<eta>. \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_IMGU_def IMGU_iff_Idem_and_MGU MGU_def
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> t u
(Idem \<theta> \<and> Unifier \<theta> t u \<and> (\<forall>\<theta>'. Unifier \<theta>' t u \<longrightarrow> (\<exists>\<gamma>. \<theta>' \<doteq> \<theta> \<lozenge> \<gamma>))) \<and> fst ` set \<theta> \<subseteq> vars_of t \<union> vars_of u \<and> range_vars \<theta> \<subseteq> vars_of t \<union> vars_of u

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

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

goal (1 subgoal):
 1. eligible_literal L1 P1 \<theta>
[PROOF STEP]
using lift_eligible_literal
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L1 P1 \<sigma>
\<lbrakk>eligible_literal ?L ?C ?\<sigma>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> eligible_literal ?L ?C ?\<theta>

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

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

goal (1 subgoal):
 1. ck_unifier t u \<theta> FirstOrder
[PROOF STEP]
unfolding ck_unifier_def
[PROOF STATE]
proof (prove)
using this:
min_IMGU \<theta> t u

goal (1 subgoal):
 1. if FirstOrder = FirstOrder then min_IMGU \<theta> t u else Unifier \<theta> t u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ck_unifier t u \<theta> FirstOrder

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst s \<sigma>) = (subst (subst s \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst v \<sigma>) = (subst (subst v \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. t \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<theta> \<noteq> v \<lhd> \<theta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>orient_lit_inst L1 t s pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s pos \<sigma>
[PROOF STEP]
have "orient_lit_inst L1 t s pos \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s pos \<sigma>

goal (1 subgoal):
 1. orient_lit_inst L1 t s pos \<theta>
[PROOF STEP]
using lift_orient_lit_inst
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s pos \<sigma>
\<lbrakk>orient_lit_inst ?L ?t ?s ?polarity ?\<theta>; ?\<theta> \<doteq> ?\<sigma> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> orient_lit_inst ?L ?t ?s ?polarity ?\<sigma>

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>orient_lit_inst L2 u v pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L2 u v pos \<sigma>
[PROOF STEP]
have "orient_lit_inst L2 u v pos \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L2 u v pos \<sigma>

goal (1 subgoal):
 1. orient_lit_inst L2 u v pos \<theta>
[PROOF STEP]
using lift_orient_lit_inst
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L2 u v pos \<sigma>
\<lbrakk>orient_lit_inst ?L ?t ?s ?polarity ?\<theta>; ?\<theta> \<doteq> ?\<sigma> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> orient_lit_inst ?L ?t ?s ?polarity ?\<sigma>

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

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain E where "E = (trms_ecl P1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E. E = trms_ecl P1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E = trms_ecl P1

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(Cl_C = (subst_cl C' \<sigma>))\<close>
      \<open>trms_C = (get_trms  Cl_C
          (dom_trms Cl_C (subst_set ( (trms_ecl P1) \<union> (proper_subterms_of t) ) \<sigma>))) Ground\<close>
[PROOF STATE]
proof (chain)
picking this:
E = trms_ecl P1
Cl_C = subst_cl C' \<sigma>
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) Ground
[PROOF STEP]
have "trms_C = (get_trms Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        (E \<union> (proper_subterms_of t))  \<sigma>)) Ground)"
[PROOF STATE]
proof (prove)
using this:
E = trms_ecl P1
Cl_C = subst_cl C' \<sigma>
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> proper_subterms_of t) \<sigma>)) Ground

goal (1 subgoal):
 1. trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> proper_subterms_of t) \<sigma>)) Ground
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> proper_subterms_of t) \<sigma>)) Ground

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?Cl_C' = "(subst_cl C' \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from  \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>trms_C = (get_trms Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        (E \<union> (proper_subterms_of t))  \<sigma>)) Ground)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> proper_subterms_of t) \<sigma>)) Ground
[PROOF STEP]
have "\<exists>T'. ( (subst_set T' \<eta>) \<subseteq> trms_C \<and> T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> (proper_subterms_of t)) \<theta>)) FirstOrder)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> proper_subterms_of t) \<sigma>)) Ground

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
[PROOF STEP]
using lift_irreducible_terms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> proper_subterms_of t) \<sigma>)) Ground
\<lbrakk>?T = get_trms ?C (dom_trms (subst_cl ?D ?\<sigma>) (subst_set ?E ?\<sigma>)) Ground; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> \<exists>T'. subst_set T' ?\<eta> \<subseteq> ?T \<and> T' = get_trms ?C' (dom_trms (subst_cl ?D ?\<theta>) (subst_set ?E ?\<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
[PROOF STEP]
obtain T' where "(subst_set T' \<eta>) \<subseteq> trms_C"
      and "T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> (proper_subterms_of t)) \<theta>)) FirstOrder"
[PROOF STATE]
proof (prove)
using this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>subst_set T' \<eta> \<subseteq> trms_C; T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_set T' \<eta> \<subseteq> trms_C
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain C_fo where "C_fo = (Ecl ?Cl_C' T')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C_fo. C_fo = Ecl (subst_cl C' \<theta>) T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. subst_cl C' \<theta> = subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl C' \<theta> = subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>C_fo = (Ecl ?Cl_C' T')\<close>
[PROOF STATE]
proof (chain)
picking this:
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "?Cl_C' = (cl_ecl C_fo)"
[PROOF STATE]
proof (prove)
using this:
C_fo = Ecl (subst_cl C' \<theta>) T'

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from
      \<open>eligible_literal L1 P1 \<theta>\<close>
      \<open>L1 \<in> (cl_ecl P1)\<close> \<open>L2 \<in> (cl_ecl P1) - { L1 }\<close> \<open>?Cl_C' = (cl_ecl C_fo)\<close> \<open>(Cl_P = (cl_ecl P1))\<close>
      \<open>(orient_lit_inst L1 t s pos \<theta>)\<close>
      \<open>(orient_lit_inst L2 u v pos \<theta>)\<close>
      \<open>((subst t \<theta>) \<noteq> (subst s \<theta>))\<close>
      \<open>(subst t \<theta>) \<noteq> (subst v \<theta>)\<close>
      \<open>(ck_unifier t u \<theta> FirstOrder)\<close>
      \<open>(L' = Neg (Eq s v))\<close>
      \<open>C_fo = (Ecl ?Cl_C' T')\<close>
      \<open>T' = get_trms?Cl_C'
        (dom_trms ?Cl_C' (subst_set (E \<union> (proper_subterms_of t)) \<theta>)) FirstOrder\<close>
      \<open>(?Cl_C' = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) \<theta>))\<close>
      \<open>C' = ( (Cl_P - { L2 }) \<union> { L' } )\<close>
      \<open>E = (trms_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
L2 \<in> cl_ecl P1 - {L1}
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s pos \<theta>
orient_lit_inst L2 u v pos \<theta>
t \<lhd> \<theta> \<noteq> s \<lhd> \<theta>
t \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
ck_unifier t u \<theta> FirstOrder
L' = Neg (Eq s v)
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>
C' = Cl_P - {L2} \<union> {L'}
E = trms_ecl P1
[PROOF STEP]
have "factorization P1 C_fo \<theta> FirstOrder C'"
[PROOF STATE]
proof (prove)
using this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
L2 \<in> cl_ecl P1 - {L1}
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s pos \<theta>
orient_lit_inst L2 u v pos \<theta>
t \<lhd> \<theta> \<noteq> s \<lhd> \<theta>
t \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
ck_unifier t u \<theta> FirstOrder
L' = Neg (Eq s v)
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>
C' = Cl_P - {L2} \<union> {L'}
E = trms_ecl P1

goal (1 subgoal):
 1. factorization P1 C_fo \<theta> FirstOrder C'
[PROOF STEP]
unfolding factorization_def
[PROOF STATE]
proof (prove)
using this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
L2 \<in> cl_ecl P1 - {L1}
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s pos \<theta>
orient_lit_inst L2 u v pos \<theta>
t \<lhd> \<theta> \<noteq> s \<lhd> \<theta>
t \<lhd> \<theta> \<noteq> v \<lhd> \<theta>
ck_unifier t u \<theta> FirstOrder
L' = Neg (Eq s v)
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> proper_subterms_of t) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>
C' = Cl_P - {L2} \<union> {L'}
E = trms_ecl P1

goal (1 subgoal):
 1. \<exists>L1 L2 L' t s u v Cl_P Cl_C trms_C. eligible_literal L1 P1 \<theta> \<and> L1 \<in> cl_ecl P1 \<and> L2 \<in> cl_ecl P1 - {L1} \<and> Cl_C = cl_ecl C_fo \<and> Cl_P = cl_ecl P1 \<and> orient_lit_inst L1 t s pos \<theta> \<and> orient_lit_inst L2 u v pos \<theta> \<and> t \<lhd> \<theta> \<noteq> s \<lhd> \<theta> \<and> t \<lhd> \<theta> \<noteq> v \<lhd> \<theta> \<and> ck_unifier t u \<theta> FirstOrder \<and> L' = Neg (Eq s v) \<and> (C_fo = 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) \<theta>)) FirstOrder) \<and> Cl_C = subst_cl C' \<theta> \<and> C' = Cl_P - {L2} \<union> {L'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
factorization P1 C_fo \<theta> FirstOrder C'

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>P = { P1 }\<close>  \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
factorization P1 C_fo \<theta> FirstOrder C'
P = {P1}
P \<subseteq> S
[PROOF STEP]
have "(derivable C_fo P S \<theta> FirstOrder C')"
[PROOF STATE]
proof (prove)
using this:
factorization P1 C_fo \<theta> FirstOrder C'
P = {P1}
P \<subseteq> S

goal (1 subgoal):
 1. derivable C_fo P S \<theta> FirstOrder C'
[PROOF STEP]
unfolding derivable_def
[PROOF STATE]
proof (prove)
using this:
factorization P1 C_fo \<theta> FirstOrder C'
P = {P1}
P \<subseteq> S

goal (1 subgoal):
 1. (\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C_fo \<theta> FirstOrder C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derivable C_fo P S \<theta> FirstOrder C'

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

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have ii: "(subst_cl (subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) \<theta>) \<eta>)
      =  (subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using composition_of_substs_cl [of "( (Cl_P - { L2 }) \<union> { L' } )" ]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) ?\<sigma>) ?\<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) \<sigma>)
      = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_cl [of \<sigma> "\<theta> \<lozenge> \<eta>" "( (Cl_P - { L2 }) \<union> { L' } )" ]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and i ii  \<open>Cl_C = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } ) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>
[PROOF STEP]
have "(subst_cl ?Cl_C' \<eta>) = Cl_C"
[PROOF STATE]
proof (prove)
using this:
subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P - {L2} \<union> {L'}) \<theta>) \<eta> = subst_cl (Cl_P - {L2} \<union> {L'}) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_set T' \<eta>) \<subseteq> trms_C\<close>
      and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)\<close> \<open>(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
have "(trms_subsumes C_fo C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. trms_subsumes C_fo C \<eta>
[PROOF STEP]
unfolding trms_subsumes_def
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C \<and> subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_subsumes C_fo C \<eta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(derivable C_fo P S \<theta> FirstOrder C')\<close> and \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and hyp
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>P1. {P1} = P \<and> factorization P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<Longrightarrow> False
[PROOF STEP]
have not_ref: "\<not> (\<exists>P1. ({ P1 } = P \<and> reflexion P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. ({ P1 } = P  \<and> reflexion P1 C \<sigma> Ground C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
{P1} = P
reflexion P1 C \<sigma> Ground C'
[PROOF STEP]
obtain L1 t s Cl_P Cl_C trms_C
  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)"
      "(C = (Ecl Cl_C trms_C))"
      "(trms_C = get_trms Cl_C
          (dom_trms Cl_C (subst_set ( (trms_ecl P1) \<union> { t } ) \<sigma>)) Ground)"
     "(Cl_C = (subst_cl ((Cl_P - { L1 }) )) \<sigma>)"
     "(C' = ((Cl_P - { L1 }) ))"
[PROOF STATE]
proof (prove)
using this:
{P1} = P
reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>L1 Cl_C Cl_P t s trms_C. \<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; C = Ecl Cl_C trms_C; trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) Ground; Cl_C = subst_cl (Cl_P - {L1}) \<sigma>; C' = Cl_P - {L1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding reflexion_def get_trms_def
[PROOF STATE]
proof (prove)
using this:
{P1} = P
\<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 = (if Ground = FirstOrder then filter_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) else dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) \<and> Cl_C = subst_cl C' \<sigma> \<and> C' = Cl_P - {L1}

goal (1 subgoal):
 1. (\<And>L1 Cl_C Cl_P t s trms_C. \<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; C = Ecl Cl_C trms_C; trms_C = (if Ground = FirstOrder then filter_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) else dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)); Cl_C = subst_cl (Cl_P - {L1}) \<sigma>; C' = Cl_P - {L1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[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
C = Ecl Cl_C trms_C
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) Ground
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>
C' = Cl_P - {L1}

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

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Unifier \<sigma> t s
[PROOF STEP]
have "(subst t \<sigma>) = (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> t s

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>
[PROOF STEP]
have "unify t s \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. unify t s \<noteq> None
[PROOF STEP]
using MGU_exists
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = s \<lhd> \<sigma>
\<forall>\<sigma>. ?t \<lhd> \<sigma> = ?s \<lhd> \<sigma> \<longrightarrow> unify ?t ?s \<noteq> None

goal (1 subgoal):
 1. unify t s \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unify t s \<noteq> None

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
unify t s \<noteq> None
[PROOF STEP]
obtain \<theta> where "unify t s = Some \<theta>"
[PROOF STATE]
proof (prove)
using this:
unify t s \<noteq> None

goal (1 subgoal):
 1. (\<And>\<theta>. unify t s = Some \<theta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unify t s = Some \<theta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
hence "min_IMGU \<theta> t s"
[PROOF STATE]
proof (prove)
using this:
unify t s = Some \<theta>

goal (1 subgoal):
 1. min_IMGU \<theta> t s
[PROOF STEP]
by (rule unify_computes_min_IMGU)
[PROOF STATE]
proof (state)
this:
min_IMGU \<theta> t s

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
with \<open>Unifier \<sigma> t s\<close>
[PROOF STATE]
proof (chain)
picking this:
Unifier \<sigma> t s
min_IMGU \<theta> t s
[PROOF STEP]
obtain \<eta> where "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> t s
min_IMGU \<theta> t s

goal (1 subgoal):
 1. (\<And>\<eta>. \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_IMGU_def IMGU_iff_Idem_and_MGU MGU_def
[PROOF STATE]
proof (prove)
using this:
Unifier \<sigma> t s
(Idem \<theta> \<and> Unifier \<theta> t s \<and> (\<forall>\<theta>'. Unifier \<theta>' t s \<longrightarrow> (\<exists>\<gamma>. \<theta>' \<doteq> \<theta> \<lozenge> \<gamma>))) \<and> fst ` set \<theta> \<subseteq> vars_of t \<union> vars_of s \<and> range_vars \<theta> \<subseteq> vars_of t \<union> vars_of s

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and \<open>(eligible_literal L1 P1 \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L1 P1 \<sigma>
[PROOF STEP]
have "eligible_literal L1 P1 \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L1 P1 \<sigma>

goal (1 subgoal):
 1. eligible_literal L1 P1 \<theta>
[PROOF STEP]
using lift_eligible_literal
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
eligible_literal L1 P1 \<sigma>
\<lbrakk>eligible_literal ?L ?C ?\<sigma>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> eligible_literal ?L ?C ?\<theta>

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>min_IMGU \<theta> t s\<close>
[PROOF STATE]
proof (chain)
picking this:
min_IMGU \<theta> t s
[PROOF STEP]
have "ck_unifier t s \<theta> FirstOrder"
[PROOF STATE]
proof (prove)
using this:
min_IMGU \<theta> t s

goal (1 subgoal):
 1. ck_unifier t s \<theta> FirstOrder
[PROOF STEP]
unfolding ck_unifier_def
[PROOF STATE]
proof (prove)
using this:
min_IMGU \<theta> t s

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>orient_lit_inst L1 t s neg \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s neg \<sigma>
[PROOF STEP]
have "orient_lit_inst L1 t s neg \<theta>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s neg \<sigma>

goal (1 subgoal):
 1. orient_lit_inst L1 t s neg \<theta>
[PROOF STEP]
using lift_orient_lit_inst
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
orient_lit_inst L1 t s neg \<sigma>
\<lbrakk>orient_lit_inst ?L ?t ?s ?polarity ?\<theta>; ?\<theta> \<doteq> ?\<sigma> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> orient_lit_inst ?L ?t ?s ?polarity ?\<sigma>

goal (1 subgoal):
 1. orient_lit_inst L1 t s neg \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst L1 t s neg \<theta>

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain E where "E = (trms_ecl P1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E. E = trms_ecl P1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E = trms_ecl P1

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(Cl_C = (subst_cl C' \<sigma>))\<close>
      \<open>trms_C = (get_trms Cl_C
          (dom_trms Cl_C (subst_set ( (trms_ecl P1)  \<union> { t } ) \<sigma>))) Ground\<close>
[PROOF STATE]
proof (chain)
picking this:
E = trms_ecl P1
Cl_C = subst_cl C' \<sigma>
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) Ground
[PROOF STEP]
have "trms_C = (get_trms Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        (E  \<union> { t })  \<sigma>)) Ground)"
[PROOF STATE]
proof (prove)
using this:
E = trms_ecl P1
Cl_C = subst_cl C' \<sigma>
trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<sigma>)) Ground

goal (1 subgoal):
 1. trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> {t}) \<sigma>)) Ground
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> {t}) \<sigma>)) Ground

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
let ?Cl_C' = "(subst_cl C' \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from  \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>trms_C = (get_trms  Cl_C
        (dom_trms (subst_cl C' \<sigma>) (subst_set
        (E  \<union> { t })  \<sigma>)) Ground)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> {t}) \<sigma>)) Ground
[PROOF STEP]
have "\<exists>T'. ( (subst_set T' \<eta>) \<subseteq> trms_C \<and> T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set (E  \<union> { t }) \<theta>)) FirstOrder)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> {t}) \<sigma>)) Ground

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
[PROOF STEP]
using lift_irreducible_terms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_C = get_trms Cl_C (dom_trms (subst_cl C' \<sigma>) (subst_set (E \<union> {t}) \<sigma>)) Ground
\<lbrakk>?T = get_trms ?C (dom_trms (subst_cl ?D ?\<sigma>) (subst_set ?E ?\<sigma>)) Ground; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> \<exists>T'. subst_set T' ?\<eta> \<subseteq> ?T \<and> T' = get_trms ?C' (dom_trms (subst_cl ?D ?\<theta>) (subst_set ?E ?\<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
[PROOF STEP]
obtain T' where "(subst_set T' \<eta>) \<subseteq> trms_C"
      and "T' = get_trms ?Cl_C'
    (dom_trms (subst_cl C' \<theta>) (subst_set (E  \<union> { t }) \<theta>)) FirstOrder"
[PROOF STATE]
proof (prove)
using this:
\<exists>T'. subst_set T' \<eta> \<subseteq> trms_C \<and> T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>subst_set T' \<eta> \<subseteq> trms_C; T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_set T' \<eta> \<subseteq> trms_C
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
obtain C_fo where "C_fo = (Ecl ?Cl_C' T')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C_fo. C_fo = Ecl (subst_cl C' \<theta>) T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>C_fo = (Ecl ?Cl_C' T')\<close>
[PROOF STATE]
proof (chain)
picking this:
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "?Cl_C' = (cl_ecl C_fo)"
[PROOF STATE]
proof (prove)
using this:
C_fo = Ecl (subst_cl C' \<theta>) T'

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

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from
      \<open>(eligible_literal L1 P1 \<theta>)\<close>
      \<open>(L1 \<in> (cl_ecl P1))\<close> \<open>?Cl_C' = (cl_ecl C_fo)\<close> \<open>(Cl_P = (cl_ecl P1))\<close>
      \<open>(orient_lit_inst L1 t s neg \<theta>)\<close>
      \<open>(ck_unifier t s \<theta> FirstOrder)\<close>
      \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
      \<open>(T' = get_trms  ?Cl_C'
          (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> { t }) \<theta>)) FirstOrder)\<close>
     \<open>(?Cl_C' = (subst_cl ((Cl_P - { L1 }) )) \<theta>)\<close>
     \<open>(C' = ((Cl_P - { L1 }) ))\<close>
     \<open>E = (trms_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s neg \<theta>
ck_unifier t s \<theta> FirstOrder
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>
C' = Cl_P - {L1}
E = trms_ecl P1
[PROOF STEP]
have "reflexion P1 C_fo \<theta> FirstOrder C'"
[PROOF STATE]
proof (prove)
using this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s neg \<theta>
ck_unifier t s \<theta> FirstOrder
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>
C' = Cl_P - {L1}
E = trms_ecl P1

goal (1 subgoal):
 1. reflexion P1 C_fo \<theta> FirstOrder C'
[PROOF STEP]
unfolding reflexion_def
[PROOF STATE]
proof (prove)
using this:
eligible_literal L1 P1 \<theta>
L1 \<in> cl_ecl P1
subst_cl C' \<theta> = cl_ecl C_fo
Cl_P = cl_ecl P1
orient_lit_inst L1 t s neg \<theta>
ck_unifier t s \<theta> FirstOrder
C_fo = Ecl (subst_cl C' \<theta>) T'
T' = get_trms (subst_cl C' \<theta>) (dom_trms (subst_cl C' \<theta>) (subst_set (E \<union> {t}) \<theta>)) FirstOrder
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>
C' = Cl_P - {L1}
E = trms_ecl P1

goal (1 subgoal):
 1. \<exists>L1 t s Cl_P Cl_C trms_C. eligible_literal L1 P1 \<theta> \<and> L1 \<in> cl_ecl P1 \<and> Cl_C = cl_ecl C_fo \<and> Cl_P = cl_ecl P1 \<and> orient_lit_inst L1 t s neg \<theta> \<and> ck_unifier t s \<theta> FirstOrder \<and> C_fo = Ecl Cl_C trms_C \<and> trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl P1 \<union> {t}) \<theta>)) FirstOrder \<and> Cl_C = subst_cl C' \<theta> \<and> C' = Cl_P - {L1}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
reflexion P1 C_fo \<theta> FirstOrder C'

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this \<open>{ P1 } = P\<close>  \<open>P \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
reflexion P1 C_fo \<theta> FirstOrder C'
{P1} = P
P \<subseteq> S
[PROOF STEP]
have "(derivable C_fo P S \<theta> FirstOrder C')"
[PROOF STATE]
proof (prove)
using this:
reflexion P1 C_fo \<theta> FirstOrder C'
{P1} = P
P \<subseteq> S

goal (1 subgoal):
 1. derivable C_fo P S \<theta> FirstOrder C'
[PROOF STEP]
unfolding derivable_def
[PROOF STATE]
proof (prove)
using this:
reflexion P1 C_fo \<theta> FirstOrder C'
{P1} = P
P \<subseteq> S

goal (1 subgoal):
 1. (\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C_fo \<theta> FirstOrder C') \<or> (\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C_fo \<theta> FirstOrder C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derivable C_fo P S \<theta> FirstOrder C'

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(?Cl_C' = (subst_cl ((Cl_P - { L1 }) )) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>
[PROOF STEP]
have
      i: "(subst_cl ?Cl_C' \<eta>) =
      (subst_cl (subst_cl ((Cl_P - { L1 }) ) \<theta>)) \<eta>"
[PROOF STATE]
proof (prove)
using this:
subst_cl C' \<theta> = subst_cl (Cl_P - {L1}) \<theta>

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
have ii: "(subst_cl (subst_cl ((Cl_P - { L1 }) ) \<theta>) \<eta>)
      =  (subst_cl ((Cl_P - { L1 }) ) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using composition_of_substs_cl [of "((Cl_P - { L1 }) )" ]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (Cl_P - {L1}) ?\<sigma>) ?\<eta> = subst_cl (Cl_P - {L1}) (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_cl((Cl_P - { L1 }) ) \<sigma>)
      = (subst_cl ((Cl_P - { L1 }) ) (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_cl [of \<sigma> "\<theta> \<lozenge> \<eta>" "((Cl_P - { L1 }) )" ]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<Longrightarrow> subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and i ii  \<open>Cl_C = (subst_cl ((Cl_P - { L1 }) ) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>
[PROOF STEP]
have "(subst_cl ?Cl_C' \<eta>) = Cl_C"
[PROOF STATE]
proof (prove)
using this:
subst_cl (Cl_P - {L1}) \<sigma> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
subst_cl (subst_cl C' \<theta>) \<eta> = subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta>
subst_cl (subst_cl (Cl_P - {L1}) \<theta>) \<eta> = subst_cl (Cl_P - {L1}) (\<theta> \<lozenge> \<eta>)
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>

goal (1 subgoal):
 1. subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl C' \<theta>) \<eta> = Cl_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_set T' \<eta>) \<subseteq> trms_C\<close>
      and \<open>(C = (Ecl Cl_C trms_C))\<close> and \<open>(C_fo = (Ecl ?Cl_C' T'))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'
[PROOF STEP]
have "(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)"
[PROOF STATE]
proof (prove)
using this:
subst_set T' \<eta> \<subseteq> trms_C
C = Ecl Cl_C trms_C
C_fo = Ecl (subst_cl C' \<theta>) T'

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

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_cl (cl_ecl C_fo) \<eta>) = (cl_ecl C)\<close>
        \<open>(subst_set (trms_ecl C_fo) \<eta>) \<subseteq> (trms_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
have "(trms_subsumes C_fo C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. trms_subsumes C_fo C \<eta>
[PROOF STEP]
unfolding trms_subsumes_def
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C
subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C

goal (1 subgoal):
 1. subst_cl (cl_ecl C_fo) \<eta> = cl_ecl C \<and> subst_set (trms_ecl C_fo) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_subsumes C_fo C \<eta>

goal (1 subgoal):
 1. \<exists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(derivable C_fo P S \<theta> FirstOrder C')\<close> and \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> and hyp
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trms_subsumes C_fo C \<eta>
derivable C_fo P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'

goal (1 subgoal):
 1. \<nexists>D \<theta> \<eta>. derivable D P S \<theta> FirstOrder C' \<and> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D C \<eta> \<Longrightarrow> False
[PROOF STEP]
from not_sup not_ref not_fact and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<nexists>P1 P2. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. {P1} = 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. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. {P1} = 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. P = {P1, P2} \<and> superposition P1 P2 C \<sigma> Ground C'
\<nexists>P1. {P1} = P \<and> reflexion P1 C \<sigma> Ground C'
\<nexists>P1. {P1} = 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