[STATEMENT]
lemma derivable_clauses_lemma:
  assumes "derivable C P S \<sigma> k C'"
  shows "((cl_ecl C) = (subst_cl C' \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_ecl C = subst_cl C' \<sigma>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cl_ecl C \<noteq> subst_cl C' \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume hyp: "\<not> ((cl_ecl C) = (subst_cl C' \<sigma>))"
[PROOF STATE]
proof (state)
this:
cl_ecl C \<noteq> subst_cl C' \<sigma>

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>Cl_C = (subst_cl ((Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } )) \<sigma>)\<close>
      \<open>(C' = (Cl_P1 - { L }) \<union> ((Cl_P2 - { M }) \<union> { L' } ))\<close> \<open>C = (Ecl Cl_C T)\<close> hyp
[PROOF STATE]
proof (chain)
picking this:
Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Cl_C = subst_cl (Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})) \<sigma>
C' = Cl_P1 - {L} \<union> (Cl_P2 - {M} \<union> {L'})
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>

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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>Cl_C = (subst_cl ((Cl_P - { L1 }) )) \<sigma>\<close>
      \<open>(C' = ((Cl_P - { L1 }) ))\<close> \<open>C = (Ecl Cl_C T)\<close> hyp
[PROOF STATE]
proof (chain)
picking this:
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>
C' = Cl_P - {L1}
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Cl_C = subst_cl (Cl_P - {L1}) \<sigma>
C' = Cl_P - {L1}
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>

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> S \<and> reflexion P1 C \<sigma> k C'

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>Cl_C = (subst_cl ( (Cl_P - { L2 }) \<union> { L' } )) \<sigma>\<close>
      \<open>C' = ( (Cl_P - { L2 }) \<union> { L' } )\<close> \<open>C = (Ecl Cl_C T)\<close> hyp
[PROOF STATE]
proof (chain)
picking this:
Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>
C' = Cl_P - {L2} \<union> {L'}
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Cl_C = subst_cl (Cl_P - {L2} \<union> {L'}) \<sigma>
C' = Cl_P - {L2} \<union> {L'}
C = Ecl Cl_C T
cl_ecl C \<noteq> subst_cl C' \<sigma>

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> S \<and> factorization P1 C \<sigma> k C'

goal (1 subgoal):
 1. cl_ecl C \<noteq> subst_cl C' \<sigma> \<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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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


[STATEMENT]
lemma substs_preserves_decompose_literal:
  assumes "decompose_literal L t s polarity"
  shows "decompose_literal (subst_lit L \<eta>) (subst t \<eta>) (subst s \<eta>) polarity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?L = "(subst_lit L \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?t = "(subst t \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?s = "(subst s \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
have "polarity = pos \<or> polarity = neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polarity = pos \<or> polarity = neg
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
 2. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
assume "polarity = pos"
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
 2. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
decompose_literal L t s polarity
[PROOF STEP]
have "L = Pos (Eq t s) \<or> L = Pos (Eq s t)"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
decompose_literal L t s polarity

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

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
 2. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from \<open>L = Pos (Eq t s) \<or> L = Pos (Eq s t)\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
have "?L = Pos (Eq ?t ?s) \<or> ?L = Pos (Eq ?s ?t)"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
 2. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from this \<open>polarity = pos\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<eta> = Pos (Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>)) \<or> subst_lit L \<eta> = Pos (Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>))
polarity = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<eta> = Pos (Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>)) \<or> subst_lit L \<eta> = Pos (Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>))
polarity = pos

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
unfolding decompose_literal_def
      decompose_equation_def
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<eta> = Pos (Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>)) \<or> subst_lit L \<eta> = Pos (Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>))
polarity = pos

goal (1 subgoal):
 1. \<exists>e. polarity = pos \<and> subst_lit L \<eta> = Pos e \<and> (e = Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>) \<or> e = Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>)) \<or> polarity = neg \<and> subst_lit L \<eta> = Neg e \<and> (e = Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>) \<or> e = Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
assume "polarity = neg"
[PROOF STATE]
proof (state)
this:
polarity = neg

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
decompose_literal L t s polarity
[PROOF STEP]
have "L = Neg (Eq t s) \<or> L = Neg (Eq s t)"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
decompose_literal L t s polarity

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

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from this \<open>polarity = neg\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
polarity = neg

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
unfolding decompose_literal_def
      decompose_equation_def
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
polarity = neg

