YES Proof: This system is quasi-decreasing. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: isnoc(cons(y, nil)) -> tp2(nil, y) isnoc(cons(x, ys)) -> tp2(cons(x, isnoc(ys)), isnoc(ys)) isnoc(cons(x, ys)) -> isnoc(ys) tp2(x, y) -> x tp2(x, y) -> y cons(x, y) -> x cons(x, y) -> y isnoc(x) -> x DP Processor: DPs: isnoc#(cons(y,nil())) -> tp2#(nil(),y) isnoc#(cons(x,ys)) -> isnoc#(ys) isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys)) isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys)) TRS: isnoc(cons(y,nil())) -> tp2(nil(),y) isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys)) isnoc(cons(x,ys)) -> isnoc(ys) tp2(x,y) -> x tp2(x,y) -> y cons(x,y) -> x cons(x,y) -> y isnoc(x) -> x TDG Processor: DPs: isnoc#(cons(y,nil())) -> tp2#(nil(),y) isnoc#(cons(x,ys)) -> isnoc#(ys) isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys)) isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys)) TRS: isnoc(cons(y,nil())) -> tp2(nil(),y) isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys)) isnoc(cons(x,ys)) -> isnoc(ys) tp2(x,y) -> x tp2(x,y) -> y cons(x,y) -> x cons(x,y) -> y isnoc(x) -> x graph: isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(x,ys)) -> tp2#(cons(x,isnoc(ys)),isnoc(ys)) isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(x,ys)) -> cons#(x,isnoc(ys)) isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(x,ys)) -> isnoc#(ys) isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(y,nil())) -> tp2#(nil(),y) SCC Processor: #sccs: 1 #rules: 1 #arcs: 4/16 DPs: isnoc#(cons(x,ys)) -> isnoc#(ys) TRS: isnoc(cons(y,nil())) -> tp2(nil(),y) isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys)) isnoc(cons(x,ys)) -> isnoc(ys) tp2(x,y) -> x tp2(x,y) -> y cons(x,y) -> x cons(x,y) -> y isnoc(x) -> x Subterm Criterion Processor: simple projection: pi(isnoc#) = 0 problem: DPs: TRS: isnoc(cons(y,nil())) -> tp2(nil(),y) isnoc(cons(x,ys)) -> tp2(cons(x,isnoc(ys)),isnoc(ys)) isnoc(cons(x,ys)) -> isnoc(ys) tp2(x,y) -> x tp2(x,y) -> y cons(x,y) -> x cons(x,y) -> y isnoc(x) -> x Qed