YES Input TRS: 1: isnoc(cons(y,nil())) -> tp2(nil(),y) 2: isnoc(cons(x,ys)) -> tp2(cons(x,xs),y) | isnoc(ys) --> tp2(xs,y) Infeasibility test: isnoc(nil()) --> tp2(x3,x4) Symbol transition graph: isnoc --> tp2 Collapsable symbols: { }