[STATEMENT]
lemma trms_subsumes_and_red_inf:
  assumes "trms_subsumes D C \<eta>"
  assumes "redundant_inference (subst_ecl D \<eta>) S P \<sigma>"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  shows "redundant_inference C S P \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
redundant_inference (subst_ecl D \<eta>) S P \<sigma>
[PROOF STEP]
obtain S' where "S' \<subseteq> (instances S)"
    "(set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>)))"
    "(\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl (subst_ecl D \<eta>))))"
    "(\<forall>x \<in> S'. \<exists>D' \<in> P. (((fst x),(snd x)),(D',\<sigma>)) \<in> ecl_ord)"
[PROOF STATE]
proof (prove)
using this:
redundant_inference (subst_ecl D \<eta>) S P \<sigma>

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<subseteq> instances S; set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>)); \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>)); \<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding redundant_inference_def
[PROOF STATE]
proof (prove)
using this:
\<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>)) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))) \<and> (\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord)

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<subseteq> instances S; set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>)); \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>)); \<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S' \<subseteq> instances S
set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>))
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))
\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes D C \<eta>
[PROOF STEP]
have "(subst_cl (cl_ecl D) \<eta>) = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
trms_subsumes D C \<eta>

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

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
obtain Cl_D T where "D = Ecl Cl_D T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Cl_D T. D = Ecl Cl_D 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_D T. D = Ecl Cl_D T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D = Ecl Cl_D T

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
D = Ecl Cl_D T
[PROOF STEP]
have "(cl_ecl D) = Cl_D" and "trms_ecl D = T"
[PROOF STATE]
proof (prove)
using this:
D = Ecl Cl_D T

goal (1 subgoal):
 1. cl_ecl D = Cl_D &&& trms_ecl D = T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl D = Cl_D
trms_ecl D = T

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from \<open>D = Ecl Cl_D T\<close>
[PROOF STATE]
proof (chain)
picking this:
D = Ecl Cl_D T
[PROOF STEP]
have "subst_ecl D \<eta> = Ecl (subst_cl Cl_D \<eta>) (subst_set T \<eta>)"
[PROOF STATE]
proof (prove)
using this:
D = Ecl Cl_D T

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_ecl D \<eta> = Ecl (subst_cl Cl_D \<eta>) (subst_set T \<eta>)
[PROOF STEP]
have "(cl_ecl (subst_ecl D \<eta>)) = (subst_cl Cl_D \<eta>)"
    and "trms_ecl (subst_ecl D \<eta>) = (subst_set T \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_ecl D \<eta> = Ecl (subst_cl Cl_D \<eta>) (subst_set T \<eta>)

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from \<open>(cl_ecl (subst_ecl D \<eta>)) = (subst_cl Cl_D \<eta>)\<close>
    and \<open>(cl_ecl D) = Cl_D\<close> \<open>(subst_cl (cl_ecl D) \<eta>) = (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl (subst_ecl D \<eta>) = subst_cl Cl_D \<eta>
cl_ecl D = Cl_D
subst_cl (cl_ecl D) \<eta> = cl_ecl C
[PROOF STEP]
have "(cl_ecl (subst_ecl D \<eta>)) = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
cl_ecl (subst_ecl D \<eta>) = subst_cl Cl_D \<eta>
cl_ecl D = Cl_D
subst_cl (cl_ecl D) \<eta> = cl_ecl C

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from this and \<open>(set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>)))\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl (subst_ecl D \<eta>) = cl_ecl C
set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>))
[PROOF STEP]
have "(set_entails_clause (clset_instances S') (cl_ecl C))"
[PROOF STATE]
proof (prove)
using this:
cl_ecl (subst_ecl D \<eta>) = cl_ecl C
set_entails_clause (clset_instances S') (cl_ecl (subst_ecl D \<eta>))

goal (1 subgoal):
 1. set_entails_clause (clset_instances S') (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_entails_clause (clset_instances S') (cl_ecl C)

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from \<open>trms_ecl D = T\<close> and \<open>trms_ecl (subst_ecl D \<eta>) = (subst_set T \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
trms_ecl D = T
trms_ecl (subst_ecl D \<eta>) = subst_set T \<eta>
[PROOF STEP]
have "trms_ecl (subst_ecl D \<eta>) = (subst_set (trms_ecl D) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
trms_ecl D = T
trms_ecl (subst_ecl D \<eta>) = subst_set T \<eta>

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes D C \<eta>
[PROOF STEP]
have "(subst_set (trms_ecl D) \<eta>) \<subseteq> (trms_ecl C)"
[PROOF STATE]
proof (prove)
using this:
trms_subsumes D C \<eta>

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

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

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
have ii: "(\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl C)))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C))

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C))
[PROOF STEP]
obtain x where "x \<in> S'" and
      "\<not>( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C))"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S'; \<not> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> S'
