[STATEMENT]
lemma subts_of_irred_trms_are_irred:
  assumes "trm_rep y S \<noteq> y"
  shows "\<And> x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. subterm x [] y \<longrightarrow> trm_rep x S \<noteq> x
 2. \<And>a p x. (\<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x) \<Longrightarrow> subterm x (a # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. subterm x [] y \<longrightarrow> trm_rep x S \<noteq> x
 2. \<And>a p x. (\<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x) \<Longrightarrow> subterm x (a # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
trm_rep y S \<noteq> y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trm_rep y S \<noteq> y

goal (1 subgoal):
 1. subterm x [] y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
by (metis subterm.simps(1))
[PROOF STATE]
proof (state)
this:
subterm x [] y \<longrightarrow> trm_rep x S \<noteq> x

goal (1 subgoal):
 1. \<And>a p x. (\<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x) \<Longrightarrow> subterm x (a # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p x. (\<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x) \<Longrightarrow> subterm x (a # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
case (Cons i p)
[PROOF STATE]
proof (state)
this:
subterm ?x p y \<longrightarrow> trm_rep ?x S \<noteq> ?x

goal (1 subgoal):
 1. \<And>a p x. (\<And>x. subterm x p y \<longrightarrow> trm_rep x S \<noteq> x) \<Longrightarrow> subterm x (a # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
show "\<And> x. subterm x (Cons i p) y \<longrightarrow> trm_rep x S \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
assume "subterm x (Cons i p) y"
[PROOF STATE]
proof (state)
this:
subterm x (i # p) y

goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm x (i # p) y
[PROOF STEP]
obtain x1 x2 where "x = Comb x1 x2"
[PROOF STATE]
proof (prove)
using this:
subterm x (i # p) y

goal (1 subgoal):
 1. (\<And>x1 x2. x = x1 \<cdot> x2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subterm.elims(2)
[PROOF STATE]
proof (prove)
using this:
subterm x (i # p) y
\<lbrakk>subterm ?x ?xa ?xb; \<And>T S. \<lbrakk>?x = T; ?xa = []; ?xb = S; T = S\<rbrakk> \<Longrightarrow> ?P; \<And>x y next S. \<lbrakk>?x = x \<cdot> y; ?xa = indices.Left # next; ?xb = S; subterm x next S\<rbrakk> \<Longrightarrow> ?P; \<And>x y next S. \<lbrakk>?x = x \<cdot> y; ?xa = indices.Right # next; ?xb = S; subterm y next S\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x1 x2. x = x1 \<cdot> x2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = x1 \<cdot> x2

goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
have "i = Left | i = Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = indices.Left \<or> i = indices.Right
[PROOF STEP]
using indices.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = indices.Left \<Longrightarrow> ?P; ?y = indices.Right \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. i = indices.Left \<or> i = indices.Right
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. \<And>x. subterm x (i # p) y \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left \<or> i = indices.Right
[PROOF STEP]
show "trm_rep x S \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. trm_rep x S \<noteq> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
assume "i = Left"
[PROOF STATE]
proof (state)
this:
i = indices.Left

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and \<open>subterm x (Cons i p) y\<close> \<open>x = Comb x1 x2\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left
subterm x (i # p) y
x = x1 \<cdot> x2
[PROOF STEP]
have "subterm x1 p y"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left
subterm x (i # p) y
x = x1 \<cdot> x2

goal (1 subgoal):
 1. subterm x1 p y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm x1 p y

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and Cons.IH
[PROOF STATE]
proof (chain)
picking this:
subterm x1 p y
subterm ?x p y \<longrightarrow> trm_rep ?x S \<noteq> ?x
[PROOF STEP]
have "trm_rep x1 S \<noteq> x1"
[PROOF STATE]
proof (prove)
using this:
subterm x1 p y
subterm ?x p y \<longrightarrow> trm_rep ?x S \<noteq> ?x

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

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and \<open>x = Comb x1 x2\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep x1 S \<noteq> x1
x = x1 \<cdot> x2
[PROOF STEP]
have "subterm_reduction_applicable S x"
[PROOF STATE]
proof (prove)
using this:
trm_rep x1 S \<noteq> x1
x = x1 \<cdot> x2

goal (1 subgoal):
 1. subterm_reduction_applicable S x
[PROOF STEP]
unfolding subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x1 S \<noteq> x1
x = x1 \<cdot> x2

goal (1 subgoal):
 1. is_compound x \<and> (trm_rep (lhs x) S \<noteq> lhs x \<or> trm_rep (rhs x) S \<noteq> rhs x)
[PROOF STEP]
by (metis is_compound.simps(3) lhs.simps(1))
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S x

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S, x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
using  trm_rep_is_lower_subt_red
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
subterm_reduction_applicable ?S ?x \<Longrightarrow> (trm_rep ?x ?S, ?x) \<in> trm_ord

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

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> trm_rep x S \<noteq> x
 2. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S \<noteq> x
[PROOF STEP]
using trm_ord_irrefl
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord
irrefl trm_ord

goal (1 subgoal):
 1. trm_rep x S \<noteq> x
[PROOF STEP]
unfolding irrefl_def
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord
\<forall>a. (a, a) \<notin> trm_ord

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

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
assume "i = Right"
[PROOF STATE]
proof (state)
this:
i = indices.Right

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and \<open>subterm x (Cons i p) y\<close> \<open>x = Comb x1 x2\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Right
subterm x (i # p) y
x = x1 \<cdot> x2
[PROOF STEP]
have "subterm x2 p y"
[PROOF STATE]
proof (prove)
using this:
i = indices.Right
subterm x (i # p) y
x = x1 \<cdot> x2

goal (1 subgoal):
 1. subterm x2 p y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm x2 p y

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and Cons.IH
[PROOF STATE]
proof (chain)
picking this:
subterm x2 p y
subterm ?x p y \<longrightarrow> trm_rep ?x S \<noteq> ?x
[PROOF STEP]
have "trm_rep x2 S \<noteq> x2"
[PROOF STATE]
proof (prove)
using this:
subterm x2 p y
subterm ?x p y \<longrightarrow> trm_rep ?x S \<noteq> ?x

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

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this and \<open>x = Comb x1 x2\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep x2 S \<noteq> x2
x = x1 \<cdot> x2
[PROOF STEP]
have "subterm_reduction_applicable S x"
[PROOF STATE]
proof (prove)
using this:
trm_rep x2 S \<noteq> x2
x = x1 \<cdot> x2

goal (1 subgoal):
 1. subterm_reduction_applicable S x
[PROOF STEP]
unfolding subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x2 S \<noteq> x2
x = x1 \<cdot> x2

goal (1 subgoal):
 1. is_compound x \<and> (trm_rep (lhs x) S \<noteq> lhs x \<or> trm_rep (rhs x) S \<noteq> rhs x)
[PROOF STEP]
by (metis is_compound.simps(3) rhs.simps(1))
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S, x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
using  trm_rep_is_lower_subt_red
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
subterm_reduction_applicable ?S ?x \<Longrightarrow> (trm_rep ?x ?S, ?x) \<in> trm_ord

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

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> trm_rep x S \<noteq> x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S \<noteq> x
[PROOF STEP]
using trm_ord_irrefl
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord
irrefl trm_ord

goal (1 subgoal):
 1. trm_rep x S \<noteq> x
[PROOF STEP]
unfolding irrefl_def
[PROOF STATE]
proof (prove)
using this:
(trm_rep x S, x) \<in> trm_ord
\<forall>a. (a, a) \<notin> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trm_rep x S \<noteq> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subterm ?x (i # p) y \<longrightarrow> trm_rep ?x S \<noteq> ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allowed_redex_coincide:
  assumes "allowed_redex t C \<sigma>"
  assumes "t \<in> subterms_of_cl (cl_ecl C)"
  assumes "coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))"
  assumes "well_constrained C"
  shows "allowed_redex t C \<sigma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allowed_redex t C \<sigma>'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
assume "\<not>allowed_redex t C \<sigma>'"
[PROOF STATE]
proof (state)
this:
\<not> allowed_redex t C \<sigma>'

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

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> trms_ecl C; occurs_in (t \<lhd> \<sigma>') (s \<lhd> \<sigma>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding allowed_redex_def
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> (\<exists>s\<in>trms_ecl C. occurs_in (t \<lhd> \<sigma>') (s \<lhd> \<sigma>'))

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

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from \<open>s \<in> trms_ecl C\<close> and assms(4)
[PROOF STATE]
proof (chain)
picking this:
s \<in> trms_ecl C
well_constrained C
[PROOF STEP]
have "vars_of s \<subseteq> vars_of_cl (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
s \<in> trms_ecl C
well_constrained C

goal (1 subgoal):
 1. vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
using dom_trm_vars
[PROOF STATE]
proof (prove)
using this:
s \<in> trms_ecl C
well_constrained C
dom_trm ?t ?C \<Longrightarrow> vars_of ?t \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
unfolding well_constrained_def
[PROOF STATE]
proof (prove)
using this:
s \<in> trms_ecl C
\<forall>y. y \<in> trms_ecl C \<longrightarrow> dom_trm y (cl_ecl C)
dom_trm ?t ?C \<Longrightarrow> vars_of ?t \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
have "vars_of s \<subseteq> vars_of_cl (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
using subterm_vars
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)
?u \<in> subterms_of_cl ?C \<Longrightarrow> vars_of ?u \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of s \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "coincide_on \<sigma> \<sigma>' (vars_of s)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))

goal (1 subgoal):
 1. coincide_on \<sigma> \<sigma>' (vars_of s)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_cl (cl_ecl C)
\<forall>x\<in>vars_of_cl (cl_ecl C). Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'

goal (1 subgoal):
 1. \<forall>x\<in>vars_of s. Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<sigma>' (vars_of s)

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> \<sigma>' (vars_of s)
[PROOF STEP]
have "(subst s \<sigma>) = (subst s \<sigma>')"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of s)

goal (1 subgoal):
 1. s \<lhd> \<sigma> = s \<lhd> \<sigma>'
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of s)
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

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

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
t \<in> subterms_of_cl (cl_ecl C)
[PROOF STEP]
have "vars_of t \<subseteq> vars_of_cl (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
t \<in> subterms_of_cl (cl_ecl C)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
using subterm_vars
[PROOF STATE]
proof (prove)
using this:
t \<in> subterms_of_cl (cl_ecl C)
?u \<in> subterms_of_cl ?C \<Longrightarrow> vars_of ?u \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "coincide_on \<sigma> \<sigma>' (vars_of t)"
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))

goal (1 subgoal):
 1. coincide_on \<sigma> \<sigma>' (vars_of t)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_cl (cl_ecl C)
\<forall>x\<in>vars_of_cl (cl_ecl C). Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'

goal (1 subgoal):
 1. \<forall>x\<in>vars_of t. Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<sigma>' (vars_of t)

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> \<sigma>' (vars_of t)
[PROOF STEP]
have "(subst t \<sigma>) = (subst t \<sigma>')"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of t)

goal (1 subgoal):
 1. t \<lhd> \<sigma> = t \<lhd> \<sigma>'
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of t)
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

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

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst s \<sigma>) = (subst s \<sigma>')\<close> and \<open>occurs_in (subst t \<sigma>') (subst s \<sigma>')\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = t \<lhd> \<sigma>'
s \<lhd> \<sigma> = s \<lhd> \<sigma>'
occurs_in (t \<lhd> \<sigma>') (s \<lhd> \<sigma>')
[PROOF STEP]
have "occurs_in (subst t \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = t \<lhd> \<sigma>'
s \<lhd> \<sigma> = s \<lhd> \<sigma>'
occurs_in (t \<lhd> \<sigma>') (s \<lhd> \<sigma>')

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

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this and \<open>s \<in> trms_ecl C\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C
[PROOF STEP]
have "\<not>allowed_redex t C \<sigma>"
[PROOF STATE]
proof (prove)
using this:
occurs_in (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>
[PROOF STEP]
unfolding allowed_redex_def
[PROOF STATE]
proof (prove)
using this:
occurs_in (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C

goal (1 subgoal):
 1. \<not> \<not> (\<exists>s\<in>trms_ecl C. occurs_in (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> allowed_redex t C \<sigma>

goal (1 subgoal):
 1. \<not> allowed_redex t C \<sigma>' \<Longrightarrow> False
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<not> allowed_redex t C \<sigma>
allowed_redex t C \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> allowed_redex t C \<sigma>
allowed_redex t C \<sigma>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irred_terms_and_reduced_subst:
  assumes "f = (\<lambda>t. (trm_rep t S))"
  assumes "\<eta> = (map_subst f \<sigma>)"
  assumes "all_trms_irreducible (subst_set E \<sigma>) f"
  assumes "I = int_clset S"
  assumes "equivalent_on  \<sigma> \<eta> (vars_of_cl (cl_ecl C)) I"
  assumes "lower_on \<eta> \<sigma>  (vars_of_cl (cl_ecl C))"
  assumes "E = (trms_ecl C)"
  assumes "\<forall>x \<in> S. \<forall>y. (y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x))"
  assumes "C \<in> S"
  assumes "fo_interpretation I"
  shows "all_trms_irreducible (subst_set E \<eta> ) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_trms_irreducible (subst_set E \<eta>) f
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
assume "\<not>all_trms_irreducible (subst_set E \<eta>) f"
[PROOF STATE]
proof (state)
this:
\<not> all_trms_irreducible (subst_set E \<eta>) f

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> all_trms_irreducible (subst_set E \<eta>) f
[PROOF STEP]
obtain t y where "y \<in> (subst_set E \<eta>)" "occurs_in t y" "f t \<noteq> t"
[PROOF STATE]
proof (prove)
using this:
\<not> all_trms_irreducible (subst_set E \<eta>) f

goal (1 subgoal):
 1. (\<And>y t. \<lbrakk>y \<in> subst_set E \<eta>; occurs_in t y; f t \<noteq> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding all_trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x y. x \<in> subst_set E \<eta> \<longrightarrow> occurs_in y x \<longrightarrow> f y = y)

goal (1 subgoal):
 1. (\<And>y t. \<lbrakk>y \<in> subst_set E \<eta>; occurs_in t y; f t \<noteq> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
y \<in> subst_set E \<eta>
occurs_in t y
f t \<noteq> t

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>occurs_in t y\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in t y
[PROOF STEP]
obtain p where "subterm y p t"
[PROOF STATE]
proof (prove)
using this:
occurs_in t y

goal (1 subgoal):
 1. (\<And>p. subterm y p t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding occurs_in_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. subterm y p t

goal (1 subgoal):
 1. (\<And>p. subterm y p t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm y p t

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this and \<open>f t \<noteq> t\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
subterm y p t
f t \<noteq> t
f = (\<lambda>t. trm_rep t S)
[PROOF STEP]
have "f y \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
subterm y p t
f t \<noteq> t
f = (\<lambda>t. trm_rep t S)

goal (1 subgoal):
 1. f y \<noteq> y
[PROOF STEP]
using subts_of_irred_trms_are_irred
[PROOF STATE]
proof (prove)
using this:
subterm y p t
f t \<noteq> t
f = (\<lambda>t. trm_rep t S)
trm_rep ?y ?S \<noteq> ?y \<Longrightarrow> subterm ?x ?p ?y \<longrightarrow> trm_rep ?x ?S \<noteq> ?x

goal (1 subgoal):
 1. f y \<noteq> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f y \<noteq> y

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>y \<in> (subst_set E \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> subst_set E \<eta>
[PROOF STEP]
obtain z where "z \<in> E" and "y = (subst z \<eta>)"
[PROOF STATE]
proof (prove)
using this:
y \<in> subst_set E \<eta>

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

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>z \<in> E\<close>
[PROOF STATE]
proof (chain)
picking this:
z \<in> E
[PROOF STEP]
have "(subst z \<sigma>) \<in> (subst_set E \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
z \<in> E

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

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
have "subterm (subst z \<sigma>) [] (subst z \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterm (z \<lhd> \<sigma>) [] (z \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm (z \<lhd> \<sigma>) [] (z \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subterm (z \<lhd> \<sigma>) [] (z \<lhd> \<sigma>)
[PROOF STEP]
have "occurs_in (subst z \<sigma>) (subst z \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subterm (z \<lhd> \<sigma>) [] (z \<lhd> \<sigma>)

goal (1 subgoal):
 1. occurs_in (z \<lhd> \<sigma>) (z \<lhd> \<sigma>)
[PROOF STEP]
unfolding occurs_in_def
[PROOF STATE]
proof (prove)
using this:
subterm (z \<lhd> \<sigma>) [] (z \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<exists>p. subterm (z \<lhd> \<sigma>) p (z \<lhd> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
occurs_in (z \<lhd> \<sigma>) (z \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) and \<open>(subst z \<sigma>) \<in> (subst_set E \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in (z \<lhd> \<sigma>) (z \<lhd> \<sigma>)
all_trms_irreducible (subst_set E \<sigma>) f
z \<lhd> \<sigma> \<in> subst_set E \<sigma>
[PROOF STEP]
have "f (subst z \<sigma>) = (subst z \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
occurs_in (z \<lhd> \<sigma>) (z \<lhd> \<sigma>)
all_trms_irreducible (subst_set E \<sigma>) f
z \<lhd> \<sigma> \<in> subst_set E \<sigma>

goal (1 subgoal):
 1. f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>
[PROOF STEP]
unfolding all_trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
occurs_in (z \<lhd> \<sigma>) (z \<lhd> \<sigma>)
\<forall>x y. x \<in> subst_set E \<sigma> \<longrightarrow> occurs_in y x \<longrightarrow> f y = y
z \<lhd> \<sigma> \<in> subst_set E \<sigma>

goal (1 subgoal):
 1. f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this and \<open>f y \<noteq> y\<close> and \<open>y = (subst z \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>
f y \<noteq> y
y = z \<lhd> \<eta>
[PROOF STEP]
have "(subst z \<sigma>) \<noteq> (subst z \<eta>)"
[PROOF STATE]
proof (prove)
using this:
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>
f y \<noteq> y
y = z \<lhd> \<eta>

goal (1 subgoal):
 1. z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>z \<in> E\<close> and assms(7) assms(8) assms(9)
[PROOF STATE]
proof (chain)
picking this:
z \<in> E
E = trms_ecl C
\<forall>x\<in>S. \<forall>y. y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x)
C \<in> S
[PROOF STEP]
have "dom_trm z (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
z \<in> E
E = trms_ecl C
\<forall>x\<in>S. \<forall>y. y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x)
C \<in> S

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

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
dom_trm z (cl_ecl C)
[PROOF STEP]
have "vars_of z \<subseteq> vars_of_cl (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
dom_trm z (cl_ecl C)

goal (1 subgoal):
 1. vars_of z \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
using dom_trm_vars
[PROOF STATE]
proof (prove)
using this:
dom_trm z (cl_ecl C)
dom_trm ?t ?C \<Longrightarrow> vars_of ?t \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of z \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this assms(5)
[PROOF STATE]
proof (chain)
picking this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
equivalent_on \<sigma> \<eta> (vars_of_cl (cl_ecl C)) I
[PROOF STEP]
have "equivalent_on \<sigma> \<eta> (vars_of z) I"
[PROOF STATE]
proof (prove)
using this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
equivalent_on \<sigma> \<eta> (vars_of_cl (cl_ecl C)) I

goal (1 subgoal):
 1. equivalent_on \<sigma> \<eta> (vars_of z) I
[PROOF STEP]
unfolding equivalent_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
\<forall>x\<in>vars_of_cl (cl_ecl C). I (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>)

goal (1 subgoal):
 1. \<forall>x\<in>vars_of z. I (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
equivalent_on \<sigma> \<eta> (vars_of z) I

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>vars_of z \<subseteq> vars_of_cl (cl_ecl C)\<close> assms(6)
[PROOF STATE]
proof (chain)
picking this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
lower_on \<eta> \<sigma> (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "lower_on \<eta> \<sigma>  (vars_of z)"
[PROOF STATE]
proof (prove)
using this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
lower_on \<eta> \<sigma> (vars_of_cl (cl_ecl C))

goal (1 subgoal):
 1. lower_on \<eta> \<sigma> (vars_of z)
[PROOF STEP]
unfolding lower_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of z \<subseteq> vars_of_cl (cl_ecl C)
\<forall>x\<in>vars_of_cl (cl_ecl C). lower_or_eq (Var x \<lhd> \<eta>) (Var x \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<forall>x\<in>vars_of z. lower_or_eq (Var x \<lhd> \<eta>) (Var x \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lower_on \<eta> \<sigma> (vars_of z)

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst z \<sigma>) \<noteq> (subst z \<eta>)\<close>
       \<open>lower_on \<eta> \<sigma>  (vars_of z)\<close>
[PROOF STATE]
proof (chain)
picking this:
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
lower_on \<eta> \<sigma> (vars_of z)
[PROOF STEP]
have "( (subst z \<eta>),(subst z \<sigma>) ) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
lower_on \<eta> \<sigma> (vars_of z)

goal (1 subgoal):
 1. (z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using lower_on_term
[PROOF STATE]
proof (prove)
using this:
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
lower_on \<eta> \<sigma> (vars_of z)
lower_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> lower_or_eq (?t \<lhd> ?\<sigma>) (?t \<lhd> ?\<eta>)

goal (1 subgoal):
 1. (z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding lower_or_eq_def
[PROOF STATE]
proof (prove)
using this:
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
lower_on \<eta> \<sigma> (vars_of z)
lower_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta> \<or> (?t \<lhd> ?\<sigma>, ?t \<lhd> ?\<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "( (subst z \<sigma>),(subst z \<eta>) ) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
using trm_ord_trans trm_ord_irrefl irrefl_def trans_def
[PROOF STATE]
proof (prove)
using this:
(z \<lhd> \<eta>, z \<lhd> \<sigma>) \<in> trm_ord
trans trm_ord
irrefl trm_ord
irrefl ?r = (\<forall>a. (a, a) \<notin> ?r)
trans ?r = (\<forall>x y z. (x, y) \<in> ?r \<longrightarrow> (y, z) \<in> ?r \<longrightarrow> (x, z) \<in> ?r)

goal (1 subgoal):
 1. (z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from assms(10) \<open>equivalent_on \<sigma> \<eta> (vars_of z) I\<close>
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
equivalent_on \<sigma> \<eta> (vars_of z) I
[PROOF STEP]
have "(I (subst z \<sigma>) (subst z \<eta>))"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
equivalent_on \<sigma> \<eta> (vars_of z) I

goal (1 subgoal):
 1. I (z \<lhd> \<sigma>) (z \<lhd> \<eta>)
[PROOF STEP]
using equivalent_on_term
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
equivalent_on \<sigma> \<eta> (vars_of z) I
\<lbrakk>congruence ?I; equivalent_on ?\<sigma> ?\<eta> (vars_of ?t) ?I\<rbrakk> \<Longrightarrow> ?I (?t \<lhd> ?\<sigma>) (?t \<lhd> ?\<eta>)

goal (1 subgoal):
 1. I (z \<lhd> \<sigma>) (z \<lhd> \<eta>)
[PROOF STEP]
unfolding fo_interpretation_def
[PROOF STATE]
proof (prove)
using this:
congruence I
equivalent_on \<sigma> \<eta> (vars_of z) I
\<lbrakk>congruence ?I; equivalent_on ?\<sigma> ?\<eta> (vars_of ?t) ?I\<rbrakk> \<Longrightarrow> ?I (?t \<lhd> ?\<sigma>) (?t \<lhd> ?\<eta>)

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

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this and assms(4) assms(1) \<open>f (subst z \<sigma>) = (subst z \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
I (z \<lhd> \<sigma>) (z \<lhd> \<eta>)
I = int_clset S
f = (\<lambda>t. trm_rep t S)
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>
[PROOF STEP]
have "(subst z \<sigma>) = f (subst z \<eta>)"
[PROOF STATE]
proof (prove)
using this:
I (z \<lhd> \<sigma>) (z \<lhd> \<eta>)
I = int_clset S
f = (\<lambda>t. trm_rep t S)
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>

goal (1 subgoal):
 1. z \<lhd> \<sigma> = f (z \<lhd> \<eta>)
[PROOF STEP]
unfolding same_values_def int_clset_def
[PROOF STATE]
proof (prove)
using this:
I (z \<lhd> \<sigma>) (z \<lhd> \<eta>)
I = (\<lambda>x y. trm_rep x S = trm_rep y S)
f = (\<lambda>t. trm_rep t S)
f (z \<lhd> \<sigma>) = z \<lhd> \<sigma>

goal (1 subgoal):
 1. z \<lhd> \<sigma> = f (z \<lhd> \<eta>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z \<lhd> \<sigma> = f (z \<lhd> \<eta>)

goal (1 subgoal):
 1. \<not> all_trms_irreducible (subst_set E \<eta>) f \<Longrightarrow> False
[PROOF STEP]
from this \<open>( (subst z \<sigma>),(subst z \<eta>) ) \<notin> trm_ord\<close>
    \<open>(subst z \<sigma>) \<noteq> (subst z \<eta>)\<close> assms(1)
[PROOF STATE]
proof (chain)
picking this:
z \<lhd> \<sigma> = f (z \<lhd> \<eta>)
(z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
f = (\<lambda>t. trm_rep t S)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
z \<lhd> \<sigma> = f (z \<lhd> \<eta>)
(z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
f = (\<lambda>t. trm_rep t S)

goal (1 subgoal):
 1. False
[PROOF STEP]
using trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
z \<lhd> \<sigma> = f (z \<lhd> \<eta>)
(z \<lhd> \<sigma>, z \<lhd> \<eta>) \<notin> trm_ord
z \<lhd> \<sigma> \<noteq> z \<lhd> \<eta>
f = (\<lambda>t. trm_rep t S)
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_valid_literal:
  assumes "L \<in> C"
  assumes "orient_lit_inst L t s pos \<sigma>"
  assumes "\<not>(validate_ground_clause (int_clset S) (subst_cl C \<sigma>))"
  shows "trm_rep (subst t \<sigma>) S \<noteq> trm_rep (subst s \<sigma>) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S \<noteq> trm_rep (s \<lhd> \<sigma>) S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
assume neg_hyp: "trm_rep (subst t \<sigma>) S = trm_rep (subst s \<sigma>) S"
[PROOF STATE]
proof (state)
this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
let ?I = "int_clset S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from neg_hyp
[PROOF STATE]
proof (chain)
picking this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
[PROOF STEP]
have "validate_ground_eq ?I (Eq (subst t \<sigma>) (subst s \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S

goal (1 subgoal):
 1. validate_ground_eq (int_clset S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
unfolding same_values_def int_clset_def
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S

goal (1 subgoal):
 1. validate_ground_eq (\<lambda>x y. trm_rep x S = trm_rep y S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
using validate_ground_eq.simps
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_eq (\<lambda>x y. trm_rep x S = trm_rep y S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
validate_ground_eq (int_clset S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from \<open>trm_rep (subst t \<sigma>) S = trm_rep (subst s \<sigma>) S\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
[PROOF STEP]
have "validate_ground_eq ?I (Eq (subst s \<sigma>) (subst t \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S

goal (1 subgoal):
 1. validate_ground_eq (int_clset S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
[PROOF STEP]
unfolding same_values_def  int_clset_def
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S

goal (1 subgoal):
 1. validate_ground_eq (\<lambda>x y. trm_rep x S = trm_rep y S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
[PROOF STEP]
using validate_ground_eq.simps
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
validate_ground_eq ?I (Eq ?t ?s) = ?I ?t ?s

goal (1 subgoal):
 1. validate_ground_eq (\<lambda>x y. trm_rep x S = trm_rep y S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
validate_ground_eq (int_clset S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst L t s pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L t s pos \<sigma>
[PROOF STEP]
have "L = (Pos (Eq t s)) \<or> L = (Pos (Eq s t))"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s pos \<sigma>

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

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

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
have "subst_lit L \<sigma> = (Pos (Eq (subst t \<sigma>)  (subst s \<sigma>))) \<or>
            subst_lit L \<sigma> = (Pos (Eq (subst s \<sigma>)  (subst t \<sigma>)))"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

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

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>validate_ground_eq ?I (Eq (subst s \<sigma>) (subst t \<sigma>))\<close>
        and \<open>validate_ground_eq ?I (Eq (subst t \<sigma>) (subst s \<sigma>))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<sigma> = Pos (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Pos (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
validate_ground_eq (int_clset S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
validate_ground_eq (int_clset S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))
[PROOF STEP]
have "validate_ground_lit ?I (subst_lit L \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> = Pos (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Pos (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
validate_ground_eq (int_clset S) (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))
validate_ground_eq (int_clset S) (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>))

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

goal (1 subgoal):
 1. validate_ground_lit (int_clset S) (subst_lit L \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
validate_ground_lit (int_clset S) (subst_lit L \<sigma>)

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
L \<in> C
[PROOF STEP]
have "(subst_lit L \<sigma>) \<in> (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> C

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

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from \<open>(subst_lit L \<sigma>) \<in> (subst_cl C \<sigma>)\<close>
          and \<open>validate_ground_lit ?I (subst_lit L \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
validate_ground_lit (int_clset S) (subst_lit L \<sigma>)
[PROOF STEP]
have "validate_ground_clause ?I (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
validate_ground_lit (int_clset S) (subst_lit L \<sigma>)

goal (1 subgoal):
 1. validate_ground_clause (int_clset S) (subst_cl C \<sigma>)
[PROOF STEP]
using validate_ground_clause.elims(3)
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> \<in> subst_cl C \<sigma>
validate_ground_lit (int_clset S) (subst_lit L \<sigma>)
\<lbrakk>\<not> validate_ground_clause ?x ?xa; \<And>I C. \<lbrakk>?x = I; ?xa = C; \<nexists>L. L \<in> C \<and> validate_ground_lit I L\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. validate_ground_clause (int_clset S) (subst_cl C \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
validate_ground_clause (int_clset S) (subst_cl C \<sigma>)

goal (1 subgoal):
 1. trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> validate_ground_clause ?I (subst_cl C \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause (int_clset S) (subst_cl C \<sigma>)
\<not> validate_ground_clause (int_clset S) (subst_cl C \<sigma>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause (int_clset S) (subst_cl C \<sigma>)
\<not> validate_ground_clause (int_clset S) (subst_cl C \<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L t s polarity \<theta>
[PROOF STEP]
have "L = Pos (Eq t s) \<or> L = Pos (Eq s t)"
      and "( (subst t \<theta>),  (subst s \<theta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L t s polarity \<theta>

goal (1 subgoal):
 1. L = Pos (Eq t s) \<or> L = Pos (Eq s t) &&& (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
polarity = pos
(L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = neg

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
have "(subst t \<theta>) = (subst (subst t \<sigma>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
have "(subst s \<theta>) = (subst (subst s \<sigma>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from \<open>(subst t \<theta>) = (subst (subst t \<sigma>) \<eta>)\<close>
         \<open>(subst s \<theta>) = (subst (subst s \<sigma>) \<eta>)\<close>
         \<open>( (subst t \<theta>),  (subst s \<theta>)) \<notin> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<theta> = t \<lhd> \<sigma> \<lhd> \<eta>
s \<lhd> \<theta> = s \<lhd> \<sigma> \<lhd> \<eta>
(t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord
[PROOF STEP]
have "( (subst (subst t \<sigma>) \<eta>),(subst (subst s \<sigma>) \<eta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<theta> = t \<lhd> \<sigma> \<lhd> \<eta>
s \<lhd> \<theta> = s \<lhd> \<sigma> \<lhd> \<eta>
(t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
have "( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using trm_ord_subst
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord
\<forall>s x y. (x, y) \<in> trm_ord \<longrightarrow> (x \<lhd> s, y \<lhd> s) \<in> trm_ord

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

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

goal (1 subgoal):
 1. orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
polarity = pos
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. (L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
orient_lit_inst L t s polarity \<sigma>

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L t s polarity \<theta>
[PROOF STEP]
have "L = Neg (Eq t s) \<or> L = Neg (Eq s t)"
      and "( (subst t \<theta>),  (subst s \<theta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L t s polarity \<theta>

goal (1 subgoal):
 1. L = Neg (Eq t s) \<or> L = Neg (Eq s t) &&& (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
polarity = neg
(L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord \<and> polarity = neg

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
have "(subst t \<theta>) = (subst (subst t \<sigma>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
have "(subst s \<theta>) = (subst (subst s \<sigma>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from \<open>(subst t \<theta>) = (subst (subst t \<sigma>) \<eta>)\<close>
         \<open>(subst s \<theta>) = (subst (subst s \<sigma>) \<eta>)\<close>
         \<open>( (subst t \<theta>),  (subst s \<theta>)) \<notin> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<theta> = t \<lhd> \<sigma> \<lhd> \<eta>
s \<lhd> \<theta> = s \<lhd> \<sigma> \<lhd> \<eta>
(t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord
[PROOF STEP]
have "( (subst (subst t \<sigma>) \<eta>),(subst (subst s \<sigma>) \<eta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<theta> = t \<lhd> \<sigma> \<lhd> \<eta>
s \<lhd> \<theta> = s \<lhd> \<sigma> \<lhd> \<eta>
(t \<lhd> \<theta>, s \<lhd> \<theta>) \<notin> trm_ord

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
have "( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using trm_ord_subst
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma> \<lhd> \<eta>, s \<lhd> \<sigma> \<lhd> \<eta>) \<notin> trm_ord
\<forall>s x y. (x, y) \<in> trm_ord \<longrightarrow> (x \<lhd> s, y \<lhd> s) \<in> trm_ord

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

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

goal (1 subgoal):
 1. orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
polarity = neg
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (1 subgoal):
 1. (L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
orient_lit_inst L t s polarity \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
orient_lit_inst L t s polarity \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_maximal_literal:
  assumes "maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)"
  shows "maximal_literal L C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_literal L C
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal L C \<Longrightarrow> False
[PROOF STEP]
assume "\<not>maximal_literal L C"
[PROOF STATE]
proof (state)
this:
\<not> maximal_literal L C

goal (1 subgoal):
 1. \<not> maximal_literal L C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal_literal L C
[PROOF STEP]
obtain M where "M \<in> C" and "(L,M) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal L C

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>M \<in> C; (L, M) \<in> lit_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. x \<in> C \<longrightarrow> (L, x) \<notin> lit_ord)

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>M \<in> C; (L, M) \<in> lit_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<in> C
(L, M) \<in> lit_ord

goal (1 subgoal):
 1. \<not> maximal_literal L C \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> C
[PROOF STEP]
have "(subst_lit M \<sigma>) \<in> (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
M \<in> C

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

goal (1 subgoal):
 1. \<not> maximal_literal L C \<Longrightarrow> False
[PROOF STEP]
from \<open>(L,M) \<in> lit_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(L, M) \<in> lit_ord
[PROOF STEP]
have "((subst_lit L \<sigma>),(subst_lit M \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(L, M) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
using lit_ord_subst
[PROOF STATE]
proof (prove)
using this:
(L, M) \<in> lit_ord
(?L, ?M) \<in> lit_ord \<Longrightarrow> (subst_lit ?L ?\<sigma>, subst_lit ?M ?\<sigma>) \<in> lit_ord

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

goal (1 subgoal):
 1. \<not> maximal_literal L C \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst_lit M \<sigma>) \<in> (subst_cl C \<sigma>)\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
subst_lit M \<sigma> \<in> subst_cl C \<sigma>
maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
subst_lit M \<sigma> \<in> subst_cl C \<sigma>
maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
subst_lit M \<sigma> \<in> subst_cl C \<sigma>
\<forall>x. x \<in> subst_cl C \<sigma> \<longrightarrow> (subst_lit L \<sigma>, x) \<notin> lit_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_eligible_literal:
  assumes "eligible_literal L C \<sigma>"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  shows "eligible_literal L C \<theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
eligible_literal L C \<sigma>
[PROOF STEP]
have "(L \<in> sel (cl_ecl C) \<or>
    (sel(cl_ecl C) = {}
    \<and> (maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>))))"
[PROOF STATE]
proof (prove)
using this:
eligible_literal L C \<sigma>

goal (1 subgoal):
 1. L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
unfolding eligible_literal_def
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L \<in> sel (cl_ecl C) \<Longrightarrow> eligible_literal L C \<theta>
 2. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
assume "L \<in> sel (cl_ecl C)"
[PROOF STATE]
proof (state)
this:
L \<in> sel (cl_ecl C)

goal (2 subgoals):
 1. L \<in> sel (cl_ecl C) \<Longrightarrow> eligible_literal L C \<theta>
 2. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in> sel (cl_ecl C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C)

goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
unfolding eligible_literal_def
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C)

goal (1 subgoal):
 1. L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eligible_literal L C \<theta>

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
assume "sel(cl_ecl C) = {}
     \<and> (maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>))"
[PROOF STATE]
proof (state)
this:
sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
have "sel (cl_ecl C) = {}" and "maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. sel (cl_ecl C) = {} &&& maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sel (cl_ecl C) = {}
maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
let ?\<sigma> = "\<theta> \<lozenge> \<eta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_lit L \<sigma>) = (subst_lit L ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_lit
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
?\<sigma> \<doteq> ?\<eta> \<Longrightarrow> subst_lit ?l ?\<sigma> = subst_lit ?l ?\<eta>

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

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<sigma> = subst_lit L (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "(subst_lit L \<sigma>) = (subst_lit (subst_lit L \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> = subst_lit L (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit (subst_lit L \<theta>) \<eta>
[PROOF STEP]
using composition_of_substs_lit [of L \<theta> \<eta>]
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> = subst_lit L (\<theta> \<lozenge> \<eta>)
subst_lit (subst_lit L \<theta>) \<eta> = subst_lit L (\<theta> \<lozenge> \<eta>)

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

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_cl (cl_ecl C) \<sigma>) = (subst_cl (cl_ecl C) ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

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

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_cl (cl_ecl C) \<sigma> = subst_cl (cl_ecl C) (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
have "(subst_cl (cl_ecl C) \<sigma>) = (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
subst_cl (cl_ecl C) \<sigma> = subst_cl (cl_ecl C) (\<theta> \<lozenge> \<eta>)

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

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

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
from \<open>maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)\<close>
      \<open>(subst_lit L \<sigma>) = (subst_lit (subst_lit L \<theta>) \<eta>)\<close>
      \<open>(subst_cl (cl_ecl C) \<sigma>) = (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
subst_lit L \<sigma> = subst_lit (subst_lit L \<theta>) \<eta>
subst_cl (cl_ecl C) \<sigma> = subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>
[PROOF STEP]
have "maximal_literal (subst_lit (subst_lit L \<theta>) \<eta>)
         (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)
subst_lit L \<sigma> = subst_lit (subst_lit L \<theta>) \<eta>
subst_cl (cl_ecl C) \<sigma> = subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>

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

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit (subst_lit L \<theta>) \<eta>) (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
[PROOF STEP]
have "maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)"
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit (subst_lit L \<theta>) \<eta>) (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)

goal (1 subgoal):
 1. maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
using lift_maximal_literal
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit (subst_lit L \<theta>) \<eta>) (subst_cl (subst_cl (cl_ecl C) \<theta>) \<eta>)
maximal_literal (subst_lit ?L ?\<sigma>) (subst_cl ?C ?\<sigma>) \<Longrightarrow> maximal_literal ?L ?C

goal (1 subgoal):
 1. maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)

goal (1 subgoal):
 1. sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>) \<Longrightarrow> eligible_literal L C \<theta>
[PROOF STEP]
from this and \<open>sel (cl_ecl C) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
sel (cl_ecl C) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
sel (cl_ecl C) = {}

goal (1 subgoal):
 1. eligible_literal L C \<theta>
[PROOF STEP]
unfolding eligible_literal_def
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
sel (cl_ecl C) = {}

goal (1 subgoal):
 1. L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<theta>) (subst_cl (cl_ecl C) \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eligible_literal L C \<theta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eligible_literal L C \<theta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_allowed_redex:
    assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
    assumes "(allowed_redex u C \<sigma>)"
    shows "(allowed_redex u C \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allowed_redex u C \<theta>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(allowed_redex u C \<theta>)"
[PROOF STATE]
proof (state)
this:
\<not> allowed_redex u C \<theta>

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> allowed_redex u C \<theta>
[PROOF STEP]
obtain s where "s \<in> (trms_ecl C)" and "(occurs_in (subst u \<theta>) (subst s \<theta>))"
[PROOF STATE]
proof (prove)
using this:
\<not> allowed_redex u C \<theta>

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> trms_ecl C; occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding allowed_redex_def
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> (\<exists>s\<in>trms_ecl C. occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> trms_ecl C; occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s \<in> trms_ecl C
occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from \<open>(occurs_in (subst u \<theta>) (subst s \<theta>))\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)
[PROOF STEP]
have "(occurs_in (subst (subst u \<theta>) \<eta>) (subst (subst s \<theta>) \<eta>))"
[PROOF STATE]
proof (prove)
using this:
occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)

goal (1 subgoal):
 1. occurs_in (u \<lhd> \<theta> \<lhd> \<eta>) (s \<lhd> \<theta> \<lhd> \<eta>)
[PROOF STEP]
using substs_preserve_occurs_in
[PROOF STATE]
proof (prove)
using this:
occurs_in (u \<lhd> \<theta>) (s \<lhd> \<theta>)
occurs_in ?s ?t \<Longrightarrow> occurs_in (?s \<lhd> ?\<sigma>) (?t \<lhd> ?\<sigma>)

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

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst u \<sigma>) = (subst (subst u \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from \<open>\<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst s \<sigma>) = (subst (subst s \<theta>) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from \<open>(occurs_in (subst (subst u \<theta>) \<eta>) (subst (subst s \<theta>) \<eta>))\<close>
    \<open>(subst u \<sigma>) = (subst (subst u \<theta>) \<eta>)\<close>
    \<open>(subst s \<sigma>) = (subst (subst s \<theta>) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in (u \<lhd> \<theta> \<lhd> \<eta>) (s \<lhd> \<theta> \<lhd> \<eta>)
u \<lhd> \<sigma> = u \<lhd> \<theta> \<lhd> \<eta>
s \<lhd> \<sigma> = s \<lhd> \<theta> \<lhd> \<eta>
[PROOF STEP]
have "(occurs_in (subst u \<sigma>) (subst s \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
occurs_in (u \<lhd> \<theta> \<lhd> \<eta>) (s \<lhd> \<theta> \<lhd> \<eta>)
u \<lhd> \<sigma> = u \<lhd> \<theta> \<lhd> \<eta>
s \<lhd> \<sigma> = s \<lhd> \<theta> \<lhd> \<eta>

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

goal (1 subgoal):
 1. \<not> allowed_redex u C \<theta> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>s \<in> (trms_ecl C)\<close> assms(2)
[PROOF STATE]
proof (chain)
picking this:
occurs_in (u \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C
allowed_redex u C \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
occurs_in (u \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C
allowed_redex u C \<sigma>

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding allowed_redex_def
[PROOF STATE]
proof (prove)
using this:
occurs_in (u \<lhd> \<sigma>) (s \<lhd> \<sigma>)
s \<in> trms_ecl C
\<not> (\<exists>s\<in>trms_ecl C. occurs_in (u \<lhd> \<sigma>) (s \<lhd> \<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_decompose_literal:
  assumes "decompose_literal (subst_lit L \<sigma>) t s polarity"
  assumes "subst_eq \<theta> (comp \<sigma> \<eta>)"
  shows "decompose_literal (subst_lit L \<theta>) (subst t \<eta>) (subst s \<eta>) polarity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?L = "(subst_lit L \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?t' = "(subst t \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?s' = "(subst s \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?\<theta> = "(comp \<sigma> \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
let ?L' = "(subst_lit ?L \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_lit L \<theta>) = (subst_lit L ?\<theta>)"
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_lit L \<theta> = subst_lit L (\<sigma> \<lozenge> \<eta>)
[PROOF STEP]
using
      subst_eq_lit
[PROOF STATE]
proof (prove)
using this:
\<theta> \<doteq> \<sigma> \<lozenge> \<eta>
?\<sigma> \<doteq> ?\<eta> \<Longrightarrow> subst_lit ?l ?\<sigma> = subst_lit ?l ?\<eta>

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

goal (1 subgoal):
 1. decompose_literal (subst_lit L \<theta>) (t \<lhd> \<eta>) (s \<lhd> \<eta>) polarity
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<theta> = subst_lit L (\<sigma> \<lozenge> \<eta>)
[PROOF STEP]
have "(subst_lit L \<theta>) = ?L'"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<theta> = subst_lit L (\<sigma> \<lozenge> \<eta>)

goal (1 subgoal):
 1. subst_lit L \<theta> = subst_lit (subst_lit L \<sigma>) \<eta>
[PROOF STEP]
using composition_of_substs_lit
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<theta> = subst_lit L (\<sigma> \<lozenge> \<eta>)
subst_lit (subst_lit ?l ?\<sigma>) ?\<eta> = subst_lit ?l (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_lit L \<theta> = subst_lit (subst_lit L \<sigma>) \<eta>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
subst_lit L \<theta> = subst_lit (subst_lit L \<sigma>) \<eta>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed