118.53/31.22	MAYBE
118.53/31.22	
118.53/31.22	Proof:
118.53/31.22	ConCon could not decide confluence of the system.
118.53/31.22	\cite{ALS94}, Theorem 4.1 does not apply.
118.53/31.22	This system is of type 3 or smaller.
118.53/31.22	This system is strongly deterministic.
118.53/31.22	This system is of type 3 or smaller.
118.53/31.22	This system is deterministic.
118.53/31.22	ConCon could not decide if this system is quasi-decreasing.
118.53/31.22	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
118.53/31.22	This system is of type 3 or smaller.
118.53/31.22	This system is deterministic.
118.53/31.22	System R transformed to U(R).
118.53/31.22	The external tool could not decide termination of the system.
118.53/31.22	Call external tool:
118.53/31.22	./ttt2.sh
118.53/31.22	Input:
118.53/31.22	(VAR x z q y n)
118.53/31.22	(RULES
118.53/31.22	  add(0, x) -> x
118.53/31.22	  add(s(x), y) -> s(add(x, y))
118.53/31.22	  mult(0, y) -> 0
118.53/31.22	  mult(s(x), y) -> add(mult(x, y), y)
118.53/31.22	  lte(0, y) -> true
118.53/31.22	  lte(s(x), 0) -> false
118.53/31.22	  lte(s(x), s(y)) -> lte(x, y)
118.53/31.22	  minus(0, s(y)) -> 0
118.53/31.22	  minus(x, 0) -> x
118.53/31.22	  minus(s(x), s(y)) -> minus(x, y)
118.53/31.22	  mod(0, y) -> 0
118.53/31.22	  mod(x, 0) -> x
118.53/31.22	  ?1(true, x, y) -> mod(minus(x, s(y)), s(y))
118.53/31.22	  mod(x, s(y)) -> ?1(lte(s(y), x), x, y)
118.53/31.22	  ?2(false, x, y) -> x
118.53/31.22	  mod(x, s(y)) -> ?2(lte(s(y), x), x, y)
118.53/31.22	  div(0, s(x)) -> 0
118.53/31.22	  ?3(true, x, y) -> 0
118.53/31.22	  div(s(x), s(y)) -> ?3(lte(s(x), y), x, y)
118.53/31.22	  ?5(q, x, y) -> s(q)
118.53/31.22	  ?4(false, x, y) -> ?5(div(minus(x, y), s(y)), x, y)
118.53/31.22	  div(s(x), s(y)) -> ?4(lte(s(x), y), x, y)
118.53/31.22	  power(x, 0) -> s(0)
118.53/31.22	  ?7(y, x, n) -> mult(mult(y, y), s(0))
118.53/31.22	  ?6(0, x, n) -> ?7(power(x, div(n, s(s(0)))), x, n)
118.53/31.22	  power(x, n) -> ?6(mod(n, s(s(0))), x, n)
118.53/31.22	  ?9(y, x, n, z) -> mult(mult(y, y), x)
118.53/31.22	  ?8(s(z), x, n) -> ?9(power(x, div(n, s(s(0)))), x, n, z)
118.53/31.22	  power(x, n) -> ?8(mod(n, s(s(0))), x, n)
118.53/31.22	)
118.53/31.22	
118.53/31.22	
118.57/31.24	EOF