\<not> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> S'\<close> and \<open>(\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl (subst_ecl D \<eta>))))\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> S'
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))
[PROOF STEP]
have "( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl (subst_ecl D \<eta>)))"
[PROOF STATE]
proof (prove)
using this:
x \<in> S'
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))

goal (1 subgoal):
 1. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
obtain E1 where "E1 = (subst_set (trms_ecl (fst x)) (snd x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E1. E1 = subst_set (trms_ecl (fst x)) (snd x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E1 = subst_set (trms_ecl (fst x)) (snd x)

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
obtain E2 where "E2 = (subst_set (trms_ecl D) \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E2. E2 = subst_set (trms_ecl D) \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E2 = subst_set (trms_ecl D) \<eta>

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
obtain E2' where "E2' = (trms_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E2'. E2' = trms_ecl C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E2' = trms_ecl C

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from \<open>E2 = (subst_set (trms_ecl D) \<eta>)\<close> \<open>E2' = (trms_ecl C)\<close>
          \<open>(subst_set (trms_ecl D) \<eta>) \<subseteq> (trms_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
E2 = subst_set (trms_ecl D) \<eta>
E2' = trms_ecl C
subst_set (trms_ecl D) \<eta> \<subseteq> trms_ecl C
[PROOF STEP]
have "E2 \<subseteq> E2'"
[PROOF STATE]
proof (prove)
using this:
E2 = subst_set (trms_ecl D) \<eta>
E2' = trms_ecl C
subst_set (trms_ecl D) \<eta> \<subseteq> trms_ecl C

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

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from \<open>E1 = (subst_set (trms_ecl (fst x)) (snd x))\<close>
         \<open>E2 = (subst_set (trms_ecl D) \<eta>)\<close>
         \<open>trms_ecl (subst_ecl D \<eta>) = (subst_set (trms_ecl D) \<eta>)\<close>
         \<open>( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl (subst_ecl D \<eta>)))\<close>
[PROOF STATE]
proof (chain)
picking this:
E1 = subst_set (trms_ecl (fst x)) (snd x)
E2 = subst_set (trms_ecl D) \<eta>
trms_ecl (subst_ecl D \<eta>) = subst_set (trms_ecl D) \<eta>
subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))
[PROOF STEP]
have "subterms_inclusion E1 E2"
[PROOF STATE]
proof (prove)
using this:
E1 = subst_set (trms_ecl (fst x)) (snd x)
E2 = subst_set (trms_ecl D) \<eta>
trms_ecl (subst_ecl D \<eta>) = subst_set (trms_ecl D) \<eta>
subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl D \<eta>))

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

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>E2 \<subseteq> E2'\<close>
[PROOF STATE]
proof (chain)
picking this:
subterms_inclusion E1 E2
E2 \<subseteq> E2'
[PROOF STEP]
have "subterms_inclusion E1 E2'"
[PROOF STATE]
proof (prove)
using this:
subterms_inclusion E1 E2
E2 \<subseteq> E2'

goal (1 subgoal):
 1. subterms_inclusion E1 E2'
[PROOF STEP]
using subterms_inclusion_subset
[PROOF STATE]
proof (prove)
using this:
subterms_inclusion E1 E2
E2 \<subseteq> E2'
\<lbrakk>subterms_inclusion ?E1.0 ?E2.0; ?E2.0 \<subseteq> ?E2'\<rbrakk> \<Longrightarrow> subterms_inclusion ?E1.0 ?E2'

goal (1 subgoal):
 1. subterms_inclusion E1 E2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterms_inclusion E1 E2'

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>E1 = (subst_set (trms_ecl (fst x)) (snd x))\<close> \<open>E2' = (trms_ecl C)\<close>
      and \<open>\<not>( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl C))\<close>
