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