3.92/1.94	YES
3.92/1.94	
3.92/1.94	Problem:
3.92/1.95	pin(a()) -> pout(b())
3.92/1.95	pin(b()) -> pout(c())
3.92/1.95	tc(x) -> x
3.92/1.95	tc(x) -> y <= pin(x) = pout(z()), tc(z()) = y
3.92/1.95	
3.92/1.95	Proof:
3.92/1.95	This system is confluent.
3.92/1.95	By \cite{ALS94}, Theorem 4.1.
3.92/1.95	This system is of type 3 or smaller.
3.92/1.95	This system is strongly deterministic.
3.92/1.95	All 2 critical pairs are joinable.
3.92/1.95	CP: x = y <= pin(x) = pout(z()), tc(z()) = y:
3.92/1.95	This critical pair is infeasible.
3.92/1.95	This critical pair is conditional.
3.92/1.95	This critical pair has some non-trivial conditions.
3.92/1.95	usable rules
3.92/1.95	pin(a()) -> pout(b())
3.92/1.95	pin(b()) -> pout(c())
3.92/1.95	'\Sigma(pin(x)) \cap (->^*_R)[\Sigma(REN(pout(z())))]' is empty.
3.92/1.95	CP: x = z <= pin(z) = pout(z()), tc(z()) = x:
3.92/1.95	This critical pair is infeasible.
3.92/1.95	This critical pair is conditional.
3.92/1.95	This critical pair has some non-trivial conditions.
3.92/1.95	'[\Sigma(REN(conds(pout(z()), x)))](->^*_R^-1_\alpha) \cap \Sigma(conds(pin(z), tc(z())))' is empty.
3.92/1.95	This system is quasi-decreasing.
3.92/1.95	By \cite{O02}, p. 214, Proposition 7.2.50.
3.92/1.95	This system is of type 3 or smaller.
3.92/1.95	This system is deterministic.
3.92/1.95	System R transformed to U(R).
3.92/1.95	This system is terminating.
3.92/1.95	Call external tool:
3.92/1.95	./ttt2.sh
3.92/1.95	Input:
3.92/1.95	  pin(a()) -> pout(b())
3.92/1.95	  pin(b()) -> pout(c())
3.92/1.95	  tc(x) -> x
3.92/1.95	  ?2(y, x) -> y
3.92/1.95	  ?1(pout(z()), x) -> ?2(tc(z()), x)
3.92/1.95	  tc(x) -> ?1(pin(x), x)
3.92/1.95	
3.92/1.95	 Matrix Interpretation Processor: dim=1
3.92/1.95	  
3.92/1.95	  interpretation:
3.92/1.95	   [?1](x0, x1) = x0 + x1,
3.92/1.95	   
3.92/1.95	   [z] = 0,
3.92/1.95	   
3.92/1.95	   [?2](x0, x1) = x0 + x1 + 1,
3.92/1.95	   
3.92/1.95	   [tc](x0) = 7x0,
3.92/1.95	   
3.92/1.95	   [c] = 0,
3.92/1.95	   
3.92/1.95	   [pout](x0) = x0 + 1,
3.92/1.95	   
3.92/1.95	   [b] = 1,
3.92/1.95	   
3.92/1.95	   [pin](x0) = 5x0,
3.92/1.95	   
3.92/1.95	   [a] = 5
3.92/1.95	  orientation:
3.92/1.95	   pin(a()) = 25 >= 2 = pout(b())
3.92/1.95	   
3.92/1.95	   pin(b()) = 5 >= 1 = pout(c())
3.92/1.95	   
3.92/1.95	   tc(x) = 7x >= x = x
3.92/1.95	   
3.92/1.95	   ?2(y,x) = x + y + 1 >= y = y
3.92/1.95	   
3.92/1.95	   ?1(pout(z()),x) = x + 1 >= x + 1 = ?2(tc(z()),x)
3.92/1.95	   
3.92/1.95	   tc(x) = 7x >= 6x = ?1(pin(x),x)
3.92/1.95	  problem:
3.92/1.95	   tc(x) -> x
3.92/1.95	   ?1(pout(z()),x) -> ?2(tc(z()),x)
3.92/1.95	   tc(x) -> ?1(pin(x),x)
3.92/1.95	  Matrix Interpretation Processor: dim=1
3.92/1.95	   
3.92/1.95	   interpretation:
3.92/1.95	    [?1](x0, x1) = x0 + 6x1,
3.92/1.95	    
3.92/1.95	    [z] = 1,
3.92/1.95	    
3.92/1.95	    [?2](x0, x1) = x0 + 2x1 + 1,
3.92/1.95	    
3.92/1.95	    [tc](x0) = 7x0,
3.92/1.95	    
3.92/1.95	    [pout](x0) = 2x0 + 7,
3.92/1.95	    
3.92/1.95	    [pin](x0) = x0
3.92/1.95	   orientation:
3.92/1.95	    tc(x) = 7x >= x = x
3.92/1.95	    
3.92/1.95	    ?1(pout(z()),x) = 6x + 9 >= 2x + 8 = ?2(tc(z()),x)
3.92/1.95	    
3.92/1.95	    tc(x) = 7x >= 7x = ?1(pin(x),x)
3.92/1.95	   problem:
3.92/1.95	    tc(x) -> x
3.92/1.95	    tc(x) -> ?1(pin(x),x)
3.92/1.95	   Matrix Interpretation Processor: dim=1
3.92/1.95	    
3.92/1.95	    interpretation:
3.92/1.95	     [?1](x0, x1) = x0 + x1,
3.92/1.95	     
3.92/1.95	     [tc](x0) = 6x0 + 4,
3.92/1.95	     
3.92/1.95	     [pin](x0) = 4x0 + 2
3.92/1.95	    orientation:
3.92/1.95	     tc(x) = 6x + 4 >= x = x
3.92/1.95	     
3.92/1.95	     tc(x) = 6x + 4 >= 5x + 2 = ?1(pin(x),x)
3.92/1.95	    problem:
3.92/1.95	     
3.92/1.95	    Qed
3.92/1.95	
5.64/2.02	EOF