5.38/2.20	YES
5.38/2.20	
5.38/2.20	Proof:
5.38/2.20	This system is confluent.
5.38/2.20	By \cite{ALS94}, Theorem 4.1.
5.38/2.20	This system is of type 3 or smaller.
5.38/2.20	This system is strongly deterministic.
5.38/2.20	This system is quasi-decreasing.
5.38/2.20	By \cite{O02}, p. 214, Proposition 7.2.50.
5.38/2.20	This system is of type 3 or smaller.
5.38/2.20	This system is deterministic.
5.38/2.20	System R transformed to optimized U(R).
5.38/2.20	This system is terminating.
5.38/2.20	Call external tool:
5.38/2.20	./ttt2.sh
5.38/2.20	Input:
5.38/2.20	(VAR y x ys xs)
5.38/2.20	(RULES
5.38/2.20	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.38/2.20	  isnoc(cons(x, ys)) -> ?1(isnoc(ys), x, ys)
5.38/2.20	  ?1(tp2(xs, y), x, ys) -> tp2(cons(x, xs), y)
5.38/2.20	)
5.38/2.20	
5.38/2.20	 Matrix Interpretation Processor: dim=3
5.38/2.20	  
5.38/2.20	  interpretation:
5.38/2.20	                      [1 0 0]     [1 0 1]     [1 1 0]     [0]
5.38/2.20	   [?1](x0, x1, x2) = [0 1 0]x0 + [1 0 1]x1 + [0 0 0]x2 + [1]
5.38/2.20	                      [0 0 0]     [0 0 0]     [0 0 0]     [0],
5.38/2.20	   
5.38/2.20	                   [1 0 0]     [1 0 1]  
5.38/2.20	   [tp2](x0, x1) = [0 1 0]x0 + [0 0 0]x1
5.38/2.20	                   [0 0 0]     [0 0 0]  ,
5.38/2.20	   
5.38/2.20	                 [1 1 1]     [0]
5.38/2.20	   [isnoc](x0) = [0 1 0]x0 + [1]
5.38/2.20	                 [0 1 0]     [0],
5.38/2.20	   
5.38/2.20	                    [1 0 1]     [1 0 0]     [0]
5.38/2.20	   [cons](x0, x1) = [1 0 1]x0 + [0 1 0]x1 + [1]
5.38/2.20	                    [0 0 1]     [1 1 1]     [0],
5.38/2.20	   
5.38/2.20	           [0]
5.38/2.20	   [nil] = [0]
5.38/2.20	           [1]
5.38/2.20	  orientation:
5.38/2.20	                          [2 0 3]    [2]    [1 0 1]                
5.38/2.21	   isnoc(cons(y,nil())) = [1 0 1]y + [2] >= [0 0 0]y = tp2(nil(),y)
5.38/2.21	                          [1 0 1]    [1]    [0 0 0]                
5.38/2.21	   
5.38/2.21	                       [2 0 3]    [2 2 1]     [1]    [1 0 1]    [2 2 1]     [0]                     
5.38/2.21	   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.38/2.23	                       [1 0 1]    [0 1 0]     [1]    [0 0 0]    [0 0 0]     [0]                     
5.38/2.23	   
5.38/2.23	                        [1 0 1]    [1 0 0]     [1 0 1]    [1 1 0]     [0]    [1 0 1]    [1 0 0]     [1 0 1]    [0]                    
5.38/2.23	   ?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.38/2.23	                        [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]     [0]    [0 0 0]    [0 0 0]     [0 0 0]    [0]                    
5.38/2.23	  problem:
5.38/2.23	   ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
5.38/2.23	  Matrix Interpretation Processor: dim=3
5.38/2.23	   
5.38/2.23	   interpretation:
5.38/2.23	                       [1 0 0]     [1 0 0]     [1 0 0]     [1]
5.38/2.23	    [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
5.38/2.23	                       [0 0 0]     [0 0 0]     [0 0 0]     [0],
5.38/2.23	    
5.38/2.23	                    [1 0 1]     [1 0 0]  
5.38/2.23	    [tp2](x0, x1) = [0 0 0]x0 + [0 0 0]x1
5.38/2.23	                    [0 0 0]     [0 0 0]  ,
5.38/2.23	    
5.38/2.23	                     [1 0 0]     [1 0 0]  
5.38/2.23	    [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
5.38/2.23	                     [0 0 0]     [0 0 1]  
5.38/2.23	   orientation:
5.38/2.23	                         [1 0 0]    [1 0 1]     [1 0 0]    [1 0 0]     [1]    [1 0 0]    [1 0 1]     [1 0 0]                     
5.38/2.23	    ?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.38/2.23	                         [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]     [0]    [0 0 0]    [0 0 0]     [0 0 0]                     
5.38/2.23	   problem:
5.38/2.23	    
5.38/2.23	   Qed
5.38/2.23	All 2 critical pairs are joinable.
5.38/2.23	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: {(z,x), (z',nil)})
5.38/2.23	CP: tp2(nil, x) = tp2(cons(x, x'), y') <= isnoc(nil) = tp2(x', y')
5.38/2.23	This critical pair is infeasible.
5.38/2.23	This critical pair is conditional.
5.38/2.23	This critical pair has some non-trivial conditions.
5.38/2.23	Call external tool:
5.38/2.23	./waldmeister
5.38/2.23	Input:
5.38/2.23	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.38/2.23	  isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
5.38/2.23	
5.38/2.23	By Waldmeister.
5.38/2.23	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: {(x,z), (z',nil)})
5.38/2.23	CP: tp2(cons(z, x'), y') = tp2(nil, z) <= isnoc(nil) = tp2(x', y')
5.38/2.23	This critical pair is infeasible.
5.38/2.23	This critical pair is conditional.
5.38/2.23	This critical pair has some non-trivial conditions.
5.38/2.23	'tcap_{R_u}(isnoc(nil))' and 'tp2(x', y')' are not unifiable.
5.38/2.23	
5.38/2.25	EOF