[STATEMENT]
lemma lit_ord_dominating_term:
  assumes "(s1,s2) \<in> trm_ord \<or> (s1,t2) \<in> trm_ord"
  assumes "orient_lit x1 s1 t1 p1"
  assumes "orient_lit x2 s2 t2 p2"
  assumes "vars_of_lit x1 = {}"
  assumes "vars_of_lit x2 = {}"
  shows "(x1,x2) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of_lit x1 = {}\<close> and \<open>orient_lit x1 s1 t1 p1\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x1 = {}
orient_lit x1 s1 t1 p1
[PROOF STEP]
have "vars_of t1 = {}" and "vars_of s1 = {}"
    and "\<not>(s1,t1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
orient_lit x1 s1 t1 p1

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s1 = {} &&& (s1, t1) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
(x1 = Pos (Eq s1 t1) \<or> x1 = Pos (Eq t1 s1)) \<and> (s1, t1) \<notin> trm_ord \<and> p1 = pos \<or> (x1 = Neg (Eq s1 t1) \<or> x1 = Neg (Eq t1 s1)) \<and> (s1, t1) \<notin> trm_ord \<and> p1 = neg

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s1 = {} &&& (s1, t1) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t1 = {}
vars_of s1 = {}
(s1, t1) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(5) and \<open>orient_lit x2 s2 t2 p2\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x2 = {}
orient_lit x2 s2 t2 p2
[PROOF STEP]
have "vars_of t2 = {}" and "vars_of s2 = {}"
    and "\<not>(s2,t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
orient_lit x2 s2 t2 p2

goal (1 subgoal):
 1. vars_of t2 = {} &&& vars_of s2 = {} &&& (s2, t2) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
(x2 = Pos (Eq s2 t2) \<or> x2 = Pos (Eq t2 s2)) \<and> (s2, t2) \<notin> trm_ord \<and> p2 = pos \<or> (x2 = Neg (Eq s2 t2) \<or> x2 = Neg (Eq t2 s2)) \<and> (s2, t2) \<notin> trm_ord \<and> p2 = neg

goal (1 subgoal):
 1. vars_of t2 = {} &&& vars_of s2 = {} &&& (s2, t2) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t2 = {}
vars_of s2 = {}
(s2, t2) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t1 = {}\<close> and \<open>vars_of s1 = {}\<close> and \<open>\<not>(s1,t1) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t1 = {}
vars_of s1 = {}
(s1, t1) \<notin> trm_ord
[PROOF STEP]
have o1: "t1 = s1 \<or> (t1,s1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s1 = {}
(s1, t1) \<notin> trm_ord

goal (1 subgoal):
 1. t1 = s1 \<or> (t1, s1) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s1 = {}
(s1, t1) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t1 = s1 \<or> (t1, s1) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s1 = {}
(s1, t1) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t2 = {}\<close> and \<open>vars_of s2 = {}\<close> and \<open>\<not>(s2,t2) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t2 = {}
vars_of s2 = {}
(s2, t2) \<notin> trm_ord
[PROOF STEP]
have o2: "t2 = s2 \<or> (t2,s2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s2 = {}
(s2, t2) \<notin> trm_ord

goal (1 subgoal):
 1. t2 = s2 \<or> (t2, s2) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s2 = {}
(s2, t2) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t2 = s2 \<or> (t2, s2) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s2 = {}
(s2, t2) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>\<not>(s2,t2) \<in> trm_ord\<close> and assms(1)
[PROOF STATE]
proof (chain)
picking this:
(s2, t2) \<notin> trm_ord
(s1, s2) \<in> trm_ord \<or> (s1, t2) \<in> trm_ord
[PROOF STEP]
have "(s1,s2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(s2, t2) \<notin> trm_ord
(s1, s2) \<in> trm_ord \<or> (s1, t2) \<in> trm_ord

goal (1 subgoal):
 1. (s1, s2) \<in> trm_ord
[PROOF STEP]
by (metis assms(1) o2 trm_ord_trans transE)
[PROOF STATE]
proof (state)
this:
(s1, s2) \<in> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m1 = "mset_lit x1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m2 = "mset_lit x2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(1) and o1 and o2
[PROOF STATE]
proof (chain)
picking this:
(s1, s2) \<in> trm_ord \<or> (s1, t2) \<in> trm_ord
t1 = s1 \<or> (t1, s1) \<in> trm_ord
t2 = s2 \<or> (t2, s2) \<in> trm_ord
[PROOF STEP]
have "(t1,s2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> trm_ord \<or> (s1, t2) \<in> trm_ord
t1 = s1 \<or> (t1, s1) \<in> trm_ord
t2 = s2 \<or> (t2, s2) \<in> trm_ord

goal (1 subgoal):
 1. (t1, s2) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
     trans_def
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> trm_ord \<or> (s1, t2) \<in> trm_ord
t1 = s1 \<or> (t1, s1) \<in> trm_ord
t2 = s2 \<or> (t2, s2) \<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. (t1, s2) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(t1, s2) \<in> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>(s1,s2) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(t1, s2) \<in> trm_ord
(s1, s2) \<in> trm_ord
[PROOF STEP]
have
    s2max: "\<forall>x. (x \<in># {# t1,t1,s1,s1 #} \<longrightarrow> (x,s2) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(t1, s2) \<in> trm_ord
(s1, s2) \<in> trm_ord

goal (1 subgoal):
 1. \<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
have "{# s2 #} \<subset># {# t2,t2,s2,s2 #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#s2#} \<subset># {#t2, t2, s2, s2#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#s2#} \<subset># {#t2, t2, s2, s2#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>{# s2 #} \<subset># {# t2,t2,s2,s2 #}\<close>
[PROOF STATE]
proof (chain)
picking this:
{#s2#} \<subset># {#t2, t2, s2, s2#}
[PROOF STEP]
have "( {# s2 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
{#s2#} \<subset># {#t2, t2, s2, s2#}

goal (1 subgoal):
 1. ({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
using trm_ord_trans multiset_order_inclusion [of "{# s2 #}" "{# t2,t2,s2,s2 #}" "trm_ord"]
[PROOF STATE]
proof (prove)
using this:
{#s2#} \<subset># {#t2, t2, s2, s2#}
trans trm_ord
\<lbrakk>{#s2#} \<subset># {#t2, t2, s2, s2#}; trans trm_ord\<rbrakk> \<Longrightarrow> ({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
have "p1 = neg \<or> p1 = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 = neg \<or> p1 = pos
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p1 = neg \<or> p1 = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p1 = neg \<or> p1 = pos

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p1 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p1 = neg"
[PROOF STATE]
proof (state)
this:
p1 = neg

goal (2 subgoals):
 1. p1 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x1 s1 t1 p1\<close>
[PROOF STATE]
proof (chain)
picking this:
p1 = neg
orient_lit x1 s1 t1 p1
[PROOF STEP]
have "x1 = (Neg (Eq t1 s1)) \<or> x1 = (Neg (Eq s1 t1))"
[PROOF STATE]
proof (prove)
using this:
p1 = neg
orient_lit x1 s1 t1 p1

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

goal (1 subgoal):
 1. x1 = Neg (Eq t1 s1) \<or> x1 = Neg (Eq s1 t1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x1 = Neg (Eq t1 s1) \<or> x1 = Neg (Eq s1 t1)

goal (2 subgoals):
 1. p1 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Neg (Eq t1 s1) \<or> x1 = Neg (Eq s1 t1)
[PROOF STEP]
have m1: "?m1 = {# t1,t1,s1,s1 #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Neg (Eq t1 s1) \<or> x1 = Neg (Eq s1 t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, t1, s1, s1#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Neg (Eq t1 s1) \<or> x1 = Neg (Eq s1 t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x1 = {#t1, t1, s1, s1#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x1 = {#t1, t1, s1, s1#}

goal (2 subgoals):
 1. p1 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have "p2 = neg \<or> p2 = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 = neg \<or> p2 = pos
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (2 subgoals):
 1. p1 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p2 = neg \<or> p2 = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p2 = neg \<or> p2 = pos

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p2 = neg"
[PROOF STATE]
proof (state)
this:
p2 = neg

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x2 s2 t2 p2\<close>
[PROOF STATE]
proof (chain)
picking this:
p2 = neg
orient_lit x2 s2 t2 p2
[PROOF STEP]
have "x2 = (Neg (Eq t2 s2)) \<or> x2 = (Neg (Eq s2 t2))"
[PROOF STATE]
proof (prove)
using this:
p2 = neg
orient_lit x2 s2 t2 p2

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

goal (1 subgoal):
 1. x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
[PROOF STEP]
have m2: "?m2 = {# t2,t2,s2,s2 #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x2 = {#t2, t2, s2, s2#}

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from s2max
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
[PROOF STEP]
have "({# t1,t1,s1,s1 #}, {# s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s2 #}" "{#}" s2 "{# t1,t1,s1,s1 #}" "{# t1,t1,s1,s1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
{#s2#} = {#} + {#s2#} \<and> {#t1, t1, s1, s1#} = {#} + {#t1, t1, s1, s1#} \<and> (\<forall>b. b \<in># {#t1, t1, s1, s1#} \<longrightarrow> (b, s2) \<in> trm_ord) \<Longrightarrow> ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>( {# s2 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord\<close> and \<open>({# t1,t1,s1,s1 #}, {# s2 #}) \<in> mult trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
have "( {# t1,t1,s1,s1 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult_trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
trans (mult trm_ord)

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
\<forall>x y z. (x, y) \<in> mult trm_ord \<longrightarrow> (y, z) \<in> mult trm_ord \<longrightarrow> (x, z) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p2 = pos"
[PROOF STATE]
proof (state)
this:
p2 = pos

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x2 s2 t2 p2\<close>
[PROOF STATE]
proof (chain)
picking this:
p2 = pos
orient_lit x2 s2 t2 p2
[PROOF STEP]
have "x2 = (Pos (Eq t2 s2)) \<or> x2 = (Pos (Eq s2 t2))"
[PROOF STATE]
proof (prove)
using this:
p2 = pos
orient_lit x2 s2 t2 p2

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

goal (1 subgoal):
 1. x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
[PROOF STEP]
have m2: "?m2 = {# t2,s2 #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, s2#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x2 = {#t2, s2#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x2 = {#t2, s2#}

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from s2max
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
[PROOF STEP]
have "({# t1,t1,s1,s1 #}, {# s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s2 #}" "{#}" s2 "{# t1,t1,s1,s1 #}" "{# t1,t1,s1,s1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
{#s2#} = {#} + {#s2#} \<and> {#t1, t1, s1, s1#} = {#} + {#t1, t1, s1, s1#} \<and> (\<forall>b. b \<in># {#t1, t1, s1, s1#} \<longrightarrow> (b, s2) \<in> trm_ord) \<Longrightarrow> ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>( {# s2 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,t1,s1,s1 #}, {# t2,s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,t1,s1,s1 #}" " {# s2 #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, t1, s1, s1#}, {#s2#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, t1, s1, s1#}, {#s2#} + {#t2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, s2#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, s2#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s1, s1#}
mset_lit x2 = {#t2, s2#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p1 = pos"
[PROOF STATE]
proof (state)
this:
p1 = pos

goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x1 s1 t1 p1\<close>
[PROOF STATE]
proof (chain)
picking this:
p1 = pos
orient_lit x1 s1 t1 p1
[PROOF STEP]
have "x1 = (Pos (Eq t1 s1)) \<or> x1 = (Pos (Eq s1 t1))"
[PROOF STATE]
proof (prove)
using this:
p1 = pos
orient_lit x1 s1 t1 p1

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

goal (1 subgoal):
 1. x1 = Pos (Eq t1 s1) \<or> x1 = Pos (Eq s1 t1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x1 = Pos (Eq t1 s1) \<or> x1 = Pos (Eq s1 t1)

goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Pos (Eq t1 s1) \<or> x1 = Pos (Eq s1 t1)
[PROOF STEP]
have m1: "?m1 = {# t1,s1 #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s1) \<or> x1 = Pos (Eq s1 t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, s1#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s1) \<or> x1 = Pos (Eq s1 t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x1 = {#t1, s1#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x1 = {#t1, s1#}

goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have "p2 = neg \<or> p2 = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 = neg \<or> p2 = pos
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. p1 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p2 = neg \<or> p2 = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p2 = neg \<or> p2 = pos

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p2 = neg"
[PROOF STATE]
proof (state)
this:
p2 = neg

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x2 s2 t2 p2\<close>
[PROOF STATE]
proof (chain)
picking this:
p2 = neg
orient_lit x2 s2 t2 p2
[PROOF STEP]
have "x2 = (Neg (Eq t2 s2)) \<or> x2 = (Neg (Eq s2 t2))"
[PROOF STATE]
proof (prove)
using this:
p2 = neg
orient_lit x2 s2 t2 p2

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

goal (1 subgoal):
 1. x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
[PROOF STEP]
have m2: "?m2 = {# t2,t2,s2,s2 #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s2) \<or> x2 = Neg (Eq s2 t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x2 = {#t2, t2, s2, s2#}

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from s2max
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
[PROOF STEP]
have "({# t1,s1 #}, {# s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s2 #}" "{#}" s2 "{# t1,s1 #}" "{# t1,s1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
{#s2#} = {#} + {#s2#} \<and> {#t1, s1#} = {#} + {#t1, s1#} \<and> (\<forall>b. b \<in># {#t1, s1#} \<longrightarrow> (b, s2) \<in> trm_ord) \<Longrightarrow> ({#t1, s1#}, {#s2#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

goal (1 subgoal):
 1. ({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#t1, s1#}, {#s2#}) \<in> mult trm_ord

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>( {# s2 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord\<close> and \<open>({# t1,s1 #}, {# s2 #}) \<in> mult trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
have "( {# t1,s1 #}, {# t2,t2,s2,s2 #} ) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, s1#}, {#s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult_trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, s1#}, {#s2#}) \<in> mult trm_ord
trans (mult trm_ord)

goal (1 subgoal):
 1. ({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
({#s2#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
({#t1, s1#}, {#s2#}) \<in> mult trm_ord
\<forall>x y z. (x, y) \<in> mult trm_ord \<longrightarrow> (y, z) \<in> mult trm_ord \<longrightarrow> (x, z) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord

goal (2 subgoals):
 1. p2 = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#t2, t2, s2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, t2, s2, s2#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p2 = pos"
[PROOF STATE]
proof (state)
this:
p2 = pos

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x2 s2 t2 p2\<close>
[PROOF STATE]
proof (chain)
picking this:
p2 = pos
orient_lit x2 s2 t2 p2
[PROOF STEP]
have "x2 = (Pos (Eq t2 s2)) \<or> x2 = (Pos (Eq s2 t2))"
[PROOF STATE]
proof (prove)
using this:
p2 = pos
orient_lit x2 s2 t2 p2

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

goal (1 subgoal):
 1. x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
[PROOF STEP]
have m2: "?m2 = {# t2,s2 #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, s2#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s2) \<or> x2 = Pos (Eq s2 t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

goal (1 subgoal):
 1. mset_lit x2 = {#t2, s2#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit x2 = {#t2, s2#}

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from s2max
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
[PROOF STEP]
have "({# t1,s1 #}, {# s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s2 #}" "{#}" s2 "{# t1,s1 #}" "{# t1,s1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1, t1, s1, s1#} \<longrightarrow> (x, s2) \<in> trm_ord
{#s2#} = {#} + {#s2#} \<and> {#t1, s1#} = {#} + {#t1, s1#} \<and> (\<forall>b. b \<in># {#t1, s1#} \<longrightarrow> (b, s2) \<in> trm_ord) \<Longrightarrow> ({#t1, s1#}, {#s2#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

goal (1 subgoal):
 1. ({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#t1, s1#}, {#s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
({#t1, s1#}, {#s2#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,s1 #}, {# t2,s2 #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,s1 #}" " {# s2 #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#s2#}) \<in> mult trm_ord
({#t1, s1#}, {#s2#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, s1#}, {#s2#} + {#t2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord

goal (1 subgoal):
 1. p2 = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, s2#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, s2#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, s1#}, {#t2, s2#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s1#}
mset_lit x2 = {#t2, s2#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lit_ord_neg_lit_lhs:
  assumes "orient_lit x1 s t1 pos"
  assumes "orient_lit x2 s t2 neg"
  assumes "vars_of_lit x1 = {}"
  assumes "vars_of_lit x2 = {}"
  shows "(x1,x2) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(3) and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x1 = {}
orient_lit x1 s t1 pos
[PROOF STEP]
have "vars_of t1 = {}" and "vars_of s = {}"
    and "\<not>(s,t1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
orient_lit x1 s t1 pos

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
(x1 = Pos (Eq s t1) \<or> x1 = Pos (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> pos = pos \<or> (x1 = Neg (Eq s t1) \<or> x1 = Neg (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(4) and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x2 = {}
orient_lit x2 s t2 neg
[PROOF STEP]
have "vars_of t2 = {}"
    and "\<not>(s,t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
orient_lit x2 s t2 neg

goal (1 subgoal):
 1. vars_of t2 = {} &&& (s, t2) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
(x2 = Pos (Eq s t2) \<or> x2 = Pos (Eq t2 s)) \<and> (s, t2) \<notin> trm_ord \<and> neg = pos \<or> (x2 = Neg (Eq s t2) \<or> x2 = Neg (Eq t2 s)) \<and> (s, t2) \<notin> trm_ord \<and> neg = neg

goal (1 subgoal):
 1. vars_of t2 = {} &&& (s, t2) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t2 = {}
(s, t2) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t1 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(s,t1) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
[PROOF STEP]
have o1: "t1 = s \<or> (t1,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t2 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(s,t2) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
[PROOF STEP]
have o2: "t2 = s \<or> (t2,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (t2, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (t2, s) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m1 = "mset_lit x1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m2 = "mset_lit x2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit x1 s t1 pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit x1 s t1 pos
[PROOF STEP]
have "x1 = (Pos (Eq t1 s)) \<or> x1 = (Pos (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
orient_lit x1 s t1 pos

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

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
[PROOF STEP]
have m1: "?m1 = {# t1,s #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit x2 s t2 neg\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit x2 s t2 neg
[PROOF STEP]
have "x2 = (Neg (Eq t2 s)) \<or> x2 = (Neg (Eq s t2))"
[PROOF STATE]
proof (prove)
using this:
orient_lit x2 s t2 neg

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

goal (1 subgoal):
 1. x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
have m2: "?m2 = {# t2,t2,s,s #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "t1 = s"
[PROOF STATE]
proof (state)
this:
t1 = s

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have "({# s,s #}, {# t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# t2,s,s #}" "{# s,s #}" t2 "{# s,s #}" "{#}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
{#t2, s, s#} = {#s, s#} + {#t2#} \<and> {#s, s#} = {#s, s#} + {#} \<and> (\<forall>b. b \<in># {#} \<longrightarrow> (b, t2) \<in> trm_ord) \<Longrightarrow> ({#s, s#}, {#t2, s, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# s,s #}, {# t2,t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# s,s #}" " {# t2,s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#s, s#}, {#t2, s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>t1 = s\<close> and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "t1 \<noteq> s"
[PROOF STATE]
proof (state)
this:
t1 \<noteq> s

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and o1
[PROOF STATE]
proof (chain)
picking this:
t1 \<noteq> s
t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
have "(t1,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t1 \<noteq> s
t1 = s \<or> (t1, s) \<in> trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(t1, s) \<in> trm_ord
[PROOF STEP]
have smax: "\<forall>x. (x \<in># {# t1 #} \<longrightarrow> (x,s) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(t1, s) \<in> trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from smax
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord
[PROOF STEP]
have "({# t1,s #}, {# s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s,s #}" "{# s #}" s "{# t1,s #}" "{# t1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord
{#s, s#} = {#s#} + {#s#} \<and> {#t1, s#} = {#s#} + {#t1#} \<and> (\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, s) \<in> trm_ord) \<Longrightarrow> ({#t1, s#}, {#s, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,s #}, {# t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,s #}" " {# s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord
({#t1, s#}, {#s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, s#}, {#s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,s #}, {# t2,t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,s #}" " {# t2,s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, s#}, {#t2, s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lit_ord_neg_lit_rhs:
  assumes "orient_lit x1 s t1 pos"
  assumes "orient_lit x2 t2 s neg"
  assumes "vars_of_lit x1 = {}"
  assumes "vars_of_lit x2 = {}"
  shows "(x1,x2) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(3) and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x1 = {}
orient_lit x1 s t1 pos
[PROOF STEP]
have "vars_of t1 = {}" and "vars_of s = {}"
    and "\<not>(s,t1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
orient_lit x1 s t1 pos

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x1 = {}
(x1 = Pos (Eq s t1) \<or> x1 = Pos (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> pos = pos \<or> (x1 = Neg (Eq s t1) \<or> x1 = Neg (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(4) and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x2 = {}
orient_lit x2 t2 s neg
[PROOF STEP]
have "vars_of t2 = {}"
    and "\<not>(t2,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
orient_lit x2 t2 s neg

goal (1 subgoal):
 1. vars_of t2 = {} &&& (t2, s) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x2 = {}
(x2 = Pos (Eq t2 s) \<or> x2 = Pos (Eq s t2)) \<and> (t2, s) \<notin> trm_ord \<and> neg = pos \<or> (x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)) \<and> (t2, s) \<notin> trm_ord \<and> neg = neg

goal (1 subgoal):
 1. vars_of t2 = {} &&& (t2, s) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t2 = {}
(t2, s) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t1 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(s,t1) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
[PROOF STEP]
have o1: "t1 = s \<or> (t1,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t2 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(t2,s) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t2 = {}
vars_of s = {}
(t2, s) \<notin> trm_ord
[PROOF STEP]
have o2: "t2 = s \<or> (s,t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(t2, s) \<notin> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (s, t2) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(t2, s) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (s, t2) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(t2, s) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m1 = "mset_lit x1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m2 = "mset_lit x2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit x1 s t1 pos\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit x1 s t1 pos
[PROOF STEP]
have "x1 = (Pos (Eq t1 s)) \<or> x1 = (Pos (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
orient_lit x1 s t1 pos

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

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
[PROOF STEP]
have m1: "?m1 = {# t1,s #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit x2 t2 s neg\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit x2 t2 s neg
[PROOF STEP]
have "x2 = (Neg (Eq t2 s)) \<or> x2 = (Neg (Eq s t2))"
[PROOF STATE]
proof (prove)
using this:
orient_lit x2 t2 s neg

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

goal (1 subgoal):
 1. x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
have m2: "?m2 = {# t2,t2,s,s #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "t1 = s"
[PROOF STATE]
proof (state)
this:
t1 = s

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have "({# s,s #}, {# t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# t2,s,s #}" "{# s,s #}" t2 "{# s,s #}" "{#}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
{#t2, s, s#} = {#s, s#} + {#t2#} \<and> {#s, s#} = {#s, s#} + {#} \<and> (\<forall>b. b \<in># {#} \<longrightarrow> (b, t2) \<in> trm_ord) \<Longrightarrow> ({#s, s#}, {#t2, s, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# s,s #}, {# t2,t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# s,s #}" " {# t2,s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord
({#s, s#}, {#t2, s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#s, s#}, {#t2, s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>t1 = s\<close> and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
t1 = s
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "t1 \<noteq> s"
[PROOF STATE]
proof (state)
this:
t1 \<noteq> s

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and o1
[PROOF STATE]
proof (chain)
picking this:
t1 \<noteq> s
t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
have "(t1,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t1 \<noteq> s
t1 = s \<or> (t1, s) \<in> trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(t1, s) \<in> trm_ord
[PROOF STEP]
have smax: "\<forall>x. (x \<in># {# t1 #} \<longrightarrow> (x,s) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(t1, s) \<in> trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from smax
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord
[PROOF STEP]
have "({# t1,s #}, {# s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# s,s #}" "{# s #}" s "{# t1,s #}" "{# t1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in># {#t1#} \<longrightarrow> (x, s) \<in> trm_ord
{#s, s#} = {#s#} + {#s#} \<and> {#t1, s#} = {#s#} + {#t1#} \<and> (\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, s) \<in> trm_ord) \<Longrightarrow> ({#t1, s#}, {#s, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,s #}, {# t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,s #}" " {# s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#s, s#}) \<in> mult trm_ord
({#t1, s#}, {#s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, s#}, {#s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,s #}, {# t2,t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,s #}" " {# t2,s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord
({#t1, s#}, {#t2, s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, s#}, {#t2, s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. t1 \<noteq> s \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, t2, s, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lit_ord_rhs:
  assumes "(t1,t2) \<in> trm_ord"
  assumes "orient_lit x1 s t1 p"
  assumes "orient_lit x2 s t2 p"
  assumes "vars_of_lit x1 = {}"
  assumes "vars_of_lit x2 = {}"
  shows "(x1,x2) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(2) and assms(4)
[PROOF STATE]
proof (chain)
picking this:
orient_lit x1 s t1 p
vars_of_lit x1 = {}
[PROOF STEP]
have "vars_of t1 = {}" and "vars_of s = {}"
    and "\<not>(s,t1) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit x1 s t1 p
vars_of_lit x1 = {}

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
(x1 = Pos (Eq s t1) \<or> x1 = Pos (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> p = pos \<or> (x1 = Neg (Eq s t1) \<or> x1 = Neg (Eq t1 s)) \<and> (s, t1) \<notin> trm_ord \<and> p = neg
vars_of_lit x1 = {}

goal (1 subgoal):
 1. vars_of t1 = {} &&& vars_of s = {} &&& (s, t1) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(3) and assms(5)
[PROOF STATE]
proof (chain)
picking this:
orient_lit x2 s t2 p
vars_of_lit x2 = {}
[PROOF STEP]
have "vars_of t2 = {}"
    and "\<not>(s,t2) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit x2 s t2 p
vars_of_lit x2 = {}

goal (1 subgoal):
 1. vars_of t2 = {} &&& (s, t2) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_def
[PROOF STATE]
proof (prove)
using this:
(x2 = Pos (Eq s t2) \<or> x2 = Pos (Eq t2 s)) \<and> (s, t2) \<notin> trm_ord \<and> p = pos \<or> (x2 = Neg (Eq s t2) \<or> x2 = Neg (Eq t2 s)) \<and> (s, t2) \<notin> trm_ord \<and> p = neg
vars_of_lit x2 = {}

goal (1 subgoal):
 1. vars_of t2 = {} &&& (s, t2) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t2 = {}
(s, t2) \<notin> trm_ord

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t1 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(s,t1) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
[PROOF STEP]
have o1: "t1 = s \<or> (t1,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t1 = s \<or> (t1, s) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t1 = {}
vars_of s = {}
(s, t1) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of t2 = {}\<close> and \<open>vars_of s = {}\<close> and \<open>\<not>(s,t2) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
[PROOF STEP]
have o2: "t2 = s \<or> (t2,s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (t2, s) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t2 = s \<or> (t2, s) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of t2 = {}
vars_of s = {}
(s, t2) \<notin> trm_ord
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m1 = "mset_lit x1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
let ?m2 = "mset_lit x2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
have "p = pos \<or> p = neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = pos \<or> p = neg
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = pos \<or> p = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = pos \<or> p = neg

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p = pos"
[PROOF STATE]
proof (state)
this:
p = pos

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x1 s t1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = pos
orient_lit x1 s t1 p
[PROOF STEP]
have "x1 = (Pos (Eq t1 s)) \<or> x1 = (Pos (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
p = pos
orient_lit x1 s t1 p

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

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

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
[PROOF STEP]
have m1: "?m1 = {# t1,s #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Pos (Eq t1 s) \<or> x1 = Pos (Eq s t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>p = pos\<close> and \<open>orient_lit x2 s t2 p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = pos
orient_lit x2 s t2 p
[PROOF STEP]
have "x2 = (Pos (Eq t2 s)) \<or> x2 = (Pos (Eq s t2))"
[PROOF STATE]
proof (prove)
using this:
p = pos
orient_lit x2 s t2 p

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

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

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Pos (Eq t2 s) \<or> x2 = Pos (Eq s t2)
[PROOF STEP]
have m2: "?m2 = {# t2,s #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s) \<or> x2 = Pos (Eq s t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Pos (Eq t2 s) \<or> x2 = Pos (Eq s t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(t1, t2) \<in> trm_ord
[PROOF STEP]
have "(\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(t1, t2) \<in> trm_ord

goal (1 subgoal):
 1. \<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord
[PROOF STEP]
have "({# t1,s #}, {# t2,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, s#}, {#t2, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# t2,s #}" "{# s #}" t2 "{# t1,s #}" "{# t1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord
{#t2, s#} = {#s#} + {#t2#} \<and> {#t1, s#} = {#s#} + {#t1#} \<and> (\<forall>b. b \<in># {#t1#} \<longrightarrow> (b, t2) \<in> trm_ord) \<Longrightarrow> ({#t1, s#}, {#t2, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (2 subgoals):
 1. p = pos \<Longrightarrow> (x1, x2) \<in> lit_ord
 2. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, s#}, {#t2, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, s#}, {#t2, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, s#}
mset_lit x2 = {#t2, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
assume "p = neg"
[PROOF STATE]
proof (state)
this:
p = neg

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit x1 s t1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg
orient_lit x1 s t1 p
[PROOF STEP]
have "x1 = (Neg (Eq t1 s)) \<or> x1 = (Neg (Eq s t1))"
[PROOF STATE]
proof (prove)
using this:
p = neg
orient_lit x1 s t1 p

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

goal (1 subgoal):
 1. x1 = Neg (Eq t1 s) \<or> x1 = Neg (Eq s t1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x1 = Neg (Eq t1 s) \<or> x1 = Neg (Eq s t1)

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x1 = Neg (Eq t1 s) \<or> x1 = Neg (Eq s t1)
[PROOF STEP]
have m1: "?m1 = {# t1,t1,s,s #}"
[PROOF STATE]
proof (prove)
using this:
x1 = Neg (Eq t1 s) \<or> x1 = Neg (Eq s t1)

goal (1 subgoal):
 1. mset_lit x1 = {#t1, t1, s, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x1 = Neg (Eq t1 s) \<or> x1 = Neg (Eq s t1)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from \<open>p = neg\<close> and \<open>orient_lit x2 s t2 p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg
orient_lit x2 s t2 p
[PROOF STEP]
have "x2 = (Neg (Eq t2 s)) \<or> x2 = (Neg (Eq s t2))"
[PROOF STATE]
proof (prove)
using this:
p = neg
orient_lit x2 s t2 p

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

goal (1 subgoal):
 1. x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
[PROOF STEP]
have m2: "?m2 = {# t2,t2,s,s #}"
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)

goal (1 subgoal):
 1. mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
using mset_lit.simps
[PROOF STATE]
proof (prove)
using this:
x2 = Neg (Eq t2 s) \<or> x2 = Neg (Eq s t2)
mset_lit (Pos (Eq ?t ?s)) = {#?t, ?s#}
mset_lit (Neg (Eq ?t ?s)) = {#?t, ?t, ?s, ?s#}

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

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(t1, t2) \<in> trm_ord
[PROOF STEP]
have max: "(\<forall>b. b \<in># {#t1,t1#} \<longrightarrow> (b, t2) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(t1, t2) \<in> trm_ord

goal (1 subgoal):
 1. \<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have i: "{# t2,s,s #} = {# s,s,t2 #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#t2, s, s#} = {#s, s, t2#}
[PROOF STEP]
by (simp add: add.commute add.left_commute)
[PROOF STATE]
proof (state)
this:
{#t2, s, s#} = {#s, s, t2#}

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
have ii: "{# t1,t1,s,s #} = {# s,s,t1,t1 #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#t1, t1, s, s#} = {#s, s, t1, t1#}
[PROOF STEP]
by (simp add: add.commute add.left_commute)
[PROOF STATE]
proof (state)
this:
{#t1, t1, s, s#} = {#s, s, t1, t1#}

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from i and ii and max
[PROOF STATE]
proof (chain)
picking this:
{#t2, s, s#} = {#s, s, t2#}
{#t1, t1, s, s#} = {#s, s, t1, t1#}
\<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord
[PROOF STEP]
have "({# t1,t1,s,s #}, {# t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
{#t2, s, s#} = {#s, s, t2#}
{#t1, t1, s, s#} = {#s, s, t1, t1#}
\<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mult1_def_lemma [of "{# t2,s,s #}" "{# s,s #}" t2 "{# t1,t1,s,s #}" "{# t1,t1 #}" trm_ord]
        mult_def
[PROOF STATE]
proof (prove)
using this:
{#t2, s, s#} = {#s, s, t2#}
{#t1, t1, s, s#} = {#s, s, t1, t1#}
\<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord
{#t2, s, s#} = {#s, s#} + {#t2#} \<and> {#t1, t1, s, s#} = {#s, s#} + {#t1, t1#} \<and> (\<forall>b. b \<in># {#t1, t1#} \<longrightarrow> (b, t2) \<in> trm_ord) \<Longrightarrow> ({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult1 trm_ord
mult ?r = (mult1 ?r)\<^sup>+

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

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
have "({# t1,t1,s,s #}, {# t2,t2,s,s #}) \<in> mult trm_ord"
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#t1, t1, s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
[PROOF STEP]
using mset_ordering_add1 [of "{# t1,t1,s,s #}" " {# t2,s,s #}" trm_ord t2]
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult trm_ord
({#t1, t1, s, s#}, {#t2, s, s#}) \<in> mult trm_ord \<Longrightarrow> ({#t1, t1, s, s#}, {#t2, s, s#} + {#t2#}) \<in> mult trm_ord

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

goal (1 subgoal):
 1. p = neg \<Longrightarrow> (x1, x2) \<in> lit_ord
[PROOF STEP]
from this and m1 and m2
[PROOF STATE]
proof (chain)
picking this:
({#t1, t1, s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s, s#}
mset_lit x2 = {#t2, t2, s, s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s, s#}
mset_lit x2 = {#t2, t2, s, s#}

goal (1 subgoal):
 1. (x1, x2) \<in> lit_ord
[PROOF STEP]
using lit_ord_def
[PROOF STATE]
proof (prove)
using this:
({#t1, t1, s, s#}, {#t2, t2, s, s#}) \<in> mult trm_ord
mset_lit x1 = {#t1, t1, s, s#}
mset_lit x2 = {#t2, t2, s, s#}
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_preserves_eq_semantics:
  assumes "fo_interpretation I"
  assumes "(I (subst t1 \<sigma>) (subst t2 \<sigma>))"
  assumes "(validate_ground_eq I (subst_equation (Eq t1 s) \<sigma>))"
  shows "(validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
[PROOF STEP]
have "transitive I" and "symmetric I"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I

goal (1 subgoal):
 1. transitive I &&& symmetric I
[PROOF STEP]
unfolding
    fo_interpretation_def congruence_def equivalence_relation_def
[PROOF STATE]
proof (prove)
using this:
(reflexive I \<and> symmetric I \<and> transitive I) \<and> compatible_with_structure I

goal (1 subgoal):
 1. transitive I &&& symmetric I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
transitive I
symmetric I

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
have "(subst_equation (Eq t1 s) \<sigma>) = (Eq (subst t1 \<sigma>) (subst s \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_equation (Eq t1 s) \<sigma> = Eq (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subst_equation (Eq t1 s) \<sigma> = Eq (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
subst_equation (Eq t1 s) \<sigma> = Eq (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
validate_ground_eq I (subst_equation (Eq t1 s) \<sigma>)
[PROOF STEP]
have "I (subst t1 \<sigma>)  (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
subst_equation (Eq t1 s) \<sigma> = Eq (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
validate_ground_eq I (subst_equation (Eq t1 s) \<sigma>)

goal (1 subgoal):
 1. I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
from this and assms(2) and \<open>transitive I\<close> and \<open>symmetric I\<close>
[PROOF STATE]
proof (chain)
picking this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I
[PROOF STEP]
have "I (subst t2 \<sigma>) (subst s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
transitive I
symmetric I

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
unfolding transitive_def symmetric_def
[PROOF STATE]
proof (prove)
using this:
I (t1 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t1 \<lhd> \<sigma>) (t2 \<lhd> \<sigma>)
\<forall>y z u. I y z \<longrightarrow> I z u \<longrightarrow> I y u
\<forall>y z. I y z = I z y

goal (1 subgoal):
 1. I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
have "(subst_equation (Eq t2 s) \<sigma>) = (Eq (subst t2 \<sigma>) (subst s \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_equation (Eq t2 s) \<sigma> = Eq (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subst_equation (Eq t2 s) \<sigma> = Eq (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
from this and \<open>I (subst t2 \<sigma>) (subst s \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_equation (Eq t2 s) \<sigma> = Eq (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subst_equation (Eq t2 s) \<sigma> = Eq (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)
I (t2 \<lhd> \<sigma>) (s \<lhd> \<sigma>)

goal (1 subgoal):
 1. validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
validate_ground_eq I (subst_equation (Eq t2 s) \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed