[STATEMENT]
lemma redundant_inference_clause:
  assumes "redundant_clause E S \<sigma> C'"
  assumes "derivable C P S \<sigma> Ground C'"
  assumes "grounding_set P \<sigma>"
  assumes "\<forall>x \<in> S. (finite (cl_ecl x))"
  shows "redundant_inference E S P \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant_inference E S P \<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_inference E S P \<sigma>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
redundant_clause E S \<sigma> C'
[PROOF STEP]
obtain S' where "S' \<subseteq> (instances S)"
    "(set_entails_clause (clset_instances S') (cl_ecl E))"
    "(\<forall>x \<in> S'. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl E)))"
    "(\<forall>x \<in> S'. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)))"
[PROOF STATE]
proof (prove)
using this:
redundant_clause E S \<sigma> C'

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<subseteq> instances S; set_entails_clause (clset_instances S') (cl_ecl E); \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl E); \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[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 E) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl E)) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>))

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<subseteq> instances S; set_entails_clause (clset_instances S') (cl_ecl E); \<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl E); \<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)\<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 E)
\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl E)
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. redundant_inference E S P \<sigma>
[PROOF STEP]
from assms(3) assms(4) \<open>derivable C P S \<sigma> Ground C'\<close>
[PROOF STATE]
proof (chain)
picking this:
grounding_set P \<sigma>
\<forall>x\<in>S. finite (cl_ecl x)
derivable C P S \<sigma> Ground C'
[PROOF STEP]
obtain D where "D \<in> P"
      "(( (mset_cl (C',\<sigma>)), (mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord)))"
[PROOF STATE]
proof (prove)
using this:
grounding_set P \<sigma>
\<forall>x\<in>S. finite (cl_ecl x)
derivable C P S \<sigma> Ground C'

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> P; (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using conclusion_is_smaller_than_premisses
[PROOF STATE]
proof (prove)
using this:
grounding_set P \<sigma>
\<forall>x\<in>S. finite (cl_ecl x)
derivable C P S \<sigma> Ground C'
\<lbrakk>derivable ?C ?P ?S ?\<sigma> Ground ?C'; \<forall>x\<in>?S. finite (cl_ecl x); grounding_set ?P ?\<sigma>\<rbrakk> \<Longrightarrow> \<exists>D. D \<in> ?P \<and> (mset_cl (?C', ?\<sigma>), mset_ecl (D, ?\<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> P; (mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D \<in> P
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. redundant_inference E S P \<sigma>
[PROOF STEP]
have "(\<forall>x \<in> S'. \<exists>D' \<in> P. (((fst x),(snd x)),(D',\<sigma>)) \<in> ecl_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S' \<Longrightarrow> \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S' \<Longrightarrow> \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
assume "x \<in> S'"
[PROOF STATE]
proof (state)
this:
x \<in> S'

goal (1 subgoal):
 1. \<And>x. x \<in> S' \<Longrightarrow> \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this and \<open>(\<forall>x \<in> S'. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)))\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> S'
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
have "((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord)) \<or>
            (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> S'
\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

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

goal (1 subgoal):
 1. \<And>x. x \<in> S' \<Longrightarrow> \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
have "(((fst x),(snd x)),(D,\<sigma>)) \<in> ecl_ord"
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
 2. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
assume "((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (state)
this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord)

