7.82/3.02	MAYBE
7.82/3.02	
7.82/3.02	Proof:
7.82/3.02	ConCon could not decide confluence of the system.
7.82/3.02	\cite{ALS94}, Theorem 4.1 does not apply.
7.82/3.02	This system is of type 3 or smaller.
7.82/3.02	This system is strongly deterministic.
7.82/3.02	This system is of type 3 or smaller.
7.82/3.02	This system is deterministic.
7.82/3.02	This system is non-terminating.
7.82/3.02	Call external tool:
7.82/3.02	./ttt2.sh
7.82/3.02	Input:
7.82/3.03	(VAR x y z)
7.82/3.03	(RULES
7.82/3.03	  iadd(add(x, y)) -> tp2(x, y)
7.82/3.03	  iadd(s(z)) -> u1(iadd(z))
7.82/3.03	  gcd(y, z) -> ?2(iadd(z), y, z)
7.82/3.03	  ?2(tp2(x, y), y, z) -> gcd(x, y)
7.82/3.03	  gcd(0, x) -> x
7.82/3.03	  gcd(z, y) -> ?1(iadd(z), z, y)
7.82/3.03	  ?1(tp2(x, y), z, y) -> gcd(x, y)
7.82/3.03	  iadd(y) -> tp2(0, y)
7.82/3.03	  gcd(x, 0) -> x
7.82/3.03	  u1(tp2(x, y)) -> tp2(s(x), y)
7.82/3.03	)
7.82/3.03	
7.82/3.03	 Matrix Interpretation Processor: dim=1
7.82/3.03	  
7.82/3.03	  interpretation:
7.82/3.03	   [?1](x0, x1, x2) = 3x0 + 2x1 + 4x2 + 3,
7.82/3.03	   
7.82/3.03	   [0] = 0,
7.82/3.03	   
7.82/3.03	   [?2](x0, x1, x2) = x0 + 6x1 + 5x2 + 3,
7.82/3.03	   
7.82/3.03	   [gcd](x0, x1) = 6x0 + 7x1 + 3,
7.82/3.03	   
7.82/3.03	   [u1](x0) = x0,
7.82/3.03	   
7.82/3.03	   [s](x0) = x0,
7.82/3.03	   
7.82/3.03	   [tp2](x0, x1) = 7x0 + x1,
7.82/3.03	   
7.82/3.03	   [iadd](x0) = x0,
7.82/3.03	   
7.82/3.03	   [add](x0, x1) = 7x0 + 4x1 + 2
7.82/3.03	  orientation:
7.82/3.03	   iadd(add(x,y)) = 7x + 4y + 2 >= 7x + y = tp2(x,y)
7.82/3.03	   
7.82/3.03	   iadd(s(z)) = z >= z = u1(iadd(z))
7.82/3.03	   
7.82/3.03	   gcd(y,z) = 6y + 7z + 3 >= 6y + 6z + 3 = ?2(iadd(z),y,z)
7.82/3.03	   
7.82/3.03	   ?2(tp2(x,y),y,z) = 7x + 7y + 5z + 3 >= 6x + 7y + 3 = gcd(x,y)
7.82/3.03	   
7.82/3.03	   gcd(0(),x) = 7x + 3 >= x = x
7.82/3.03	   
7.82/3.03	   gcd(z,y) = 7y + 6z + 3 >= 4y + 5z + 3 = ?1(iadd(z),z,y)
7.82/3.03	   
7.82/3.03	   ?1(tp2(x,y),z,y) = 21x + 7y + 2z + 3 >= 6x + 7y + 3 = gcd(x,y)
7.82/3.03	   
7.82/3.03	   iadd(y) = y >= y = tp2(0(),y)
7.82/3.03	   
7.82/3.03	   gcd(x,0()) = 6x + 3 >= x = x
7.82/3.03	   
7.82/3.03	   u1(tp2(x,y)) = 7x + y >= 7x + y = tp2(s(x),y)
7.82/3.03	  problem:
7.82/3.03	   iadd(s(z)) -> u1(iadd(z))
7.82/3.03	   gcd(y,z) -> ?2(iadd(z),y,z)
7.82/3.03	   ?2(tp2(x,y),y,z) -> gcd(x,y)
7.82/3.03	   gcd(z,y) -> ?1(iadd(z),z,y)
7.82/3.03	   ?1(tp2(x,y),z,y) -> gcd(x,y)
7.82/3.03	   iadd(y) -> tp2(0(),y)
7.82/3.03	   u1(tp2(x,y)) -> tp2(s(x),y)
7.82/3.03	  Unfolding Processor:
7.82/3.03	   loop length: 3
7.82/3.03	   terms:
7.82/3.03	    ?2(iadd(0()),0(),0())
7.82/3.03	    ?2(tp2(0(),0()),0(),0())
7.82/3.03	    gcd(0(),0())
7.82/3.03	   context: []
7.82/3.03	   substitution:
7.82/3.03	    
7.82/3.03	   Qed
7.82/3.03	ConCon could not decide if this system is quasi-decreasing.
7.82/3.03	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
7.82/3.03	This system is of type 3 or smaller.
7.82/3.03	This system is deterministic.
7.82/3.03	This system is non-terminating.
7.82/3.03	Call external tool:
7.82/3.03	./ttt2.sh
7.82/3.03	Input:
7.82/3.03	(VAR x y z)
7.82/3.03	(RULES
7.82/3.03	  iadd(add(x, y)) -> tp2(x, y)
7.82/3.03	  iadd(s(z)) -> u1(iadd(z))
7.82/3.03	  gcd(y, z) -> ?2(iadd(z), y, z)
7.82/3.03	  ?2(tp2(x, y), y, z) -> gcd(x, y)
7.82/3.03	  gcd(0, x) -> x
7.82/3.03	  gcd(z, y) -> ?1(iadd(z), z, y)
7.82/3.03	  ?1(tp2(x, y), z, y) -> gcd(x, y)
7.82/3.03	  iadd(y) -> tp2(0, y)
7.82/3.03	  gcd(x, 0) -> x
7.82/3.03	  u1(tp2(x, y)) -> tp2(s(x), y)
7.82/3.03	)
7.82/3.03	
7.82/3.03	 Matrix Interpretation Processor: dim=1
7.82/3.03	  
7.82/3.03	  interpretation:
7.82/3.03	   [?1](x0, x1, x2) = 3x0 + 2x1 + 4x2 + 3,
7.82/3.03	   
7.82/3.03	   [0] = 0,
7.82/3.03	   
7.82/3.03	   [?2](x0, x1, x2) = x0 + 6x1 + 5x2 + 3,
7.82/3.03	   
7.82/3.03	   [gcd](x0, x1) = 6x0 + 7x1 + 3,
7.82/3.03	   
7.82/3.03	   [u1](x0) = x0,
7.82/3.03	   
7.82/3.03	   [s](x0) = x0,
7.82/3.03	   
7.82/3.03	   [tp2](x0, x1) = 7x0 + x1,
7.82/3.03	   
7.82/3.03	   [iadd](x0) = x0,
7.82/3.03	   
7.82/3.03	   [add](x0, x1) = 7x0 + 4x1 + 2
7.82/3.03	  orientation:
7.82/3.03	   iadd(add(x,y)) = 7x + 4y + 2 >= 7x + y = tp2(x,y)
7.82/3.03	   
7.82/3.03	   iadd(s(z)) = z >= z = u1(iadd(z))
7.82/3.03	   
7.82/3.03	   gcd(y,z) = 6y + 7z + 3 >= 6y + 6z + 3 = ?2(iadd(z),y,z)
7.82/3.03	   
7.82/3.03	   ?2(tp2(x,y),y,z) = 7x + 7y + 5z + 3 >= 6x + 7y + 3 = gcd(x,y)
7.82/3.03	   
7.82/3.03	   gcd(0(),x) = 7x + 3 >= x = x
7.82/3.03	   
7.82/3.03	   gcd(z,y) = 7y + 6z + 3 >= 4y + 5z + 3 = ?1(iadd(z),z,y)
7.82/3.03	   
7.82/3.03	   ?1(tp2(x,y),z,y) = 21x + 7y + 2z + 3 >= 6x + 7y + 3 = gcd(x,y)
7.82/3.03	   
7.82/3.03	   iadd(y) = y >= y = tp2(0(),y)
7.82/3.03	   
7.82/3.03	   gcd(x,0()) = 6x + 3 >= x = x
7.82/3.03	   
7.82/3.03	   u1(tp2(x,y)) = 7x + y >= 7x + y = tp2(s(x),y)
7.82/3.03	  problem:
7.82/3.03	   iadd(s(z)) -> u1(iadd(z))
7.82/3.03	   gcd(y,z) -> ?2(iadd(z),y,z)
7.82/3.03	   ?2(tp2(x,y),y,z) -> gcd(x,y)
7.82/3.03	   gcd(z,y) -> ?1(iadd(z),z,y)
7.82/3.03	   ?1(tp2(x,y),z,y) -> gcd(x,y)
7.82/3.03	   iadd(y) -> tp2(0(),y)
7.82/3.03	   u1(tp2(x,y)) -> tp2(s(x),y)
7.82/3.03	  Unfolding Processor:
7.82/3.03	   loop length: 3
7.82/3.03	   terms:
7.82/3.03	    ?2(iadd(0()),0(),0())
7.82/3.03	    ?2(tp2(0(),0()),0(),0())
7.82/3.03	    gcd(0(),0())
7.82/3.03	   context: []
7.82/3.03	   substitution:
7.82/3.04	    
7.82/3.04	   Qed
7.82/3.04	
8.55/3.07	EOF