[PROOF STATE]
proof (chain)
picking this:
subterms_inclusion E1 E2'
E1 = subst_set (trms_ecl (fst x)) (snd x)
E2' = trms_ecl C
\<not> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
subterms_inclusion E1 E2'
E1 = subst_set (trms_ecl (fst x)) (snd x)
E2' = trms_ecl C
\<not> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_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:
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
from this and \<open>(set_entails_clause (clset_instances S') (cl_ecl C))\<close>
      and \<open>(\<forall>x \<in> S'. \<exists>D' \<in> P. (((fst x),(snd x)),(D',\<sigma>)) \<in> ecl_ord)\<close>
      and \<open>S' \<subseteq> (instances S)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
S' \<subseteq> instances S
[PROOF STEP]
show "redundant_inference C S P \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
S' \<subseteq> instances S

goal (1 subgoal):
 1. redundant_inference C S P \<sigma>
[PROOF STEP]
unfolding redundant_inference_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
S' \<subseteq> instances S

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
redundant_inference C S P \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_inference:
  assumes "inference_saturated S"
  shows "ground_inference_saturated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_inference_saturated S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ground_inference_saturated S \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (ground_inference_saturated S)"
[PROOF STATE]
proof (state)
this:
\<not> ground_inference_saturated S

goal (1 subgoal):
 1. \<not> ground_inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> ground_inference_saturated S
[PROOF STEP]
obtain C P \<sigma> C' where "derivable C P S \<sigma> Ground C'" "ground_clause (cl_ecl C)"
    "grounding_set P \<sigma>" "\<not>redundant_inference C S P \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<not> ground_inference_saturated S

goal (1 subgoal):
 1. (\<And>C P \<sigma> C'. \<lbrakk>derivable C P S \<sigma> Ground C'; ground_clause (cl_ecl C); grounding_set P \<sigma>; \<not> redundant_inference C S P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ground_inference_saturated_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C P \<sigma> C'. derivable C P S \<sigma> Ground C' \<longrightarrow> ground_clause (cl_ecl C) \<longrightarrow> grounding_set P \<sigma> \<longrightarrow> redundant_inference C S P \<sigma>)

goal (1 subgoal):
 1. (\<And>C P \<sigma> C'. \<lbrakk>derivable C P S \<sigma> Ground C'; ground_clause (cl_ecl C); grounding_set P \<sigma>; \<not> redundant_inference C S P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derivable C P S \<sigma> Ground C'
ground_clause (cl_ecl C)
grounding_set P \<sigma>
\<not> redundant_inference C S P \<sigma>

goal (1 subgoal):
 1. \<not> ground_inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>derivable C P S \<sigma> Ground C'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable C P S \<sigma> Ground C'
[PROOF STEP]
obtain D \<theta> \<eta> where "derivable D P S \<theta> FirstOrder C'"
    "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>" "trms_subsumes D C \<eta>"
[PROOF STATE]
proof (prove)
using this:
derivable C P S \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>D \<theta> \<eta>. \<lbrakk>derivable D P S \<theta> FirstOrder C'; \<sigma> \<doteq> \<theta> \<lozenge> \<eta>; trms_subsumes D C \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lifting_lemma
[PROOF STATE]
proof (prove)
using this:
derivable C P S \<sigma> Ground C'
derivable ?C ?P ?S ?\<sigma> Ground ?C' \<Longrightarrow> \<exists>D \<theta> \<eta>. derivable D ?P ?S \<theta> FirstOrder ?C' \<and> ?\<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<and> trms_subsumes D ?C \<eta>

goal (1 subgoal):
 1. (\<And>D \<theta> \<eta>. \<lbrakk>derivable D P S \<theta> FirstOrder C'; \<sigma> \<doteq> \<theta> \<lozenge> \<eta>; trms_subsumes D C \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derivable D P S \<theta> FirstOrder C'
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
trms_subsumes D C \<eta>

goal (1 subgoal):
 1. \<not> ground_inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>trms_subsumes D C \<eta>\<close> and \<open>\<not>redundant_inference C S P \<sigma>\<close>  \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes D C \<eta>
\<not> redundant_inference C S P \<sigma>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>"
[PROOF STATE]
proof (prove)
using this:
trms_subsumes D C \<eta>
\<not> redundant_inference C S P \<sigma>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. \<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
[PROOF STEP]
using trms_subsumes_and_red_inf
[PROOF STATE]
proof (prove)
using this:
trms_subsumes D C \<eta>
\<not> redundant_inference C S P \<sigma>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<lbrakk>trms_subsumes ?D ?C ?\<eta>; redundant_inference (subst_ecl ?D ?\<eta>) ?S ?P ?\<sigma>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> redundant_inference ?C ?S ?P ?\<sigma>

goal (1 subgoal):
 1. \<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>

goal (1 subgoal):
 1. \<not> ground_inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>derivable C P S \<sigma> Ground C'\<close> \<open>derivable D P S \<theta> FirstOrder C'\<close> \<open>trms_subsumes D C \<eta>\<close>
   \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close> \<open>ground_clause (cl_ecl C)\<close> \<open>grounding_set P \<sigma>\<close>
   \<open>\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>\<close>
    assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
derivable C P S \<sigma> Ground C'
derivable D P S \<theta> FirstOrder C'
trms_subsumes D C \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
ground_clause (cl_ecl C)
grounding_set P \<sigma>
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
inference_saturated S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
derivable C P S \<sigma> Ground C'
derivable D P S \<theta> FirstOrder C'
trms_subsumes D C \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
ground_clause (cl_ecl C)
grounding_set P \<sigma>
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
inference_saturated S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding inference_saturated_def
[PROOF STATE]
proof (prove)
using this:
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
derivable C P S \<sigma> Ground C'
derivable D P S \<theta> FirstOrder C'
trms_subsumes D C \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
ground_clause (cl_ecl C)
grounding_set P \<sigma>
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
\<forall>C P \<sigma> C' D \<theta> \<eta>. derivable C P S \<sigma> Ground C' \<longrightarrow> ground_clause (cl_ecl C) \<longrightarrow> grounding_set P \<sigma> \<longrightarrow> derivable D P S \<theta> FirstOrder C' \<longrightarrow> trms_subsumes D C \<eta> \<longrightarrow> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<longrightarrow> redundant_inference (subst_ecl D \<eta>) S P \<sigma>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_redundant_cl :
  assumes "C' = subst_cl D \<theta>"
  assumes "redundant_clause C S \<eta> C'"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  assumes "finite D"
  shows "redundant_clause C S \<sigma> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
redundant_clause C S \<eta> C'
[PROOF STEP]
have
    "(\<exists>S'. (S' \<subseteq> (instances S) \<and> (set_entails_clause (clset_instances S') (cl_ecl C)) \<and>
            (\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl C))) \<and>
            (\<forall>x \<in> S'. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<eta>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<eta>)))))"
[PROOF STATE]
proof (prove)
using this:
redundant_clause C S \<eta> C'

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))
[PROOF STEP]
unfolding  redundant_clause_def
[PROOF STATE]
proof (prove)
using this:
\<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))

goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))
[PROOF STEP]
obtain S' where i: "S' \<subseteq> (instances S)"
    and ii: "(set_entails_clause (clset_instances S') (cl_ecl C))"
  and iii: "(\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl C)))"
  and
  iv: "(\<forall>x \<in> S'. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<eta>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<eta>)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>))

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<subseteq> instances S; set_entails_clause (clset_instances S') (cl_ecl C); \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C); \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S' \<subseteq> instances S
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)

goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
let ?m1 = "mset_cl (C',\<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
let ?m2 = "mset_cl (D,\<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
from assms(1) assms(3) assms(4)
[PROOF STATE]
proof (chain)
picking this:
C' = subst_cl D \<theta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
finite D
[PROOF STEP]
have "mset_cl (C',\<eta>) = mset_cl (D,\<sigma>) \<or> (mset_cl (C',\<eta>),mset_cl (D,\<sigma>)) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
C' = subst_cl D \<theta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
finite D

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
using mset_subst
[PROOF STATE]
proof (prove)
using this:
C' = subst_cl D \<theta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
finite D
\<lbrakk>?C' = subst_cl ?D ?\<theta>; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>; finite ?D\<rbrakk> \<Longrightarrow> mset_cl (?C', ?\<eta>) = mset_cl (?D, ?\<sigma>) \<or> (mset_cl (?C', ?\<eta>), mset_cl (?D, ?\<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
from this iv
[PROOF STATE]
proof (chain)
picking this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)
[PROOF STEP]
have "(\<forall>x \<in> S'. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (D,\<sigma>))) \<in> (mult (mult trm_ord))
            \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (D,\<sigma>)))"
[PROOF STATE]
proof (prove)
using this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)

goal (1 subgoal):
 1. \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
[PROOF STEP]
using mult_mult_trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)
trans (mult (mult trm_ord))

goal (1 subgoal):
 1. \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<eta>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<eta>)