goal (2 subgoals):
 1. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
 2. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this and \<open>(( (mset_cl (C',\<sigma>)), (mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord)))\<close>
[PROOF STATE]
proof (chain)
picking this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord)
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
have "((mset_ecl ((fst x),(snd x))),(mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord)
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

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

goal (1 subgoal):
 1. (mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord)
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
\<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. (mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (2 subgoals):
 1. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
 2. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
unfolding ecl_ord_def
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ((fst x, snd x), D, \<sigma>) \<in> {(x, y). (mset_ecl x, mset_ecl y) \<in> mult (mult trm_ord)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((fst x, snd x), D, \<sigma>) \<in> ecl_ord

goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
assume "(mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)"
[PROOF STATE]
proof (state)
this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this and \<open>(( (mset_cl (C',\<sigma>)), (mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord)))\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
have "((mset_ecl ((fst x),(snd x))),(mset_ecl (D,\<sigma>))) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
(mset_cl (C', \<sigma>), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. (mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>) \<Longrightarrow> ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ((fst x, snd x), D, \<sigma>) \<in> ecl_ord
[PROOF STEP]
unfolding ecl_ord_def
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (fst x, snd x), mset_ecl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal (1 subgoal):
 1. ((fst x, snd x), D, \<sigma>) \<in> {(x, y). (mset_ecl x, mset_ecl y) \<in> mult (mult trm_ord)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((fst x, snd x), D, \<sigma>) \<in> ecl_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((fst x, snd x), D, \<sigma>) \<in> ecl_ord

goal (1 subgoal):
 1. \<And>x. x \<in> S' \<Longrightarrow> \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
from this and \<open>D \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
((fst x, snd x), D, \<sigma>) \<in> ecl_ord
D \<in> P
[PROOF STEP]
show "\<exists>D' \<in> P. (((fst x),(snd x)),(D',\<sigma>)) \<in> ecl_ord"
[PROOF STATE]
proof (prove)
using this:
((fst x, snd x), D, \<sigma>) \<in> ecl_ord
D \<in> P

goal (1 subgoal):
 1. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S'. \<exists>D'\<in>P. ((fst x, snd x), D', \<sigma>) \<in> ecl_ord

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

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

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl E) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl E)) \<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 E S P \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<not> inference_saturated S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inference_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>" "grounding_set P \<sigma>"
          "\<not>redundant_inference (subst_ecl D \<eta>) S P \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<not> inference_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>; grounding_set P \<sigma>; \<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding inference_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> 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. (\<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>; grounding_set P \<sigma>; \<not> redundant_inference (subst_ecl D \<eta>) 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)
derivable D P S \<theta> FirstOrder C'
trms_subsumes D C \<eta>
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
grounding_set P \<sigma>
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>

goal (1 subgoal):
 1. \<not> inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from assms(2) \<open>grounding_set P \<sigma>\<close> \<open>derivable C P S \<sigma> Ground C'\<close>
    \<open>\<not>redundant_inference (subst_ecl D \<eta>) S P \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. finite (cl_ecl x)
grounding_set P \<sigma>
derivable C P S \<sigma> Ground C'
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
[PROOF STEP]
have "\<not>redundant_clause (subst_ecl D \<eta>) S \<sigma> C'"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. finite (cl_ecl x)
grounding_set P \<sigma>
derivable C P S \<sigma> Ground C'
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>

goal (1 subgoal):
 1. \<not> redundant_clause (subst_ecl D \<eta>) S \<sigma> C'
[PROOF STEP]
using redundant_inference_clause
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. finite (cl_ecl x)
grounding_set P \<sigma>
derivable C P S \<sigma> Ground C'
\<not> redundant_inference (subst_ecl D \<eta>) S P \<sigma>
\<lbrakk>redundant_clause ?E ?S ?\<sigma> ?C'; derivable ?C ?P ?S ?\<sigma> Ground ?C'; grounding_set ?P ?\<sigma>; \<forall>x\<in>?S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> redundant_inference ?E ?S ?P ?\<sigma>

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

goal (1 subgoal):
 1. \<not> inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
clause_saturated S
[PROOF STEP]
have "\<And>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')"
[PROOF STATE]
proof (prove)
using this:
clause_saturated S

goal (1 subgoal):
 1. \<And>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'
[PROOF STEP]
unfolding clause_saturated_def
[PROOF STATE]
proof (prove)
using this:
\<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>. 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'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
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. \<not> inference_saturated S \<Longrightarrow> False
[PROOF STEP]
from this  and \<open>derivable C P S \<sigma> Ground C'\<close> \<open>ground_clause (cl_ecl 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> assms(1)
[PROOF STATE]
proof (chain)
picking this:
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'
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>
clause_saturated S
[PROOF STEP]
have "redundant_clause (subst_ecl D \<eta>) S \<sigma> C'"
[PROOF STATE]
proof (prove)
using this:
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'
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>
clause_saturated S

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

goal (1 subgoal):
 1. \<not> inference_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


[STATEMENT]
lemma same_values_fo_int:
  assumes "value_is_compatible_with_structure f"
  shows "fo_interpretation (same_values f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
let ?I = "(same_values f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
have ref: "reflexive ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive (same_values f)
[PROOF STEP]
unfolding same_values_def reflexive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. f y = f y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reflexive (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
have sym: "symmetric ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric (same_values f)
[PROOF STEP]
unfolding same_values_def symmetric_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y z. (f y = f z) = (f z = f y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
symmetric (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
have trans: "transitive ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive (same_values f)
[PROOF STEP]
unfolding same_values_def transitive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y z u. f y = f z \<longrightarrow> f z = f u \<longrightarrow> f y = f u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
transitive (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
value_is_compatible_with_structure f
[PROOF STEP]
have comp: "compatible_with_structure ?I"
[PROOF STATE]
proof (prove)
using this:
value_is_compatible_with_structure f

goal (1 subgoal):
 1. compatible_with_structure (same_values f)
[PROOF STEP]
unfolding same_values_def
      compatible_with_structure_def value_is_compatible_with_structure_def [of f]
[PROOF STATE]
proof (prove)
using this:
\<forall>t s. f (t \<cdot> s) = f (f t \<cdot> f s)

goal (1 subgoal):
 1. \<forall>t1 t2 s1 s2. f t1 = f s1 \<longrightarrow> f t2 = f s2 \<longrightarrow> f (t1 \<cdot> t2) = f (s1 \<cdot> s2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
compatible_with_structure (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
from ref trans sym comp
[PROOF STATE]
proof (chain)
picking this:
reflexive (same_values f)
transitive (same_values f)
symmetric (same_values f)
compatible_with_structure (same_values f)
[PROOF STEP]
have "congruence ?I"
[PROOF STATE]
proof (prove)
using this:
reflexive (same_values f)
transitive (same_values f)
symmetric (same_values f)
compatible_with_structure (same_values f)

goal (1 subgoal):
 1. congruence (same_values f)
[PROOF STEP]
unfolding congruence_def equivalence_relation_def
[PROOF STATE]
proof (prove)
using this:
reflexive (same_values f)
transitive (same_values f)
symmetric (same_values f)
compatible_with_structure (same_values f)

goal (1 subgoal):
 1. (reflexive (same_values f) \<and> symmetric (same_values f) \<and> transitive (same_values f)) \<and> compatible_with_structure (same_values f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
congruence (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
congruence (same_values f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
congruence (same_values f)

goal (1 subgoal):
 1. fo_interpretation (same_values f)
[PROOF STEP]
unfolding fo_interpretation_def
[PROOF STATE]
proof (prove)
using this:
congruence (same_values f)

goal (1 subgoal):
 1. congruence (same_values f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fo_interpretation (same_values f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_trms_not_empty:
  assumes "E \<noteq> {}"
  shows "min_trms E \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
E \<noteq> {}
[PROOF STEP]
obtain x where "x \<in> E"
[PROOF STATE]
proof (prove)
using this:
E \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> E \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> E

goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
let ?pair_ordering = "{ (x,y). ((snd x),(snd y)) \<in> trm_ord }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
from trm_ord_wf
[PROOF STATE]
proof (chain)
picking this:
wf trm_ord
[PROOF STEP]
have "wf ?pair_ordering"
[PROOF STATE]
proof (prove)
using this:
wf trm_ord

goal (1 subgoal):
 1. wf {(x, y). (snd x, snd y) \<in> trm_ord}
[PROOF STEP]
using  measure_wf
[PROOF STATE]
proof (prove)
using this:
wf trm_ord
\<lbrakk>wf ?r; ?r' = {(x, y). (?m x, ?m y) \<in> ?r}\<rbrakk> \<Longrightarrow> wf ?r'

goal (1 subgoal):
 1. wf {(x, y). (snd x, snd y) \<in> trm_ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf {(x, y). (snd x, snd y) \<in> trm_ord}

goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
from this \<open>x \<in> E\<close>
[PROOF STATE]
proof (chain)
picking this:
wf {(x, y). (snd x, snd y) \<in> trm_ord}
x \<in> E
[PROOF STEP]
obtain y where "y \<in> E" and "\<forall>z. (z,y) \<in> ?pair_ordering \<longrightarrow> (z \<notin> E)"
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (snd x, snd y) \<in> trm_ord}
x \<in> E

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> E; \<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfE_min [of ?pair_ordering ]
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (snd x, snd y) \<in> trm_ord}
x \<in> E
\<lbrakk>wf {(x, y). (snd x, snd y) \<in> trm_ord}; ?x \<in> ?Q; \<And>z. \<lbrakk>z \<in> ?Q; \<And>y. (y, z) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<Longrightarrow> y \<notin> ?Q\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> E; \<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
y \<in> E
\<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E

goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
y \<in> E
\<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E
[PROOF STEP]
have "fst y \<in> min_trms E"
[PROOF STATE]
proof (prove)
using this:
y \<in> E
\<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E

goal (1 subgoal):
 1. fst y \<in> min_trms E
[PROOF STEP]
unfolding min_trms_def
[PROOF STATE]
proof (prove)
using this:
y \<in> E
\<forall>z. (z, y) \<in> {(x, y). (snd x, snd y) \<in> trm_ord} \<longrightarrow> z \<notin> E

goal (1 subgoal):
 1. fst y \<in> {x. \<exists>pair. (pair \<in> E \<and> (\<forall>pair'\<in>E. (snd pair', snd pair) \<notin> trm_ord)) \<and> x = fst pair}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst y \<in> min_trms E

goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst y \<in> min_trms E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst y \<in> min_trms E

goal (1 subgoal):
 1. min_trms E \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min_trms E \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smaller_lits_are_false_if_cl_not_valid:
  assumes "\<not>(validate_ground_clause (int_clset S) C)"
  shows "smaller_lits_are_false t C S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smaller_lits_are_false t C S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> smaller_lits_are_false t C S \<Longrightarrow> False
[PROOF STEP]
let ?I = "int_clset S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> smaller_lits_are_false t C S \<Longrightarrow> False
[PROOF STEP]
assume "\<not>smaller_lits_are_false t C S"
[PROOF STATE]
proof (state)
this:
\<not> smaller_lits_are_false t C S

goal (1 subgoal):
 1. \<not> smaller_lits_are_false t C S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> smaller_lits_are_false t C S
[PROOF STEP]
obtain L u v where "L \<in> C"
    and "(orient_lit L u v pos \<and> (trm_rep u S) =  (trm_rep v S))
          \<or> (orient_lit L u v neg \<and> (trm_rep u S) \<noteq> (trm_rep v S))"
[PROOF STATE]
proof (prove)
using this:
\<not> smaller_lits_are_false t C S

goal (1 subgoal):
 1. (\<And>L u v. \<lbrakk>L \<in> C; orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding smaller_lits_are_false_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>L u v. (L \<in> C \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> C \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S))

goal (1 subgoal):
 1. (\<And>L u v. \<lbrakk>L \<in> C; orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L \<in> C
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. \<not> smaller_lits_are_false t C S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in> C
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
have "(orient_lit L u v pos \<and> (trm_rep u S) =  (trm_rep v S))
          \<or> (orient_lit L u v neg \<and> (trm_rep u S) \<noteq> (trm_rep v S))"
[PROOF STATE]
proof (prove)
using this:
L \<in> C
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. \<not> smaller_lits_are_false t C S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<or> orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
assume c_pos: "(orient_lit L u v pos \<and> (trm_rep u S) =  (trm_rep v S))"
[PROOF STATE]
proof (state)
this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S

goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S
[PROOF STEP]
have "orient_lit L u v pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S

goal (1 subgoal):
 1. orient_lit L u v pos
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
orient_lit L u v pos

goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from c_pos
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S
[PROOF STEP]
have "(trm_rep u S) =  (trm_rep v S)"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v pos \<and> trm_rep u S = trm_rep v S

goal (1 subgoal):
 1. trm_rep u S = trm_rep v S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep u S = trm_rep v S

goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit L u v pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v pos
[PROOF STEP]
have "L = (Pos (Eq u v)) \<or> L = (Pos (Eq v u))"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v pos

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

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

goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(trm_rep u S) =  (trm_rep v S)\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq u v) \<or> L = Pos (Eq v u)
trm_rep u S = trm_rep v S
[PROOF STEP]
have "validate_ground_lit ?I L"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq u v) \<or> L = Pos (Eq v u)
trm_rep u S = trm_rep v S

goal (1 subgoal):
 1. validate_ground_lit (int_clset S) L
[PROOF STEP]
using validate_ground_lit.simps(1) validate_ground_eq.simps
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq u v) \<or> L = Pos (Eq v u)
trm_rep u S = trm_rep v S
validate_ground_lit ?I (Pos ?E) = validate_ground_eq ?I ?E
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_lit (int_clset S) L
[PROOF STEP]
unfolding same_values_def int_clset_def
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq u v) \<or> L = Pos (Eq v u)
trm_rep u S = trm_rep v S
validate_ground_lit ?I (Pos ?E) = validate_ground_eq ?I ?E
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) L
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
validate_ground_lit (int_clset S) L

goal (2 subgoals):
 1. orient_lit L u v pos \<and> trm_rep u S = trm_rep v S \<Longrightarrow> False
 2. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L \<in> C\<close> and assms
[PROOF STATE]
proof (chain)
picking this:
validate_ground_lit (int_clset S) L
L \<in> C
\<not> validate_ground_clause (int_clset S) C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (int_clset S) L
L \<in> C
\<not> validate_ground_clause (int_clset S) C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding int_clset_def
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (same_values (\<lambda>x. trm_rep x S)) L
L \<in> C
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x S)) C

goal (1 subgoal):
 1. False
[PROOF STEP]
using validate_ground_clause.simps
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (same_values (\<lambda>x. trm_rep x S)) L
L \<in> C
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x S)) C
validate_ground_clause ?I ?C = (\<exists>L. L \<in> ?C \<and> validate_ground_lit ?I L)

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

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
assume c_neg: "(orient_lit L u v neg \<and> (trm_rep u S) \<noteq> (trm_rep v S))"
[PROOF STATE]
proof (state)
this:
orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
have "orient_lit L u v neg"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. orient_lit L u v neg
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
orient_lit L u v neg

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from c_neg
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
have "(trm_rep u S) \<noteq> (trm_rep v S)"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit L u v neg\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit L u v neg
[PROOF STEP]
have "L = (Neg (Eq u v)) \<or> L = (Neg (Eq v u))"
[PROOF STATE]
proof (prove)
using this:
orient_lit L u v neg

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

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

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(trm_rep u S) \<noteq> (trm_rep v S)\<close>
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq u v) \<or> L = Neg (Eq v u)
trm_rep u S \<noteq> trm_rep v S
[PROOF STEP]
have "validate_ground_lit ?I L"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq u v) \<or> L = Neg (Eq v u)
trm_rep u S \<noteq> trm_rep v S

goal (1 subgoal):
 1. validate_ground_lit (int_clset S) L
[PROOF STEP]
using validate_ground_lit.simps(2) validate_ground_eq.simps
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq u v) \<or> L = Neg (Eq v u)
trm_rep u S \<noteq> trm_rep v S
validate_ground_lit ?I (Neg ?E) = (\<not> validate_ground_eq ?I ?E)
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_lit (int_clset S) L
[PROOF STEP]
unfolding same_values_def int_clset_def
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq u v) \<or> L = Neg (Eq v u)
trm_rep u S \<noteq> trm_rep v S
validate_ground_lit ?I (Neg ?E) = (\<not> validate_ground_eq ?I ?E)
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) L
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
validate_ground_lit (int_clset S) L

goal (1 subgoal):
 1. orient_lit L u v neg \<and> trm_rep u S \<noteq> trm_rep v S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>L \<in> C\<close> and assms
[PROOF STATE]
proof (chain)
picking this:
validate_ground_lit (int_clset S) L
L \<in> C
\<not> validate_ground_clause (int_clset S) C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (int_clset S) L
L \<in> C
\<not> validate_ground_clause (int_clset S) C

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding int_clset_def
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (same_values (\<lambda>x. trm_rep x S)) L
L \<in> C
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x S)) C

goal (1 subgoal):
 1. False
[PROOF STEP]
using validate_ground_clause.simps
[PROOF STATE]
proof (prove)
using this:
validate_ground_lit (same_values (\<lambda>x. trm_rep x S)) L
L \<in> C
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x S)) C
validate_ground_clause ?I ?C = (\<exists>L. L \<in> ?C \<and> validate_ground_lit ?I L)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trms_irreducible_lemma:
  assumes "all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t S)"
  shows "trms_irreducible C \<sigma> S t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trms_irreducible C \<sigma> S t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
assume "\<not>trms_irreducible C \<sigma> S t"
[PROOF STATE]
proof (state)
this:
\<not> trms_irreducible C \<sigma> S t

goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> trms_irreducible C \<sigma> S t
[PROOF STEP]
obtain x where "\<exists>x'\<in> trms_ecl C. occurs_in x (subst x' \<sigma>)" and
          "trm_rep x S \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
\<not> trms_irreducible C \<sigma> S t

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>); trm_rep x S \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. (\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>)) \<longrightarrow> (x, t) \<in> trm_ord \<longrightarrow> trm_rep x S = x)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>); trm_rep x S \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>)
trm_rep x S \<noteq> x

goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
from \<open>\<exists>x'\<in> trms_ecl C. occurs_in x (subst x' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>)
[PROOF STEP]
obtain x' where
    "x' \<in> trms_ecl C" and "occurs_in x (subst x' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x'\<in>trms_ecl C. occurs_in x (x' \<lhd> \<sigma>)

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> trms_ecl C; occurs_in x (x' \<lhd> \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> trms_ecl C
occurs_in x (x' \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
from \<open>x' \<in> trms_ecl C\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> trms_ecl C
[PROOF STEP]
have "(subst x' \<sigma>) \<in> (subst_set (trms_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
x' \<in> trms_ecl C

goal (1 subgoal):
 1. x' \<lhd> \<sigma> \<in> subst_set (trms_ecl C) \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<lhd> \<sigma> \<in> subst_set (trms_ecl C) \<sigma>

goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
from this and assms(1) \<open>occurs_in x (subst x' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<lhd> \<sigma> \<in> subst_set (trms_ecl C) \<sigma>
all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t S)
occurs_in x (x' \<lhd> \<sigma>)
[PROOF STEP]
have "trm_rep x S = x"
[PROOF STATE]
proof (prove)
using this:
x' \<lhd> \<sigma> \<in> subst_set (trms_ecl C) \<sigma>
all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t S)
occurs_in x (x' \<lhd> \<sigma>)

goal (1 subgoal):
 1. trm_rep x S = x
[PROOF STEP]
unfolding all_trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
x' \<lhd> \<sigma> \<in> subst_set (trms_ecl C) \<sigma>
\<forall>x y. x \<in> subst_set (trms_ecl C) \<sigma> \<longrightarrow> occurs_in y x \<longrightarrow> trm_rep y S = y
occurs_in x (x' \<lhd> \<sigma>)

goal (1 subgoal):
 1. trm_rep x S = x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = x

goal (1 subgoal):
 1. \<not> trms_irreducible C \<sigma> S t \<Longrightarrow> False
[PROOF STEP]
from this and \<open>trm_rep x S \<noteq> x\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = x
trm_rep x S \<noteq> x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = x
trm_rep x S \<noteq> x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_is_lower_aux:
  assumes "\<forall>y. (y,t) \<in> trm_ord \<longrightarrow>
      (y \<noteq> (trm_rep y S) \<longrightarrow> ((trm_rep y S),y) \<in> trm_ord)"
  assumes "(subterm_reduction_applicable S t)"
  shows "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
have "(lhs t,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lhs t, t) \<in> trm_ord
[PROOF STEP]
using \<open>subterm_reduction_applicable S t\<close> args_are_strictly_lower
      subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S t
is_compound ?t \<Longrightarrow> (lhs ?t, ?t) \<in> trm_ord \<and> (rhs ?t, ?t) \<in> trm_ord
subterm_reduction_applicable ?S ?t = (is_compound ?t \<and> (trm_rep (lhs ?t) ?S \<noteq> lhs ?t \<or> trm_rep (rhs ?t) ?S \<noteq> rhs ?t))

goal (1 subgoal):
 1. (lhs t, t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(lhs t, t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
have "(rhs t,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rhs t, t) \<in> trm_ord
[PROOF STEP]
using \<open>subterm_reduction_applicable S t\<close> args_are_strictly_lower
    subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S t
is_compound ?t \<Longrightarrow> (lhs ?t, ?t) \<in> trm_ord \<and> (rhs ?t, ?t) \<in> trm_ord
subterm_reduction_applicable ?S ?t = (is_compound ?t \<and> (trm_rep (lhs ?t) ?S \<noteq> lhs ?t \<or> trm_rep (rhs ?t) ?S \<noteq> rhs ?t))

goal (1 subgoal):
 1. (rhs t, t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(rhs t, t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from assms(1) and \<open>(lhs t,t) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y, t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
(lhs t, t) \<in> trm_ord
[PROOF STEP]
have
    l: "( (lhs t \<noteq> (trm_rep (lhs t) S)) \<longrightarrow> ((trm_rep  (lhs t) S), (lhs t)) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
(lhs t, t) \<in> trm_ord

goal (1 subgoal):
 1. lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from assms(1) and \<open>(rhs t,t) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y, t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
(rhs t, t) \<in> trm_ord
[PROOF STEP]
have
    r: "(rhs t \<noteq> (trm_rep (rhs t) S) \<longrightarrow> ((trm_rep  (rhs t) S), (rhs t)) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y, t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
(rhs t, t) \<in> trm_ord

goal (1 subgoal):
 1. rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from \<open>subterm_reduction_applicable S t\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S t
[PROOF STEP]
have "((trm_rep (lhs t) S) \<noteq> (lhs t) \<or> (trm_rep (rhs t) S) \<noteq> (rhs t))"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S t

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t
[PROOF STEP]
unfolding subterm_reduction_applicable_def [of S t]
[PROOF STATE]
proof (prove)
using this:
is_compound t \<and> (trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t)

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs t) S \<noteq> lhs t \<or> trm_rep (rhs t) S \<noteq> rhs t

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (lhs t) S) \<noteq> (lhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (lhs t) S \<noteq> lhs t

goal (2 subgoals):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and l
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs t) S \<noteq> lhs t
lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
have "((trm_rep  (lhs t) S), (lhs t)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs t) S \<noteq> lhs t
lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (2 subgoals):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
have i: "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),(Comb (lhs t)  (trm_rep (rhs t) S)))
      \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord
[PROOF STEP]
using trm_ord_reduction_left
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (x1 \<cdot> y, x2 \<cdot> y) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord

goal (2 subgoals):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (rhs t) S) = (rhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (rhs t) S = rhs t

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this
        and \<open>((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),(Comb (lhs t)  (trm_rep (rhs t) S)))
          \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (rhs t) S = rhs t
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t)  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (rhs t) S = rhs t
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
by (metis assms(2) is_compound.elims(2) lhs.simps(1)
            rhs.simps(1) subterm_reduction_applicable_def)
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (rhs t) S) \<noteq> (rhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (rhs t) S \<noteq> rhs t

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and r
[PROOF STATE]
proof (chain)
picking this:
trm_rep (rhs t) S \<noteq> rhs t
rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
have "((trm_rep  (rhs t) S), (rhs t)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (rhs t) S \<noteq> rhs t
rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
have "((Comb (lhs t) (trm_rep (rhs t) S)), ((Comb (lhs t) (rhs t))))  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (lhs t \<cdot> trm_rep (rhs t) S, lhs t \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
using trm_ord_reduction_right
[PROOF STATE]
proof (prove)
using this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (y \<cdot> x1, y \<cdot> x2) \<in> trm_ord

goal (1 subgoal):
 1. (lhs t \<cdot> trm_rep (rhs t) S, lhs t \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(lhs t \<cdot> trm_rep (rhs t) S, lhs t \<cdot> rhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and i
[PROOF STATE]
proof (chain)
picking this:
(lhs t \<cdot> trm_rep (rhs t) S, lhs t \<cdot> rhs t) \<in> trm_ord
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t)  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(lhs t \<cdot> trm_rep (rhs t) S, lhs t \<cdot> rhs t) \<in> trm_ord
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, lhs t \<cdot> trm_rep (rhs t) S) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
by (metis assms(2) is_compound.elims(2) lhs.simps(1) rhs.simps(1)
            subterm_reduction_applicable_def trm_ord_trans transE)
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (rhs t) S) \<noteq> (rhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (rhs t) S \<noteq> rhs t

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and r
[PROOF STATE]
proof (chain)
picking this:
trm_rep (rhs t) S \<noteq> rhs t
rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
have "((trm_rep  (rhs t) S), (rhs t)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (rhs t) S \<noteq> rhs t
rhs t \<noteq> trm_rep (rhs t) S \<longrightarrow> (trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord
[PROOF STEP]
have i: "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),(Comb (trm_rep (lhs t) S) (rhs t)))
                \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
using trm_ord_reduction_right
[PROOF STATE]
proof (prove)
using this:
(trm_rep (rhs t) S, rhs t) \<in> trm_ord
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (y \<cdot> x1, y \<cdot> x2) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (rhs t) S \<noteq> rhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (lhs t) S) = (lhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (lhs t) S = lhs t

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and
     \<open>((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),(Comb (trm_rep (lhs t) S) (rhs t))) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs t) S = lhs t
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t)  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs t) S = lhs t
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
by (metis assms(2) basic_superposition.subterm_reduction_applicable_def
            basic_superposition_axioms is_compound.elims(2) lhs.simps(1) rhs.simps(1))
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
assume "(trm_rep (lhs t) S) \<noteq> (lhs t)"
[PROOF STATE]
proof (state)
this:
trm_rep (lhs t) S \<noteq> lhs t

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and l
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs t) S \<noteq> lhs t
lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
have "((trm_rep  (lhs t) S), (lhs t)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs t) S \<noteq> lhs t
lhs t \<noteq> trm_rep (lhs t) S \<longrightarrow> (trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord
[PROOF STEP]
have "((Comb (trm_rep (lhs t) S)  (rhs t)), ((Comb (lhs t) (rhs t))))  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> rhs t, lhs t \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
using trm_ord_reduction_left
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S, lhs t) \<in> trm_ord
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (x1 \<cdot> y, x2 \<cdot> y) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> rhs t, lhs t \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> rhs t, lhs t \<cdot> rhs t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (lhs t) S \<noteq> lhs t \<Longrightarrow> (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
from this and i
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs t) S \<cdot> rhs t, lhs t \<cdot> rhs t) \<in> trm_ord
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord
[PROOF STEP]
show "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t)  \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S \<cdot> rhs t, lhs t \<cdot> rhs t) \<in> trm_ord
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, trm_rep (lhs t) S \<cdot> rhs t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
by (metis assms(2) basic_superposition.subterm_reduction_applicable_def
            basic_superposition_axioms is_compound.elims(2) lhs.simps(1) rhs.simps(1)
            trm_ord_trans transE)
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_init_def:
  shows "(trm_rep t) = (\<lambda>S. (if (subterm_reduction_applicable_aux S t)
                        then (subterm_reduction_aux S t)
                        else (get_min t (set_of_candidate_values S t))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep t = (\<lambda>S. if subterm_reduction_applicable_aux S t then subterm_reduction_aux S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
unfolding subterm_reduction_aux_def set_of_candidate_values_def candidate_values_def
   subterm_reduction_applicable_aux_def maximal_literal_is_unique_def smaller_lits_are_false_def
   trms_irreducible_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep t = (\<lambda>S. if is_compound t \<and> (lhs t, t) \<in> trm_ord \<and> (rhs t, t) \<in> trm_ord \<and> (((lhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (lhs t) S \<noteq> lhs t) \<or> ((rhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (rhs t) S \<noteq> rhs t)) then if (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord then trm_rep (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S) S else t else get_min t {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> (\<forall>x. (\<exists>x'\<in>trms_ecl CC. occurs_in x (x' \<lhd> \<sigma>)) \<longrightarrow> (x, t) \<in> trm_ord \<longrightarrow> trm_rep x S = x) \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> (\<forall>L u v. (L \<in> C \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> C \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S)) \<and> (\<forall>s''. eq_occurs_in_cl t s'' (C' - {L'}) \<sigma> \<longrightarrow> (s'', t) \<in> trm_ord \<longrightarrow> (s, t) \<in> trm_ord \<longrightarrow> trm_rep s S \<noteq> trm_rep s'' S)})
[PROOF STEP]
using trm_rep.simps [of t]
[PROOF STATE]
proof (prove)
using this:
trm_rep t = (\<lambda>S. if is_compound t \<and> (lhs t, t) \<in> trm_ord \<and> (rhs t, t) \<in> trm_ord \<and> (((lhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (lhs t) S \<noteq> lhs t) \<or> ((rhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (rhs t) S \<noteq> rhs t)) then if (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord then trm_rep (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S) S else t else get_min t {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> (\<forall>x. (\<exists>x'\<in>trms_ecl CC. occurs_in x (x' \<lhd> \<sigma>)) \<longrightarrow> (x, t) \<in> trm_ord \<longrightarrow> trm_rep x S = x) \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> (\<forall>L u v. (L \<in> C \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> C \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S)) \<and> (\<forall>s''. eq_occurs_in_cl t s'' (C' - {L'}) \<sigma> \<longrightarrow> (s'', t) \<in> trm_ord \<longrightarrow> (s, t) \<in> trm_ord \<longrightarrow> trm_rep s S \<noteq> trm_rep s'' S)})

goal (1 subgoal):
 1. trm_rep t = (\<lambda>S. if is_compound t \<and> (lhs t, t) \<in> trm_ord \<and> (rhs t, t) \<in> trm_ord \<and> (((lhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (lhs t) S \<noteq> lhs t) \<or> ((rhs t, t) \<in> trm_ord \<longrightarrow> trm_rep (rhs t) S \<noteq> rhs t)) then if (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord then trm_rep (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S) S else t else get_min t {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> (\<forall>x. (\<exists>x'\<in>trms_ecl CC. occurs_in x (x' \<lhd> \<sigma>)) \<longrightarrow> (x, t) \<in> trm_ord \<longrightarrow> trm_rep x S = x) \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> (\<forall>L u v. (L \<in> C \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> C \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t) \<in> trm_ord \<longrightarrow> (v, t) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S)) \<and> (\<forall>s''. eq_occurs_in_cl t s'' (C' - {L'}) \<sigma> \<longrightarrow> (s'', t) \<in> trm_ord \<longrightarrow> (s, t) \<in> trm_ord \<longrightarrow> trm_rep s S \<noteq> trm_rep s'' S)})
[PROOF STEP]
by force


[STATEMENT]
lemma trm_rep_aux_def:
  assumes "\<forall>y. (y,t) \<in> trm_ord \<longrightarrow>
      (y \<noteq> (trm_rep y S) \<longrightarrow> ((trm_rep y S),y) \<in> trm_ord)"
  shows "(trm_rep t S) = (if (subterm_reduction_applicable S t)
                        then (subterm_reduction S t)
                        else (get_min t (set_of_candidate_values S t)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
 2. \<not> ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
assume "subterm_reduction_applicable S t"
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S t

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
 2. \<not> ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S t
[PROOF STEP]
have "subterm_reduction_applicable_aux S t"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S t

goal (1 subgoal):
 1. subterm_reduction_applicable_aux S t
[PROOF STEP]
using args_are_strictly_lower
      subterm_reduction_applicable_def subterm_reduction_applicable_aux_def
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S t
is_compound ?t \<Longrightarrow> (lhs ?t, ?t) \<in> trm_ord \<and> (rhs ?t, ?t) \<in> trm_ord
subterm_reduction_applicable ?S ?t = (is_compound ?t \<and> (trm_rep (lhs ?t) ?S \<noteq> lhs ?t \<or> trm_rep (rhs ?t) ?S \<noteq> rhs ?t))
subterm_reduction_applicable_aux ?S ?t = (is_compound ?t \<and> (lhs ?t, ?t) \<in> trm_ord \<and> (rhs ?t, ?t) \<in> trm_ord \<and> (((lhs ?t, ?t) \<in> trm_ord \<longrightarrow> trm_rep (lhs ?t) ?S \<noteq> lhs ?t) \<or> ((rhs ?t, ?t) \<in> trm_ord \<longrightarrow> trm_rep (rhs ?t) ?S \<noteq> rhs ?t)))

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
 2. \<not> ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable_aux S t
[PROOF STEP]
have "(trm_rep t S) = (subterm_reduction_aux S t)"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable_aux S t

goal (1 subgoal):
 1. trm_rep t S = subterm_reduction_aux S t
[PROOF STEP]
using trm_rep_init_def [of t]
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable_aux S t
trm_rep t = (\<lambda>S. if subterm_reduction_applicable_aux S t then subterm_reduction_aux S t else get_min t (set_of_candidate_values S t))

goal (1 subgoal):
 1. trm_rep t S = subterm_reduction_aux S t
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
trm_rep t S = subterm_reduction_aux S t

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
 2. \<not> ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep t S = subterm_reduction_aux S t
[PROOF STEP]
have "((Comb (trm_rep (lhs t) S) (trm_rep (rhs t) S)),t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
trm_rep t S = subterm_reduction_aux S t

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
using \<open>subterm_reduction_applicable S t\<close> assms trm_rep_is_lower_aux
[PROOF STATE]
proof (prove)
using this:
trm_rep t S = subterm_reduction_aux S t
subterm_reduction_applicable S t
\<forall>y. (y, t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
\<lbrakk>\<forall>y. (y, ?t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y ?S \<longrightarrow> (trm_rep y ?S, y) \<in> trm_ord; subterm_reduction_applicable ?S ?t\<rbrakk> \<Longrightarrow> (trm_rep (lhs ?t) ?S \<cdot> trm_rep (rhs ?t) ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
 2. \<not> ?P \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs t) S \<cdot> trm_rep (rhs t) S, t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
by (metis \<open>trm_rep t S = subterm_reduction_aux S t\<close>
        \<open>subterm_reduction_applicable S t\<close>
        subterm_reduction_def
        subterm_reduction_aux_def)
[PROOF STATE]
proof (state)
this:
trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S t \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S t \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
assume "\<not>subterm_reduction_applicable S t"
[PROOF STATE]
proof (state)
this:
\<not> subterm_reduction_applicable S t

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S t \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S t
[PROOF STEP]
have "\<not>subterm_reduction_applicable_aux S t"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S t

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable_aux S t
[PROOF STEP]
using subterm_reduction_applicable_def subterm_reduction_applicable_aux_def
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S t
subterm_reduction_applicable ?S ?t = (is_compound ?t \<and> (trm_rep (lhs ?t) ?S \<noteq> lhs ?t \<or> trm_rep (rhs ?t) ?S \<noteq> rhs ?t))
subterm_reduction_applicable_aux ?S ?t = (is_compound ?t \<and> (lhs ?t, ?t) \<in> trm_ord \<and> (rhs ?t, ?t) \<in> trm_ord \<and> (((lhs ?t, ?t) \<in> trm_ord \<longrightarrow> trm_rep (lhs ?t) ?S \<noteq> lhs ?t) \<or> ((rhs ?t, ?t) \<in> trm_ord \<longrightarrow> trm_rep (rhs ?t) ?S \<noteq> rhs ?t)))

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable_aux S t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> subterm_reduction_applicable_aux S t

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S t \<Longrightarrow> trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
from this and \<open>\<not>subterm_reduction_applicable S t\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable_aux S t
\<not> subterm_reduction_applicable S t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable_aux S t
\<not> subterm_reduction_applicable S t

goal (1 subgoal):
 1. trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
by (meson trm_rep_init_def)
[PROOF STATE]
proof (state)
this:
trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))

goal:
No subgoals!
[PROOF STEP]
qed