[STATEMENT]
lemma cl_ord_eq_trans:
  shows "trans cl_ord_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
have "\<forall>r. trans r = (\<forall>p pa pb. ((p::'a literal set \<times> ('a \<times> 'a trm) list, pa) \<notin> r \<or> (pa, pb) \<notin> r)
          \<or> (p, pb) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. trans r = (\<forall>p pa pb. ((p, pa) \<notin> r \<or> (pa, pb) \<notin> r) \<or> (p, pb) \<in> r)
[PROOF STEP]
by (simp add: trans_def)
[PROOF STATE]
proof (state)
this:
\<forall>r. trans r = (\<forall>p pa pb. ((p, pa) \<notin> r \<or> (pa, pb) \<notin> r) \<or> (p, pb) \<in> r)

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. trans r = (\<forall>p pa pb. ((p, pa) \<notin> r \<or> (pa, pb) \<notin> r) \<or> (p, pb) \<in> r)
[PROOF STEP]
obtain pp :: "(('a literal set \<times> ('a \<times> 'a trm) list) \<times> 'a literal set \<times> ('a \<times> 'a trm) list) set \<Rightarrow> 'a literal set \<times> ('a \<times> 'a trm) list" and ppa :: "(('a literal set \<times> ('a \<times> 'a trm) list) \<times> 'a literal set \<times> ('a \<times> 'a trm) list) set \<Rightarrow> 'a literal set \<times> ('a \<times> 'a trm) list" and ppb :: "(('a literal set \<times> ('a \<times> 'a trm) list) \<times> 'a literal set \<times> ('a \<times> 'a trm) list) set \<Rightarrow> 'a literal set \<times> ('a \<times> 'a trm) list" where
    f1: "\<forall>r. (\<not> trans r \<or> (\<forall>p pa pb. (p, pa) \<notin> r \<or> (pa, pb) \<notin> r \<or> (p, pb) \<in> r)) \<and> (trans r \<or> (pp r, ppa r) \<in> r \<and> (ppa r, ppb r) \<in> r \<and> (pp r, ppb r) \<notin> r)"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. trans r = (\<forall>p pa pb. ((p, pa) \<notin> r \<or> (pa, pb) \<notin> r) \<or> (p, pb) \<in> r)

goal (1 subgoal):
 1. (\<And>pp ppa ppb. \<forall>r. (\<not> trans r \<or> (\<forall>p pa pb. (p, pa) \<notin> r \<or> (pa, pb) \<notin> r \<or> (p, pb) \<in> r)) \<and> (trans r \<or> (pp r, ppa r) \<in> r \<and> (ppa r, ppb r) \<in> r \<and> (pp r, ppb r) \<notin> r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types))
[PROOF STATE]
proof (state)
this:
\<forall>r. (\<not> trans r \<or> (\<forall>p pa pb. (p, pa) \<notin> r \<or> (pa, pb) \<notin> r \<or> (p, pb) \<in> r)) \<and> (trans r \<or> (pp r, ppa r) \<in> r \<and> (ppa r, ppb r) \<in> r \<and> (pp r, ppb r) \<notin> r)

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
have f2: "trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}
[PROOF STEP]
using cl_ord_def cl_ord_trans
[PROOF STATE]
proof (prove)
using this:
cl_ord = {(x, y). (mset_cl x, mset_cl y) \<in> mult (mult trm_ord)}
trans cl_ord

goal (1 subgoal):
 1. trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
assume "\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa)"
[PROOF STATE]
proof (state)
this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa)

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa)

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
assume "(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}"
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
assume "(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord)"
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord)

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord)
[PROOF STEP]
have "(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))"
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord)

goal (1 subgoal):
 1. (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))
[PROOF STEP]
have "((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}"
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))

goal (1 subgoal):
 1. ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
using f2 f1
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<noteq> mset_cl (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))
trans {(p, pa). (mset_cl p, mset_cl pa) \<in> mult (mult trm_ord)}
\<forall>r. (\<not> trans r \<or> (\<forall>p pa pb. (p, pa) \<notin> r \<or> (pa, pb) \<notin> r \<or> (p, pb) \<in> r)) \<and> (trans r \<or> (pp r, ppa r) \<in> r \<and> (ppa r, ppb r) \<in> r \<and> (pp r, ppb r) \<notin> r)

goal (1 subgoal):
 1. ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord) \<Longrightarrow> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord) \<Longrightarrow> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
