4.39/2.02	YES
4.39/2.02	
4.39/2.02	Proof:
4.39/2.02	This system is confluent.
4.39/2.02	Inlined conditions in System R.
4.39/2.02	By \cite{ALS94}, Theorem 4.1.
4.39/2.02	This system is of type 3 or smaller.
4.39/2.03	This system is strongly deterministic.
4.39/2.03	This system is quasi-decreasing.
4.39/2.03	By \cite{O02}, p. 214, Proposition 7.2.50.
4.39/2.03	This system is of type 3 or smaller.
4.39/2.03	This system is deterministic.
4.39/2.03	System R transformed to optimized U(R).
4.39/2.03	This system is terminating.
4.39/2.03	Call external tool:
4.39/2.03	./ttt2.sh
4.39/2.03	Input:
4.39/2.03	(VAR x)
4.39/2.03	(RULES
4.39/2.03	  pin(a) -> pout(b)
4.39/2.03	  pin(b) -> pout(c)
4.39/2.03	  tc(x) -> x
4.39/2.03	  tc(x) -> ?1(pin(x), x)
4.39/2.03	  ?1(pout(z), x) -> tc(z)
4.39/2.03	)
4.39/2.03	
4.39/2.03	 Matrix Interpretation Processor: dim=1
4.39/2.03	  
4.39/2.03	  interpretation:
4.39/2.03	   [z] = 0,
4.39/2.03	   
4.39/2.03	   [?1](x0, x1) = x0 + 4x1 + 3,
4.39/2.03	   
4.39/2.03	   [tc](x0) = 7x0 + 4,
4.39/2.03	   
4.39/2.03	   [c] = 0,
4.39/2.03	   
4.39/2.03	   [pout](x0) = x0 + 1,
4.39/2.03	   
4.39/2.03	   [b] = 2,
4.39/2.03	   
4.39/2.03	   [pin](x0) = 2x0,
4.39/2.03	   
4.39/2.03	   [a] = 4
4.39/2.03	  orientation:
4.39/2.03	   pin(a()) = 8 >= 3 = pout(b())
4.39/2.03	   
4.39/2.03	   pin(b()) = 4 >= 1 = pout(c())
4.39/2.03	   
4.39/2.03	   tc(x) = 7x + 4 >= x = x
4.39/2.03	   
4.39/2.03	   tc(x) = 7x + 4 >= 6x + 3 = ?1(pin(x),x)
4.39/2.03	   
4.39/2.03	   ?1(pout(z()),x) = 4x + 4 >= 4 = tc(z())
4.39/2.03	  problem:
4.39/2.03	   ?1(pout(z()),x) -> tc(z())
4.39/2.03	  Matrix Interpretation Processor: dim=3
4.39/2.03	   
4.39/2.03	   interpretation:
4.39/2.03	          [0]
4.39/2.03	    [z] = [0]
4.39/2.03	          [0],
4.39/2.03	    
4.39/2.03	                   [1 0 0]     [1 0 0]     [1]
4.39/2.03	    [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
4.39/2.03	                   [0 0 0]     [0 0 0]     [0],
4.39/2.03	    
4.39/2.03	               [1 0 0]  
4.39/2.03	    [tc](x0) = [0 0 0]x0
4.39/2.03	               [0 0 0]  ,
4.39/2.03	    
4.39/2.03	                 [1 0 0]  
4.39/2.03	    [pout](x0) = [0 0 0]x0
4.39/2.03	                 [0 0 0]  
4.39/2.03	   orientation:
4.39/2.03	                      [1 0 0]    [1]    [0]          
4.39/2.03	    ?1(pout(z()),x) = [0 0 0]x + [1] >= [0] = tc(z())
4.39/2.03	                      [0 0 0]    [0]    [0]          
4.39/2.03	   problem:
4.39/2.03	    
4.39/2.03	   Qed
4.39/2.03	All 2 critical pairs are joinable.
4.39/2.03	Overlap: (rule1: tc(y) -> tc(z) <= pin(y) = pout(z), rule2: tc(x') -> x', pos: ε, mgu: {(y,x')})
4.39/2.03	CP: x' = tc(z) <= pin(x') = pout(z)
4.39/2.03	This critical pair is infeasible.
4.39/2.03	This critical pair is conditional.
4.39/2.03	This critical pair has some non-trivial conditions.
4.39/2.03	'\Sigma(pin(x')) \cap (->^*_R)[\Sigma(REN(pout(z)))]' is empty by ETAC.
4.39/2.03	Overlap: (rule1: tc(y) -> y, rule2: tc(x') -> tc(z) <= pin(x') = pout(z), pos: ε, mgu: {(y,x')})
4.39/2.03	CP: tc(z) = x' <= pin(x') = pout(z)
4.39/2.03	This critical pair is infeasible.
4.39/2.03	This critical pair is conditional.
4.39/2.03	This critical pair has some non-trivial conditions.
4.39/2.03	'\Sigma(pin(x')) \cap (->^*_R)[\Sigma(REN(pout(z)))]' is empty by ETAC.
4.39/2.03	
4.39/2.06	EOF