3.73/1.48	YES
3.73/1.48	
3.73/1.48	Proof:
3.73/1.48	This system is confluent.
3.73/1.48	By \cite{ALS94}, Theorem 4.1.
3.73/1.49	This system is of type 3 or smaller.
3.73/1.49	This system is strongly deterministic.
3.73/1.49	This system is quasi-decreasing.
3.73/1.49	By \cite{O02}, p. 214, Proposition 7.2.50.
3.73/1.49	This system is of type 3 or smaller.
3.73/1.49	This system is deterministic.
3.73/1.49	System R transformed to U(R).
3.73/1.49	This system is terminating.
3.73/1.49	Call external tool:
3.73/1.49	./ttt2.sh
3.73/1.49	Input:
3.73/1.49	  ?2(i(z), x, y) -> g(x, y, z)
3.73/1.49	  ?1(i(y), x) -> ?2(h(a, y), x, y)
3.73/1.49	  f(x) -> ?1(h(a, x), x)
3.73/1.49	  h(a, a) -> i(b)
3.73/1.49	  h(a, b) -> i(c)
3.73/1.49	  h(b, b) -> i(d)
3.73/1.49	
3.73/1.49	 Matrix Interpretation Processor: dim=1
3.73/1.49	  
3.73/1.49	  interpretation:
3.73/1.49	   [d] = 0,
3.73/1.49	   
3.73/1.49	   [c] = 0,
3.73/1.49	   
3.73/1.49	   [b] = 0,
3.73/1.49	   
3.73/1.49	   [f](x0) = 5x0 + 6,
3.73/1.49	   
3.73/1.49	   [h](x0, x1) = 2x0 + x1,
3.73/1.49	   
3.73/1.49	   [a] = 0,
3.73/1.49	   
3.73/1.49	   [?1](x0, x1) = 4x0 + x1 + 4,
3.73/1.49	   
3.73/1.49	   [g](x0, x1, x2) = x0 + x1 + 4x2,
3.73/1.49	   
3.73/1.49	   [?2](x0, x1, x2) = 2x0 + x1 + 2x2,
3.73/1.49	   
3.73/1.49	   [i](x0) = 4x0
3.73/1.49	  orientation:
3.73/1.49	   ?2(i(z),x,y) = x + 2y + 8z >= x + y + 4z = g(x,y,z)
3.73/1.49	   
3.73/1.49	   ?1(i(y),x) = x + 16y + 4 >= x + 4y = ?2(h(a(),y),x,y)
3.73/1.49	   
3.73/1.49	   f(x) = 5x + 6 >= 5x + 4 = ?1(h(a(),x),x)
3.73/1.49	   
3.73/1.49	   h(a(),a()) = 0 >= 0 = i(b())
3.73/1.49	   
3.73/1.49	   h(a(),b()) = 0 >= 0 = i(c())
3.73/1.49	   
3.73/1.50	   h(b(),b()) = 0 >= 0 = i(d())
3.73/1.50	  problem:
3.73/1.50	   ?2(i(z),x,y) -> g(x,y,z)
3.73/1.50	   h(a(),a()) -> i(b())
3.73/1.50	   h(a(),b()) -> i(c())
3.73/1.50	   h(b(),b()) -> i(d())
3.73/1.50	  Matrix Interpretation Processor: dim=3
3.73/1.50	   
3.73/1.50	   interpretation:
3.73/1.50	          [0]
3.73/1.50	    [d] = [0]
3.73/1.50	          [0],
3.73/1.50	    
3.73/1.50	          [0]
3.73/1.50	    [c] = [0]
3.73/1.50	          [0],
3.73/1.50	    
3.73/1.50	          [0]
3.73/1.50	    [b] = [0]
3.73/1.50	          [1],
3.73/1.50	    
3.73/1.50	                  [1 0 0]     [1 0 0]     [1]
3.73/1.50	    [h](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
3.73/1.50	                  [0 0 0]     [0 1 0]     [0],
3.73/1.50	    
3.73/1.50	          [0]
3.73/1.50	    [a] = [1]
3.73/1.50	          [0],
3.73/1.50	    
3.73/1.50	                      [1 0 0]     [1 0 0]     [1 0 0]  
3.73/1.50	    [g](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
3.73/1.50	                      [0 0 0]     [0 0 0]     [0 0 0]  ,
3.73/1.50	    
3.73/1.50	                       [1 0 0]     [1 0 0]     [1 0 0]     [1]
3.73/1.50	    [?2](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
3.73/1.50	                       [0 0 0]     [0 0 0]     [0 0 0]     [0],
3.73/1.50	    
3.73/1.50	              [1 0 0]  
3.73/1.50	    [i](x0) = [0 0 0]x0
3.73/1.51	              [0 0 1]  
3.73/1.51	   orientation:
3.73/1.51	                   [1 0 0]    [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1 0 0]            
3.73/1.51	    ?2(i(z),x,y) = [0 0 0]x + [0 0 0]y + [0 0 0]z + [0] >= [0 0 0]x + [0 0 0]y + [0 0 0]z = g(x,y,z)
3.73/1.51	                   [0 0 0]    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0 0 0]            
3.73/1.51	    
3.73/1.51	                 [1]    [0]         
3.73/1.51	    h(a(),a()) = [0] >= [0] = i(b())
3.73/1.51	                 [1]    [1]         
3.73/1.51	    
3.73/1.51	                 [1]    [0]         
3.73/1.51	    h(a(),b()) = [0] >= [0] = i(c())
3.73/1.51	                 [0]    [0]         
3.73/1.51	    
3.73/1.51	                 [1]    [0]         
3.73/1.51	    h(b(),b()) = [0] >= [0] = i(d())
3.73/1.51	                 [0]    [0]         
3.73/1.51	   problem:
3.73/1.51	    
3.73/1.51	   Qed
3.73/1.51	All 0 critical pairs are joinable.
3.73/1.51	
4.26/1.64	EOF