5.31/2.35	MAYBE
5.31/2.35	
5.31/2.35	Proof:
5.31/2.35	ConCon could not decide confluence of the system.
5.31/2.35	\cite{ALS94}, Theorem 4.1 does not apply.
5.31/2.35	This system is of type 3 or smaller.
5.31/2.35	This system is strongly deterministic.
5.31/2.35	This system is of type 3 or smaller.
5.31/2.35	This system is deterministic.
5.31/2.35	This system is non-terminating.
5.31/2.35	Call external tool:
5.31/2.35	./ttt2.sh
5.31/2.35	Input:
5.31/2.35	(VAR x y q r)
5.31/2.35	(RULES
5.31/2.35	  m(x, 0) -> x
5.31/2.35	  leq(0, x) -> true
5.31/2.35	  m(s(x), s(y)) -> m(x, y)
5.31/2.35	  greater(s(x), s(y)) -> greater(x, y)
5.31/2.35	  div(x, y) -> ?2(leq(y, x), x, y)
5.31/2.35	  ?2(true, x, y) -> ?3(div(m(x, y), y), x, y)
5.31/2.35	  ?3(pair(q, r), x, y) -> pair(s(q), r)
5.31/2.35	  div(x, y) -> ?1(greater(y, x), x, y)
5.31/2.35	  ?1(true, x, y) -> pair(0, y)
5.31/2.35	  m(0, y) -> 0
5.31/2.35	  leq(s(x), s(y)) -> leq(x, y)
5.31/2.35	  greater(s(x), 0) -> true
5.31/2.35	)
5.31/2.35	
5.31/2.35	 Unfolding Processor:
5.31/2.35	  loop length: 3
5.31/2.35	  terms:
5.31/2.35	   div(x1158,0())
5.31/2.35	   ?2(leq(0(),x1158),x1158,0())
5.31/2.35	   ?2(true(),x1158,0())
5.31/2.35	  context: ?3([],x1158,0())
5.31/2.35	  substitution:
5.31/2.35	   x1158 -> m(x1158,0())
5.31/2.35	  Qed
5.31/2.35	ConCon could not decide if this system is quasi-decreasing.
5.31/2.35	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
5.31/2.35	This system is of type 3 or smaller.
5.31/2.35	This system is deterministic.
5.31/2.35	This system is non-terminating.
5.31/2.35	Call external tool:
5.31/2.35	./ttt2.sh
5.31/2.35	Input:
5.31/2.35	(VAR x y q r)
5.31/2.35	(RULES
5.31/2.35	  m(x, 0) -> x
5.31/2.35	  leq(0, x) -> true
5.31/2.35	  m(s(x), s(y)) -> m(x, y)
5.31/2.35	  greater(s(x), s(y)) -> greater(x, y)
5.31/2.35	  div(x, y) -> ?2(leq(y, x), x, y)
5.31/2.35	  ?2(true, x, y) -> ?3(div(m(x, y), y), x, y)
5.31/2.35	  ?3(pair(q, r), x, y) -> pair(s(q), r)
5.31/2.35	  div(x, y) -> ?1(greater(y, x), x, y)
5.31/2.35	  ?1(true, x, y) -> pair(0, y)
5.31/2.35	  m(0, y) -> 0
5.31/2.35	  leq(s(x), s(y)) -> leq(x, y)
5.31/2.35	  greater(s(x), 0) -> true
5.31/2.35	)
5.31/2.35	
5.31/2.35	 Unfolding Processor:
5.31/2.35	  loop length: 3
5.31/2.35	  terms:
5.31/2.35	   div(x1158,0())
5.31/2.35	   ?2(leq(0(),x1158),x1158,0())
5.31/2.35	   ?2(true(),x1158,0())
5.31/2.35	  context: ?3([],x1158,0())
5.31/2.35	  substitution:
5.31/2.35	   x1158 -> m(x1158,0())
5.31/2.35	  Qed
5.31/2.35	
5.31/2.37	EOF