have "(mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}"
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)}
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<notin> mult (mult trm_ord) \<Longrightarrow> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
have "(mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}"
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
using cl_ord_def
[PROOF STATE]
proof (prove)
using this:
(ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p}
cl_ord = {(x, y). (mset_cl x, mset_cl y) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa) \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa) \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
have "(pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}"
[PROOF STATE]
proof (prove)
using this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa) \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
using cl_ord_def
[PROOF STATE]
proof (prove)
using this:
\<not> (case (ppa (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa}), ppb (cl_ord \<union> {(p, pa). mset_cl p = mset_cl pa})) of (p, pa) \<Rightarrow> mset_cl p = mset_cl pa) \<Longrightarrow> (mset_cl (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})), mset_cl (ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}))) \<in> mult (mult trm_ord) \<or> ((pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> {(pa, p). mset_cl pa = mset_cl p}) \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). (mset_cl pa, mset_cl p) \<in> mult (mult trm_ord)} \<and> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
cl_ord = {(x, y). (mset_cl x, mset_cl y) \<in> mult (mult trm_ord)}

goal (1 subgoal):
 1. (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
[PROOF STEP]
have "trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})"
[PROOF STATE]
proof (prove)
using this:
(pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}

goal (1 subgoal):
 1. trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
(pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (ppa (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<notin> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p} \<or> (pp (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}), ppb (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})) \<in> cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p}
\<forall>r. (\<not> trans r \<or> (\<forall>p pa pb. (p, pa) \<notin> r \<or> (pa, pb) \<notin> r \<or> (p, pb) \<in> r)) \<and> (trans r \<or> (pp r, ppa r) \<in> r \<and> (ppa r, ppb r) \<in> r \<and> (pp r, ppb r) \<notin> r)

goal (1 subgoal):
 1. trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})

goal (1 subgoal):
 1. trans cl_ord_eq
[PROOF STEP]
unfolding cl_ord_eq_def
[PROOF STATE]
proof (prove)
using this:
trans (cl_ord \<union> {(pa, p). mset_cl pa = mset_cl p})

goal (1 subgoal):
 1. trans (cl_ord \<union> {(x, y). mset_cl x = mset_cl y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trans cl_ord_eq

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_ecl_ord:
  shows "wf ecl_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ecl_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf ecl_ord
[PROOF STEP]
have "wf (mult trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (mult trm_ord)
[PROOF STEP]
using trm_ord_wf and wf_mult
[PROOF STATE]
proof (prove)
using this:
wf trm_ord
wf ?r \<Longrightarrow> wf (mult ?r)

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

goal (1 subgoal):
 1. wf ecl_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf (mult trm_ord)
[PROOF STEP]
have "wf (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
using this:
wf (mult trm_ord)

goal (1 subgoal):
 1. wf (mult (mult trm_ord))
[PROOF STEP]
using wf_mult
[PROOF STATE]
proof (prove)
using this:
wf (mult trm_ord)
wf ?r \<Longrightarrow> wf (mult ?r)

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

goal (1 subgoal):
 1. wf ecl_ord
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wf (mult (mult trm_ord))

goal (1 subgoal):
 1. wf ecl_ord
[PROOF STEP]
using ecl_ord_def
        and measure_wf [of "(mult (mult trm_ord))" ecl_ord mset_ecl]
[PROOF STATE]
proof (prove)
using this:
wf (mult (mult trm_ord))
ecl_ord = {(x, y). (mset_ecl x, mset_ecl y) \<in> mult (mult trm_ord)}
\<lbrakk>wf (mult (mult trm_ord)); ecl_ord = {(x, y). (mset_ecl x, mset_ecl y) \<in> mult (mult trm_ord)}\<rbrakk> \<Longrightarrow> wf ecl_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> = subst_cl (cl_ecl C) \<sigma>'
[PROOF STEP]
using coincide_on_cl
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))
coincide_on ?\<sigma> ?\<eta> (vars_of_cl ?C) \<Longrightarrow> subst_cl ?C ?\<sigma> = subst_cl ?C ?\<eta>

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

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

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

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

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

goal (1 subgoal):
 1. subst_lit L \<sigma> = subst_lit L \<sigma>'
[PROOF STEP]
using coincide_on_lit
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (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 \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit L \<sigma> = subst_lit L \<sigma>'

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_or_eq_monotonic:
  assumes "lower_or_eq t1 s1"
  assumes "lower_or_eq t2 s2"
  shows "lower_or_eq (Comb t1 t2) (Comb s1 s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lower_or_eq (t1 \<cdot> t2) (s1 \<cdot> s2)
[PROOF STEP]
unfolding lower_or_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t1 \<cdot> t2 = s1 \<cdot> s2 \<or> (t1 \<cdot> t2, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
using trm_ord_reduction_left trm_ord_reduction_right
[PROOF STATE]
proof (prove)
using this:
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (x1 \<cdot> y, x2 \<cdot> y) \<in> trm_ord
\<forall>x1 x2 y. (x1, x2) \<in> trm_ord \<longrightarrow> (y \<cdot> x1, y \<cdot> x2) \<in> trm_ord

goal (1 subgoal):
 1. t1 \<cdot> t2 = s1 \<cdot> s2 \<or> (t1 \<cdot> t2, s1 \<cdot> s2) \<in> trm_ord
[PROOF STEP]
by (metis assms(1) assms(2) lower_or_eq_def trm_ord_trans transD)


[STATEMENT]
lemma lower_on_term:
  shows "\<And> \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t) \<Longrightarrow>
    (lower_or_eq (subst t \<sigma>) (subst t \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t) \<Longrightarrow> lower_or_eq (t \<lhd> \<sigma>) (t \<lhd> \<eta>)
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Var x)) \<Longrightarrow> lower_or_eq (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>)
 2. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Const x)) \<Longrightarrow> lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
 3. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:
lower_on \<sigma> \<eta> (vars_of (Var x))

goal (3 subgoals):
 1. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Var x)) \<Longrightarrow> lower_or_eq (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>)
 2. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Const x)) \<Longrightarrow> lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
 3. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of (Var x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of (Var x))

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

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

goal (2 subgoals):
 1. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Const x)) \<Longrightarrow> lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
 2. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Const x)) \<Longrightarrow> lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
 2. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
case (Const x)
[PROOF STATE]
proof (state)
this:
lower_on \<sigma> \<eta> (vars_of (Const x))

goal (2 subgoals):
 1. \<And>x \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Const x)) \<Longrightarrow> lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
 2. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)
[PROOF STEP]
unfolding lower_or_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Const x \<lhd> \<sigma> = Const x \<lhd> \<eta> \<or> (Const x \<lhd> \<sigma>, Const x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lower_or_eq (Const x \<lhd> \<sigma>) (Const x \<lhd> \<eta>)

goal (1 subgoal):
 1. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
case (Comb t1 t2)
[PROOF STATE]
proof (state)
this:
lower_on ?\<sigma> ?\<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> ?\<sigma>) (t1 \<lhd> ?\<eta>)
lower_on ?\<sigma> ?\<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> ?\<sigma>) (t2 \<lhd> ?\<eta>)
lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))

goal (1 subgoal):
 1. \<And>t1 t2 \<sigma> \<eta>. \<lbrakk>\<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t1) \<Longrightarrow> lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>); \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of t2) \<Longrightarrow> lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>); lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))\<rbrakk> \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
show "\<And> \<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (Comb t1 t2)) \<Longrightarrow>
    (lower_or_eq (subst  (Comb t1 t2) \<sigma>) (subst  (Comb t1 t2) \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
fix \<sigma> \<eta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
assume "lower_on \<sigma> \<eta> (vars_of (Comb t1 t2))"
[PROOF STATE]
proof (state)
this:
lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))

goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))
[PROOF STEP]
have "lower_on \<sigma> \<eta> (vars_of t1)" and "lower_on \<sigma> \<eta> (vars_of t2)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2))

goal (1 subgoal):
 1. lower_on \<sigma> \<eta> (vars_of t1) &&& lower_on \<sigma> \<eta> (vars_of t2)
[PROOF STEP]
unfolding lower_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars_of (t1 \<cdot> t2). lower_or_eq (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>)

goal (1 subgoal):
 1. \<forall>x\<in>vars_of t1. lower_or_eq (Var x \<lhd> \<sigma>) (Var x \<lhd> \<eta>) &&& \<forall>x\<in>vars_of t2. 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 t1)
lower_on \<sigma> \<eta> (vars_of t2)

goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
from \<open>lower_on \<sigma> \<eta> (vars_of t1)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of t1)
[PROOF STEP]
have "lower_or_eq (subst t1 \<sigma>) (subst t1 \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of t1)

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

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

goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
from \<open>lower_on \<sigma> \<eta> (vars_of t2)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_on \<sigma> \<eta> (vars_of t2)
[PROOF STEP]
have "lower_or_eq (subst t2 \<sigma>) (subst t2 \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_on \<sigma> \<eta> (vars_of t2)

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

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

goal (1 subgoal):
 1. \<And>\<sigma> \<eta>. lower_on \<sigma> \<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
from \<open>lower_or_eq (subst t1 \<sigma>) (subst t1 \<eta>)\<close> \<open>lower_or_eq (subst t2 \<sigma>) (subst t2 \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>)
lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>)
[PROOF STEP]
show "lower_or_eq (subst  (Comb t1 t2) \<sigma>) (subst (Comb t1 t2) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>)
lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>)

goal (1 subgoal):
 1. lower_or_eq (t1 \<cdot> t2 \<lhd> \<sigma>) (t1 \<cdot> t2 \<lhd> \<eta>)
[PROOF STEP]
using lower_or_eq_monotonic
[PROOF STATE]
proof (prove)
using this:
lower_or_eq (t1 \<lhd> \<sigma>) (t1 \<lhd> \<eta>)
lower_or_eq (t2 \<lhd> \<sigma>) (t2 \<lhd> \<eta>)
\<lbrakk>lower_or_eq ?t1.0 ?s1.0; lower_or_eq ?t2.0 ?s2.0\<rbrakk> \<Longrightarrow> lower_or_eq (?t1.0 \<cdot> ?t2.0) (?s1.0 \<cdot> ?s2.0)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lower_on ?\<sigma> ?\<eta> (vars_of (t1 \<cdot> t2)) \<Longrightarrow> lower_or_eq (t1 \<cdot> t2 \<lhd> ?\<sigma>) (t1 \<cdot> t2 \<lhd> ?\<eta>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_substs_yield_diff_trms:
  assumes "(subst (Var x) \<sigma>) \<noteq> (subst (Var x) \<eta>)"
  shows "(x \<in> vars_of t)
   \<Longrightarrow> (subst t \<sigma>) \<noteq> (subst t \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars_of t \<Longrightarrow> t \<lhd> \<sigma> \<noteq> t \<lhd> \<eta>
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa. x \<in> vars_of (Var xa) \<Longrightarrow> Var xa \<lhd> \<sigma> \<noteq> Var xa \<lhd> \<eta>
 2. \<And>xa. x \<in> vars_of (Const xa) \<Longrightarrow> Const xa \<lhd> \<sigma> \<noteq> Const xa \<lhd> \<eta>
 3. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
case (Var y)
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (Var y)

goal (3 subgoals):
 1. \<And>xa. x \<in> vars_of (Var xa) \<Longrightarrow> Var xa \<lhd> \<sigma> \<noteq> Var xa \<lhd> \<eta>
 2. \<And>xa. x \<in> vars_of (Const xa) \<Longrightarrow> Const xa \<lhd> \<sigma> \<noteq> Const xa \<lhd> \<eta>
 3. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
show "(x \<in> vars_of (Var y))  \<Longrightarrow> (subst  (Var y) \<sigma>) \<noteq> (subst  (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars_of (Var y) \<Longrightarrow> Var y \<lhd> \<sigma> \<noteq> Var y \<lhd> \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars_of (Var y) \<Longrightarrow> Var y \<lhd> \<sigma> \<noteq> Var y \<lhd> \<eta>
[PROOF STEP]
assume "(x \<in> vars_of  (Var y))"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (Var y)

goal (1 subgoal):
 1. x \<in> vars_of (Var y) \<Longrightarrow> Var y \<lhd> \<sigma> \<noteq> Var y \<lhd> \<eta>
[PROOF STEP]
from \<open>(x \<in> vars_of  (Var y))\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of (Var y)
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of (Var y)

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

goal (1 subgoal):
 1. x \<in> vars_of (Var y) \<Longrightarrow> Var y \<lhd> \<sigma> \<noteq> Var y \<lhd> \<eta>
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
x = y
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
[PROOF STEP]
show "(subst  (Var y) \<sigma>) \<noteq> (subst  (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x = y
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (Var y) \<Longrightarrow> Var y \<lhd> \<sigma> \<noteq> Var y \<lhd> \<eta>

goal (2 subgoals):
 1. \<And>xa. x \<in> vars_of (Const xa) \<Longrightarrow> Const xa \<lhd> \<sigma> \<noteq> Const xa \<lhd> \<eta>
 2. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. x \<in> vars_of (Const xa) \<Longrightarrow> Const xa \<lhd> \<sigma> \<noteq> Const xa \<lhd> \<eta>
 2. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
case (Const y)
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (Const y)

goal (2 subgoals):
 1. \<And>xa. x \<in> vars_of (Const xa) \<Longrightarrow> Const xa \<lhd> \<sigma> \<noteq> Const xa \<lhd> \<eta>
 2. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
show " (x \<in> vars_of (Const y))
   \<Longrightarrow> (subst  (Const y) \<sigma>) \<noteq> (subst  (Const y) \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars_of (Const y) \<Longrightarrow> Const y \<lhd> \<sigma> \<noteq> Const y \<lhd> \<eta>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> vars_of (Const y); \<not> Const y \<lhd> \<sigma> \<noteq> Const y \<lhd> \<eta>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>(x \<in> vars_of  (Const y))\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of (Const y)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of (Const y)

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:
x \<in> vars_of (Const y) \<Longrightarrow> Const y \<lhd> \<sigma> \<noteq> Const y \<lhd> \<eta>

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
case (Comb t1 t2)
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>
x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>
x \<in> vars_of (t1 \<cdot> t2)

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>; x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>; x \<in> vars_of (t1 \<cdot> t2)\<rbrakk> \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
show " (x \<in> vars_of (Comb t1 t2))
   \<Longrightarrow> (subst  (Comb t1 t2) \<sigma>) \<noteq> (subst (Comb t1 t2) \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vars_of (t1 \<cdot> t2) \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars_of (t1 \<cdot> t2) \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
assume "(x \<in> vars_of (Comb t1 t2))"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (t1 \<cdot> t2)

goal (1 subgoal):
 1. x \<in> vars_of (t1 \<cdot> t2) \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
from \<open>x \<in> vars_of (Comb t1 t2)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of (t1 \<cdot> t2)
[PROOF STEP]
have "x \<in> vars_of t1 \<or> x \<in> vars_of t2"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of (t1 \<cdot> t2)

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

goal (1 subgoal):
 1. x \<in> vars_of (t1 \<cdot> t2) \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t1 \<or> x \<in> vars_of t2
[PROOF STEP]
show "(subst  (Comb t1 t2) \<sigma>) \<noteq> (subst (Comb t1 t2) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t1 \<or> x \<in> vars_of t2

goal (1 subgoal):
 1. t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> vars_of t1 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
 2. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
assume "x \<in> vars_of t1"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t1

goal (2 subgoals):
 1. x \<in> vars_of t1 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
 2. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t1
[PROOF STEP]
have "(subst t1 \<sigma>) \<noteq> (subst t1 \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t1

goal (1 subgoal):
 1. t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>
[PROOF STEP]
using Comb.IH
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t1
x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>
x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>

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

goal (2 subgoals):
 1. x \<in> vars_of t1 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
 2. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>

goal (1 subgoal):
 1. t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>

goal (1 subgoal):
 1. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
assume "x \<in> vars_of t2"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of t2

goal (1 subgoal):
 1. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of t2
[PROOF STEP]
have "(subst t2 \<sigma>) \<noteq> (subst t2 \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t2

goal (1 subgoal):
 1. t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>
[PROOF STEP]
using Comb.IH
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of t2
x \<in> vars_of t1 \<Longrightarrow> t1 \<lhd> \<sigma> \<noteq> t1 \<lhd> \<eta>
x \<in> vars_of t2 \<Longrightarrow> t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>

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

goal (1 subgoal):
 1. x \<in> vars_of t2 \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t2 \<lhd> \<sigma> \<noteq> t2 \<lhd> \<eta>

goal (1 subgoal):
 1. t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> vars_of (t1 \<cdot> t2) \<Longrightarrow> t1 \<cdot> t2 \<lhd> \<sigma> \<noteq> t1 \<cdot> t2 \<lhd> \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_subst_yields_lower_trms:
  assumes "lower_on \<sigma> \<eta> (vars_of t)"
  assumes "((subst (Var x) \<sigma>),(subst (Var x) \<eta>)) \<in> trm_ord"
  assumes "(x \<in> vars_of t)"
  shows "((subst t \<sigma>),(subst t \<eta>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from assms(1)
[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 (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
have "(subst (Var x) \<sigma>) \<noteq> (subst (Var x) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
(Var x \<lhd> \<sigma>, Var x \<lhd> \<eta>) \<in> trm_ord

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

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

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
x \<in> vars_of t
[PROOF STEP]
have "(subst t \<sigma>) \<noteq> (subst t \<eta>)"
[PROOF STATE]
proof (prove)
using this:
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta>
x \<in> vars_of t

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

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

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
from this and \<open>lower_or_eq (subst t \<sigma>) (subst t \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<noteq> t \<lhd> \<eta>
lower_or_eq (t \<lhd> \<sigma>) (t \<lhd> \<eta>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> t \<lhd> \<eta>
lower_or_eq (t \<lhd> \<sigma>) (t \<lhd> \<eta>)

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, t \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
unfolding lower_or_eq_def
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> t \<lhd> \<eta>
t \<lhd> \<sigma> = t \<lhd> \<eta> \<or> (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:
No subgoals!
[PROOF STEP]
qed