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