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