\<forall>x y z. (x, y) \<in> mult (mult trm_ord) \<longrightarrow> (y, z) \<in> mult (mult trm_ord) \<longrightarrow> (x, z) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
from this and i ii iii
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
S' \<subseteq> instances S
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
S' \<subseteq> instances S
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)

goal (1 subgoal):
 1. redundant_clause C S \<sigma> D
[PROOF STEP]
unfolding  redundant_clause_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>)
S' \<subseteq> instances S
set_entails_clause (clset_instances S') (cl_ecl C)
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl C) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl C)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (D, \<sigma>))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
redundant_clause C S \<sigma> D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inference_closed_sets_are_saturated:
  assumes "inference_closed S"
  assumes "\<forall>x \<in> S. (finite (cl_ecl x))"
  shows "clause_saturated S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clause_saturated S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> clause_saturated S

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> clause_saturated S
[PROOF STEP]
obtain C P \<sigma> C' D \<theta> \<eta>
    where
     "(derivable C P S \<sigma> Ground C')" "(ground_clause (cl_ecl C))"
     "(derivable D P S \<theta> FirstOrder C')" "(trms_subsumes D C \<eta>)"
     "(\<sigma> \<doteq> \<theta> \<lozenge> \<eta>)"
     "\<not>(redundant_clause (subst_ecl D \<eta>) S \<sigma> C')"
[PROOF STATE]
proof (prove)
using this:
\<not> clause_saturated S

goal (1 subgoal):
 1. (\<And>C P \<sigma> C' D \<theta> \<eta>. \<lbrakk>derivable C P S \<sigma> Ground C'; ground_clause (cl_ecl C); derivable D P S \<theta> FirstOrder C'; trms_subsumes D C \<eta>; \<sigma> \<doteq> \<theta> \<lozenge> \<eta>; \<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding clause_saturated_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C P \<sigma> C' D \<theta> \<eta>. derivable C P S \<sigma> Ground C' \<longrightarrow> ground_clause (cl_ecl C) \<longrightarrow> derivable D P S \<theta> FirstOrder C' \<longrightarrow> trms_subsumes D C \<eta> \<longrightarrow> \<sigma> \<doteq> \<theta> \<lozenge> \<eta> \<longrightarrow> redundant_clause (subst_ecl D \<eta>) S \<sigma> C')

goal (1 subgoal):
 1. (\<And>C P \<sigma> C' D \<theta> \<eta>. \<lbrakk>derivable C P S \<sigma> Ground C'; ground_clause (cl_ecl C); derivable D P S \<theta> FirstOrder C'; trms_subsumes D C \<eta>; \<sigma> \<doteq> \<theta> \<lozenge> \<eta>; \<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derivable C P S \<sigma> Ground C'
ground_clause (cl_ecl C)
derivable D P S \<theta> FirstOrder C'
trms_subsumes D C \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>(derivable D P S \<theta> FirstOrder C')\<close> assms(1)
[PROOF STATE]
proof (chain)
picking this:
derivable D P S \<theta> FirstOrder C'
inference_closed S
[PROOF STEP]
have "D \<in> S"
[PROOF STATE]
proof (prove)
using this:
derivable D P S \<theta> FirstOrder C'
inference_closed S

goal (1 subgoal):
 1. D \<in> S
[PROOF STEP]
unfolding inference_closed_def
[PROOF STATE]
proof (prove)
using this:
derivable D P S \<theta> FirstOrder C'
\<forall>P C' D \<theta>. derivable D P S \<theta> FirstOrder C' \<longrightarrow> D \<in> S

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>derivable D P S \<theta> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable D P S \<theta> FirstOrder C'
[PROOF STEP]
have "(cl_ecl D) = (subst_cl C' \<theta>)"
[PROOF STATE]
proof (prove)
using this:
derivable D P S \<theta> FirstOrder C'

goal (1 subgoal):
 1. cl_ecl D = subst_cl C' \<theta>
[PROOF STEP]
using derivable_clauses_lemma
[PROOF STATE]
proof (prove)
using this:
derivable D P S \<theta> FirstOrder C'
derivable ?C ?P ?S ?\<sigma> ?k ?C' \<Longrightarrow> cl_ecl ?C = subst_cl ?C' ?\<sigma>

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>trms_subsumes D C \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
trms_subsumes D C \<eta>
[PROOF STEP]
have "(cl_ecl C) = (subst_cl (cl_ecl D) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
trms_subsumes D C \<eta>

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

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "subst_cl (cl_ecl D) \<sigma> = subst_cl (cl_ecl D) (\<theta> \<lozenge> \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_cl (cl_ecl D) \<sigma> = subst_cl (cl_ecl D) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_cl
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
?\<sigma> \<doteq> ?\<eta> \<Longrightarrow> subst_cl ?C ?\<sigma> = subst_cl ?C ?\<eta>

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl D) \<sigma> = subst_cl (cl_ecl D) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "(subst_cl (cl_ecl D) \<sigma>) = (subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl D) \<sigma> = subst_cl (cl_ecl D) (\<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(cl_ecl C) = (subst_cl (cl_ecl D) \<eta>)\<close>
    \<open>(ground_clause (cl_ecl C))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl D) \<sigma> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
cl_ecl C = subst_cl (cl_ecl D) \<eta>
ground_clause (cl_ecl C)
[PROOF STEP]
have "ground_clause (subst_cl (cl_ecl D) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl D) \<sigma> = subst_cl (subst_cl (cl_ecl D) \<theta>) \<eta>
cl_ecl C = subst_cl (cl_ecl D) \<eta>
ground_clause (cl_ecl C)

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this \<open>D \<in> S\<close> \<open>(cl_ecl D) = (subst_cl C' \<theta>)\<close>
    \<open>(cl_ecl D) = (subst_cl C' \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_clause (subst_cl (cl_ecl D) \<eta>)
D \<in> S
cl_ecl D = subst_cl C' \<theta>
cl_ecl D = subst_cl C' \<theta>
[PROOF STEP]
have "redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)"
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl D) \<eta>)
D \<in> S
cl_ecl D = subst_cl C' \<theta>
cl_ecl D = subst_cl C' \<theta>

goal (1 subgoal):
 1. redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)
