MAYBE Problem: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(2ndspos(s(N),cons(X,Z))) -> cons2#(X,Z) active#(2ndspos(s(N),cons(X,Z))) -> 2ndspos#(s(N),cons2(X,Z)) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> 2ndsneg#(N,Z) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> posrecip#(Y) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> rcons#(posrecip(Y),2ndsneg(N,Z)) active#(2ndsneg(s(N),cons(X,Z))) -> cons2#(X,Z) active#(2ndsneg(s(N),cons(X,Z))) -> 2ndsneg#(s(N),cons2(X,Z)) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> 2ndspos#(N,Z) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> negrecip#(Y) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> rcons#(negrecip(Y),2ndspos(N,Z)) active#(pi(X)) -> from#(0()) active#(pi(X)) -> 2ndspos#(X,from(0())) active#(plus(s(X),Y)) -> plus#(X,Y) active#(plus(s(X),Y)) -> s#(plus(X,Y)) active#(times(s(X),Y)) -> times#(X,Y) active#(times(s(X),Y)) -> plus#(Y,times(X,Y)) active#(square(X)) -> times#(X,X) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(posrecip(X)) -> active#(X) active#(posrecip(X)) -> posrecip#(active(X)) active#(negrecip(X)) -> active#(X) active#(negrecip(X)) -> negrecip#(active(X)) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(cons2(X1,X2)) -> active#(X2) active#(cons2(X1,X2)) -> cons2#(X1,active(X2)) active#(rcons(X1,X2)) -> active#(X1) active#(rcons(X1,X2)) -> rcons#(active(X1),X2) active#(rcons(X1,X2)) -> active#(X2) active#(rcons(X1,X2)) -> rcons#(X1,active(X2)) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(2ndspos(X1,X2)) -> active#(X1) active#(2ndspos(X1,X2)) -> 2ndspos#(active(X1),X2) active#(2ndspos(X1,X2)) -> active#(X2) active#(2ndspos(X1,X2)) -> 2ndspos#(X1,active(X2)) active#(2ndsneg(X1,X2)) -> active#(X1) active#(2ndsneg(X1,X2)) -> 2ndsneg#(active(X1),X2) active#(2ndsneg(X1,X2)) -> active#(X2) active#(2ndsneg(X1,X2)) -> 2ndsneg#(X1,active(X2)) active#(pi(X)) -> active#(X) active#(pi(X)) -> pi#(active(X)) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(times(X1,X2)) -> active#(X1) active#(times(X1,X2)) -> times#(active(X1),X2) active#(times(X1,X2)) -> active#(X2) active#(times(X1,X2)) -> times#(X1,active(X2)) active#(square(X)) -> active#(X) active#(square(X)) -> square#(active(X)) s#(mark(X)) -> s#(X) posrecip#(mark(X)) -> posrecip#(X) negrecip#(mark(X)) -> negrecip#(X) cons#(mark(X1),X2) -> cons#(X1,X2) cons2#(X1,mark(X2)) -> cons2#(X1,X2) rcons#(mark(X1),X2) -> rcons#(X1,X2) rcons#(X1,mark(X2)) -> rcons#(X1,X2) from#(mark(X)) -> from#(X) 2ndspos#(mark(X1),X2) -> 2ndspos#(X1,X2) 2ndspos#(X1,mark(X2)) -> 2ndspos#(X1,X2) 2ndsneg#(mark(X1),X2) -> 2ndsneg#(X1,X2) 2ndsneg#(X1,mark(X2)) -> 2ndsneg#(X1,X2) pi#(mark(X)) -> pi#(X) plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) times#(mark(X1),X2) -> times#(X1,X2) times#(X1,mark(X2)) -> times#(X1,X2) square#(mark(X)) -> square#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(posrecip(X)) -> proper#(X) proper#(posrecip(X)) -> posrecip#(proper(X)) proper#(negrecip(X)) -> proper#(X) proper#(negrecip(X)) -> negrecip#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons2(X1,X2)) -> proper#(X2) proper#(cons2(X1,X2)) -> proper#(X1) proper#(cons2(X1,X2)) -> cons2#(proper(X1),proper(X2)) proper#(rcons(X1,X2)) -> proper#(X2) proper#(rcons(X1,X2)) -> proper#(X1) proper#(rcons(X1,X2)) -> rcons#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(2ndspos(X1,X2)) -> proper#(X2) proper#(2ndspos(X1,X2)) -> proper#(X1) proper#(2ndspos(X1,X2)) -> 2ndspos#(proper(X1),proper(X2)) proper#(2ndsneg(X1,X2)) -> proper#(X2) proper#(2ndsneg(X1,X2)) -> proper#(X1) proper#(2ndsneg(X1,X2)) -> 2ndsneg#(proper(X1),proper(X2)) proper#(pi(X)) -> proper#(X) proper#(pi(X)) -> pi#(proper(X)) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(times(X1,X2)) -> proper#(X2) proper#(times(X1,X2)) -> proper#(X1) proper#(times(X1,X2)) -> times#(proper(X1),proper(X2)) proper#(square(X)) -> proper#(X) proper#(square(X)) -> square#(proper(X)) s#(ok(X)) -> s#(X) posrecip#(ok(X)) -> posrecip#(X) negrecip#(ok(X)) -> negrecip#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) cons2#(ok(X1),ok(X2)) -> cons2#(X1,X2) rcons#(ok(X1),ok(X2)) -> rcons#(X1,X2) from#(ok(X)) -> from#(X) 2ndspos#(ok(X1),ok(X2)) -> 2ndspos#(X1,X2) 2ndsneg#(ok(X1),ok(X2)) -> 2ndsneg#(X1,X2) pi#(ok(X)) -> pi#(X) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) times#(ok(X1),ok(X2)) -> times#(X1,X2) square#(ok(X)) -> square#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(2ndspos(s(N),cons(X,Z))) -> cons2#(X,Z) active#(2ndspos(s(N),cons(X,Z))) -> 2ndspos#(s(N),cons2(X,Z)) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> 2ndsneg#(N,Z) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> posrecip#(Y) active#(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> rcons#(posrecip(Y),2ndsneg(N,Z)) active#(2ndsneg(s(N),cons(X,Z))) -> cons2#(X,Z) active#(2ndsneg(s(N),cons(X,Z))) -> 2ndsneg#(s(N),cons2(X,Z)) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> 2ndspos#(N,Z) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> negrecip#(Y) active#(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> rcons#(negrecip(Y),2ndspos(N,Z)) active#(pi(X)) -> from#(0()) active#(pi(X)) -> 2ndspos#(X,from(0())) active#(plus(s(X),Y)) -> plus#(X,Y) active#(plus(s(X),Y)) -> s#(plus(X,Y)) active#(times(s(X),Y)) -> times#(X,Y) active#(times(s(X),Y)) -> plus#(Y,times(X,Y)) active#(square(X)) -> times#(X,X) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(posrecip(X)) -> active#(X) active#(posrecip(X)) -> posrecip#(active(X)) active#(negrecip(X)) -> active#(X) active#(negrecip(X)) -> negrecip#(active(X)) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(cons2(X1,X2)) -> active#(X2) active#(cons2(X1,X2)) -> cons2#(X1,active(X2)) active#(rcons(X1,X2)) -> active#(X1) active#(rcons(X1,X2)) -> rcons#(active(X1),X2) active#(rcons(X1,X2)) -> active#(X2) active#(rcons(X1,X2)) -> rcons#(X1,active(X2)) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(2ndspos(X1,X2)) -> active#(X1) active#(2ndspos(X1,X2)) -> 2ndspos#(active(X1),X2) active#(2ndspos(X1,X2)) -> active#(X2) active#(2ndspos(X1,X2)) -> 2ndspos#(X1,active(X2)) active#(2ndsneg(X1,X2)) -> active#(X1) active#(2ndsneg(X1,X2)) -> 2ndsneg#(active(X1),X2) active#(2ndsneg(X1,X2)) -> active#(X2) active#(2ndsneg(X1,X2)) -> 2ndsneg#(X1,active(X2)) active#(pi(X)) -> active#(X) active#(pi(X)) -> pi#(active(X)) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(times(X1,X2)) -> active#(X1) active#(times(X1,X2)) -> times#(active(X1),X2) active#(times(X1,X2)) -> active#(X2) active#(times(X1,X2)) -> times#(X1,active(X2)) active#(square(X)) -> active#(X) active#(square(X)) -> square#(active(X)) s#(mark(X)) -> s#(X) posrecip#(mark(X)) -> posrecip#(X) negrecip#(mark(X)) -> negrecip#(X) cons#(mark(X1),X2) -> cons#(X1,X2) cons2#(X1,mark(X2)) -> cons2#(X1,X2) rcons#(mark(X1),X2) -> rcons#(X1,X2) rcons#(X1,mark(X2)) -> rcons#(X1,X2) from#(mark(X)) -> from#(X) 2ndspos#(mark(X1),X2) -> 2ndspos#(X1,X2) 2ndspos#(X1,mark(X2)) -> 2ndspos#(X1,X2) 2ndsneg#(mark(X1),X2) -> 2ndsneg#(X1,X2) 2ndsneg#(X1,mark(X2)) -> 2ndsneg#(X1,X2) pi#(mark(X)) -> pi#(X) plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) times#(mark(X1),X2) -> times#(X1,X2) times#(X1,mark(X2)) -> times#(X1,X2) square#(mark(X)) -> square#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(posrecip(X)) -> proper#(X) proper#(posrecip(X)) -> posrecip#(proper(X)) proper#(negrecip(X)) -> proper#(X) proper#(negrecip(X)) -> negrecip#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons2(X1,X2)) -> proper#(X2) proper#(cons2(X1,X2)) -> proper#(X1) proper#(cons2(X1,X2)) -> cons2#(proper(X1),proper(X2)) proper#(rcons(X1,X2)) -> proper#(X2) proper#(rcons(X1,X2)) -> proper#(X1) proper#(rcons(X1,X2)) -> rcons#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(2ndspos(X1,X2)) -> proper#(X2) proper#(2ndspos(X1,X2)) -> proper#(X1) proper#(2ndspos(X1,X2)) -> 2ndspos#(proper(X1),proper(X2)) proper#(2ndsneg(X1,X2)) -> proper#(X2) proper#(2ndsneg(X1,X2)) -> proper#(X1) proper#(2ndsneg(X1,X2)) -> 2ndsneg#(proper(X1),proper(X2)) proper#(pi(X)) -> proper#(X) proper#(pi(X)) -> pi#(proper(X)) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(times(X1,X2)) -> proper#(X2) proper#(times(X1,X2)) -> proper#(X1) proper#(times(X1,X2)) -> times#(proper(X1),proper(X2)) proper#(square(X)) -> proper#(X) proper#(square(X)) -> square#(proper(X)) s#(ok(X)) -> s#(X) posrecip#(ok(X)) -> posrecip#(X) negrecip#(ok(X)) -> negrecip#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) cons2#(ok(X1),ok(X2)) -> cons2#(X1,X2) rcons#(ok(X1),ok(X2)) -> rcons#(X1,X2) from#(ok(X)) -> from#(X) 2ndspos#(ok(X1),ok(X2)) -> 2ndspos#(X1,X2) 2ndsneg#(ok(X1),ok(X2)) -> 2ndsneg#(X1,X2) pi#(ok(X)) -> pi#(X) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) times#(ok(X1),ok(X2)) -> times#(X1,X2) square#(ok(X)) -> square#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: ... SCC Processor: #sccs: 16 #rules: 71 #arcs: 1970/15376 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Open DPs: active#(s(X)) -> active#(X) active#(posrecip(X)) -> active#(X) active#(negrecip(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons2(X1,X2)) -> active#(X2) active#(rcons(X1,X2)) -> active#(X1) active#(rcons(X1,X2)) -> active#(X2) active#(from(X)) -> active#(X) active#(2ndspos(X1,X2)) -> active#(X1) active#(2ndspos(X1,X2)) -> active#(X2) active#(2ndsneg(X1,X2)) -> active#(X1) active#(2ndsneg(X1,X2)) -> active#(X2) active#(pi(X)) -> active#(X) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X2) active#(times(X1,X2)) -> active#(X1) active#(times(X1,X2)) -> active#(X2) active#(square(X)) -> active#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(active#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(s(X)) -> proper#(X) proper#(posrecip(X)) -> proper#(X) proper#(negrecip(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons2(X1,X2)) -> proper#(X2) proper#(cons2(X1,X2)) -> proper#(X1) proper#(rcons(X1,X2)) -> proper#(X2) proper#(rcons(X1,X2)) -> proper#(X1) proper#(from(X)) -> proper#(X) proper#(2ndspos(X1,X2)) -> proper#(X2) proper#(2ndspos(X1,X2)) -> proper#(X1) proper#(2ndsneg(X1,X2)) -> proper#(X2) proper#(2ndsneg(X1,X2)) -> proper#(X1) proper#(pi(X)) -> proper#(X) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(times(X1,X2)) -> proper#(X2) proper#(times(X1,X2)) -> proper#(X1) proper#(square(X)) -> proper#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(proper#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: square#(mark(X)) -> square#(X) square#(ok(X)) -> square#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(square#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: times#(mark(X1),X2) -> times#(X1,X2) times#(X1,mark(X2)) -> times#(X1,X2) times#(ok(X1),ok(X2)) -> times#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(times#) = 1 problem: DPs: times#(mark(X1),X2) -> times#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(times#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(plus#) = 1 problem: DPs: plus#(mark(X1),X2) -> plus#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(plus#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: pi#(mark(X)) -> pi#(X) pi#(ok(X)) -> pi#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(pi#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: 2ndsneg#(mark(X1),X2) -> 2ndsneg#(X1,X2) 2ndsneg#(X1,mark(X2)) -> 2ndsneg#(X1,X2) 2ndsneg#(ok(X1),ok(X2)) -> 2ndsneg#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(2ndsneg#) = 1 problem: DPs: 2ndsneg#(mark(X1),X2) -> 2ndsneg#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(2ndsneg#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: 2ndspos#(mark(X1),X2) -> 2ndspos#(X1,X2) 2ndspos#(X1,mark(X2)) -> 2ndspos#(X1,X2) 2ndspos#(ok(X1),ok(X2)) -> 2ndspos#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(2ndspos#) = 1 problem: DPs: 2ndspos#(mark(X1),X2) -> 2ndspos#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(2ndspos#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: from#(mark(X)) -> from#(X) from#(ok(X)) -> from#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(from#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: rcons#(mark(X1),X2) -> rcons#(X1,X2) rcons#(X1,mark(X2)) -> rcons#(X1,X2) rcons#(ok(X1),ok(X2)) -> rcons#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(rcons#) = 1 problem: DPs: rcons#(mark(X1),X2) -> rcons#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(rcons#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: cons2#(X1,mark(X2)) -> cons2#(X1,X2) cons2#(ok(X1),ok(X2)) -> cons2#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons2#) = 1 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: cons#(mark(X1),X2) -> cons#(X1,X2) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons#) = 1 problem: DPs: cons#(mark(X1),X2) -> cons#(X1,X2) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: negrecip#(mark(X)) -> negrecip#(X) negrecip#(ok(X)) -> negrecip#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(negrecip#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: posrecip#(mark(X)) -> posrecip#(X) posrecip#(ok(X)) -> posrecip#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(posrecip#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(s#) = 0 problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z))) active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z))) active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) -> mark(2ndspos(X,from(0()))) active(plus(0(),Y)) -> mark(Y) active(plus(s(X),Y)) -> mark(s(plus(X,Y))) active(times(0(),Y)) -> mark(0()) active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) active(square(X)) -> mark(times(X,X)) active(s(X)) -> s(active(X)) active(posrecip(X)) -> posrecip(active(X)) active(negrecip(X)) -> negrecip(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons2(X1,X2)) -> cons2(X1,active(X2)) active(rcons(X1,X2)) -> rcons(active(X1),X2) active(rcons(X1,X2)) -> rcons(X1,active(X2)) active(from(X)) -> from(active(X)) active(2ndspos(X1,X2)) -> 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) -> 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) -> 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) -> 2ndsneg(X1,active(X2)) active(pi(X)) -> pi(active(X)) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(times(X1,X2)) -> times(active(X1),X2) active(times(X1,X2)) -> times(X1,active(X2)) active(square(X)) -> square(active(X)) s(mark(X)) -> mark(s(X)) posrecip(mark(X)) -> mark(posrecip(X)) negrecip(mark(X)) -> mark(negrecip(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons2(X1,mark(X2)) -> mark(cons2(X1,X2)) rcons(mark(X1),X2) -> mark(rcons(X1,X2)) rcons(X1,mark(X2)) -> mark(rcons(X1,X2)) from(mark(X)) -> mark(from(X)) 2ndspos(mark(X1),X2) -> mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) -> mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) -> mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) -> mark(2ndsneg(X1,X2)) pi(mark(X)) -> mark(pi(X)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) times(mark(X1),X2) -> mark(times(X1,X2)) times(X1,mark(X2)) -> mark(times(X1,X2)) square(mark(X)) -> mark(square(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(posrecip(X)) -> posrecip(proper(X)) proper(negrecip(X)) -> negrecip(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(cons2(X1,X2)) -> cons2(proper(X1),proper(X2)) proper(rnil()) -> ok(rnil()) proper(rcons(X1,X2)) -> rcons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(2ndspos(X1,X2)) -> 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) -> 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) -> pi(proper(X)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(times(X1,X2)) -> times(proper(X1),proper(X2)) proper(square(X)) -> square(proper(X)) s(ok(X)) -> ok(s(X)) posrecip(ok(X)) -> ok(posrecip(X)) negrecip(ok(X)) -> ok(negrecip(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) cons2(ok(X1),ok(X2)) -> ok(cons2(X1,X2)) rcons(ok(X1),ok(X2)) -> ok(rcons(X1,X2)) from(ok(X)) -> ok(from(X)) 2ndspos(ok(X1),ok(X2)) -> ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) -> ok(2ndsneg(X1,X2)) pi(ok(X)) -> ok(pi(X)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) times(ok(X1),ok(X2)) -> ok(times(X1,X2)) square(ok(X)) -> ok(square(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed