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