12.01/3.96	YES
12.01/3.96	
12.01/3.96	Proof:
12.01/3.96	This system is confluent.
12.01/3.96	By \cite{SMI95}, Corollary 4.7 or 5.3.
12.01/3.96	This system is oriented.
12.01/3.96	This system is of type 3 or smaller.
12.01/3.96	This system is right-stable.
12.01/3.96	This system is properly oriented.
12.01/3.96	This is an overlay system.
12.01/3.96	This system is left-linear.
12.01/3.96	All 4 critical pairs are trivial or infeasible.
12.01/3.96	Overlap: (rule1: div(y', z') -> pair(s(z), x') <= leq(z', y') = true, div(m(y', z'), z') = pair(z, x'), rule2: div($1, $2) -> pair(0, $2) <= greater($2, $1) = true, pos: ε, mgu: {(y',$1), (z',$2)})
12.01/3.96	CP: pair(0, $2) = pair(s(z), x') <= leq($2, $1) = true, div(m($1, $2), $2) = pair(z, x'), greater($2, $1) = true
12.01/3.96	This critical pair is infeasible.
12.01/3.96	This critical pair is conditional.
12.01/3.96	This critical pair has some non-trivial conditions.
12.01/3.96	Call external tool:
12.01/3.96	./waldmeister
12.01/3.96	Input:
12.01/3.96	  div(x, y) -> pair(0, y) <= greater(y, x) = true
12.01/3.96	  div(x, y) -> pair(s(q), r) <= leq(y, x) = true, div(m(x, y), y) = pair(q, r)
12.01/3.96	  m(x, 0) -> x
12.01/3.96	  m(0, y) -> 0
12.01/3.96	  m(s(x), s(y)) -> m(x, y)
12.01/3.96	  greater(s(x), s(y)) -> greater(x, y)
12.01/3.96	  greater(s(x), 0) -> true
12.01/3.96	  leq(s(x), s(y)) -> leq(x, y)
12.01/3.96	  leq(0, x) -> true
12.01/3.96	
12.01/3.96	By Waldmeister.
12.01/3.96	Overlap: (rule1: div(z, x') -> pair(0, x') <= greater(x', z) = true, rule2: div($1, $2) -> pair(s(y'), z') <= leq($2, $1) = true, div(m($1, $2), $2) = pair(y', z'), pos: ε, mgu: {(z,$1), (x',$2)})
12.01/3.96	CP: pair(s(y'), z') = pair(0, $2) <= greater($2, $1) = true, leq($2, $1) = true, div(m($1, $2), $2) = pair(y', z')
12.01/3.96	This critical pair is infeasible.
12.01/3.96	This critical pair is conditional.
12.01/3.96	This critical pair has some non-trivial conditions.
12.01/3.96	Call external tool:
12.01/3.96	./waldmeister
12.01/3.96	Input:
12.01/3.96	  div(x, y) -> pair(0, y) <= greater(y, x) = true
12.01/3.96	  div(x, y) -> pair(s(q), r) <= leq(y, x) = true, div(m(x, y), y) = pair(q, r)
12.01/3.96	  m(x, 0) -> x
12.01/3.96	  m(0, y) -> 0
12.01/3.96	  m(s(x), s(y)) -> m(x, y)
12.01/3.96	  greater(s(x), s(y)) -> greater(x, y)
12.01/3.96	  greater(s(x), 0) -> true
12.01/3.96	  leq(s(x), s(y)) -> leq(x, y)
12.01/3.96	  leq(0, x) -> true
12.01/3.96	
12.01/3.96	By Waldmeister.
12.01/3.96	Overlap: (rule1: m(0, x) -> 0, rule2: m(y, 0) -> y, pos: ε, mgu: {(y,0), (x,0)})
12.01/3.96	CP: 0 = 0
12.01/3.96	This critical pair is trivial.
12.01/3.96	Overlap: (rule1: m(y, 0) -> y, rule2: m(0, x) -> 0, pos: ε, mgu: {(y,0), (x,0)})
12.01/3.96	CP: 0 = 0
12.01/3.96	This critical pair is trivial.
12.01/3.96	
12.18/4.02	EOF