3.08/1.68	YES
3.08/1.68	
3.08/1.68	Proof:
3.08/1.68	This system is confluent.
3.08/1.68	Removed infeasible rules from system R.
3.08/1.68	By \cite{ALS94}, Theorem 4.1.
3.08/1.68	This system is of type 3 or smaller.
3.08/1.68	This system is strongly deterministic.
3.08/1.68	This system is quasi-decreasing.
3.08/1.68	By \cite{O02}, p. 214, Proposition 7.2.50.
3.08/1.68	This system is of type 3 or smaller.
3.08/1.68	This system is deterministic.
3.08/1.68	System R transformed to U(R).
3.08/1.68	This system is terminating.
3.08/1.68	Call external tool:
3.08/1.68	./ttt2.sh
3.08/1.68	Input:
3.08/1.68	(VAR n r)
3.08/1.68	(RULES
3.08/1.68	  filter(n, r, nil) -> pair(mo, nil)
3.08/1.68	)
3.08/1.68	
3.08/1.68	 Matrix Interpretation Processor: dim=3
3.08/1.68	  
3.08/1.68	  interpretation:
3.08/1.68	                    [1 0 0]     [1 0 0]     [0]
3.08/1.68	   [pair](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
3.08/1.68	                    [0 0 0]     [0 0 0]     [0],
3.08/1.68	   
3.08/1.68	          [0]
3.08/1.68	   [mo] = [0]
3.08/1.68	          [0],
3.08/1.68	   
3.08/1.68	                          [1 0 0]     [1 0 0]     [1 0 0]     [1]
3.08/1.68	   [filter](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [1]
3.08/1.68	                          [0 0 0]     [0 0 0]     [0 0 0]     [0],
3.08/1.68	   
3.08/1.68	           [0]
3.08/1.68	   [nil] = [0]
3.08/1.68	           [0]
3.08/1.68	  orientation:
3.08/1.68	                       [1 0 0]    [1 0 0]    [1]    [0]                   
3.08/1.68	   filter(n,r,nil()) = [0 0 0]n + [0 0 0]r + [1] >= [1] = pair(mo(),nil())
3.08/1.68	                       [0 0 0]    [0 0 0]    [0]    [0]                   
3.08/1.68	  problem:
3.08/1.68	   
3.08/1.68	  Qed
3.08/1.68	All 0 critical pairs are joinable.
3.08/1.68	
3.34/1.71	EOF