5.23/2.25	YES
5.23/2.25	
5.23/2.25	Proof:
5.23/2.26	This system is confluent.
5.23/2.26	By \cite{ALS94}, Theorem 4.1.
5.23/2.26	This system is of type 3 or smaller.
5.23/2.26	This system is strongly deterministic.
5.23/2.26	This system is quasi-decreasing.
5.23/2.26	By \cite{A14}, Theorem 11.5.9.
5.23/2.26	This system is of type 3 or smaller.
5.23/2.26	This system is deterministic.
5.23/2.26	System R transformed to V(R) + Emb.
5.23/2.26	This system is terminating.
5.23/2.26	Call external tool:
5.23/2.26	./ttt2.sh
5.23/2.26	Input:
5.23/2.26	(VAR y x ys)
5.23/2.26	(RULES
5.23/2.26	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.23/2.26	  isnoc(cons(x, ys)) -> tp2(cons(x, isnoc(ys)), isnoc(ys))
5.23/2.26	  isnoc(cons(x, ys)) -> isnoc(ys)
5.23/2.26	  tp2(x, y) -> x
5.23/2.26	  tp2(x, y) -> y
5.23/2.26	  cons(x, y) -> x
5.23/2.26	  cons(x, y) -> y
5.23/2.26	  isnoc(x) -> x
5.23/2.26	)
5.23/2.26	
5.23/2.26	 DP Processor:
5.23/2.26	  DPs:
5.23/2.26	   isnoc#(cons(y,nil())) -> tp2#(nil(),y)
5.23/2.26	   isnoc#(cons(x,ys)) -> isnoc#(ys)
5.23/2.26	   isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys))
5.23/2.26	   isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	  TRS:
5.23/2.26	   isnoc(cons(y,nil())) -> tp2(nil(),y)
5.23/2.26	   isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	   isnoc(cons(x,ys)) -> isnoc(ys)
5.23/2.26	   tp2(x,y) -> x
5.23/2.26	   tp2(x,y) -> y
5.23/2.26	   cons(x,y) -> x
5.23/2.26	   cons(x,y) -> y
5.23/2.26	   isnoc(x) -> x
5.23/2.26	  TDG Processor:
5.23/2.26	   DPs:
5.23/2.26	    isnoc#(cons(y,nil())) -> tp2#(nil(),y)
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys)
5.23/2.26	    isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys))
5.23/2.26	    isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	   TRS:
5.23/2.26	    isnoc(cons(y,nil())) -> tp2(nil(),y)
5.23/2.26	    isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	    isnoc(cons(x,ys)) -> isnoc(ys)
5.23/2.26	    tp2(x,y) -> x
5.23/2.26	    tp2(x,y) -> y
5.23/2.26	    cons(x,y) -> x
5.23/2.26	    cons(x,y) -> y
5.23/2.26	    isnoc(x) -> x
5.23/2.26	   graph:
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys) ->
5.23/2.26	    isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys) ->
5.23/2.26	    isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys))
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys) ->
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys)
5.23/2.26	    isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(y,nil())) -> tp2#(nil(),y)
5.23/2.26	   SCC Processor:
5.23/2.26	    #sccs: 1
5.23/2.26	    #rules: 1
5.23/2.26	    #arcs: 4/16
5.23/2.26	    DPs:
5.23/2.26	     isnoc#(cons(x,ys)) -> isnoc#(ys)
5.23/2.26	    TRS:
5.23/2.26	     isnoc(cons(y,nil())) -> tp2(nil(),y)
5.23/2.26	     isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	     isnoc(cons(x,ys)) -> isnoc(ys)
5.23/2.26	     tp2(x,y) -> x
5.23/2.26	     tp2(x,y) -> y
5.23/2.26	     cons(x,y) -> x
5.23/2.26	     cons(x,y) -> y
5.23/2.26	     isnoc(x) -> x
5.23/2.26	    Subterm Criterion Processor:
5.23/2.26	     simple projection:
5.23/2.26	      pi(isnoc#) = 0
5.23/2.26	     problem:
5.23/2.26	      DPs:
5.23/2.26	       
5.23/2.26	      TRS:
5.23/2.26	       isnoc(cons(y,nil())) -> tp2(nil(),y)
5.23/2.26	       isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys))
5.23/2.26	       isnoc(cons(x,ys)) -> isnoc(ys)
5.23/2.26	       tp2(x,y) -> x
5.23/2.26	       tp2(x,y) -> y
5.23/2.26	       cons(x,y) -> x
5.23/2.26	       cons(x,y) -> y
5.23/2.26	       isnoc(x) -> x
5.23/2.26	     Qed
5.23/2.26	All 2 critical pairs are joinable.
5.23/2.26	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.23/2.26	CP: tp2(nil, x) = tp2(cons(x, x'), y') <= isnoc(nil) = tp2(x', y')
5.23/2.26	This critical pair is infeasible.
5.23/2.26	This critical pair is conditional.
5.23/2.26	This critical pair has some non-trivial conditions.
5.23/2.26	Call external tool:
5.23/2.26	./waldmeister
5.23/2.26	Input:
5.23/2.26	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.23/2.26	  isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
5.23/2.26	
5.23/2.26	By Waldmeister.
5.23/2.26	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.23/2.26	CP: tp2(cons(z, x'), y') = tp2(nil, z) <= isnoc(nil) = tp2(x', y')
5.23/2.26	This critical pair is infeasible.
5.23/2.26	This critical pair is conditional.
5.23/2.26	This critical pair has some non-trivial conditions.
5.23/2.26	Call external tool:
5.23/2.26	./waldmeister
5.23/2.26	Input:
5.23/2.26	  isnoc(cons(y, nil)) -> tp2(nil, y)
5.23/2.26	  isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
5.23/2.26	
5.23/2.26	By Waldmeister.
5.23/2.26	
5.59/2.32	EOF