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