9.41/3.29	YES
9.41/3.30	
9.41/3.30	Proof:
9.41/3.30	This system is confluent.
9.41/3.30	By \cite{ALS94}, Theorem 4.1.
9.41/3.30	This system is of type 3 or smaller.
9.41/3.30	This system is strongly deterministic.
9.41/3.30	This system is quasi-decreasing.
9.41/3.30	By \cite{A14}, Theorem 11.5.9.
9.41/3.30	This system is of type 3 or smaller.
9.41/3.30	This system is deterministic.
9.41/3.30	System R transformed to V(R) + Emb.
9.41/3.30	This system is terminating.
9.41/3.30	Call external tool:
9.41/3.30	./ttt2.sh
9.41/3.30	Input:
9.41/3.30	(VAR y' x'' x y'' y x')
9.41/3.30	(RULES
9.41/3.30	  f(x', x'') -> g(x')
9.41/3.30	  f(x', x'') -> x''
9.41/3.30	  f(x', x'') -> x'
9.41/3.30	  f(y', h(y'')) -> g(y')
9.41/3.30	  f(y', h(y'')) -> y''
9.41/3.30	  f(y', h(y'')) -> y'
9.41/3.30	  h(x) -> x
9.41/3.30	  g(x) -> x
9.41/3.30	  f(x, y) -> x
9.41/3.30	  f(x, y) -> y
9.41/3.30	)
9.41/3.30	
9.41/3.30	 Matrix Interpretation Processor: dim=3
9.41/3.30	  
9.41/3.30	  interpretation:
9.41/3.30	               
9.41/3.30	   [h](x0) = x0
9.41/3.30	               ,
9.41/3.30	   
9.41/3.30	               
9.41/3.30	   [g](x0) = x0
9.41/3.30	               ,
9.41/3.30	   
9.41/3.30	                           [1]
9.41/3.30	   [f](x0, x1) = x0 + x1 + [0]
9.41/3.30	                           [0]
9.41/3.30	  orientation:
9.41/3.30	                          [1]              
9.41/3.30	   f(x',x'') = x' + x'' + [0] >= x' = g(x')
9.41/3.30	                          [0]              
9.41/3.30	   
9.41/3.30	                          [1]             
9.41/3.30	   f(x',x'') = x' + x'' + [0] >= x'' = x''
9.41/3.30	                          [0]             
9.41/3.30	   
9.41/3.30	                          [1]           
9.41/3.30	   f(x',x'') = x' + x'' + [0] >= x' = x'
9.41/3.30	                          [0]           
9.41/3.30	   
9.41/3.30	                             [1]              
9.41/3.30	   f(y',h(y'')) = y' + y'' + [0] >= y' = g(y')
9.41/3.30	                             [0]              
9.41/3.30	   
9.41/3.30	                             [1]             
9.41/3.30	   f(y',h(y'')) = y' + y'' + [0] >= y'' = y''
9.41/3.30	                             [0]             
9.41/3.30	   
9.41/3.30	                             [1]           
9.41/3.30	   f(y',h(y'')) = y' + y'' + [0] >= y' = y'
9.41/3.30	                             [0]           
9.41/3.30	   
9.41/3.30	                    
9.41/3.30	   h(x) = x >= x = x
9.41/3.31	                    
9.41/3.31	   
9.41/3.31	                    
9.41/3.31	   g(x) = x >= x = x
9.41/3.31	                    
9.41/3.31	   
9.41/3.31	                    [1]         
9.41/3.31	   f(x,y) = x + y + [0] >= x = x
9.41/3.31	                    [0]         
9.41/3.31	   
9.41/3.31	                    [1]         
9.41/3.31	   f(x,y) = x + y + [0] >= y = y
9.41/3.31	                    [0]         
9.41/3.31	  problem:
9.41/3.31	   h(x) -> x
9.41/3.31	   g(x) -> x
9.41/3.31	  Matrix Interpretation Processor: dim=3
9.41/3.31	   
9.41/3.31	   interpretation:
9.41/3.31	                
9.41/3.31	    [h](x0) = x0
9.41/3.31	                ,
9.41/3.31	    
9.41/3.31	                   [1]
9.41/3.31	    [g](x0) = x0 + [0]
9.41/3.31	                   [0]
9.41/3.31	   orientation:
9.41/3.31	                     
9.41/3.31	    h(x) = x >= x = x
9.41/3.31	                     
9.41/3.31	    
9.41/3.31	               [1]         
9.41/3.31	    g(x) = x + [0] >= x = x
9.41/3.31	               [0]         
9.41/3.31	   problem:
9.41/3.31	    h(x) -> x
9.41/3.31	   Matrix Interpretation Processor: dim=3
9.41/3.31	    
9.41/3.31	    interpretation:
9.41/3.31	                    [1]
9.41/3.31	     [h](x0) = x0 + [0]
9.41/3.31	                    [0]
9.41/3.31	    orientation:
9.41/3.31	                [1]         
9.41/3.31	     h(x) = x + [0] >= x = x
9.41/3.31	                [0]         
9.41/3.31	    problem:
9.41/3.31	     
9.41/3.31	    Qed
9.41/3.31	All 2 critical pairs are joinable.
9.41/3.31	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'))})
9.41/3.31	CP: g(y) = g(x) <= y' = x, x' = x, y' = y, h(x') = y
9.41/3.31	This critical pair is infeasible.
9.41/3.31	This critical pair is conditional.
9.41/3.31	This critical pair has some non-trivial conditions.
9.41/3.31	Call external tool:
9.41/3.31	./waldmeister
9.41/3.31	Input:
9.41/3.31	  f(x', x'') -> g(x) <= x' = x, x'' = x
9.41/3.31	  f(y', h(y'')) -> g(y) <= y' = y, y'' = y
9.41/3.31	
9.41/3.31	By Waldmeister.
9.41/3.31	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'))})
9.41/3.31	CP: g(x) = g(y) <= x' = y, h(z') = y, x' = x, z' = x
9.41/3.31	This critical pair is infeasible.
9.41/3.31	This critical pair is conditional.
9.41/3.31	This critical pair has some non-trivial conditions.
9.41/3.31	Call external tool:
9.41/3.31	./waldmeister
9.41/3.31	Input:
9.41/3.31	  f(x', x'') -> g(x) <= x' = x, x'' = x
9.41/3.31	  f(y', h(y'')) -> g(y) <= y' = y, y'' = y
9.41/3.31	
9.41/3.31	By Waldmeister.
9.41/3.31	
9.41/3.33	EOF