[STATEMENT]
lemma ground_superposition_is_sound :
  assumes "finite (cl_ecl P1)"
  assumes "finite (cl_ecl P2)"
  assumes "superposition P1 P2 C \<sigma> k C'"
  assumes "(ground_clause (subst_cl (cl_ecl C) \<theta>))"
  shows "set_entails_clause
    { (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>),
      (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) }
          (subst_cl (cl_ecl C) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?P1 = "(cl_ecl P1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?P2 = "(cl_ecl P2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?C = "(cl_ecl C)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> set_entails_clause
    { (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>),
      (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) }
          (subst_cl (cl_ecl C) \<theta>)"
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
obtain I
    where "validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)"
    and "validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)"
      and "\<not> (validate_clause I (subst_cl (cl_ecl C) \<theta>))" and "fo_interpretation I"
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)

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

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>); validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>); \<not> validate_clause I (subst_cl (cl_ecl C) \<theta>); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson insert_iff validate_clause_set.elims(2))
[PROOF STATE]
proof (state)
this:
validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
fo_interpretation I

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
obtain t s u v M p polarity t' u' L L'   where
    "orient_lit_inst M u v pos \<sigma>"
    and "orient_lit_inst L t s polarity \<sigma>"
    and "subterm t p u'"
    and "ck_unifier u' u \<sigma> k"
    and "replace_subterm t p v t'"
    and "L' = mk_lit polarity (Eq t' s)"
    and "?C = (subst_cl ((?P1 - { L }) \<union> ((?P2 - { M }) \<union> { L' } )) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C \<sigma> k C'

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

goal (1 subgoal):
 1. (\<And>M u v L t s polarity p u' t' L'. \<lbrakk>orient_lit_inst M u v pos \<sigma>; orient_lit_inst L t s polarity \<sigma>; subterm t p u'; ck_unifier u' u \<sigma> k; replace_subterm t p v t'; L' = mk_lit polarity (Eq t' s); cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst M u v pos \<sigma>
orient_lit_inst L t s polarity \<sigma>
subterm t p u'
ck_unifier u' u \<sigma> k
replace_subterm t p v t'
L' = mk_lit polarity (Eq t' s)
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?P1' = "(subst_cl (subst_cl ?P1 \<sigma>) \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?P2' = "(subst_cl (subst_cl ?P2 \<sigma>) \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
[PROOF STEP]
have "finite ?P1'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P2)
[PROOF STEP]
have "finite ?P2'"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P2)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?vars = "(vars_of_cl ?P1') \<union> (vars_of_cl ?P2')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>finite ?P1'\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
[PROOF STEP]
have "finite (vars_of_cl ?P1')"
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)

goal (1 subgoal):
 1. finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>))
[PROOF STEP]
using set_of_variables_is_finite_cl [of ?P1']
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
finite (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<Longrightarrow> finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>))

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>finite ?P2'\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
[PROOF STEP]
have "finite (vars_of_cl ?P2')"
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)

goal (1 subgoal):
 1. finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))
[PROOF STEP]
using set_of_variables_is_finite_cl [of ?P2']
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
finite (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<Longrightarrow> finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>finite (vars_of_cl ?P1')\<close> and \<open>finite (vars_of_cl ?P2')\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>))
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))
[PROOF STEP]
have "finite ?vars"
[PROOF STATE]
proof (prove)
using this:
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>))
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))
[PROOF STEP]
obtain \<eta> where "ground_on ?vars \<eta>"
[PROOF STATE]
proof (prove)
using this:
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))

goal (1 subgoal):
 1. (\<And>\<eta>. ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ground_subst_exists
[PROOF STATE]
proof (prove)
using this:
finite (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>))
finite ?V \<Longrightarrow> \<exists>\<sigma>. ground_on ?V \<sigma>

goal (1 subgoal):
 1. (\<And>\<eta>. ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
have "ground_on (vars_of_cl ?P1') \<eta>"
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
unfolding ground_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>). ground_term (Var x \<lhd> \<eta>)

goal (1 subgoal):
 1. \<forall>x\<in>vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>). ground_term (Var x \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
have "ground_clause (subst_cl
        (subst_cl (subst_cl ?P1 \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
using ground_substs_yield_ground_clause
        [of "(subst_cl (subst_cl ?P1 \<sigma>) \<theta>)" \<eta>]
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta>
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)) \<eta> \<Longrightarrow> ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_on ?vars \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
have "ground_on (vars_of_cl ?P2') \<eta>"
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
unfolding ground_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars_of_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<union> vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>). ground_term (Var x \<lhd> \<eta>)

goal (1 subgoal):
 1. \<forall>x\<in>vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>). ground_term (Var x \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>
[PROOF STEP]
have "ground_clause (subst_cl
        (subst_cl (subst_cl ?P2 \<sigma>) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>

goal (1 subgoal):
 1. ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
using ground_substs_yield_ground_clause
        [of "(subst_cl (subst_cl ?P2 \<sigma>) \<theta>)" \<eta>]
[PROOF STATE]
proof (prove)
using this:
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta>
ground_on (vars_of_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)) \<eta> \<Longrightarrow> ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)\<close>
    and \<open>validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
[PROOF STEP]
have "validate_ground_clause I ?P1''"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
obtain l1' where "l1' \<in> ?P1''" and "validate_ground_lit I l1'"
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
have "?P2'' = (subst_cl (subst_cl ?P2 ?\<sigma>'') \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta> = subst_cl (subst_cl (cl_ecl P2) (\<sigma> \<lozenge> \<theta>)) \<eta>
[PROOF STEP]
using composition_of_substs_cl [of ?P2]
[PROOF STATE]
proof (prove)
using this:
subst_cl (subst_cl (cl_ecl P2) ?\<sigma>) ?\<eta> = subst_cl (cl_ecl P2) (?\<sigma> \<lozenge> ?\<eta>)

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

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

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)\<close> \<open>validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
[PROOF STEP]
have "validate_ground_clause I ?P2''"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)
[PROOF STEP]
obtain l2' where "l2' \<in> ?P2''" and "validate_ground_lit I l2'"
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>l1' \<in> ?P1''\<close> and \<open>?P1'' = (subst_cl ?P1 ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
l1' \<in> subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl P1) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
obtain l1 where
    "l1 \<in> ?P1" and "l1' = (subst_lit l1 ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
