1.26/1.15	YES
1.26/1.15	
1.26/1.15	Proof:
1.26/1.15	This system is confluent.
1.26/1.15	By \cite{ALS94}, Theorem 4.1.
1.26/1.15	This system is of type 3 or smaller.
1.26/1.15	This system is strongly deterministic.
1.26/1.15	This system is quasi-decreasing.
1.26/1.15	By \cite{O02}, p. 214, Proposition 7.2.50.
1.26/1.15	This system is of type 3 or smaller.
1.26/1.15	This system is deterministic.
1.26/1.15	System R transformed to optimized U(R).
1.26/1.15	This system is terminating.
1.26/1.15	Call external tool:
1.26/1.15	./ttt2.sh
1.26/1.15	Input:
1.26/1.15	  f(x) -> ?1(g(x, x), x)
1.26/1.15	  ?1(a, x) -> b
1.26/1.15	
1.26/1.15	 Matrix Interpretation Processor: dim=1
1.26/1.15	  
1.26/1.16	  interpretation:
1.26/1.16	   [b] = 0,
1.26/1.16	   
1.26/1.16	   [a] = 0,
1.26/1.16	   
1.26/1.16	   [?1](x0, x1) = x0 + 4x1,
1.26/1.16	   
1.26/1.16	   [g](x0, x1) = x0 + x1,
1.26/1.16	   
1.26/1.16	   [f](x0) = 6x0 + 4
1.26/1.16	  orientation:
1.26/1.16	   f(x) = 6x + 4 >= 6x = ?1(g(x,x),x)
1.26/1.16	   
1.26/1.16	   ?1(a(),x) = 4x >= 0 = b()
1.26/1.16	  problem:
1.26/1.16	   ?1(a(),x) -> b()
1.26/1.16	  Matrix Interpretation Processor: dim=3
1.26/1.16	   
1.26/1.16	   interpretation:
1.26/1.16	          [0]
1.26/1.16	    [b] = [0]
1.26/1.16	          [0],
1.26/1.16	    
1.26/1.16	          [0]
1.26/1.16	    [a] = [0]
1.26/1.16	          [0],
1.26/1.16	    
1.26/1.16	                   [1 0 0]     [1 0 0]     [1]
1.26/1.16	    [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
1.26/1.16	                   [0 0 0]     [0 0 0]     [0]
1.26/1.16	   orientation:
1.26/1.16	                [1 0 0]    [1]    [0]      
1.26/1.16	    ?1(a(),x) = [0 0 0]x + [0] >= [0] = b()
1.26/1.16	                [0 0 0]    [0]    [0]      
1.26/1.16	   problem:
1.26/1.16	    
1.26/1.16	   Qed
1.26/1.16	All 0 critical pairs are joinable.
1.26/1.16	
1.26/1.18	EOF