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