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