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