goal (1 subgoal):
 1. \<exists>e. polarity = pos \<and> subst_lit L \<eta> = Pos e \<and> (e = Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>) \<or> e = Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>)) \<or> polarity = neg \<and> subst_lit L \<eta> = Neg e \<and> (e = Eq (t \<lhd> \<eta>) (s \<lhd> \<eta>) \<or> e = Eq (s \<lhd> \<eta>) (t \<lhd> \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
decompose_literal (subst_lit L \<eta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma substs_preserve_dom_trm:
  assumes "dom_trm t C"
  shows "dom_trm (subst t \<sigma>) (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?t = "(subst t \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
dom_trm t C
[PROOF STEP]
have "(\<exists> L u v p. (L \<in> C \<and> (decompose_literal L u v p)
        \<and> (( (p = neg \<and> t = u) \<or> (t,u) \<in> trm_ord))))"
[PROOF STATE]
proof (prove)
using this:
dom_trm t C

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

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>L u v p. L \<in> C \<and> decompose_literal L u v p \<and> (p = neg \<and> t = u \<or> (t, u) \<in> trm_ord)
[PROOF STEP]
obtain L u v p where  "L \<in> C"
    "decompose_literal L u v p" "(( (p = neg \<and> t = u) \<or> (t,u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> C \<and> decompose_literal L u v p \<and> (p = neg \<and> t = u \<or> (t, u) \<in> trm_ord)

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

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?u = "(subst u \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>L \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> C
[PROOF STEP]
have "(subst_lit L \<sigma>) \<in> (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> C

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>decompose_literal L u v p\<close>
[PROOF STATE]
proof (chain)
picking this:
decompose_literal L u v p
[PROOF STEP]
have "decompose_literal (subst_lit L \<sigma>) (subst u \<sigma>) (subst v \<sigma>) p"
[PROOF STATE]
proof (prove)
using this:
decompose_literal L u v p

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p
[PROOF STEP]
using substs_preserves_decompose_literal
[PROOF STATE]
proof (prove)
using this:
decompose_literal L u v p
decompose_literal ?L ?t ?s ?polarity \<Longrightarrow> decompose_literal (subst_lit ?L ?\<eta>) (?t \<lhd> ?\<eta>) (?s \<lhd> ?\<eta>) ?polarity

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>(( (p = neg \<and> t = u) \<or> (t,u) \<in> trm_ord))\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg \<and> t = u \<or> (t, u) \<in> trm_ord
[PROOF STEP]
have "(( (p = neg \<and> ?t = ?u) \<or> (?t,?u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t = u \<or> (t, u) \<in> trm_ord

goal (1 subgoal):
 1. p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<or> (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_subst
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t = u \<or> (t, u) \<in> trm_ord
\<forall>s x y. (x, y) \<in> trm_ord \<longrightarrow> (x \<lhd> s, y \<lhd> s) \<in> trm_ord

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this \<open>(subst_lit L \<sigma>) \<in> (subst_cl C \<sigma>)\<close>
    \<open>decompose_literal (subst_lit L \<sigma>) (subst u \<sigma>) (subst v \<sigma>) p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<or> (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p
[PROOF STEP]
show "dom_trm (subst t \<sigma>) (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<or> (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<or> (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) p

goal (1 subgoal):
 1. \<exists>L u v p. L \<in> subst_cl C \<sigma> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<sigma> = u \<or> (t \<lhd> \<sigma>, u) \<in> trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma substs_preserve_well_constrainedness:
  assumes "well_constrained C"
  shows "well_constrained (subst_ecl C \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_constrained (subst_ecl C \<sigma>)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> well_constrained (subst_ecl C \<sigma>)

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> well_constrained (subst_ecl C \<sigma>)
[PROOF STEP]
obtain y where "y \<in> trms_ecl (subst_ecl C \<sigma>)"
    and "\<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
\<not> well_constrained (subst_ecl C \<sigma>)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> trms_ecl (subst_ecl C \<sigma>); \<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding well_constrained_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. y \<in> trms_ecl (subst_ecl C \<sigma>) \<longrightarrow> dom_trm y (cl_ecl (subst_ecl C \<sigma>)))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> trms_ecl (subst_ecl C \<sigma>); \<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> trms_ecl (subst_ecl C \<sigma>)
\<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
obtain Cl_C T where "C = (Ecl Cl_C T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Cl_C T. C = Ecl Cl_C T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using "eclause.exhaust"
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = Ecl x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>Cl_C T. C = Ecl Cl_C T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = Ecl Cl_C T

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C = Ecl Cl_C T
[PROOF STEP]
have "(subst_ecl C \<sigma>)
    = (Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
C = Ecl Cl_C T

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

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)
[PROOF STEP]
have "(cl_ecl (subst_ecl C \<sigma>) = (subst_cl Cl_C \<sigma>))"
    and "trms_ecl (subst_ecl C \<sigma>) = (subst_set T \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)

goal (1 subgoal):
 1. cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma> &&& trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>(cl_ecl (subst_ecl C \<sigma>) = (subst_cl Cl_C \<sigma>))\<close>
    \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
C = Ecl Cl_C T
[PROOF STEP]
have "(cl_ecl (subst_ecl C \<sigma>) = (subst_cl (cl_ecl C) \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
C = Ecl Cl_C T

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

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>y \<in> trms_ecl (subst_ecl C \<sigma>)\<close> \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> trms_ecl (subst_ecl C \<sigma>)
C = Ecl Cl_C T
[PROOF STEP]
obtain z where "z \<in> T" and "y = (subst z \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
y \<in> trms_ecl (subst_ecl C \<sigma>)
C = Ecl Cl_C T

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> T; y = z \<lhd> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> T
y = z \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>z \<in> T\<close> assms(1) \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
z \<in> T
well_constrained C
C = Ecl Cl_C T
[PROOF STEP]
have "dom_trm z (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
z \<in> T
well_constrained C
C = Ecl Cl_C T

goal (1 subgoal):
 1. dom_trm z (cl_ecl C)
[PROOF STEP]
unfolding well_constrained_def
[PROOF STATE]
proof (prove)
using this:
z \<in> T
\<forall>y. y \<in> trms_ecl C \<longrightarrow> dom_trm y (cl_ecl C)
C = Ecl Cl_C T

goal (1 subgoal):
 1. dom_trm z (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm z (cl_ecl C)

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
dom_trm z (cl_ecl C)
[PROOF STEP]
have "dom_trm (subst z \<sigma>) (subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
dom_trm z (cl_ecl C)

goal (1 subgoal):
 1. dom_trm (z \<lhd> \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
using substs_preserve_dom_trm
[PROOF STATE]
proof (prove)
using this:
dom_trm z (cl_ecl C)
dom_trm ?t ?C \<Longrightarrow> dom_trm (?t \<lhd> ?\<sigma>) (subst_cl ?C ?\<sigma>)

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

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this \<open>y = (subst z \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
dom_trm (z \<lhd> \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
y = z \<lhd> \<sigma>
[PROOF STEP]
have "dom_trm y (subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
dom_trm (z \<lhd> \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
y = z \<lhd> \<sigma>

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

goal (1 subgoal):
 1. \<not> well_constrained (subst_ecl C \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this \<open>(cl_ecl (subst_ecl C \<sigma>) = (subst_cl (cl_ecl C) \<sigma>))\<close>
    \<open>\<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
dom_trm y (subst_cl (cl_ecl C) \<sigma>)
cl_ecl (subst_ecl C \<sigma>) = subst_cl (cl_ecl C) \<sigma>
\<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
dom_trm y (subst_cl (cl_ecl C) \<sigma>)
cl_ecl (subst_ecl C \<sigma>) = subst_cl (cl_ecl C) \<sigma>
\<not> dom_trm y (cl_ecl (subst_ecl C \<sigma>))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ck_trms_sound:
  assumes "T = get_trms D (dom_trms C E) k"
  shows "T \<subseteq> (dom_trms C E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<subseteq> dom_trms C E
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> T \<subseteq> dom_trms C E
 2. \<not> ?P \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
assume "k = FirstOrder"
[PROOF STATE]
proof (state)
this:
k = FirstOrder

goal (2 subgoals):
 1. ?P \<Longrightarrow> T \<subseteq> dom_trms C E
 2. \<not> ?P \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
from this and assms
[PROOF STATE]
proof (chain)
picking this:
k = FirstOrder
T = get_trms D (dom_trms C E) k
[PROOF STEP]
have "T = filter_trms D (dom_trms C E)"
[PROOF STATE]
proof (prove)
using this:
k = FirstOrder
T = get_trms D (dom_trms C E) k

goal (1 subgoal):
 1. T = filter_trms D (dom_trms C E)
[PROOF STEP]
unfolding get_trms_def
[PROOF STATE]
proof (prove)
using this:
k = FirstOrder
T = (if k = FirstOrder then filter_trms D (dom_trms C E) else dom_trms C E)

goal (1 subgoal):
 1. T = filter_trms D (dom_trms C E)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = filter_trms D (dom_trms C E)

goal (2 subgoals):
 1. ?P \<Longrightarrow> T \<subseteq> dom_trms C E
 2. \<not> ?P \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
T = filter_trms D (dom_trms C E)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T = filter_trms D (dom_trms C E)

goal (1 subgoal):
 1. T \<subseteq> dom_trms C E
[PROOF STEP]
using filter_trms_inclusion
[PROOF STATE]
proof (prove)
using this:
T = filter_trms D (dom_trms C E)
filter_trms ?C ?E \<subseteq> ?E

goal (1 subgoal):
 1. T \<subseteq> dom_trms C E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T \<subseteq> dom_trms C E

goal (1 subgoal):
 1. k \<noteq> FirstOrder \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> FirstOrder \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
assume "k \<noteq> FirstOrder"
[PROOF STATE]
proof (state)
this:
k \<noteq> FirstOrder

goal (1 subgoal):
 1. k \<noteq> FirstOrder \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
from this and assms
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> FirstOrder
T = get_trms D (dom_trms C E) k
[PROOF STEP]
have "T = (dom_trms C E)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> FirstOrder
T = get_trms D (dom_trms C E) k

goal (1 subgoal):
 1. T = dom_trms C E
[PROOF STEP]
unfolding get_trms_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> FirstOrder
T = (if k = FirstOrder then filter_trms D (dom_trms C E) else dom_trms C E)

goal (1 subgoal):
 1. T = dom_trms C E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = dom_trms C E

goal (1 subgoal):
 1. k \<noteq> FirstOrder \<Longrightarrow> T \<subseteq> dom_trms C E
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
T = dom_trms C E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T = dom_trms C E

goal (1 subgoal):
 1. T \<subseteq> dom_trms C E
[PROOF STEP]
using filter_trms_inclusion
[PROOF STATE]
proof (prove)
using this:
T = dom_trms C E
filter_trms ?C ?E \<subseteq> ?E

goal (1 subgoal):
 1. T \<subseteq> dom_trms C E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T \<subseteq> dom_trms C E

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<not> well_constrained C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> well_constrained C
[PROOF STEP]
obtain y where "y \<in> trms_ecl C" and "\<not> dom_trm y (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<not> well_constrained C

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> trms_ecl C; \<not> dom_trm y (cl_ecl C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding well_constrained_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. y \<in> trms_ecl C \<longrightarrow> dom_trm y (cl_ecl C))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> trms_ecl C; \<not> dom_trm y (cl_ecl C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> trms_ecl C
\<not> dom_trm y (cl_ecl C)

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

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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>superposition P1 P2 C \<sigma> k C'\<close>
[PROOF STATE]
proof (chain)
picking this:
superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
obtain Cl_C T E
      where
        "T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)"
        "Cl_C = (subst_cl C' \<sigma>)"
        "C = (Ecl Cl_C T)"
[PROOF STATE]
proof (prove)
using this:
superposition P1 P2 C \<sigma> k C'

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)\<close>
[PROOF STATE]
proof (chain)
picking this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
[PROOF STEP]
have "T \<subseteq>(dom_trms Cl_C (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
using ck_trms_sound
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
?T = get_trms ?D (dom_trms ?C ?E) ?k \<Longrightarrow> ?T \<subseteq> dom_trms ?C ?E

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> trms_ecl C\<close> and \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T
[PROOF STEP]
have
      "y \<in> (dom_trms (cl_ecl C) (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> dom_trm y (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {x \<in> subst_set E \<sigma>. dom_trm x (cl_ecl C)}
\<not> dom_trm y (cl_ecl 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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'

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

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>reflexion P1 C \<sigma> k C'\<close>
[PROOF STATE]
proof (chain)
picking this:
reflexion P1 C \<sigma> k C'
[PROOF STEP]
obtain T Cl_C E where
        "T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)"
        "Cl_C = (subst_cl C' \<sigma>)"
        "C = (Ecl Cl_C T)"
[PROOF STATE]
proof (prove)
using this:
reflexion P1 C \<sigma> k C'

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

goal (1 subgoal):
 1. (\<And>T Cl_C E. \<lbrakk>T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k; Cl_C = subst_cl C' \<sigma>; C = Ecl Cl_C T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
Cl_C = subst_cl C' \<sigma>
C = Ecl Cl_C T

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)\<close>
[PROOF STATE]
proof (chain)
picking this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
[PROOF STEP]
have "T \<subseteq>(dom_trms Cl_C (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
using ck_trms_sound
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
?T = get_trms ?D (dom_trms ?C ?E) ?k \<Longrightarrow> ?T \<subseteq> dom_trms ?C ?E

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> trms_ecl C\<close> and \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T
[PROOF STEP]
have
      "y \<in> (dom_trms (cl_ecl C) (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> dom_trm y (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {x \<in> subst_set E \<sigma>. dom_trm x (cl_ecl C)}
\<not> dom_trm y (cl_ecl 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> S \<and> reflexion P1 C \<sigma> k C'

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

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>factorization P1 C \<sigma> k C'\<close>
[PROOF STATE]
proof (chain)
picking this:
factorization P1 C \<sigma> k C'
[PROOF STEP]
obtain T Cl_C E where
        "T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)"
        "Cl_C = (subst_cl C' \<sigma>)"
        "C = (Ecl Cl_C T)"
[PROOF STATE]
proof (prove)
using this:
factorization P1 C \<sigma> k C'

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from \<open>T = (get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k)\<close>
[PROOF STATE]
proof (chain)
picking this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
[PROOF STEP]
have "T \<subseteq>(dom_trms Cl_C (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
using ck_trms_sound
[PROOF STATE]
proof (prove)
using this:
T = get_trms Cl_C (dom_trms Cl_C (subst_set E \<sigma>)) k
?T = get_trms ?D (dom_trms ?C ?E) ?k \<Longrightarrow> ?T \<subseteq> dom_trms ?C ?E

goal (1 subgoal):
 1. T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> trms_ecl C\<close> and \<open>C = (Ecl Cl_C T)\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T
[PROOF STEP]
have
      "y \<in> (dom_trms (cl_ecl C) (subst_set E \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> dom_trms Cl_C (subst_set E \<sigma>)
y \<in> trms_ecl C
C = Ecl Cl_C T

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> dom_trm y (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> dom_trms (cl_ecl C) (subst_set E \<sigma>)
\<not> dom_trm y (cl_ecl C)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
using this:
y \<in> {x \<in> subst_set E \<sigma>. dom_trm x (cl_ecl C)}
\<not> dom_trm y (cl_ecl 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> S \<and> factorization P1 C \<sigma> k C'

goal (1 subgoal):
 1. \<not> well_constrained 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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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> S \<and> P2 \<in> S \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> reflexion P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<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


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

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
obtain P1 P2 where "P1 \<in> P" "P2 \<in> P" and "superposition P1 P2 C \<sigma> k C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> 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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<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
validate_clause_set I (cl_ecl ` P)
[PROOF STEP]
have "validate_clause I (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
validate_clause_set I (cl_ecl ` P)

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

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<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
validate_clause_set I (cl_ecl ` P)
[PROOF STEP]
have "validate_clause I (cl_ecl P2)"
[PROOF STATE]
proof (prove)
using this:
P2 \<in> P
validate_clause_set I (cl_ecl ` P)

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

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

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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from assms(4) and \<open>P2 \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. finite (cl_ecl x)
P2 \<in> P
[PROOF STEP]
have "finite (cl_ecl P2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. finite (cl_ecl x)
P2 \<in> P

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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<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:
fo_interpretation I
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'
[PROOF STEP]
have "set_entails_clause { (cl_ecl P1), (cl_ecl P2) } (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
finite (cl_ecl P1)
finite (cl_ecl P2)
superposition P1 P2 C \<sigma> k C'

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

goal (1 subgoal):
 1. set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) and \<open>validate_clause I (cl_ecl P1)\<close> and \<open>validate_clause I (cl_ecl P2)\<close>
[PROOF STATE]
proof (chain)
picking this:
set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)
validate_clause I (cl_ecl P2)
[PROOF STEP]
have "validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)
validate_clause I (cl_ecl P2)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
using set_entails_clause_def [of "{ (cl_ecl P1), (cl_ecl P2) }" "cl_ecl C"]
[PROOF STATE]
proof (prove)
using this:
set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)
validate_clause I (cl_ecl P2)
set_entails_clause {cl_ecl P1, cl_ecl P2} (cl_ecl C) = (\<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. validate_clause I (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<exists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>validate_clause I (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl 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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C'

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C'
[PROOF STEP]
obtain P1 where "P1 \<in> P" and "factorization P1 C \<sigma> k C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1. P1 \<in> S \<and> P = {P1} \<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> S \<and> P = {P1} \<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
validate_clause_set I (cl_ecl ` P)
[PROOF STEP]
have "validate_clause I (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
validate_clause_set I (cl_ecl ` P)

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

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

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> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>finite (cl_ecl P1)\<close> and
      \<open>factorization P1 C \<sigma> k C'\<close>
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
finite (cl_ecl P1)
factorization P1 C \<sigma> k C'
[PROOF STEP]
have "clause_entails_clause (cl_ecl P1) (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
finite (cl_ecl P1)
factorization P1 C \<sigma> k C'

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) and \<open>validate_clause I (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
clause_entails_clause (cl_ecl P1) (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)
[PROOF STEP]
have "validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
clause_entails_clause (cl_ecl P1) (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
unfolding clause_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (cl_ecl P1) \<longrightarrow> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>validate_clause I (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl 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> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C'

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C'
[PROOF STEP]
obtain P1 where "P1 \<in> P" and "reflexion  P1 C \<sigma> k C'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P1. P1 \<in> S \<and> P = {P1} \<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> S \<and> P = {P1} \<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
validate_clause_set I (cl_ecl ` P)
[PROOF STEP]
have "validate_clause I (cl_ecl P1)"
[PROOF STATE]
proof (prove)
using this:
P1 \<in> P
validate_clause_set I (cl_ecl ` P)

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

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

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> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from assms(3) and \<open>finite (cl_ecl P1)\<close> and
      \<open>reflexion P1 C \<sigma> k C'\<close>
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
finite (cl_ecl P1)
reflexion P1 C \<sigma> k C'
[PROOF STEP]
have "clause_entails_clause (cl_ecl P1) (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
finite (cl_ecl P1)
reflexion P1 C \<sigma> k C'

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

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) and \<open>validate_clause I (cl_ecl P1)\<close>
[PROOF STATE]
proof (chain)
picking this:
clause_entails_clause (cl_ecl P1) (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)
[PROOF STEP]
have "validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
clause_entails_clause (cl_ecl P1) (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
unfolding clause_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<forall>I. fo_interpretation I \<longrightarrow> validate_clause I (cl_ecl P1) \<longrightarrow> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause I (cl_ecl P1)

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

goal (1 subgoal):
 1. \<exists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>validate_clause I (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl 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> S \<and> P = {P1} \<and> reflexion P1 C \<sigma> k C'

goal (1 subgoal):
 1. \<not> validate_clause I (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from not_sup not_fact not_ref and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<nexists>P1 P2. P1 \<in> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion 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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion 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> S \<and> P2 \<in> S \<and> P = {P1, P2} \<and> superposition P1 P2 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> factorization P1 C \<sigma> k C'
\<nexists>P1. P1 \<in> S \<and> P = {P1} \<and> reflexion 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


[STATEMENT]
lemma all_derived_clauses_are_finite:
  shows "derivable_ecl C S \<Longrightarrow> \<forall>x \<in> S. (finite (cl_ecl x)) \<Longrightarrow> finite (cl_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
proof (induction rule: derivable_ecl.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
fix C :: "'a eclause"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "C \<in> S"
[PROOF STATE]
proof (state)
this:
C \<in> S

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "\<forall>x \<in> S. (finite (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from this \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. finite (cl_ecl x)
C \<in> S
[PROOF STEP]
show "finite (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. finite (cl_ecl x)
C \<in> S

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

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
fix C S
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
fix D :: "'a eclause"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "derivable_ecl C S"
[PROOF STATE]
proof (state)
this:
derivable_ecl C S

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "\<forall>x \<in> S. (finite (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume hyp_ind: "\<forall>x \<in> S. (finite (cl_ecl x)) \<Longrightarrow> finite (cl_ecl C)"
    "(renaming_cl C D)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C)
renaming_cl C D

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from \<open>(renaming_cl C D)\<close>
[PROOF STATE]
proof (chain)
picking this:
renaming_cl C D
[PROOF STEP]
obtain \<eta> where "D = (subst_ecl C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
renaming_cl C D

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding renaming_cl_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<eta>. renaming \<eta> (vars_of_cl (cl_ecl C)) \<and> D = subst_ecl C \<eta>

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D = subst_ecl C \<eta>

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
obtain C_Cl T where "C = (Ecl C_Cl T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C_Cl T. C = Ecl C_Cl T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using "eclause.exhaust"
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = Ecl x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>C_Cl T. C = Ecl C_Cl T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = Ecl C_Cl T

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from this and \<open>D = (subst_ecl C \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
C = Ecl C_Cl T
D = subst_ecl C \<eta>
[PROOF STEP]
have "(cl_ecl D) = (subst_cl (cl_ecl C) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
C = Ecl C_Cl T
D = subst_ecl C \<eta>

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

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from this hyp_ind \<open>\<forall>x \<in> S. (finite (cl_ecl x))\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl D = subst_cl (cl_ecl C) \<eta>
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C)
renaming_cl C D
\<forall>x\<in>S. finite (cl_ecl x)
[PROOF STEP]
show "finite (cl_ecl D)"
[PROOF STATE]
proof (prove)
using this:
cl_ecl D = subst_cl (cl_ecl C) \<eta>
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C)
renaming_cl C D
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. finite (cl_ecl D)
[PROOF STEP]
using substs_preserve_finiteness
[PROOF STATE]
proof (prove)
using this:
cl_ecl D = subst_cl (cl_ecl C) \<eta>
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> finite (cl_ecl C)
renaming_cl C D
\<forall>x\<in>S. finite (cl_ecl x)
finite ?C \<Longrightarrow> finite (subst_cl ?C ?\<sigma>)

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

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
fix P S C S' \<sigma> C'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume h: "\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x))

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "derivable C P S' \<sigma> FirstOrder C'"
[PROOF STATE]
proof (state)
this:
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
assume "\<forall>x\<in>S. finite (cl_ecl x)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from h and \<open>\<forall>x\<in>S. finite (cl_ecl x)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)
[PROOF STEP]
have "\<forall>x \<in> P. (finite (cl_ecl x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. \<forall>x\<in>P. finite (cl_ecl x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>P. finite (cl_ecl x)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> finite (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl C)
[PROOF STEP]
from this and \<open>derivable C P S' \<sigma> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable C P S' \<sigma> FirstOrder C'
[PROOF STEP]
show "finite (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. finite (cl_ecl C)
[PROOF STEP]
using derivable_clauses_are_finite
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable C P S' \<sigma> FirstOrder C'
\<lbrakk>derivable ?C ?P ?S ?\<sigma> ?k ?C'; \<forall>x\<in>?P. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl ?C) \<and> finite ?C'

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

goal:
No subgoals!
[PROOF STEP]
qed