[PROOF STEP]
using self_redundant_clause
[PROOF STATE]
proof (prove)
using this:
ground_clause (subst_cl (cl_ecl D) \<eta>)
D \<in> S
cl_ecl D = subst_cl C' \<theta>
cl_ecl D = subst_cl C' \<theta>
\<lbrakk>?C \<in> ?S; ?C' = cl_ecl ?C; ground_clause (subst_cl (cl_ecl ?C) ?\<sigma>)\<rbrakk> \<Longrightarrow> redundant_clause (subst_ecl ?C ?\<sigma>) ?S ?\<sigma> ?C'

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from \<open>derivable D P S \<theta> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable D P S \<theta> FirstOrder C'
[PROOF STEP]
have "P \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
derivable D P S \<theta> FirstOrder C'

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

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this assms(2)
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> S
\<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:
P \<subseteq> S
\<forall>x\<in>S. finite (cl_ecl x)

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

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this  \<open>derivable D P S \<theta> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable D P S \<theta> FirstOrder C'
[PROOF STEP]
have  "finite C'"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable D P S \<theta> FirstOrder C'

goal (1 subgoal):
 1. finite C'
[PROOF STEP]
using derivable_clauses_are_finite
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. finite (cl_ecl x)
derivable D P S \<theta> 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 C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite C'

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this \<open>(cl_ecl D) = subst_cl C' \<theta>\<close>
      \<open>redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)\<close> \<open>(\<sigma> \<doteq> \<theta> \<lozenge> \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite C'
cl_ecl D = subst_cl C' \<theta>
redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "redundant_clause (subst_ecl D \<eta>) S \<sigma> C'"
[PROOF STATE]
proof (prove)
using this:
finite C'
cl_ecl D = subst_cl C' \<theta>
redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
[PROOF STEP]
using lift_redundant_cl
[PROOF STATE]
proof (prove)
using this:
finite C'
cl_ecl D = subst_cl C' \<theta>
redundant_clause (subst_ecl D \<eta>) S \<eta> (subst_cl C' \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<lbrakk>?C' = subst_cl ?D ?\<theta>; redundant_clause ?C ?S ?\<eta> ?C'; ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>; finite ?D\<rbrakk> \<Longrightarrow> redundant_clause ?C ?S ?\<sigma> ?D

goal (1 subgoal):
 1. redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
redundant_clause (subst_ecl D \<eta>) S \<sigma> C'

goal (1 subgoal):
 1. \<not> clause_saturated S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>(redundant_clause (subst_ecl D \<eta>) S \<sigma> C')\<close>
[PROOF STATE]
proof (chain)
picking this:
redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
\<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
\<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'

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

goal:
No subgoals!
[PROOF STEP]
qed