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