5.41/1.93	YES
5.41/1.93	
5.41/1.93	Proof:
5.41/1.93	This system is confluent.
5.41/1.93	By \cite{ALS94}, Theorem 4.1.
5.41/1.93	This system is of type 3 or smaller.
5.41/1.93	This system is strongly deterministic.
5.41/1.93	This system is quasi-decreasing.
5.41/1.93	By \cite{O02}, p. 214, Proposition 7.2.50.
5.41/1.93	This system is of type 3 or smaller.
5.41/1.93	This system is deterministic.
5.41/1.93	System R transformed to optimized U(R).
5.41/1.93	This system is terminating.
5.41/1.93	Call external tool:
5.41/1.93	./ttt2.sh
5.41/1.93	Input:
5.41/1.93	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.41/1.93	  isnoc(cons(x, ys)) -> ?1(isnoc(ys), x, ys)
5.41/1.93	  ?1(tp2(xs, y), x, ys) -> tp2(cons(x, xs), y)
5.41/1.93	
5.41/1.93	 Matrix Interpretation Processor: dim=3
5.41/1.93	  
5.41/1.93	  interpretation:
5.41/1.93	                      [1 0 0]     [1 0 1]     [1 1 0]     [0]
5.41/1.93	   [?1](x0, x1, x2) = [0 1 0]x0 + [1 0 1]x1 + [0 0 0]x2 + [1]
5.41/1.93	                      [0 0 0]     [0 0 0]     [0 0 0]     [0],
5.41/1.93	   
5.41/1.93	                   [1 0 0]     [1 0 1]  
5.41/1.93	   [tp2](x0, x1) = [0 1 0]x0 + [0 0 0]x1
5.41/1.93	                   [0 0 0]     [0 0 0]  ,
5.41/1.93	   
5.41/1.93	                 [1 1 1]     [0]
5.41/1.93	   [isnoc](x0) = [0 1 0]x0 + [1]
5.41/1.93	                 [0 1 0]     [0],
5.41/1.93	   
5.41/1.93	                    [1 0 1]     [1 0 0]     [0]
5.41/1.93	   [cons](x0, x1) = [1 0 1]x0 + [0 1 0]x1 + [1]
5.41/1.93	                    [0 0 1]     [1 1 1]     [0],
5.41/1.93	   
5.41/1.93	           [0]
5.41/1.93	   [nil] = [0]
5.41/1.93	           [1]
5.41/1.93	  orientation:
5.41/1.93	                          [2 0 3]    [2]    [1 0 1]                
5.41/1.93	   isnoc(cons(y,nil())) = [1 0 1]y + [2] >= [0 0 0]y = tp2(nil(),y)
5.41/1.93	                          [1 0 1]    [1]    [0 0 0]                
5.41/1.93	   
5.41/1.93	                       [2 0 3]    [2 2 1]     [1]    [1 0 1]    [2 2 1]     [0]                     
5.41/1.93	   isnoc(cons(x,ys)) = [1 0 1]x + [0 1 0]ys + [2] >= [1 0 1]x + [0 1 0]ys + [2] = ?1(isnoc(ys),x,ys)
5.41/1.93	                       [1 0 1]    [0 1 0]     [1]    [0 0 0]    [0 0 0]     [0]                     
5.41/1.93	   
5.41/1.93	                        [1 0 1]    [1 0 0]     [1 0 1]    [1 1 0]     [0]    [1 0 1]    [1 0 0]     [1 0 1]    [0]                    
5.41/1.93	   ?1(tp2(xs,y),x,ys) = [1 0 1]x + [0 1 0]xs + [0 0 0]y + [0 0 0]ys + [1] >= [1 0 1]x + [0 1 0]xs + [0 0 0]y + [1] = tp2(cons(x,xs),y)
5.41/1.93	                        [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]     [0]    [0 0 0]    [0 0 0]     [0 0 0]    [0]                    
5.41/1.93	  problem:
5.41/1.93	   ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
5.41/1.93	  Matrix Interpretation Processor: dim=3
5.41/1.93	   
5.41/1.93	   interpretation:
5.41/1.93	                       [1 0 0]     [1 0 0]     [1 0 0]     [1]
5.41/1.93	    [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
5.41/1.93	                       [0 0 0]     [0 0 0]     [0 0 0]     [0],
5.41/1.93	    
5.41/1.93	                    [1 0 1]     [1 0 0]  
5.41/1.93	    [tp2](x0, x1) = [0 0 0]x0 + [0 0 0]x1
5.41/1.93	                    [0 0 0]     [0 0 0]  ,
5.41/1.93	    
5.41/1.93	                     [1 0 0]     [1 0 0]  
5.41/1.93	    [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
5.41/1.93	                     [0 0 0]     [0 0 1]  
5.41/1.93	   orientation:
5.41/1.93	                         [1 0 0]    [1 0 1]     [1 0 0]    [1 0 0]     [1]    [1 0 0]    [1 0 1]     [1 0 0]                     
5.41/1.93	    ?1(tp2(xs,y),x,ys) = [0 0 0]x + [0 0 0]xs + [0 0 0]y + [0 0 0]ys + [0] >= [0 0 0]x + [0 0 0]xs + [0 0 0]y = tp2(cons(x,xs),y)
5.41/1.93	                         [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]     [0]    [0 0 0]    [0 0 0]     [0 0 0]                     
5.41/1.93	   problem:
5.41/1.93	    
5.41/1.93	   Qed
5.41/1.93	All 2 critical pairs are joinable.
5.41/1.93	Overlap: (rule1: isnoc(cons(z, z')) -> tp2(cons(z, x'), y') <= isnoc(z') = tp2(x', y'), rule2: isnoc(cons(x, nil)) -> tp2(nil, x), pos: ε, mgu: {(x,z), (z',nil)})
5.41/1.93	CP: tp2(nil, z) = tp2(cons(z, x'), y') <= isnoc(nil) = tp2(x', y')
5.41/1.93	This critical pair is infeasible.
5.41/1.93	This critical pair is conditional.
5.41/1.93	This critical pair has some non-trivial conditions.
5.41/1.93	'(tp2(x', y'))' is not reachable from '(isnoc(nil))' by generalized tcap using root-symbol analysis.
5.41/1.93	Overlap: (rule1: isnoc(cons(x, nil)) -> tp2(nil, x), rule2: isnoc(cons(z, z')) -> tp2(cons(z, x'), y') <= isnoc(z') = tp2(x', y'), pos: ε, mgu: {(z,x), (z',nil)})
5.41/1.93	CP: tp2(cons(x, x'), y') = tp2(nil, x) <= isnoc(nil) = tp2(x', y')
5.41/1.93	This critical pair is infeasible.
5.41/1.93	This critical pair is conditional.
5.41/1.93	This critical pair has some non-trivial conditions.
5.41/1.93	'(tp2(x', y'))' is not reachable from '(isnoc(nil))' by generalized tcap using root-symbol analysis.
5.41/1.93	
5.41/2.02	EOF