10.31/3.55	YES
10.31/3.55	
10.31/3.55	Proof:
10.31/3.56	This system is confluent.
10.31/3.56	By \cite{ALS94}, Theorem 4.1.
10.31/3.56	This system is of type 3 or smaller.
10.31/3.56	This system is strongly deterministic.
10.31/3.56	This system is quasi-decreasing.
10.31/3.56	By \cite{O02}, p. 214, Proposition 7.2.50.
10.31/3.56	This system is of type 3 or smaller.
10.31/3.56	This system is deterministic.
10.31/3.56	System R transformed to optimized U(R).
10.31/3.56	This system is terminating.
10.31/3.56	Call external tool:
10.31/3.56	./ttt2.sh
10.31/3.56	Input:
10.31/3.56	(VAR y' x'' x y'' y x')
10.31/3.56	(RULES
10.31/3.56	  f(x', x'') -> ?1(x', x', x'')
10.31/3.56	  ?1(x, x', x'') -> ?2(x'', x', x'', x)
10.31/3.56	  ?2(x, x', x'', x) -> g(x)
10.31/3.56	  f(y', h(y'')) -> ?3(y', y', y'')
10.31/3.56	  ?3(y, y', y'') -> ?4(y'', y', y'', y)
10.31/3.56	  ?4(y, y', y'', y) -> g(y)
10.31/3.56	)
10.31/3.56	
10.31/3.56	 Matrix Interpretation Processor: dim=1
10.31/3.56	  
10.31/3.56	  interpretation:
10.31/3.56	   [?4](x0, x1, x2, x3) = x0 + x1 + 4x2 + 2x3 + 4,
10.31/3.56	   
10.31/3.56	   [?3](x0, x1, x2) = 2x0 + x1 + 6x2 + 5,
10.31/3.56	   
10.31/3.56	   [h](x0) = 3x0 + 4,
10.31/3.56	   
10.31/3.56	   [g](x0) = x0,
10.31/3.56	   
10.31/3.56	   [?2](x0, x1, x2, x3) = 2x0 + x1 + 2x2 + 2x3,
10.31/3.56	   
10.31/3.56	   [?1](x0, x1, x2) = 2x0 + x1 + 4x2,
10.31/3.56	   
10.31/3.56	   [f](x0, x1) = 3x0 + 5x1 + 3
10.31/3.56	  orientation:
10.31/3.56	   f(x',x'') = 3x' + 5x'' + 3 >= 3x' + 4x'' = ?1(x',x',x'')
10.31/3.56	   
10.31/3.56	   ?1(x,x',x'') = 2x + x' + 4x'' >= 2x + x' + 4x'' = ?2(x'',x',x'',x)
10.31/3.56	   
10.31/3.56	   ?2(x,x',x'',x) = 4x + x' + 2x'' >= x = g(x)
10.31/3.56	   
10.31/3.56	   f(y',h(y'')) = 3y' + 15y'' + 23 >= 3y' + 6y'' + 5 = ?3(y',y',y'')
10.31/3.56	   
10.31/3.56	   ?3(y,y',y'') = 2y + y' + 6y'' + 5 >= 2y + y' + 5y'' + 4 = ?4(y'',y',y'',y)
10.31/3.56	   
10.31/3.56	   ?4(y,y',y'',y) = 3y + y' + 4y'' + 4 >= y = g(y)
10.31/3.56	  problem:
10.31/3.56	   ?1(x,x',x'') -> ?2(x'',x',x'',x)
10.31/3.56	   ?2(x,x',x'',x) -> g(x)
10.31/3.56	  Matrix Interpretation Processor: dim=2
10.31/3.56	   
10.31/3.56	   interpretation:
10.31/3.56	              [3 0]  
10.31/3.56	    [g](x0) = [0 0]x0,
10.31/3.56	    
10.31/3.56	                           [1 0]     [2 0]     [2 0]     [2 0]     [2]
10.31/3.56	    [?2](x0, x1, x2, x3) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [0],
10.31/3.56	    
10.31/3.56	                       [3 0]     [2 0]     [3 0]     [2]
10.31/3.56	    [?1](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0]
10.31/3.56	   orientation:
10.31/3.56	                   [3 0]    [2 0]     [3 0]      [2]    [2 0]    [2 0]     [3 0]      [2]                   
10.31/3.56	    ?1(x,x',x'') = [0 0]x + [0 0]x' + [0 0]x'' + [0] >= [0 0]x + [0 0]x' + [0 0]x'' + [0] = ?2(x'',x',x'',x)
10.31/3.56	    
10.31/3.56	                     [3 0]    [2 0]     [2 0]      [2]    [3 0]        
10.31/3.56	    ?2(x,x',x'',x) = [0 0]x + [0 0]x' + [0 0]x'' + [0] >= [0 0]x = g(x)
10.31/3.56	   problem:
10.31/3.56	    ?1(x,x',x'') -> ?2(x'',x',x'',x)
10.31/3.56	   Matrix Interpretation Processor: dim=2
10.31/3.56	    
10.31/3.56	    interpretation:
10.31/3.56	                            [1 0]     [1 0]     [1 2]     [1 0]  
10.31/3.56	     [?2](x0, x1, x2, x3) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3,
10.31/3.56	     
10.31/3.56	                        [1 0]     [1 0]     [2 2]     [1]
10.31/3.56	     [?1](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [1 0]x2 + [0]
10.31/3.56	    orientation:
10.31/3.56	                    [1 0]    [1 0]     [2 2]      [1]    [1 0]    [1 0]     [2 2]                      
10.31/3.56	     ?1(x,x',x'') = [0 0]x + [0 0]x' + [1 0]x'' + [0] >= [0 0]x + [0 0]x' + [0 0]x'' = ?2(x'',x',x'',x)
10.31/3.56	    problem:
10.31/3.56	     
10.31/3.57	    Qed
10.31/3.57	All 2 critical pairs are joinable.
10.31/3.57	Overlap: (rule1: f(z, h(x')) -> g(x) <= z = x, x' = x, rule2: f(y', z') -> g(y) <= y' = y, z' = y, pos: ε, mgu: {(z,y'), (z',h(x'))})
10.31/3.57	CP: g(y) = g(x) <= y' = x, x' = x, y' = y, h(x') = y
10.31/3.57	This critical pair is infeasible.
10.31/3.57	This critical pair is conditional.
10.31/3.57	This critical pair has some non-trivial conditions.
10.31/3.57	Call external tool:
10.31/3.57	./waldmeister
10.31/3.57	Input:
10.31/3.57	  f(x', x'') -> g(x) <= x' = x, x'' = x
10.31/3.57	  f(y', h(y'')) -> g(y) <= y' = y, y'' = y
10.31/3.57	
10.31/3.57	By Waldmeister.
10.31/3.57	Overlap: (rule1: f(z, y') -> g(y) <= z = y, y' = y, rule2: f(x', h(z')) -> g(x) <= x' = x, z' = x, pos: ε, mgu: {(z,x'), (y',h(z'))})
10.31/3.57	CP: g(x) = g(y) <= x' = y, h(z') = y, x' = x, z' = x
10.31/3.57	This critical pair is infeasible.
10.31/3.57	This critical pair is conditional.
10.31/3.57	This critical pair has some non-trivial conditions.
10.31/3.57	Call external tool:
10.31/3.57	./waldmeister
10.31/3.57	Input:
10.31/3.57	  f(x', x'') -> g(x) <= x' = x, x'' = x
10.31/3.57	  f(y', h(y'')) -> g(y) <= y' = y, y'' = y
10.31/3.57	
10.31/3.57	By Waldmeister.
10.31/3.57	
10.31/3.59	EOF