l1' \<in> subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl P1) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>l2' \<in> ?P2''\<close> and \<open>?P2'' = (subst_cl ?P2 ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
l2' \<in> subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl P2) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
obtain l2 where
    "l2 \<in> ?P2" and "l2' = (subst_lit l2 ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
l2' \<in> subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta>
subst_cl (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) \<eta> = subst_cl (cl_ecl P2) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
let ?C' = "(subst_cl (subst_cl ?C \<theta>) \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_clause (subst_cl ?C \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
have
    "(subst_cl ?C \<theta>) = (subst_cl (subst_cl ?C \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl C) \<theta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
have "\<not> validate_ground_clause I ?C'"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. \<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
[PROOF STEP]
by (metis assms(4) substs_preserve_ground_clause validate_clause.simps)
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
have "l1 = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l1 = L
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l1 \<noteq> L \<Longrightarrow> False
[PROOF STEP]
assume "l1 \<noteq> L"
[PROOF STATE]
proof (state)
this:
l1 \<noteq> L

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

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

goal (1 subgoal):
 1. l1 \<noteq> L \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit l1 \<sigma> \<in> cl_ecl C
[PROOF STEP]
have "(subst_lit (subst_lit (subst_lit l1 \<sigma>) \<theta>) \<eta>)
      \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
subst_lit l1 \<sigma> \<in> cl_ecl C

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

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

goal (1 subgoal):
 1. l1' \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
[PROOF STEP]
by (simp add: composition_of_substs_lit)
[PROOF STATE]
proof (state)
this:
l1' \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>

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

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

goal (1 subgoal):
 1. l1 \<noteq> L \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
have "l2 = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l2 = M
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l2 \<noteq> M \<Longrightarrow> False
[PROOF STEP]
assume "l2 \<noteq> M"
[PROOF STATE]
proof (state)
this:
l2 \<noteq> M

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

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

goal (1 subgoal):
 1. l2 \<noteq> M \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit l2 \<sigma> \<in> cl_ecl C
[PROOF STEP]
have "(subst_lit (subst_lit (subst_lit l2 \<sigma>) \<theta>) \<eta>)
      \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
subst_lit l2 \<sigma> \<in> cl_ecl C

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

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

goal (1 subgoal):
 1. l2' \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
[PROOF STEP]
by (simp add: composition_of_substs_lit)
[PROOF STATE]
proof (state)
this:
l2' \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>

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

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

goal (1 subgoal):
 1. l2 \<noteq> M \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst M u v pos \<sigma>\<close> and \<open>l2 = M\<close> and \<open>fo_interpretation I\<close>
    and \<open>validate_ground_lit I l2'\<close> and \<open>l2' = (subst_lit l2 ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst M u v pos \<sigma>
l2 = M
fo_interpretation I
validate_ground_lit I l2'
l2' = subst_lit l2 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "I (subst u ?\<sigma>') (subst v ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M u v pos \<sigma>
l2 = M
fo_interpretation I
validate_ground_lit I l2'
l2' = subst_lit l2 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>subterm t p u'\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t p u'
[PROOF STEP]
have
    "subterm (subst t ?\<sigma>') p (subst u' ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
subterm t p u'

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>ck_unifier u' u \<sigma> k\<close>
[PROOF STATE]
proof (chain)
picking this:
ck_unifier u' u \<sigma> k
[PROOF STEP]
have "(subst u \<sigma>) = (subst u' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
ck_unifier u' u \<sigma> k

goal (1 subgoal):
 1. u \<lhd> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
using ck_unifier_thm [of u' u \<sigma> k]
[PROOF STATE]
proof (prove)
using this:
ck_unifier u' u \<sigma> k
ck_unifier u' u \<sigma> k \<Longrightarrow> 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. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u \<lhd> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
have "(subst (subst (subst u \<sigma>) \<theta>) \<eta>)
    = (subst (subst (subst u' \<sigma>) \<theta> ) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<sigma> = u' \<lhd> \<sigma>

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u' \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
have "(subst u ?\<sigma>') = (subst u' ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u' \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>

goal (1 subgoal):
 1. u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
[PROOF STEP]
using composition_of_substs
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta> = u' \<lhd> \<sigma> \<lhd> \<theta> \<lhd> \<eta>
?t \<lhd> ?\<sigma> \<lhd> ?\<eta> = ?t \<lhd> ?\<sigma> \<lozenge> ?\<eta>

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst u ?\<sigma>') = (subst u' ?\<sigma>')\<close>
    and \<open>I (subst u ?\<sigma>') (subst v ?\<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "I (subst u' ?\<sigma>') (subst v ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta> = u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>
I (u \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>subterm t p u'\<close>
    and \<open>I (subst u' ?\<sigma>') (subst v ?\<sigma>')\<close>
    and \<open>fo_interpretation I\<close>
    and \<open>replace_subterm t p v t'\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t p u'
I (u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
fo_interpretation I
replace_subterm t p v t'
[PROOF STEP]
have "I (subst t ?\<sigma>') (subst t' ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
subterm t p u'
I (u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
fo_interpretation I
replace_subterm t p v t'

goal (1 subgoal):
 1. I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
unfolding fo_interpretation_def
[PROOF STATE]
proof (prove)
using this:
subterm t p u'
I (u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
congruence I
replace_subterm t p v t'

goal (1 subgoal):
 1. I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
[PROOF STEP]
using replacement_preserves_congruences [of I u' ?\<sigma>' v t p t']
[PROOF STATE]
proof (prove)
using this:
subterm t p u'
I (u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
congruence I
replace_subterm t p v t'
\<lbrakk>congruence I; I (u' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (v \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>); subterm t p u'; replace_subterm t p v t'\<rbrakk> \<Longrightarrow> I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>l1 = L\<close> and \<open>fo_interpretation I\<close> and \<open>validate_ground_lit I l1'\<close>
    and \<open>l1' = (subst_lit l1 ?\<sigma>')\<close>
    and \<open>orient_lit_inst L t s polarity \<sigma>\<close>
    and \<open>I (subst t ?\<sigma>') (subst t' ?\<sigma>')\<close>
    and \<open>L' =  mk_lit polarity (Eq t' s)\<close>
[PROOF STATE]
proof (chain)
picking this:
l1 = L
fo_interpretation I
validate_ground_lit I l1'
l1' = subst_lit l1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
orient_lit_inst L t s polarity \<sigma>
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
L' = mk_lit polarity (Eq t' s)
[PROOF STEP]
have "validate_ground_lit I (subst_lit L' ?\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
l1 = L
fo_interpretation I
validate_ground_lit I l1'
l1' = subst_lit l1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
orient_lit_inst L t s polarity \<sigma>
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
L' = mk_lit polarity (Eq t' s)

goal (1 subgoal):
 1. validate_ground_lit I (subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
[PROOF STEP]
using orient_lit_semantics_replacement [of I L t s polarity \<sigma> ?\<sigma>' t']
[PROOF STATE]
proof (prove)
using this:
l1 = L
fo_interpretation I
validate_ground_lit I l1'
l1' = subst_lit l1 (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
orient_lit_inst L t s polarity \<sigma>
I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)
L' = mk_lit polarity (Eq t' s)
\<lbrakk>fo_interpretation I; orient_lit_inst L t s polarity \<sigma>; validate_ground_lit I (subst_lit L (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)); I (t \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) (t' \<lhd> \<sigma> \<lozenge> \<theta> \<lozenge> \<eta>)\<rbrakk> \<Longrightarrow> validate_ground_lit I (subst_lit (mk_lit polarity (Eq t' s)) (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from \<open>?C = (subst_cl ((?P1 - { L }) \<union> ((?P2 - { M }) \<union> { L' } )) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
[PROOF STEP]
have "subst_lit L' \<sigma> \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_lit L' \<sigma> \<in> cl_ecl C
[PROOF STEP]
have "subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
subst_lit L' \<sigma> \<in> cl_ecl C

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

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
[PROOF STEP]
have "subst_lit L' ?\<sigma>' \<in> ?C'"
[PROOF STATE]
proof (prove)
using this:
subst_lit (subst_lit (subst_lit L' \<sigma>) \<theta>) \<eta> \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>

goal (1 subgoal):
 1. subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
[PROOF STEP]
by (simp add: composition_of_substs_lit)
[PROOF STATE]
proof (state)
this:
subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validate_ground_lit I (subst_lit L' ?\<sigma>')\<close> and \<open>\<not>validate_ground_clause I ?C'\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
validate_ground_lit I (subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>) \<in> subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
validate_ground_lit I (subst_lit L' (\<sigma> \<lozenge> \<theta> \<lozenge> \<eta>))
\<not> validate_ground_clause I (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma superposition_is_sound :
  assumes "finite (cl_ecl P1)"
  assumes "finite (cl_ecl P2)"
  assumes "superposition P1 P2 C \<sigma> k C'"
  shows "set_entails_clause { cl_ecl P1, cl_ecl P2 } (cl_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
let ?P1 = "(cl_ecl P1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
let ?P2 = "(cl_ecl P2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
let ?C = "(cl_ecl C)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> set_entails_clause { cl_ecl P1, cl_ecl P2 } (cl_ecl C)"
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)

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

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (cl_ecl P1); validate_clause I (cl_ecl P2); \<not> validate_clause I (cl_ecl C); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I {cl_ecl P1, cl_ecl P2} \<longrightarrow> validate_clause I (cl_ecl C))

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>validate_clause I (cl_ecl P1); validate_clause I (cl_ecl P2); \<not> validate_clause I (cl_ecl C); fo_interpretation I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson insert_iff validate_clause_set.elims(2))
[PROOF STATE]
proof (state)
this:
validate_clause I (cl_ecl P1)
validate_clause I (cl_ecl P2)
\<not> validate_clause I (cl_ecl C)
fo_interpretation I

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

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

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
have P1_true: "validate_clause I (subst_cl (subst_cl ?P1 \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
[PROOF STEP]
using \<open>validate_clause I (cl_ecl P1)\<close> instances_are_entailed
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl P1)
validate_clause ?I ?C \<Longrightarrow> validate_clause ?I (subst_cl ?C ?\<sigma>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
have P2_true: "validate_clause I (subst_cl (subst_cl ?P2 \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
[PROOF STEP]
using \<open>validate_clause I (cl_ecl P2)\<close> instances_are_entailed
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl P2)
validate_clause ?I ?C \<Longrightarrow> validate_clause ?I (subst_cl ?C ?\<sigma>)

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

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
have "\<not> (validate_clause I (subst_cl ?C \<theta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
by (metis \<open>\<not> validate_ground_clause I (subst_cl (cl_ecl C) \<theta>)\<close>
        \<open>ground_clause (subst_cl (cl_ecl C) \<theta>)\<close>
        substs_preserve_ground_clause validate_clause.elims(1))
[PROOF STATE]
proof (state)
this:
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
let ?S = "{ (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>),
      (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>) }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from P1_true and P2_true
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)
[PROOF STEP]
have "validate_clause_set I ?S"
[PROOF STATE]
proof (prove)
using this:
validate_clause I (subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>)
validate_clause I (subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>)

goal (1 subgoal):
 1. validate_clause_set I {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>}
[PROOF STEP]
by (metis insert_iff singletonD validate_clause_set.elims(3))
[PROOF STATE]
proof (state)
this:
validate_clause_set I {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>}

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> (validate_clause I (subst_cl ?C \<theta>))\<close> \<open>fo_interpretation I\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause_set I {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>}
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
fo_interpretation I
[PROOF STEP]
have "\<not> set_entails_clause ?S (subst_cl (cl_ecl C) \<theta>)"
[PROOF STATE]
proof (prove)
using this:
validate_clause_set I {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>}
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
fo_interpretation I

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
using set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
validate_clause_set I {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>}
\<not> validate_clause I (subst_cl (cl_ecl C) \<theta>)
fo_interpretation I
set_entails_clause ?S ?C = (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I ?S \<longrightarrow> validate_clause I ?C)

goal (1 subgoal):
 1. \<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. \<not> set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this and assms(1) and assms(2) and assms(3) and
    \<open>(ground_clause (subst_cl ?C \<theta>))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'
ground_clause (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'
ground_clause (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. False
[PROOF STEP]
using ground_superposition_is_sound
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause {subst_cl (subst_cl (cl_ecl P1) \<sigma>) \<theta>, subst_cl (subst_cl (cl_ecl P2) \<sigma>) \<theta>} (subst_cl (cl_ecl C) \<theta>)
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'
ground_clause (subst_cl (cl_ecl C) \<theta>)
\<lbrakk>finite (cl_ecl ?P1.0); finite (cl_ecl ?P2.0); superposition ?P1.0 ?P2.0 ?C ?\<sigma> ?k ?C'; ground_clause (subst_cl (cl_ecl ?C) ?\<theta>)\<rbrakk> \<Longrightarrow> set_entails_clause {subst_cl (subst_cl (cl_ecl ?P1.0) ?\<sigma>) ?\<theta>, subst_cl (subst_cl (cl_ecl ?P2.0) ?\<sigma>) ?\<theta>} (subst_cl (cl_ecl ?C) ?\<theta>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma superposition_preserves_finiteness:
  assumes "finite (cl_ecl P1)"
  assumes "finite (cl_ecl P2)"
  assumes "superposition P1 P2 C \<sigma> k C'"
  shows "finite (cl_ecl C) \<and> (finite C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
obtain L M L' where
    def_C: "(cl_ecl C) = (subst_cl (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } )) \<sigma>)"
    and def_C': "C' = (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C \<sigma> k C'

goal (1 subgoal):
 1. (\<And>L M L'. \<lbrakk>cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>; C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using superposition_def
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C \<sigma> k C'
superposition ?P1.0 ?P2.0 ?C ?\<sigma> ?k ?C' = (\<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.0 ?\<sigma> \<and> eligible_literal M ?P2.0 ?\<sigma> \<and> variable_disjoint ?P1.0 ?P2.0 \<and> Cl_P1 = cl_ecl ?P1.0 \<and> Cl_P2 = cl_ecl ?P2.0 \<and> \<not> is_a_variable u' \<and> allowed_redex u' ?P1.0 ?\<sigma> \<and> trms_C = get_trms Cl_C (dom_trms Cl_C (subst_set (trms_ecl ?P1.0 \<union> trms_ecl ?P2.0 \<union> {r. \<exists>q. (q, p) \<in> pos_ord ?P1.0 t \<and> subterm t q r}) ?\<sigma>)) ?k \<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> ?k \<and> replace_subterm t p v t' \<and> (?k = FirstOrder \<or> (subst_lit M ?\<sigma>, subst_lit L ?\<sigma>) \<in> lit_ord) \<and> (?k = FirstOrder \<or> strictly_maximal_literal ?P2.0 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 M L'. \<lbrakk>cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>; C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(1) and assms(2)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
finite (cl_ecl P2)
[PROOF STEP]
have "finite (((cl_ecl P1) - { L }) \<union> (((cl_ecl P2) - { M }) \<union> { L' } ))"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P2)

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from this and def_C def_C'
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using substs_preserve_finiteness
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'}))
cl_ecl C = subst_cl (cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})) \<sigma>
C' = cl_ecl P1 - {L} \<union> (cl_ecl P2 - {M} \<union> {L'})
finite ?C \<Longrightarrow> finite (subst_cl ?C ?\<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflexion_preserves_finiteness:
  assumes "finite (cl_ecl P1)"
  assumes "reflexion P1 C \<sigma> k C'"
  shows "finite (cl_ecl C) \<and> (finite C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
reflexion P1 C \<sigma> k C'
[PROOF STEP]
obtain L1 where
    def_C: "(cl_ecl C) = (subst_cl ((cl_ecl P1) - { L1 }) \<sigma>)"
    and def_C': "C' = ((cl_ecl P1) - { L1 })"
[PROOF STATE]
proof (prove)
using this:
reflexion P1 C \<sigma> k C'

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

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
[PROOF STEP]
have "finite ((cl_ecl P1) - { L1 })"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from this and def_C def_C'
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1 - {L1})
cl_ecl C = subst_cl (cl_ecl P1 - {L1}) \<sigma>
C' = cl_ecl P1 - {L1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L1})
cl_ecl C = subst_cl (cl_ecl P1 - {L1}) \<sigma>
C' = cl_ecl P1 - {L1}

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using substs_preserve_finiteness
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L1})
cl_ecl C = subst_cl (cl_ecl P1 - {L1}) \<sigma>
C' = cl_ecl P1 - {L1}
finite ?C \<Longrightarrow> finite (subst_cl ?C ?\<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma factorization_preserves_finiteness:
  assumes "finite (cl_ecl P1)"
  assumes "factorization P1 C \<sigma> k C'"
  shows "finite (cl_ecl C) \<and> (finite C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
factorization P1 C \<sigma> k C'
[PROOF STEP]
obtain L2 L' where
    def_C: "(cl_ecl C) = (subst_cl ( ((cl_ecl P1) - { L2 }) \<union> { L' } ) \<sigma>)"
    and def_C': "C' = ( ((cl_ecl P1) - { L2 }) \<union> { L' } )"
[PROOF STATE]
proof (prove)
using this:
factorization P1 C \<sigma> k C'

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

goal (1 subgoal):
 1. (\<And>L2 L'. \<lbrakk>cl_ecl C = subst_cl (cl_ecl P1 - {L2} \<union> {L'}) \<sigma>; C' = cl_ecl P1 - {L2} \<union> {L'}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl C = subst_cl (cl_ecl P1 - {L2} \<union> {L'}) \<sigma>
C' = cl_ecl P1 - {L2} \<union> {L'}

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1)
[PROOF STEP]
have "(finite (((cl_ecl P1) - { L2 }) \<union> { L' }))"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
from this and def_C def_C'
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl P1 - {L2} \<union> {L'})
cl_ecl C = subst_cl (cl_ecl P1 - {L2} \<union> {L'}) \<sigma>
C' = cl_ecl P1 - {L2} \<union> {L'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L2} \<union> {L'})
cl_ecl C = subst_cl (cl_ecl P1 - {L2} \<union> {L'}) \<sigma>
C' = cl_ecl P1 - {L2} \<union> {L'}

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using substs_preserve_finiteness
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1 - {L2} \<union> {L'})
cl_ecl C = subst_cl (cl_ecl P1 - {L2} \<union> {L'}) \<sigma>
C' = cl_ecl P1 - {L2} \<union> {L'}
finite ?C \<Longrightarrow> finite (subst_cl ?C ?\<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derivable_clauses_are_finite:
  assumes "derivable C P S \<sigma> k C'"
  assumes "\<forall>x \<in> P. (finite (cl_ecl x))"
  shows "finite (cl_ecl C) \<and> (finite C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (finite (cl_ecl C) \<and> finite C') \<Longrightarrow> False
[PROOF STEP]
assume hyp: "\<not> (finite (cl_ecl C)  \<and> (finite C'))"
[PROOF STATE]
proof (state)
this:
\<not> (finite (cl_ecl C) \<and> finite C')

goal (1 subgoal):
 1. \<not> (finite (cl_ecl C) \<and> finite C') \<Longrightarrow> False
[PROOF STEP]
have not_sup: "\<not> (\<exists>P1 P2. (P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1 P2. (P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'

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

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

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

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

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

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

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using superposition_preserves_finiteness [of P1 P2 C \<sigma>]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'
\<lbrakk>finite (cl_ecl P1); finite (cl_ecl P2); superposition P1 P2 C \<sigma> ?k ?C'\<rbrakk> \<Longrightarrow> finite (cl_ecl C) \<and> finite ?C'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using hyp
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl C) \<and> finite C'
\<not> (finite (cl_ecl C) \<and> finite C')

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

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

goal (1 subgoal):
 1. \<not> (finite (cl_ecl C) \<and> finite C') \<Longrightarrow> False
[PROOF STEP]
have not_ref: "\<not> (\<exists>P1. (P1 \<in> P \<and> reflexion P1 C \<sigma> k C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> k C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. (P1 \<in> P \<and> reflexion P1 C \<sigma> k C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> k C'

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

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

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

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

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using reflexion_preserves_finiteness [of P1 C \<sigma>]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
reflexion P1 C \<sigma> k C'
\<lbrakk>finite (cl_ecl P1); reflexion P1 C \<sigma> ?k ?C'\<rbrakk> \<Longrightarrow> finite (cl_ecl C) \<and> finite ?C'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using hyp
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl C) \<and> finite C'
\<not> (finite (cl_ecl C) \<and> finite C')

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

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

goal (1 subgoal):
 1. \<not> (finite (cl_ecl C) \<and> finite C') \<Longrightarrow> False
[PROOF STEP]
have not_fact: "\<not> (\<exists>P1. (P1 \<in> P \<and> factorization P1 C \<sigma> k C'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> k C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists>P1. (P1 \<in> P \<and>  factorization P1 C \<sigma> k C'))"
[PROOF STATE]
proof (state)
this:
\<exists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> k C'

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

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

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

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

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

goal (1 subgoal):
 1. finite (cl_ecl C) \<and> finite C'
[PROOF STEP]
using  factorization_preserves_finiteness [of P1 C \<sigma>]
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl P1)
factorization P1 C \<sigma> k C'
\<lbrakk>finite (cl_ecl P1); factorization P1 C \<sigma> ?k ?C'\<rbrakk> \<Longrightarrow> finite (cl_ecl C) \<and> finite ?C'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using hyp
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl C) \<and> finite C'
\<not> (finite (cl_ecl C) \<and> finite C')

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

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

goal (1 subgoal):
 1. \<not> (finite (cl_ecl C) \<and> finite C') \<Longrightarrow> False
[PROOF STEP]
from not_sup not_ref not_fact and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> k C'
derivable C P S \<sigma> k C'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<nexists>P1 P2. P1 \<in> P \<and> P2 \<in> P \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> P \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> P \<and> factorization P1 C \<sigma> k C'
derivable C P S \<sigma> k C'

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

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

goal:
No subgoals!
[PROOF STEP]
qed