[STATEMENT]
lemma lower_on_lit:
  assumes "lower_on \<sigma> \<eta> (vars_of_lit L)"
  assumes "((subst (Var x) \<sigma>),(subst (Var x) \<eta>)) \<in> trm_ord"
  assumes "x \<in> vars_of_lit L"
  shows "((subst_lit L \<sigma>), (subst_lit L \<eta>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
obtain t s where def_l: "L = Pos (Eq t s) | L = (Neg (Eq t s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t s. L = Pos (Eq t s) \<or> L = Neg (Eq t s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mset_lit.cases)
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)
[PROOF STEP]
have "vars_of t \<subseteq> vars_of_lit L" and "vars_of s \<subseteq> vars_of_lit L"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L &&& vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L
vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of s \<subseteq> vars_of_lit L\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of s)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)

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

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

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from def_l
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)
[PROOF STEP]
have def_ms_l: "mset_lit L = {# t,s #} \<or> mset_lit L = {# t,t,s,s #}"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}
[PROOF STEP]
have "t \<in># (mset_lit L)" and "s \<in># (mset_lit L)"
[PROOF STATE]
proof (prove)
using this:
mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}

goal (1 subgoal):
 1. t \<in># mset_lit L &&& s \<in># mset_lit L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in># mset_lit L
s \<in># mset_lit L

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from def_l
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)
[PROOF STEP]
have "mset_lit (subst_lit L \<sigma>) = {# (subst u \<sigma>). u \<in># (mset_lit L) #}"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from def_l
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)
[PROOF STEP]
have "mset_lit (subst_lit L \<eta>) = {# (subst u \<eta>). u \<in># (mset_lit L) #}"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from \<open>lower_on \<sigma> \<eta> (vars_of s)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of s)
[PROOF STEP]
have "lower_or_eq (subst s \<sigma>) (subst s \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of s)

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

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

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
let ?L = "mset_lit L"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
let ?M1 = "mset_lit (subst_lit L \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
let ?M2 = "mset_lit (subst_lit L \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t \<subseteq> vars_of_lit L\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of t)"
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)

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

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

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of s \<subseteq> vars_of_lit L\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of s)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)

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

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

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
have all_lower: "\<forall>u. (u \<in># (mset_lit L) \<longrightarrow> (((subst  u \<sigma>), (subst u \<eta>)) \<in> trm_ord
  \<or> (subst  u \<sigma>) = (subst u \<eta>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
proof  (rule allI,rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in># mset_lit L \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in># mset_lit L \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
assume "u \<in># (mset_lit L)"
[PROOF STATE]
proof (state)
this:
u \<in># mset_lit L

goal (1 subgoal):
 1. \<And>u. u \<in># mset_lit L \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
have "u = t \<or> u = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = t \<or> u = s
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> u = t \<or> u = s
 2. \<not> ?P \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
assume "mset_lit L = {# t,s #}"
[PROOF STATE]
proof (state)
this:
mset_lit L = {#t, s#}

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = t \<or> u = s
 2. \<not> ?P \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
from this and \<open>u \<in># (mset_lit L)\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_lit L = {#t, s#}
u \<in># mset_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset_lit L = {#t, s#}
u \<in># mset_lit L

goal (1 subgoal):
 1. u = t \<or> u = s
[PROOF STEP]
by (simp add: count_single insert_DiffM2 insert_noteq_member not_gr0)
[PROOF STATE]
proof (state)
this:
u = t \<or> u = s

goal (1 subgoal):
 1. mset_lit L \<noteq> {#t, s#} \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_lit L \<noteq> {#t, s#} \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
assume "\<not>mset_lit L = {# t,s #}"
[PROOF STATE]
proof (state)
this:
mset_lit L \<noteq> {#t, s#}

goal (1 subgoal):
 1. mset_lit L \<noteq> {#t, s#} \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
from this and def_ms_l
[PROOF STATE]
proof (chain)
picking this:
mset_lit L \<noteq> {#t, s#}
mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}
[PROOF STEP]
have "mset_lit L = {# t,t,s,s #}"
[PROOF STATE]
proof (prove)
using this:
mset_lit L \<noteq> {#t, s#}
mset_lit L = {#t, s#} \<or> mset_lit L = {#t, t, s, s#}

goal (1 subgoal):
 1. mset_lit L = {#t, t, s, s#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit L = {#t, t, s, s#}

goal (1 subgoal):
 1. mset_lit L \<noteq> {#t, s#} \<Longrightarrow> u = t \<or> u = s
[PROOF STEP]
from this and \<open>u \<in># (mset_lit L)\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_lit L = {#t, t, s, s#}
u \<in># mset_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset_lit L = {#t, t, s, s#}
u \<in># mset_lit L

goal (1 subgoal):
 1. u = t \<or> u = s
[PROOF STEP]
using not_gr0
[PROOF STATE]
proof (prove)
using this:
mset_lit L = {#t, t, s, s#}
u \<in># mset_lit L
(\<not> 0 < ?n) = (?n = 0)

goal (1 subgoal):
 1. u = t \<or> u = s
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
u = t \<or> u = s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u = t \<or> u = s

goal (1 subgoal):
 1. \<And>u. u \<in># mset_lit L \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = t \<or> u = s
[PROOF STEP]
show "(((subst  u \<sigma>), (subst u \<eta>)) \<in> trm_ord
  \<or> (subst  u \<sigma>) = (subst u \<eta>))"
[PROOF STATE]
proof (prove)
using this:
u = t \<or> u = s

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = t \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
 2. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
assume "u = t"
[PROOF STATE]
proof (state)
this:
u = t

goal (2 subgoals):
 1. u = t \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
 2. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
from \<open>lower_on \<sigma> \<eta> (vars_of t)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of t)
[PROOF STEP]
have "lower_or_eq (subst t \<sigma>) (subst t \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of t)

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

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

goal (2 subgoals):
 1. u = t \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
 2. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
lower_or_eq (t \<lhd> \<sigma>) (t \<lhd> \<eta>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lower_or_eq (t \<lhd> \<sigma>) (t \<lhd> \<eta>)

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

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
using \<open>u = t\<close>
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = t \<lhd> \<eta> \<or> (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
u = t

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

goal (1 subgoal):
 1. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
assume "u = s"
[PROOF STATE]
proof (state)
this:
u = s

goal (1 subgoal):
 1. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
from \<open>lower_on \<sigma> \<eta> (vars_of s)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of s)
[PROOF STEP]
have "lower_or_eq (subst s \<sigma>) (subst s \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of s)

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

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

goal (1 subgoal):
 1. u = s \<Longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
lower_or_eq (s \<lhd> \<sigma>) (s \<lhd> \<eta>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lower_or_eq (s \<lhd> \<sigma>) (s \<lhd> \<eta>)

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
unfolding lower_or_eq_def
[PROOF STATE]
proof (prove)
using this:
s \<lhd> \<sigma> = s \<lhd> \<eta> \<or> (s \<lhd> \<sigma>, s \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
[PROOF STEP]
using \<open>u = s\<close>
[PROOF STATE]
proof (prove)
using this:
s \<lhd> \<sigma> = s \<lhd> \<eta> \<or> (s \<lhd> \<sigma>, s \<lhd> \<eta>) \<in> trm_ord
u = s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
have sl_exists: "\<exists>u. (u \<in># (mset_lit L) \<and> ((subst u \<sigma>), (subst u \<eta>)) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from \<open>x \<in> vars_of_lit L\<close> and def_l
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_lit L
L = Pos (Eq t s) \<or> L = Neg (Eq t s)
[PROOF STEP]
have
      "x \<in> vars_of t \<or> x \<in> vars_of s"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit L
L = Pos (Eq t s) \<or> L = Neg (Eq t s)

goal (1 subgoal):
 1. x \<in> vars_of t \<or> x \<in> vars_of s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t \<or> x \<in> vars_of s

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t \<or> x \<in> vars_of s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t \<or> x \<in> vars_of s

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> vars_of t \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
 2. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
assume "x \<in> vars_of t"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t

goal (2 subgoals):
 1. x \<in> vars_of t \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
 2. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and \<open>lower_on \<sigma> \<eta> (vars_of t)\<close> assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t
lower_on \<sigma> \<eta> (vars_of t)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
have "( (subst t \<sigma>),(subst t \<eta>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t
lower_on \<sigma> \<eta> (vars_of t)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
using lower_subst_yields_lower_trms
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t
lower_on \<sigma> \<eta> (vars_of t)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
\<lbrakk>lower_on ?\<sigma> ?\<eta> (vars_of ?t); (Var ?x \<lhd> ?\<sigma>, Var ?x \<lhd> ?\<eta>) \<in> trm_ord; ?x \<in> vars_of ?t\<rbrakk> \<Longrightarrow> (?t \<lhd> ?\<sigma>, ?t \<lhd> ?\<eta>) \<in> trm_ord

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

goal (2 subgoals):
 1. x \<in> vars_of t \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
 2. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and \<open>t \<in># (mset_lit L)\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
t \<in># mset_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
t \<in># mset_lit L

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
assume "x \<in> vars_of s"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of s

goal (1 subgoal):
 1. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and \<open>lower_on \<sigma> \<eta> (vars_of s)\<close> assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of s
lower_on \<sigma> \<eta> (vars_of s)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
have "( (subst s \<sigma>),(subst s \<eta>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of s
lower_on \<sigma> \<eta> (vars_of s)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, s \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
using lower_subst_yields_lower_trms
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of s
lower_on \<sigma> \<eta> (vars_of s)
lower_on \<sigma> \<eta> (vars_of_lit L)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
\<lbrakk>lower_on ?\<sigma> ?\<eta> (vars_of ?t); (Var ?x \<lhd> ?\<sigma>, Var ?x \<lhd> ?\<eta>) \<in> trm_ord; ?x \<in> vars_of ?t\<rbrakk> \<Longrightarrow> (?t \<lhd> ?\<sigma>, ?t \<lhd> ?\<eta>) \<in> trm_ord

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

goal (1 subgoal):
 1. x \<in> vars_of s \<Longrightarrow> \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and \<open>s \<in># (mset_lit L)\<close>
[PROOF STATE]
proof (chain)
picking this:
(s \<lhd> \<sigma>, s \<lhd> \<eta>) \<in> trm_ord
s \<in># mset_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(s \<lhd> \<sigma>, s \<lhd> \<eta>) \<in> trm_ord
s \<in># mset_lit L

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from all_lower sl_exists and
  \<open>mset_lit (subst_lit L \<sigma>) = {# (subst u \<sigma>). u \<in># (mset_lit L) #}\<close>
  \<open>mset_lit (subst_lit L \<eta>) = {# (subst u \<eta>). u \<in># (mset_lit L) #}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}
mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}
[PROOF STEP]
have "(?M1,?M2) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}
mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}

goal (1 subgoal):
 1. (mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord
[PROOF STEP]
using trm_ord_irrefl image_mset_ordering
                        [of ?M1 "\<lambda>x. (subst x \<sigma>)" ?L ?M2 "\<lambda>x. (subst x \<eta>)" trm_ord]
[PROOF STATE]
proof (prove)
using this:
\<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>
\<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}
mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}
irrefl trm_ord
\<lbrakk>mset_lit (subst_lit L \<sigma>) = {#u \<lhd> \<sigma>. u \<in># mset_lit L#}; mset_lit (subst_lit L \<eta>) = {#u \<lhd> \<eta>. u \<in># mset_lit L#}; \<forall>u. u \<in># mset_lit L \<longrightarrow> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord \<or> u \<lhd> \<sigma> = u \<lhd> \<eta>; \<exists>u. u \<in># mset_lit L \<and> (u \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord; irrefl trm_ord\<rbrakk> \<Longrightarrow> (mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(mset_lit (subst_lit L \<sigma>), mset_lit (subst_lit L \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_on_lit_eq:
  assumes "lower_on \<sigma> \<eta> (vars_of_lit L)"
  shows "((subst_lit L \<sigma>) = (subst_lit L \<eta>)) \<or> ((subst_lit L \<sigma>), (subst_lit L \<eta>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
assume "coincide_on \<sigma> \<eta> (vars_of_lit L)"
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<eta> (vars_of_lit L)

goal (2 subgoals):
 1. ?P \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<eta> (vars_of_lit L)

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
using coincide_on_lit
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<eta> (vars_of_lit L)
coincide_on ?\<sigma> ?\<eta> (vars_of_lit ?l) \<Longrightarrow> subst_lit ?l ?\<sigma> = subst_lit ?l ?\<eta>

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

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> \<eta> (vars_of_lit L) \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> coincide_on \<sigma> \<eta> (vars_of_lit L) \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
assume "\<not>coincide_on \<sigma> \<eta> (vars_of_lit L)"
[PROOF STATE]
proof (state)
this:
\<not> coincide_on \<sigma> \<eta> (vars_of_lit L)

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> \<eta> (vars_of_lit L) \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> coincide_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
obtain x where "x \<in> vars_of_lit L"
    and "(subst (Var x) \<sigma>) \<noteq> (subst (Var x) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<not> coincide_on \<sigma> \<eta> (vars_of_lit L)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> vars_of_lit L; Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>vars_of_lit L. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> vars_of_lit L; Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars_of_lit L
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> \<eta> (vars_of_lit L) \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from \<open>x \<in> vars_of_lit L\<close> assms(1)
  \<open>(subst (Var x) \<sigma>) \<noteq> (subst (Var x) \<eta>)\<close>and assms(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
lower_on \<sigma> \<eta> (vars_of_lit L)
[PROOF STEP]
have "((subst (Var x) \<sigma>),(subst (Var x) \<eta>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit L
lower_on \<sigma> \<eta> (vars_of_lit L)
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
lower_on \<sigma> \<eta> (vars_of_lit L)

goal (1 subgoal):
 1. (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
unfolding lower_on_def lower_or_eq_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit L
\<forall>x\<in>vars_of_lit L. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
\<forall>x\<in>vars_of_lit L. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

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

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> \<eta> (vars_of_lit L) \<Longrightarrow> subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
from this assms(1) \<open>x \<in> vars_of_lit L\<close>
[PROOF STATE]
proof (chain)
picking this:
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
lower_on \<sigma> \<eta> (vars_of_lit L)
x \<in> vars_of_lit L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
lower_on \<sigma> \<eta> (vars_of_lit L)
x \<in> vars_of_lit L

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<eta> \<or> (subst_lit L \<sigma>, subst_lit L \<eta>) \<in> lit_ord
[PROOF STEP]
using lower_on_lit
[PROOF STATE]
proof (prove)
using this:
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
lower_on \<sigma> \<eta> (vars_of_lit L)
x \<in> vars_of_lit L
\<lbrakk>lower_on ?\<sigma> ?\<eta> (vars_of_lit ?L); (Var ?x \<lhd> ?\<sigma>, Var ?x \<lhd> ?\<eta>) \<in> trm_ord; ?x \<in> vars_of_lit ?L\<rbrakk> \<Longrightarrow> (subst_lit ?L ?\<sigma>, subst_lit ?L ?\<eta>) \<in> lit_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_on_cl:
  assumes "lower_on \<sigma> \<eta> (vars_of_cl (cl_ecl C))"
  assumes "((subst (Var x) \<sigma>),(subst (Var x) \<eta>)) \<in> trm_ord"
  assumes "x \<in> vars_of_cl (cl_ecl C)"
  assumes "finite (cl_ecl C)"
  shows "((C,\<sigma>), (C, \<eta>)) \<in> ecl_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
let ?M1 = "mset_ecl (C,\<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
let ?M2 = "mset_ecl (C,\<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
let ?M = "(mset_set (cl_ecl C))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
let ?f1 = "\<lambda>x. (mset_lit (subst_lit x \<sigma>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
let ?f2 = "\<lambda>x. (mset_lit (subst_lit x \<eta>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
have "?M1 = {# (?f1 u). u \<in># ?M #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}
[PROOF STEP]
using mset_ecl.simps
[PROOF STATE]
proof (prove)
using this:
mset_ecl (?C, ?\<sigma>) = {#mset_lit (subst_lit x ?\<sigma>). x \<in># mset_set (cl_ecl ?C)#}

goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
have "?M2 = {# (?f2 u). u \<in># ?M #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}
[PROOF STEP]
using mset_ecl.simps
[PROOF STATE]
proof (prove)
using this:
mset_ecl (?C, ?\<sigma>) = {#mset_lit (subst_lit x ?\<sigma>). x \<in># mset_set (cl_ecl ?C)#}

goal (1 subgoal):
 1. mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
have i: "\<forall>u. (u \<in># ?M \<longrightarrow> (((?f1 u), (?f2 u)) \<in> (mult trm_ord) \<or> (?f1 u) = (?f2 u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
proof ((rule allI),(rule impI))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
assume "u \<in># ?M"
[PROOF STATE]
proof (state)
this:
u \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
u \<in># mset_set (cl_ecl C)
[PROOF STEP]
have "u \<in> (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
u \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. u \<in> cl_ecl C
[PROOF STEP]
using count_mset_set(3)
[PROOF STATE]
proof (prove)
using this:
u \<in># mset_set (cl_ecl C)
?x \<notin> ?A \<Longrightarrow> count (mset_set ?A) ?x = 0

goal (1 subgoal):
 1. u \<in> cl_ecl C
[PROOF STEP]
by (simp add: assms(4))
[PROOF STATE]
proof (state)
this:
u \<in> cl_ecl C

goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
u \<in> cl_ecl C
lower_on \<sigma> \<eta> (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of_lit u)"
[PROOF STATE]
proof (prove)
using this:
u \<in> cl_ecl C
lower_on \<sigma> \<eta> (vars_of_cl (cl_ecl C))

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

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

goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of_lit u)
[PROOF STEP]
have "((subst_lit u \<sigma>) = (subst_lit u \<eta>))
      \<or> ((subst_lit u \<sigma>), (subst_lit u \<eta>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of_lit u)

goal (1 subgoal):
 1. subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
[PROOF STEP]
using lower_on_lit_eq
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of_lit u)
lower_on ?\<sigma> ?\<eta> (vars_of_lit ?L) \<Longrightarrow> subst_lit ?L ?\<sigma> = subst_lit ?L ?\<eta> \<or> (subst_lit ?L ?\<sigma>, subst_lit ?L ?\<eta>) \<in> lit_ord

goal (1 subgoal):
 1. subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord

goal (1 subgoal):
 1. \<And>u. u \<in># mset_set (cl_ecl C) \<Longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
[PROOF STEP]
show "(((?f1 u), (?f2 u)) \<in> (mult trm_ord) \<or> (?f1 u) = (?f2 u))"
[PROOF STATE]
proof (prove)
using this:
subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord

goal (1 subgoal):
 1. (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
subst_lit u \<sigma> = subst_lit u \<eta> \<or> (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
have "irrefl (mult trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irrefl (mult trm_ord)
[PROOF STEP]
by (simp add: irreflI trm_ord_wf wf_mult)
[PROOF STATE]
proof (state)
this:
irrefl (mult trm_ord)

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
have ii: "\<exists>u. (u \<in># ?M \<and> ((?f1 u), (?f2 u)) \<in> (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
from \<open>x \<in> vars_of_cl (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_cl (cl_ecl C)
[PROOF STEP]
obtain u where "u \<in> (cl_ecl C)" and "x \<in> vars_of_lit u"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_cl (cl_ecl C)

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

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
from assms(4) \<open>u \<in> (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl C)
u \<in> cl_ecl C
[PROOF STEP]
have "u \<in># ?M"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl C)
u \<in> cl_ecl C

goal (1 subgoal):
 1. u \<in># mset_set (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
from \<open>u \<in> (cl_ecl C)\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
u \<in> cl_ecl C
lower_on \<sigma> \<eta> (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of_lit u)"
[PROOF STATE]
proof (prove)
using this:
u \<in> cl_ecl C
lower_on \<sigma> \<eta> (vars_of_cl (cl_ecl C))

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

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

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
from \<open>x \<in> vars_of_lit u\<close> \<open>lower_on \<sigma> \<eta> (vars_of_lit u)\<close> assms(2)
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_lit u
lower_on \<sigma> \<eta> (vars_of_lit u)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
have "((subst_lit u \<sigma>), (subst_lit u \<eta>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit u
lower_on \<sigma> \<eta> (vars_of_lit u)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
[PROOF STEP]
using lower_on_lit
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit u
lower_on \<sigma> \<eta> (vars_of_lit u)
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
\<lbrakk>lower_on ?\<sigma> ?\<eta> (vars_of_lit ?L); (Var ?x \<lhd> ?\<sigma>, Var ?x \<lhd> ?\<eta>) \<in> trm_ord; ?x \<in> vars_of_lit ?L\<rbrakk> \<Longrightarrow> (subst_lit ?L ?\<sigma>, subst_lit ?L ?\<eta>) \<in> lit_ord

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

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
from this \<open>u \<in># ?M\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
u \<in># mset_set (cl_ecl C)
[PROOF STEP]
have "(u \<in># ?M \<and> ((?f1 u), (?f2 u)) \<in> (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
(subst_lit u \<sigma>, subst_lit u \<eta>) \<in> lit_ord
u \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(subst_lit u \<sigma>, subst_lit u \<eta>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
u \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
from i ii  \<open>?M1 = {# (?f1 u). u \<in># ?M #}\<close> \<open>?M2 = {# (?f2 u). u \<in># ?M #}\<close> \<open>irrefl (mult trm_ord)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
\<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}
mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}
irrefl (mult trm_ord)
[PROOF STEP]
have "(?M1,?M2) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
\<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}
mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}
irrefl (mult trm_ord)

goal (1 subgoal):
 1. (mset_ecl (C, \<sigma>), mset_ecl (C, \<eta>)) \<in> mult (mult trm_ord)
[PROOF STEP]
using image_mset_ordering [of ?M1 ?f1 ?M ?M2 ?f2 "(mult trm_ord)" ]
[PROOF STATE]
proof (prove)
using this:
\<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>)
\<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord
mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}
mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}
irrefl (mult trm_ord)
\<lbrakk>mset_ecl (C, \<sigma>) = {#mset_lit (subst_lit u \<sigma>). u \<in># mset_set (cl_ecl C)#}; mset_ecl (C, \<eta>) = {#mset_lit (subst_lit u \<eta>). u \<in># mset_set (cl_ecl C)#}; \<forall>u. u \<in># mset_set (cl_ecl C) \<longrightarrow> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord \<or> mset_lit (subst_lit u \<sigma>) = mset_lit (subst_lit u \<eta>); \<exists>u. u \<in># mset_set (cl_ecl C) \<and> (mset_lit (subst_lit u \<sigma>), mset_lit (subst_lit u \<eta>)) \<in> mult trm_ord; irrefl (mult trm_ord)\<rbrakk> \<Longrightarrow> (mset_ecl (C, \<sigma>), mset_ecl (C, \<eta>)) \<in> mult (mult trm_ord)

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

goal (1 subgoal):
 1. ((C, \<sigma>), C, \<eta>) \<in> ecl_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(mset_ecl (C, \<sigma>), mset_ecl (C, \<eta>)) \<in> mult (mult trm_ord)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset_ecl (C, \<sigma>), mset_ecl (C, \<eta>)) \<in> mult (mult trm_ord)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterm_trm_ord :
  shows "\<And> t  s.
           subterm t p s \<Longrightarrow> p \<noteq> []
          \<Longrightarrow> (s,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t s. \<lbrakk>subterm t [] s; [] \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
subterm t [] s
[] \<noteq> []

goal (2 subgoals):
 1. \<And>t s. \<lbrakk>subterm t [] s; [] \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from \<open>Nil \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
[] \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> []

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

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
case (Cons i q)
[PROOF STATE]
proof (state)
this:
\<lbrakk>subterm ?t q ?s; q \<noteq> []\<rbrakk> \<Longrightarrow> (?s, ?t) \<in> trm_ord
subterm t (i # q) s
i # q \<noteq> []

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from \<open>subterm t (i # q) s\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t (i # q) s
[PROOF STEP]
obtain t1 t2 where
        "t = (Comb t1 t2)"
[PROOF STATE]
proof (prove)
using this:
subterm t (i # q) s

goal (1 subgoal):
 1. (\<And>t1 t2. t = t1 \<cdot> t2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subterm.elims(2)
[PROOF STATE]
proof (prove)
using this:
subterm t (i # q) s
\<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>t1 t2. t = t1 \<cdot> t2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = t1 \<cdot> t2

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
have "i = Left \<or> 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 blast
[PROOF STATE]
proof (state)
this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>subterm t p s; p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord; subterm t (a # p) s; a # p \<noteq> []\<rbrakk> \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left \<or> i = indices.Right
[PROOF STEP]
show "(s,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s, t) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "i = Left"
[PROOF STATE]
proof (state)
this:
i = indices.Left

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s, t) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>t = Comb t1 t2\<close> and \<open>subterm t (i # q) s\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left
t = t1 \<cdot> t2
subterm t (i # q) s
[PROOF STEP]
have "subterm t1 q s"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left
t = t1 \<cdot> t2
subterm t (i # q) s

goal (1 subgoal):
 1. subterm t1 q s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm t1 q s

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s, t) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "q = Nil"
[PROOF STATE]
proof (state)
this:
q = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>subterm t1 q s\<close>
[PROOF STATE]
proof (chain)
picking this:
q = []
subterm t1 q s
[PROOF STEP]
have "t1 = s"
[PROOF STATE]
proof (prove)
using this:
q = []
subterm t1 q s

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

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

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
t1 = s
t = t1 \<cdot> t2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "q \<noteq> Nil"
[PROOF STATE]
proof (state)
this:
q \<noteq> []

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>subterm t1 q s\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> []
subterm t1 q s
[PROOF STEP]
have "(s,t1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []
subterm t1 q s

goal (1 subgoal):
 1. (s, t1) \<in> trm_ord
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []
subterm t1 q s
\<lbrakk>subterm ?t q ?s; q \<noteq> []\<rbrakk> \<Longrightarrow> (?s, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (s, t1) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, t1) \<in> trm_ord

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from \<open>t = Comb t1 t2\<close>
[PROOF STATE]
proof (chain)
picking this:
t = t1 \<cdot> t2
[PROOF STEP]
have "(t1,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t = t1 \<cdot> t2

goal (1 subgoal):
 1. (t1, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
t = t1 \<cdot> t2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>(s,t1) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t1, t) \<in> trm_ord
(s, t1) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(t1, t) \<in> trm_ord
(s, t1) \<in> trm_ord

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(t1, t) \<in> trm_ord
(s, t1) \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(t1, t) \<in> trm_ord
(s, t1) \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s, t) \<in> trm_ord

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "i = Right"
[PROOF STATE]
proof (state)
this:
i = indices.Right

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>t = Comb t1 t2\<close> and \<open>subterm t (i # q) s\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Right
t = t1 \<cdot> t2
subterm t (i # q) s
[PROOF STEP]
have "subterm t2 q s"
[PROOF STATE]
proof (prove)
using this:
i = indices.Right
t = t1 \<cdot> t2
subterm t (i # q) s

goal (1 subgoal):
 1. subterm t2 q s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm t2 q s

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "q = Nil"
[PROOF STATE]
proof (state)
this:
q = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>subterm t2 q s\<close>
[PROOF STATE]
proof (chain)
picking this:
q = []
subterm t2 q s
[PROOF STEP]
have "t2 = s"
[PROOF STATE]
proof (prove)
using this:
q = []
subterm t2 q s

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

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

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
t2 = s
t = t1 \<cdot> t2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
assume "q \<noteq> Nil"
[PROOF STATE]
proof (state)
this:
q \<noteq> []

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>subterm t2 q s\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> []
subterm t2 q s
[PROOF STEP]
have "(s,t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []
subterm t2 q s

goal (1 subgoal):
 1. (s, t2) \<in> trm_ord
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []
subterm t2 q s
\<lbrakk>subterm ?t q ?s; q \<noteq> []\<rbrakk> \<Longrightarrow> (?s, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (s, t2) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, t2) \<in> trm_ord

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from \<open>t = Comb t1 t2\<close>
[PROOF STATE]
proof (chain)
picking this:
t = t1 \<cdot> t2
[PROOF STEP]
have "(t2,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t = t1 \<cdot> t2

goal (1 subgoal):
 1. (t2, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
t = t1 \<cdot> t2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (1 subgoal):
 1. q \<noteq> [] \<Longrightarrow> (s, t) \<in> trm_ord
[PROOF STEP]
from this and \<open>(s,t2) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t2, t) \<in> trm_ord
(s, t2) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(t2, t) \<in> trm_ord
(s, t2) \<in> trm_ord

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(t2, t) \<in> trm_ord
(s, t2) \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(t2, t) \<in> trm_ord
(s, t2) \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s, t) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterm_trm_ord_eq :
  assumes "subterm t p s"
  shows "s = t \<or> (s,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
assume "p = Nil"
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p = []
subterm t p s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = []
subterm t p s

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

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
assume "p \<noteq> Nil"
[PROOF STATE]
proof (state)
this:
p \<noteq> []

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> []
subterm t p s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
subterm t p s

goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
using subterm_trm_ord
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
subterm t p s
\<lbrakk>subterm ?t ?p ?s; ?p \<noteq> []\<rbrakk> \<Longrightarrow> (?s, ?t) \<in> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterms_of_trm_ord_eq :
  assumes "s \<in> subterms_of t"
  shows "s = t \<or> (s,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
s \<in> subterms_of t
[PROOF STEP]
obtain p where "subterm t p s"
[PROOF STATE]
proof (prove)
using this:
s \<in> subterms_of t

goal (1 subgoal):
 1. (\<And>p. subterm t p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using occurs_in_def
[PROOF STATE]
proof (prove)
using this:
s \<in> subterms_of t
occurs_in ?t ?s = (\<exists>p. subterm ?s p ?t)

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

goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm t p s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subterm t p s

goal (1 subgoal):
 1. s = t \<or> (s, t) \<in> trm_ord
[PROOF STEP]
using subterm_trm_ord_eq
[PROOF STATE]
proof (prove)
using this:
subterm t p s
subterm ?t ?p ?s \<Longrightarrow> ?s = ?t \<or> (?s, ?t) \<in> trm_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subt_trm_ord:
  shows "t \<prec> s \<longrightarrow> (t,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<prec> s \<longrightarrow> (t, s) \<in> trm_ord
[PROOF STEP]
proof (induction s)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. t \<prec> Var x \<longrightarrow> (t, Var x) \<in> trm_ord
 2. \<And>x. t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord
 3. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. t \<prec> Var x \<longrightarrow> (t, Var x) \<in> trm_ord
 2. \<And>x. t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord
 3. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<prec> Var x \<longrightarrow> (t, Var x) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<prec> Var x \<Longrightarrow> (t, Var x) \<in> trm_ord
[PROOF STEP]
assume "t \<prec> Var x"
[PROOF STATE]
proof (state)
this:
t \<prec> Var x

goal (1 subgoal):
 1. t \<prec> Var x \<Longrightarrow> (t, Var x) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<prec> Var x
[PROOF STEP]
show "(t,Var x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<prec> Var x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<prec> Var x \<longrightarrow> (t, Var x) \<in> trm_ord

goal (2 subgoals):
 1. \<And>x. t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord
 2. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
case (Const x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord
 2. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<prec> Const x \<Longrightarrow> (t, Const x) \<in> trm_ord
[PROOF STEP]
assume "t \<prec> Const x"
[PROOF STATE]
proof (state)
this:
t \<prec> Const x

goal (1 subgoal):
 1. t \<prec> Const x \<Longrightarrow> (t, Const x) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<prec> Const x
[PROOF STEP]
show "(t,Const x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<prec> Const x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<prec> Const x \<longrightarrow> (t, Const x) \<in> trm_ord

goal (1 subgoal):
 1. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
case (Comb t1 t2)
[PROOF STATE]
proof (state)
this:
t \<prec> t1 \<longrightarrow> (t, t1) \<in> trm_ord
t \<prec> t2 \<longrightarrow> (t, t2) \<in> trm_ord

goal (1 subgoal):
 1. \<And>s1 s2. \<lbrakk>t \<prec> s1 \<longrightarrow> (t, s1) \<in> trm_ord; t \<prec> s2 \<longrightarrow> (t, s2) \<in> trm_ord\<rbrakk> \<Longrightarrow> t \<prec> s1 \<cdot> s2 \<longrightarrow> (t, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<prec> t1 \<cdot> t2 \<longrightarrow> (t, t1 \<cdot> t2) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<prec> t1 \<cdot> t2 \<Longrightarrow> (t, t1 \<cdot> t2) \<in> trm_ord
[PROOF STEP]
assume "t \<prec> Comb t1 t2"
[PROOF STATE]
proof (state)
this:
t \<prec> t1 \<cdot> t2

goal (1 subgoal):
 1. t \<prec> t1 \<cdot> t2 \<Longrightarrow> (t, t1 \<cdot> t2) \<in> trm_ord
[PROOF STEP]
show "(t, Comb t1 t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<in> trm_ord
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<notin> trm_ord \<Longrightarrow> False
[PROOF STEP]
assume "(t, Comb t1 t2) \<notin> trm_ord"
[PROOF STATE]
proof (state)
this:
(t, t1 \<cdot> t2) \<notin> trm_ord

goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<notin> trm_ord \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(t, t1 \<cdot> t2) \<notin> trm_ord
[PROOF STEP]
have i: "t \<noteq> t1"
[PROOF STATE]
proof (prove)
using this:
(t, t1 \<cdot> t2) \<notin> trm_ord

goal (1 subgoal):
 1. t \<noteq> t1
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
(t, t1 \<cdot> t2) \<notin> trm_ord
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

goal (1 subgoal):
 1. t \<noteq> t1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<noteq> t1

goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<notin> trm_ord \<Longrightarrow> False
[PROOF STEP]
from \<open>(t, Comb t1 t2) \<notin> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t, t1 \<cdot> t2) \<notin> trm_ord
[PROOF STEP]
have ii: "t \<noteq> t2"
[PROOF STATE]
proof (prove)
using this:
(t, t1 \<cdot> t2) \<notin> trm_ord

goal (1 subgoal):
 1. t \<noteq> t2
[PROOF STEP]
using trm_ord_subterm
[PROOF STATE]
proof (prove)
using this:
(t, t1 \<cdot> t2) \<notin> trm_ord
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

goal (1 subgoal):
 1. t \<noteq> t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<noteq> t2

goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<notin> trm_ord \<Longrightarrow> False
[PROOF STEP]
from i ii and \<open>t \<prec> Comb t1 t2\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> t1
t \<noteq> t2
t \<prec> t1 \<cdot> t2
[PROOF STEP]
have "t \<prec> t1 \<or> t \<prec> t2"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> t1
t \<noteq> t2
t \<prec> t1 \<cdot> t2

goal (1 subgoal):
 1. t \<prec> t1 \<or> t \<prec> t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<prec> t1 \<or> t \<prec> t2

goal (1 subgoal):
 1. (t, t1 \<cdot> t2) \<notin> trm_ord \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(t, Comb t1 t2) \<notin> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<prec> t1 \<or> t \<prec> t2
(t, t1 \<cdot> t2) \<notin> trm_ord
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
t \<prec> t1 \<or> t \<prec> t2
(t, t1 \<cdot> t2) \<notin> trm_ord

goal (1 subgoal):
 1. False
[PROOF STEP]
using Comb.IH trm_ord_subterm trm_ord_trans trans_def
[PROOF STATE]
proof (prove)
using this:
t \<prec> t1 \<or> t \<prec> t2
(t, t1 \<cdot> t2) \<notin> trm_ord
t \<prec> t1 \<longrightarrow> (t, t1) \<in> trm_ord
t \<prec> t2 \<longrightarrow> (t, t2) \<in> trm_ord
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord
trans trm_ord
trans ?r = (\<forall>x y z. (x, y) \<in> ?r \<longrightarrow> (y, z) \<in> ?r \<longrightarrow> (x, z) \<in> ?r)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<prec> t1 \<cdot> t2 \<longrightarrow> (t, t1 \<cdot> t2) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_ord_vars:
  assumes "(t,s) \<in> trm_ord"
  shows "vars_of t \<subseteq> vars_of s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
assume "\<not>vars_of t \<subseteq> vars_of s"
[PROOF STATE]
proof (state)
this:
\<not> vars_of t \<subseteq> vars_of s

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> vars_of t \<subseteq> vars_of s
[PROOF STEP]
obtain x where "x \<in> vars_of t" and "x \<notin> vars_of s"
[PROOF STATE]
proof (prove)
using this:
\<not> vars_of t \<subseteq> vars_of s

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> vars_of t; x \<notin> vars_of s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t
x \<notin> vars_of s

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
let ?\<sigma> = "[(x,s)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(t, s) \<in> trm_ord
[PROOF STEP]
have "((subst t ?\<sigma>),(subst s ?\<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t, s) \<in> trm_ord

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

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

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
let ?\<theta> = "[]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
let ?V = "vars_of s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
have "subst s ?\<theta> = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<lhd> [] = s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<lhd> [] = s

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
have "subst (Var x) ?\<sigma> = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Var x \<lhd> [(x, s)] = s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Var x \<lhd> [(x, s)] = s

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
have "coincide_on ?\<sigma> ?\<theta> ?V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coincide_on [(x, s)] [] (vars_of s)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> coincide_on [(x, s)] [] (vars_of s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> coincide_on ?\<sigma> ?\<theta> ?V"
[PROOF STATE]
proof (state)
this:
\<not> coincide_on [(x, s)] [] (vars_of s)

goal (1 subgoal):
 1. \<not> coincide_on [(x, s)] [] (vars_of s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> coincide_on [(x, s)] [] (vars_of s)
[PROOF STEP]
obtain y where "y \<in> ?V" "subst (Var y) ?\<sigma> \<noteq> subst (Var y) ?\<theta>"
[PROOF STATE]
proof (prove)
using this:
\<not> coincide_on [(x, s)] [] (vars_of s)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of s; Var y \<lhd> [(x, s)] \<noteq> Var y \<lhd> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>xa\<in>vars_of s. Var xa \<lhd> [(x, s)] = Var xa \<lhd> [])

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of s; Var y \<lhd> [(x, s)] \<noteq> Var y \<lhd> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of s
Var y \<lhd> [(x, s)] \<noteq> Var y \<lhd> []

goal (1 subgoal):
 1. \<not> coincide_on [(x, s)] [] (vars_of s) \<Longrightarrow> False
[PROOF STEP]
from \<open>subst (Var y) ?\<sigma> \<noteq> subst (Var y) ?\<theta>\<close>
[PROOF STATE]
proof (chain)
picking this:
Var y \<lhd> [(x, s)] \<noteq> Var y \<lhd> []
[PROOF STEP]
have "y = x"
[PROOF STATE]
proof (prove)
using this:
Var y \<lhd> [(x, s)] \<noteq> Var y \<lhd> []

goal (1 subgoal):
 1. y = x
[PROOF STEP]
by (metis assoc.simps(2) subst.simps(1))
[PROOF STATE]
proof (state)
this:
y = x

goal (1 subgoal):
 1. \<not> coincide_on [(x, s)] [] (vars_of s) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<notin> vars_of s\<close> \<open>y \<in> ?V\<close>
[PROOF STATE]
proof (chain)
picking this:
y = x
x \<notin> vars_of s
y \<in> vars_of s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y = x
x \<notin> vars_of s
y \<in> vars_of s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coincide_on [(x, s)] [] (vars_of s)

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this and \<open>subst s ?\<theta> = s\<close>
[PROOF STATE]
proof (chain)
picking this:
coincide_on [(x, s)] [] (vars_of s)
s \<lhd> [] = s
[PROOF STEP]
have "subst s ?\<sigma> = s"
[PROOF STATE]
proof (prove)
using this:
coincide_on [(x, s)] [] (vars_of s)
s \<lhd> [] = s

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

goal (1 subgoal):
 1. s \<lhd> [(x, s)] = s
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s \<lhd> [(x, s)] = s

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of t\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t
[PROOF STEP]
have "(Var x) \<prec> t"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t

goal (1 subgoal):
 1. Var x \<prec> t
[PROOF STEP]
using \<open>(subst t [(x, s)], subst s [(x, s)]) \<in> trm_ord\<close>
      \<open>subst s [(x, s)] = s\<close> trm_ord_wf vars_iff_occseq
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t
(t \<lhd> [(x, s)], s \<lhd> [(x, s)]) \<in> trm_ord
s \<lhd> [(x, s)] = s
wf trm_ord
(?x \<in> vars_of ?t) = (Var ?x \<prec> ?t \<or> Var ?x = ?t)

goal (1 subgoal):
 1. Var x \<prec> t
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Var x \<prec> t

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Var x \<prec> t
[PROOF STEP]
have "((Var x), t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
Var x \<prec> t

goal (1 subgoal):
 1. (Var x, t) \<in> trm_ord
[PROOF STEP]
using subt_trm_ord
[PROOF STATE]
proof (prove)
using this:
Var x \<prec> t
?t \<prec> ?s \<longrightarrow> (?t, ?s) \<in> trm_ord

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

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
(Var x, t) \<in> trm_ord
(t, s) \<in> trm_ord
[PROOF STEP]
have "(Var x,s) \<in>trm_ord"
[PROOF STATE]
proof (prove)
using this:
(Var x, t) \<in> trm_ord
(t, s) \<in> trm_ord

goal (1 subgoal):
 1. (Var x, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans trans_def
[PROOF STATE]
proof (prove)
using this:
(Var x, t) \<in> trm_ord
(t, s) \<in> trm_ord
trans trm_ord
trans ?r = (\<forall>x y z. (x, y) \<in> ?r \<longrightarrow> (y, z) \<in> ?r \<longrightarrow> (x, z) \<in> ?r)

goal (1 subgoal):
 1. (Var x, s) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(Var x, s) \<in> trm_ord

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(Var x, s) \<in> trm_ord
[PROOF STEP]
have "((subst (Var x) ?\<sigma>),(subst s ?\<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(Var x, s) \<in> trm_ord

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

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

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this and \<open>subst s ?\<sigma> = s\<close> \<open>subst (Var x) ?\<sigma> = s\<close>
[PROOF STATE]
proof (chain)
picking this:
(Var x \<lhd> [(x, s)], s \<lhd> [(x, s)]) \<in> trm_ord
s \<lhd> [(x, s)] = s
Var x \<lhd> [(x, s)] = s
[PROOF STEP]
have "(s,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(Var x \<lhd> [(x, s)], s \<lhd> [(x, s)]) \<in> trm_ord
s \<lhd> [(x, s)] = s
Var x \<lhd> [(x, s)] = s

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

goal (1 subgoal):
 1. \<not> vars_of t \<subseteq> vars_of s \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(s, s) \<in> trm_ord
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(s, s) \<in> trm_ord

goal (1 subgoal):
 1. False
[PROOF STEP]
using trm_ord_irrefl irrefl_def
[PROOF STATE]
proof (prove)
using this:
(s, s) \<in> trm_ord
irrefl trm_ord
irrefl ?r = (\<forall>a. (a, a) \<notin> ?r)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_on_ground:
  assumes "lower_on \<sigma> \<eta> V"
  assumes "ground_on  V \<eta>"
  shows "ground_on  V \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_on V \<sigma>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ground_on V \<sigma>"
[PROOF STATE]
proof (state)
this:
\<not> ground_on V \<sigma>

goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> ground_on V \<sigma>
[PROOF STEP]
obtain x where "x \<in> V" and "vars_of (subst (Var x) \<sigma>) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> ground_on V \<sigma>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> V; vars_of (Var x \<lhd> \<sigma>) \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ground_on_def ground_term_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>V. vars_of (Var x \<lhd> \<sigma>) = {})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> V; vars_of (Var x \<lhd> \<sigma>) \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> V
vars_of (Var x \<lhd> \<sigma>) \<noteq> {}

goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
from assms(1) \<open>x \<in> V\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> V
x \<in> V
[PROOF STEP]
have "(subst (Var x) \<sigma>) = (subst (Var x) \<eta>)
    \<or> ((subst (Var x) \<sigma>),(subst (Var x) \<eta>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> V
x \<in> V

goal (1 subgoal):
 1. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
unfolding lower_on_def lower_or_eq_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>V. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
x \<in> V

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

goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
have "vars_of (subst (Var x) \<sigma>) \<subseteq> vars_of (subst (Var x) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. vars_of (Var x \<lhd> \<sigma>) \<subseteq> vars_of (Var x \<lhd> \<eta>)
[PROOF STEP]
using trm_ord_vars
[PROOF STATE]
proof (prove)
using this:
Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<or> (Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
(?t, ?s) \<in> trm_ord \<Longrightarrow> vars_of ?t \<subseteq> vars_of ?s

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

goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>vars_of (subst (Var x) \<sigma>) \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of (Var x \<lhd> \<sigma>) \<subseteq> vars_of (Var x \<lhd> \<eta>)
vars_of (Var x \<lhd> \<sigma>) \<noteq> {}
[PROOF STEP]
have "vars_of (subst (Var x) \<eta>) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
vars_of (Var x \<lhd> \<sigma>) \<subseteq> vars_of (Var x \<lhd> \<eta>)
vars_of (Var x \<lhd> \<sigma>) \<noteq> {}

goal (1 subgoal):
 1. vars_of (Var x \<lhd> \<eta>) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of (Var x \<lhd> \<eta>) \<noteq> {}

goal (1 subgoal):
 1. \<not> ground_on V \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<in> V\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of (Var x \<lhd> \<eta>) \<noteq> {}
x \<in> V
ground_on V \<eta>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
vars_of (Var x \<lhd> \<eta>) \<noteq> {}
x \<in> V
ground_on V \<eta>

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding ground_on_def ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of (Var x \<lhd> \<eta>) \<noteq> {}
x \<in> V
\<forall>x\<in>V. vars_of (Var x \<lhd> \<eta>) = {}

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

goal:
No subgoals!
[PROOF STEP]
qed