7.02/2.35	YES
7.02/2.35	
7.02/2.35	Problem:
7.02/2.35	f(x', x'') -> g(x) <= x' = x, x'' = x
7.02/2.35	f(y', h(y'')) -> g(y) <= y' = y, y'' = y
7.02/2.35	
7.02/2.35	Proof:
7.02/2.35	This system is confluent.
7.02/2.35	By \cite{ALS94}, Theorem 4.1.
7.02/2.35	This system is of type 3 or smaller.
7.02/2.35	This system is strongly deterministic.
7.02/2.35	All 2 critical pairs are joinable.
7.02/2.35	CP: g(y') = g(z') <= $1 = z', $2 = z', $1 = y', h($2) = y':
7.02/2.35	This critical pair is infeasible.
7.02/2.35	This critical pair is conditional.
7.02/2.35	This critical pair has some non-trivial conditions.
7.02/2.35	usable rules
7.02/2.35	'\Sigma(h($2)) \cap (->^*_R)[\Sigma(REN(y'))]' is empty.
7.02/2.35	CP: g(x') = g(y') <= $1 = y', h($2) = y', $1 = x', $2 = x':
7.02/2.36	This critical pair is infeasible.
7.02/2.36	This critical pair is conditional.
7.02/2.36	This critical pair has some non-trivial conditions.
7.02/2.36	usable rules
7.02/2.36	'\Sigma(h($2)) \cap (->^*_R)[\Sigma(REN(y'))]' is empty.
7.02/2.36	This system is quasi-decreasing.
7.02/2.36	By \cite{A14}, Theorem 11.5.9.
7.02/2.36	This system is of type 3 or smaller.
7.02/2.36	This system is deterministic.
7.02/2.36	System R transformed to V(R) + Emb.
7.02/2.36	This system is terminating.
7.02/2.36	Call external tool:
7.02/2.36	./ttt2.sh
7.02/2.36	Input:
7.02/2.36	  f(x', x'') -> g(x'')
7.02/2.36	  f(x', x'') -> x''
7.02/2.36	  f(x', x'') -> x'
7.02/2.36	  f(y', h(y'')) -> g(y'')
7.02/2.36	  f(y', h(y'')) -> y''
7.02/2.36	  f(y', h(y'')) -> y'
7.02/2.36	  h(x) -> x
7.02/2.36	  g(x) -> x
7.02/2.36	  f(x, y) -> x
7.02/2.36	  f(x, y) -> y
7.02/2.36	
7.02/2.36	 Matrix Interpretation Processor: dim=3
7.02/2.36	  
7.02/2.36	  interpretation:
7.02/2.36	               
7.02/2.36	   [h](x0) = x0
7.02/2.36	               ,
7.02/2.36	   
7.02/2.36	             [1 0 0]  
7.02/2.36	   [g](x0) = [0 1 0]x0
7.02/2.36	             [0 1 1]  ,
7.02/2.36	   
7.02/2.36	                      [1 0 0]     [1]
7.02/2.36	   [f](x0, x1) = x0 + [0 1 0]x1 + [0]
7.02/2.36	                      [0 1 1]     [0]
7.02/2.36	  orientation:
7.02/2.36	                    [1 0 0]      [1]    [1 0 0]            
7.02/2.36	   f(x',x'') = x' + [0 1 0]x'' + [0] >= [0 1 0]x'' = g(x'')
7.02/2.36	                    [0 1 1]      [0]    [0 1 1]            
7.02/2.36	   
7.02/2.36	                    [1 0 0]      [1]             
7.02/2.36	   f(x',x'') = x' + [0 1 0]x'' + [0] >= x'' = x''
7.02/2.36	                    [0 1 1]      [0]             
7.02/2.36	   
7.02/2.36	                    [1 0 0]      [1]           
7.02/2.36	   f(x',x'') = x' + [0 1 0]x'' + [0] >= x' = x'
7.02/2.36	                    [0 1 1]      [0]           
7.02/2.36	   
7.02/2.36	                       [1 0 0]      [1]    [1 0 0]            
7.02/2.36	   f(y',h(y'')) = y' + [0 1 0]y'' + [0] >= [0 1 0]y'' = g(y'')
7.02/2.36	                       [0 1 1]      [0]    [0 1 1]            
7.02/2.36	   
7.02/2.36	                       [1 0 0]      [1]             
7.02/2.36	   f(y',h(y'')) = y' + [0 1 0]y'' + [0] >= y'' = y''
7.02/2.36	                       [0 1 1]      [0]             
7.02/2.36	   
7.02/2.36	                       [1 0 0]      [1]           
7.02/2.36	   f(y',h(y'')) = y' + [0 1 0]y'' + [0] >= y' = y'
7.02/2.36	                       [0 1 1]      [0]           
7.02/2.36	   
7.02/2.36	                    
7.02/2.36	   h(x) = x >= x = x
7.02/2.36	                    
7.02/2.36	   
7.02/2.36	          [1 0 0]          
7.02/2.36	   g(x) = [0 1 0]x >= x = x
7.02/2.36	          [0 1 1]          
7.02/2.36	   
7.02/2.36	                [1 0 0]    [1]         
7.02/2.36	   f(x,y) = x + [0 1 0]y + [0] >= x = x
7.02/2.36	                [0 1 1]    [0]         
7.02/2.36	   
7.02/2.36	                [1 0 0]    [1]         
7.02/2.36	   f(x,y) = x + [0 1 0]y + [0] >= y = y
7.02/2.36	                [0 1 1]    [0]         
7.02/2.36	  problem:
7.02/2.36	   h(x) -> x
7.02/2.36	   g(x) -> x
7.02/2.36	  Matrix Interpretation Processor: dim=3
7.02/2.36	   
7.02/2.36	   interpretation:
7.02/2.36	                
7.02/2.36	    [h](x0) = x0
7.02/2.36	                ,
7.02/2.36	    
7.02/2.36	                   [1]
7.02/2.36	    [g](x0) = x0 + [0]
7.02/2.36	                   [0]
7.02/2.36	   orientation:
7.02/2.36	                     
7.02/2.36	    h(x) = x >= x = x
7.02/2.36	                     
7.02/2.36	    
7.02/2.36	               [1]         
7.02/2.36	    g(x) = x + [0] >= x = x
7.02/2.36	               [0]         
7.02/2.36	   problem:
7.02/2.36	    h(x) -> x
7.02/2.36	   Matrix Interpretation Processor: dim=3
7.02/2.36	    
7.02/2.36	    interpretation:
7.02/2.36	                    [1]
7.02/2.36	     [h](x0) = x0 + [0]
7.02/2.36	                    [0]
7.02/2.36	    orientation:
7.02/2.36	                [1]         
7.02/2.36	     h(x) = x + [0] >= x = x
7.02/2.36	                [0]         
7.02/2.36	    problem:
7.02/2.36	     
7.02/2.36	    Qed
7.02/2.36	
7.02/2.39	EOF