MAYBE Problem: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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,cons(Y,Z)))) -> 2ndsneg#(N,Z) active#(2ndspos(s(N),cons(X,cons(Y,Z)))) -> posrecip#(Y) active#(2ndspos(s(N),cons(X,cons(Y,Z)))) -> rcons#(posrecip(Y),2ndsneg(N,Z)) active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) -> 2ndspos#(N,Z) active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) -> negrecip#(Y) active#(2ndsneg(s(N),cons(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#(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) 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#(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) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) EDG 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,cons(Y,Z)))) -> 2ndsneg#(N,Z) active#(2ndspos(s(N),cons(X,cons(Y,Z)))) -> posrecip#(Y) active#(2ndspos(s(N),cons(X,cons(Y,Z)))) -> rcons#(posrecip(Y),2ndsneg(N,Z)) active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) -> 2ndspos#(N,Z) active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) -> negrecip#(Y) active#(2ndsneg(s(N),cons(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#(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) 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#(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) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: 15 #rules: 66 #arcs: 1628/12769 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: proper#(square(X)) -> proper#(X) proper#(times(X1,X2)) -> proper#(X1) proper#(times(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X2) proper#(pi(X)) -> proper#(X) proper#(2ndsneg(X1,X2)) -> proper#(X1) proper#(2ndsneg(X1,X2)) -> proper#(X2) proper#(2ndspos(X1,X2)) -> proper#(X1) proper#(2ndspos(X1,X2)) -> proper#(X2) proper#(from(X)) -> proper#(X) proper#(rcons(X1,X2)) -> proper#(X1) proper#(rcons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(negrecip(X)) -> proper#(X) proper#(posrecip(X)) -> proper#(X) proper#(s(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0, [proper](x0) = x0, [square](x0) = x0 + 1, [times](x0, x1) = x0 + x1 + 1, [plus](x0, x1) = x0 + x1 + 1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x0 + x1 + 1, [2ndsneg](x0, x1) = x0 + x1 + 1, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0 + x1 + 1, [0] = 1, [mark](x0) = 0, [cons](x0, x1) = x0 + x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 + 1 orientation: proper#(square(X)) = X + 2 >= X + 1 = proper#(X) proper#(times(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(times(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(plus(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(plus(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(pi(X)) = X + 2 >= X + 1 = proper#(X) proper#(2ndsneg(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(2ndsneg(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(2ndspos(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(2ndspos(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(from(X)) = X + 2 >= X + 1 = proper#(X) proper#(rcons(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(rcons(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(cons(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = proper#(X1) proper#(cons(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = proper#(X2) proper#(negrecip(X)) = X + 1 >= X + 1 = proper#(X) proper#(posrecip(X)) = X + 1 >= X + 1 = proper#(X) proper#(s(X)) = X + 1 >= X + 1 = proper#(X) active(from(X)) = X + 1 >= 0 = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = Z + 2 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N + X + Y + Z + 1 >= 0 = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = Z + 2 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N + X + Y + Z + 1 >= 0 = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= 0 = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y + 2 >= 0 = mark(Y) active(plus(s(X),Y)) = X + Y + 1 >= 0 = mark(s(plus(X,Y))) active(times(0(),Y)) = Y + 2 >= 0 = mark(0()) active(times(s(X),Y)) = X + Y + 1 >= 0 = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= 0 = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(active(X1),X2) active(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(X1,active(X2)) active(from(X)) = X + 1 >= X + 1 = from(active(X)) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(active(X1),X2) active(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(X1,active(X2)) active(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(active(X1),X2) active(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = 0 >= 0 = mark(s(X)) posrecip(mark(X)) = 0 >= 0 = mark(posrecip(X)) negrecip(mark(X)) = 0 >= 0 = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= 0 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 + 1 >= 0 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X1 + 1 >= 0 = mark(rcons(X1,X2)) from(mark(X)) = 1 >= 0 = mark(from(X)) 2ndspos(mark(X1),X2) = X2 + 1 >= 0 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 + 1 >= 0 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X2 + 1 >= 0 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 + 1 >= 0 = mark(2ndsneg(X1,X2)) pi(mark(X)) = 1 >= 0 = mark(pi(X)) plus(mark(X1),X2) = X2 + 1 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + 1 >= 0 = mark(plus(X1,X2)) times(mark(X1),X2) = X2 + 1 >= 0 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 + 1 >= 0 = mark(times(X1,X2)) square(mark(X)) = 1 >= 0 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X >= X = s(proper(X)) proper(posrecip(X)) = X >= X = posrecip(proper(X)) proper(negrecip(X)) = X >= X = negrecip(proper(X)) proper(nil()) = 0 >= 0 = ok(nil()) proper(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(proper(X1),proper(X2)) proper(rnil()) = 0 >= 0 = ok(rnil()) proper(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X >= X = ok(s(X)) posrecip(ok(X)) = X >= X = ok(posrecip(X)) negrecip(ok(X)) = X >= X = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + X2 >= X1 + X2 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(negrecip(X)) -> proper#(X) proper#(posrecip(X)) -> proper#(X) proper#(s(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = 0, [proper](x0) = x0, [square](x0) = x0 + 1, [times](x0, x1) = x1 + 1, [plus](x0, x1) = 0, [pi](x0) = 0, [negrecip](x0) = x0, [rcons](x0, x1) = x0 + 1, [2ndsneg](x0, x1) = 0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0 + x1, [0] = 1, [mark](x0) = 0, [cons](x0, x1) = x0 + x1, [s](x0) = x0, [active](x0) = x0 + 1, [from](x0) = 0 orientation: proper#(cons(X1,X2)) = X1 + X2 >= X1 = proper#(X1) proper#(cons(X1,X2)) = X1 + X2 >= X2 = proper#(X2) proper#(negrecip(X)) = X >= X = proper#(X) proper#(posrecip(X)) = X + 1 >= X = proper#(X) proper#(s(X)) = X >= X = proper#(X) active(from(X)) = 1 >= 0 = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = Z + 2 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N + X + Y + Z + 1 >= 0 = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = 1 >= 0 = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = 1 >= 0 = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = 1 >= 0 = mark(Y) active(plus(s(X),Y)) = 1 >= 0 = mark(s(plus(X,Y))) active(times(0(),Y)) = Y + 2 >= 0 = mark(0()) active(times(s(X),Y)) = Y + 2 >= 0 = mark(plus(Y,times(X,Y))) active(square(X)) = X + 2 >= 0 = mark(times(X,X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(posrecip(X)) = X + 2 >= X + 2 = posrecip(active(X)) active(negrecip(X)) = X + 1 >= X + 1 = negrecip(active(X)) active(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(active(X1),X2) active(rcons(X1,X2)) = X1 + 2 >= X1 + 2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X1 + 2 >= X1 + 1 = rcons(X1,active(X2)) active(from(X)) = 1 >= 0 = from(active(X)) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = 1 >= 0 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = 1 >= 0 = 2ndsneg(X1,active(X2)) active(pi(X)) = 1 >= 0 = pi(active(X)) active(plus(X1,X2)) = 1 >= 0 = plus(active(X1),X2) active(plus(X1,X2)) = 1 >= 0 = plus(X1,active(X2)) active(times(X1,X2)) = X2 + 2 >= X2 + 1 = times(active(X1),X2) active(times(X1,X2)) = X2 + 2 >= X2 + 2 = times(X1,active(X2)) active(square(X)) = X + 2 >= X + 2 = square(active(X)) s(mark(X)) = 0 >= 0 = mark(s(X)) posrecip(mark(X)) = 1 >= 0 = mark(posrecip(X)) negrecip(mark(X)) = 0 >= 0 = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= 0 = mark(cons(X1,X2)) rcons(mark(X1),X2) = 1 >= 0 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X1 + 1 >= 0 = mark(rcons(X1,X2)) from(mark(X)) = 0 >= 0 = mark(from(X)) 2ndspos(mark(X1),X2) = X2 >= 0 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= 0 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = 0 >= 0 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = 0 >= 0 = mark(2ndsneg(X1,X2)) pi(mark(X)) = 0 >= 0 = mark(pi(X)) plus(mark(X1),X2) = 0 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = 0 >= 0 = mark(plus(X1,X2)) times(mark(X1),X2) = X2 + 1 >= 0 = mark(times(X1,X2)) times(X1,mark(X2)) = 1 >= 0 = mark(times(X1,X2)) square(mark(X)) = 1 >= 0 = mark(square(X)) proper(0()) = 1 >= 0 = ok(0()) proper(s(X)) = X >= X = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X >= X = negrecip(proper(X)) proper(nil()) = 0 >= 0 = ok(nil()) proper(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(proper(X1),proper(X2)) proper(rnil()) = 0 >= 0 = ok(rnil()) proper(rcons(X1,X2)) = X1 + 1 >= X1 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = 0 >= 0 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + X2 >= X1 + X2 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = 0 >= 0 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = 0 >= 0 = pi(proper(X)) proper(plus(X1,X2)) = 0 >= 0 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X2 + 1 >= X2 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = 0 >= 0 = ok(s(X)) posrecip(ok(X)) = 1 >= 0 = ok(posrecip(X)) negrecip(ok(X)) = 0 >= 0 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = 0 >= 0 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = 1 >= 0 = ok(rcons(X1,X2)) from(ok(X)) = 0 >= 0 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = 0 >= 0 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = 0 >= 0 = ok(2ndsneg(X1,X2)) pi(ok(X)) = 0 >= 0 = ok(pi(X)) plus(ok(X1),ok(X2)) = 0 >= 0 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = 1 >= 0 = ok(times(X1,X2)) square(ok(X)) = 1 >= 0 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(negrecip(X)) -> proper#(X) proper#(s(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0, [proper](x0) = x0, [square](x0) = 0, [times](x0, x1) = 0, [plus](x0, x1) = 0, [pi](x0) = 0, [negrecip](x0) = x0 + 1, [rcons](x0, x1) = 0, [2ndsneg](x0, x1) = 0, [posrecip](x0) = 0, [rnil] = 0, [2ndspos](x0, x1) = 0, [0] = 0, [mark](x0) = 0, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [active](x0) = x0, [from](x0) = 0 orientation: proper#(cons(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(cons(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(negrecip(X)) = X + 2 >= X + 1 = proper#(X) proper#(s(X)) = X + 2 >= X + 1 = proper#(X) active(from(X)) = 0 >= 0 = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = 0 >= 0 = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = 0 >= 0 = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = 0 >= 0 = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = 0 >= 0 = mark(Y) active(plus(s(X),Y)) = 0 >= 0 = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = 0 >= 0 = mark(plus(Y,times(X,Y))) active(square(X)) = 0 >= 0 = mark(times(X,X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(posrecip(X)) = 0 >= 0 = posrecip(active(X)) active(negrecip(X)) = X + 1 >= X + 1 = negrecip(active(X)) active(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(active(X1),X2) active(rcons(X1,X2)) = 0 >= 0 = rcons(active(X1),X2) active(rcons(X1,X2)) = 0 >= 0 = rcons(X1,active(X2)) active(from(X)) = 0 >= 0 = from(active(X)) active(2ndspos(X1,X2)) = 0 >= 0 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = 0 >= 0 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = 0 >= 0 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = 0 >= 0 = 2ndsneg(X1,active(X2)) active(pi(X)) = 0 >= 0 = pi(active(X)) active(plus(X1,X2)) = 0 >= 0 = plus(active(X1),X2) active(plus(X1,X2)) = 0 >= 0 = plus(X1,active(X2)) active(times(X1,X2)) = 0 >= 0 = times(active(X1),X2) active(times(X1,X2)) = 0 >= 0 = times(X1,active(X2)) active(square(X)) = 0 >= 0 = square(active(X)) s(mark(X)) = 1 >= 0 = mark(s(X)) posrecip(mark(X)) = 0 >= 0 = mark(posrecip(X)) negrecip(mark(X)) = 1 >= 0 = mark(negrecip(X)) cons(mark(X1),X2) = X2 + 1 >= 0 = mark(cons(X1,X2)) rcons(mark(X1),X2) = 0 >= 0 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = 0 >= 0 = mark(rcons(X1,X2)) from(mark(X)) = 0 >= 0 = mark(from(X)) 2ndspos(mark(X1),X2) = 0 >= 0 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = 0 >= 0 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = 0 >= 0 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = 0 >= 0 = mark(2ndsneg(X1,X2)) pi(mark(X)) = 0 >= 0 = mark(pi(X)) plus(mark(X1),X2) = 0 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = 0 >= 0 = mark(plus(X1,X2)) times(mark(X1),X2) = 0 >= 0 = mark(times(X1,X2)) times(X1,mark(X2)) = 0 >= 0 = mark(times(X1,X2)) square(mark(X)) = 0 >= 0 = mark(square(X)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = 0 >= 0 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 0 >= 0 = ok(nil()) proper(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 0 >= 0 = ok(rnil()) proper(rcons(X1,X2)) = 0 >= 0 = rcons(proper(X1),proper(X2)) proper(from(X)) = 0 >= 0 = from(proper(X)) proper(2ndspos(X1,X2)) = 0 >= 0 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = 0 >= 0 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = 0 >= 0 = pi(proper(X)) proper(plus(X1,X2)) = 0 >= 0 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = 0 >= 0 = times(proper(X1),proper(X2)) proper(square(X)) = 0 >= 0 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = 0 >= 0 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = 0 >= 0 = ok(rcons(X1,X2)) from(ok(X)) = 0 >= 0 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = 0 >= 0 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = 0 >= 0 = ok(2ndsneg(X1,X2)) pi(ok(X)) = 0 >= 0 = ok(pi(X)) plus(ok(X1),ok(X2)) = 0 >= 0 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = 0 >= 0 = ok(times(X1,X2)) square(ok(X)) = 0 >= 0 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: active#(square(X)) -> active#(X) active#(times(X1,X2)) -> active#(X2) active#(times(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> active#(X1) active#(pi(X)) -> active#(X) active#(2ndsneg(X1,X2)) -> active#(X2) active#(2ndsneg(X1,X2)) -> active#(X1) active#(2ndspos(X1,X2)) -> active#(X2) active#(2ndspos(X1,X2)) -> active#(X1) active#(from(X)) -> active#(X) active#(rcons(X1,X2)) -> active#(X2) active#(rcons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> active#(X1) active#(negrecip(X)) -> active#(X) active#(posrecip(X)) -> active#(X) active#(s(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [active#](x0) = x0 + 1, [top](x0) = 0, [nil] = 1, [ok](x0) = x0, [proper](x0) = x0, [square](x0) = x0 + 1, [times](x0, x1) = x0 + x1 + 1, [plus](x0, x1) = x0 + x1 + 1, [pi](x0) = x0 + 1, [negrecip](x0) = x0 + 1, [rcons](x0, x1) = x0 + x1 + 1, [2ndsneg](x0, x1) = x0 + x1 + 1, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0 + x1 + 1, [0] = 1, [mark](x0) = 1, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [active](x0) = x0, [from](x0) = x0 + 1 orientation: active#(square(X)) = X + 2 >= X + 1 = active#(X) active#(times(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(times(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(plus(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(plus(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(pi(X)) = X + 2 >= X + 1 = active#(X) active#(2ndsneg(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(2ndsneg(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(2ndspos(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(2ndspos(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(from(X)) = X + 2 >= X + 1 = active#(X) active#(rcons(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(rcons(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(cons(X1,X2)) = X1 + 2 >= X1 + 1 = active#(X1) active#(negrecip(X)) = X + 2 >= X + 1 = active#(X) active#(posrecip(X)) = X + 2 >= X + 1 = active#(X) active#(s(X)) = X + 2 >= X + 1 = active#(X) active(from(X)) = X + 1 >= 1 = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = Z + 2 >= 1 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N + X + 3 >= 1 = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = Z + 2 >= 1 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N + X + 3 >= 1 = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= 1 = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y + 2 >= 1 = mark(Y) active(plus(s(X),Y)) = X + Y + 2 >= 1 = mark(s(plus(X,Y))) active(times(0(),Y)) = Y + 2 >= 1 = mark(0()) active(times(s(X),Y)) = X + Y + 2 >= 1 = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= 1 = mark(times(X,X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X + 1 >= X + 1 = negrecip(active(X)) active(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(active(X1),X2) active(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(active(X1),X2) active(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(X1,active(X2)) active(from(X)) = X + 1 >= X + 1 = from(active(X)) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(active(X1),X2) active(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(X1,active(X2)) active(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(active(X1),X2) active(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = 2 >= 1 = mark(s(X)) posrecip(mark(X)) = 2 >= 1 = mark(posrecip(X)) negrecip(mark(X)) = 2 >= 1 = mark(negrecip(X)) cons(mark(X1),X2) = 2 >= 1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 + 2 >= 1 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X1 + 2 >= 1 = mark(rcons(X1,X2)) from(mark(X)) = 2 >= 1 = mark(from(X)) 2ndspos(mark(X1),X2) = X2 + 2 >= 1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 + 2 >= 1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X2 + 2 >= 1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 + 2 >= 1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = 2 >= 1 = mark(pi(X)) plus(mark(X1),X2) = X2 + 2 >= 1 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + 2 >= 1 = mark(plus(X1,X2)) times(mark(X1),X2) = X2 + 2 >= 1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 + 2 >= 1 = mark(times(X1,X2)) square(mark(X)) = 2 >= 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 0 >= 0 = ok(rnil()) proper(rcons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) -> mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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#(ok(X)) -> s#(X) s#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [s#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: s#(ok(X)) = X + 2 >= X + 1 = s#(X) s#(mark(X)) = X + 1 >= X + 1 = s#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: s#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: posrecip#(ok(X)) -> posrecip#(X) posrecip#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [posrecip#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: posrecip#(ok(X)) = X + 2 >= X + 1 = posrecip#(X) posrecip#(mark(X)) = X + 1 >= X + 1 = posrecip#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: posrecip#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: negrecip#(ok(X)) -> negrecip#(X) negrecip#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [negrecip#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: negrecip#(ok(X)) = X + 2 >= X + 1 = negrecip#(X) negrecip#(mark(X)) = X + 1 >= X + 1 = negrecip#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: negrecip#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: cons#(ok(X1),ok(X2)) -> cons#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [cons#](x0, x1) = x1 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x1, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = 0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0 + 1, [from](x0) = x0 orientation: cons#(ok(X1),ok(X2)) = X2 + 2 >= X2 + 1 = cons#(X1,X2) cons#(mark(X1),X2) = X2 + 1 >= X2 + 1 = cons#(X1,X2) active(from(X)) = X + 1 >= 0 = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N + 1 >= 0 = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = Z + 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = Z + 1 >= 0 = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= 0 = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y + 1 >= 0 = mark(Y) active(plus(s(X),Y)) = Y + 1 >= 0 = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 0 = mark(0()) active(times(s(X),Y)) = X + 1 >= 0 = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= 0 = mark(times(X,X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X + 1 >= X + 1 = negrecip(active(X)) active(cons(X1,X2)) = X2 + 1 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 + 1 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(X1,active(X2)) active(from(X)) = X + 1 >= X + 1 = from(active(X)) active(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 + 1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X2 + 1 >= X2 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X2 + 1 >= X2 + 1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 + 1 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(X1,active(X2)) active(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(active(X1),X2) active(times(X1,X2)) = X1 + 1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = 0 >= 0 = mark(s(X)) posrecip(mark(X)) = 0 >= 0 = mark(posrecip(X)) negrecip(mark(X)) = 0 >= 0 = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= 0 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= 0 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = 0 >= 0 = mark(rcons(X1,X2)) from(mark(X)) = 0 >= 0 = mark(from(X)) 2ndspos(mark(X1),X2) = 0 >= 0 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= 0 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X2 >= 0 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = 0 >= 0 = mark(2ndsneg(X1,X2)) pi(mark(X)) = 0 >= 0 = mark(pi(X)) plus(mark(X1),X2) = X2 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = 0 >= 0 = mark(plus(X1,X2)) times(mark(X1),X2) = 0 >= 0 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= 0 = mark(times(X1,X2)) square(mark(X)) = 0 >= 0 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = 1 >= 1 = s(proper(X)) proper(posrecip(X)) = 1 >= 1 = posrecip(proper(X)) proper(negrecip(X)) = 1 >= 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = 1 >= 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = 1 >= 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = 1 >= 1 = from(proper(X)) proper(2ndspos(X1,X2)) = 1 >= 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = 1 >= 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = 1 >= 1 = pi(proper(X)) proper(plus(X1,X2)) = 1 >= 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = 1 >= 1 = times(proper(X1),proper(X2)) proper(square(X)) = 1 >= 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: rcons#(ok(X1),ok(X2)) -> rcons#(X1,X2) rcons#(X1,mark(X2)) -> rcons#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [rcons#](x0, x1) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0 + 1, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = x0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: rcons#(ok(X1),ok(X2)) = X1 + 1 >= X1 = rcons#(X1,X2) rcons#(X1,mark(X2)) = X1 >= X1 = rcons#(X1,X2) rcons#(mark(X1),X2) = X1 >= X1 = rcons#(X1,X2) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X >= X = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X + 1 >= X + 1 = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= X2 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X >= X = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X + 1 >= X + 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 2 >= X + 2 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 2 >= X + 2 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 2 >= X + 2 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 2 >= X + 2 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: rcons#(X1,mark(X2)) -> rcons#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: from#(ok(X)) -> from#(X) from#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [from#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: from#(ok(X)) = X + 2 >= X + 1 = from#(X) from#(mark(X)) = X + 1 >= X + 1 = from#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: from#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: 2ndspos#(ok(X1),ok(X2)) -> 2ndspos#(X1,X2) 2ndspos#(X1,mark(X2)) -> 2ndspos#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [2ndspos#](x0, x1) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0 + 1, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = x0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: 2ndspos#(ok(X1),ok(X2)) = X1 + 1 >= X1 = 2ndspos#(X1,X2) 2ndspos#(X1,mark(X2)) = X1 >= X1 = 2ndspos#(X1,X2) 2ndspos#(mark(X1),X2) = X1 >= X1 = 2ndspos#(X1,X2) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X >= X = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X + 1 >= X + 1 = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= X2 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X >= X = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X + 1 >= X + 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 2 >= X + 2 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 2 >= X + 2 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 2 >= X + 2 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 2 >= X + 2 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: 2ndspos#(X1,mark(X2)) -> 2ndspos#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: 2ndsneg#(ok(X1),ok(X2)) -> 2ndsneg#(X1,X2) 2ndsneg#(X1,mark(X2)) -> 2ndsneg#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [2ndsneg#](x0, x1) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0 + 1, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = x0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: 2ndsneg#(ok(X1),ok(X2)) = X1 + 1 >= X1 = 2ndsneg#(X1,X2) 2ndsneg#(X1,mark(X2)) = X1 >= X1 = 2ndsneg#(X1,X2) 2ndsneg#(mark(X1),X2) = X1 >= X1 = 2ndsneg#(X1,X2) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X >= X = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X + 1 >= X + 1 = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= X2 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X >= X = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X + 1 >= X + 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 2 >= X + 2 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 2 >= X + 2 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 2 >= X + 2 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 2 >= X + 2 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: 2ndsneg#(X1,mark(X2)) -> 2ndsneg#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: pi#(ok(X)) -> pi#(X) pi#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [pi#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: pi#(ok(X)) = X + 2 >= X + 1 = pi#(X) pi#(mark(X)) = X + 1 >= X + 1 = pi#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: pi#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: plus#(ok(X1),ok(X2)) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [plus#](x0, x1) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0 + 1, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = x0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: plus#(ok(X1),ok(X2)) = X1 + 1 >= X1 = plus#(X1,X2) plus#(X1,mark(X2)) = X1 >= X1 = plus#(X1,X2) plus#(mark(X1),X2) = X1 >= X1 = plus#(X1,X2) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X >= X = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X + 1 >= X + 1 = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= X2 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X >= X = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X + 1 >= X + 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 2 >= X + 2 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 2 >= X + 2 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 2 >= X + 2 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 2 >= X + 2 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: plus#(X1,mark(X2)) -> plus#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: times#(ok(X1),ok(X2)) -> times#(X1,X2) times#(X1,mark(X2)) -> times#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [times#](x0, x1) = x0, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0 + 1, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0 + 1, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 0, [mark](x0) = x0, [cons](x0, x1) = x1, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: times#(ok(X1),ok(X2)) = X1 + 1 >= X1 = times#(X1,X2) times#(X1,mark(X2)) = X1 >= X1 = times#(X1,X2) times#(mark(X1),X2) = X1 >= X1 = times#(X1,X2) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 0 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 0 >= 0 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X + 1 >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X + 1 >= X + 1 = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X >= X = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X + 1 >= X + 1 = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X + 1 >= X + 1 = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X2 >= X2 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X >= X = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X + 1 >= X + 1 = mark(square(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 2 >= X + 2 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 1 >= X + 1 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 2 >= X + 2 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 2 >= X + 2 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 1 >= X + 1 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 2 >= X + 2 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: times#(X1,mark(X2)) -> times#(X1,X2) 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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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: square#(ok(X)) -> square#(X) square#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [square#](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [square](x0) = x0, [times](x0, x1) = x0, [plus](x0, x1) = x1, [pi](x0) = x0 + 1, [negrecip](x0) = x0, [rcons](x0, x1) = x1, [2ndsneg](x0, x1) = x0, [posrecip](x0) = x0, [rnil] = 0, [2ndspos](x0, x1) = x0, [0] = 1, [mark](x0) = x0, [cons](x0, x1) = x0, [s](x0) = x0, [active](x0) = x0, [from](x0) = x0 orientation: square#(ok(X)) = X + 2 >= X + 1 = square#(X) square#(mark(X)) = X + 1 >= X + 1 = square#(X) active(from(X)) = X >= X = mark(cons(X,from(s(X)))) active(2ndspos(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndspos(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) = 1 >= 0 = mark(rnil()) active(2ndsneg(s(N),cons(X,cons(Y,Z)))) = N >= N = mark(rcons(negrecip(Y),2ndspos(N,Z))) active(pi(X)) = X + 1 >= X = mark(2ndspos(X,from(0()))) active(plus(0(),Y)) = Y >= Y = mark(Y) active(plus(s(X),Y)) = Y >= Y = mark(s(plus(X,Y))) active(times(0(),Y)) = 1 >= 1 = mark(0()) active(times(s(X),Y)) = X >= X = mark(plus(Y,times(X,Y))) active(square(X)) = X >= X = mark(times(X,X)) active(s(X)) = X >= X = s(active(X)) active(posrecip(X)) = X >= X = posrecip(active(X)) active(negrecip(X)) = X >= X = negrecip(active(X)) active(cons(X1,X2)) = X1 >= X1 = cons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(active(X1),X2) active(rcons(X1,X2)) = X2 >= X2 = rcons(X1,active(X2)) active(from(X)) = X >= X = from(active(X)) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(active(X1),X2) active(2ndspos(X1,X2)) = X1 >= X1 = 2ndspos(X1,active(X2)) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(active(X1),X2) active(2ndsneg(X1,X2)) = X1 >= X1 = 2ndsneg(X1,active(X2)) active(pi(X)) = X + 1 >= X + 1 = pi(active(X)) active(plus(X1,X2)) = X2 >= X2 = plus(active(X1),X2) active(plus(X1,X2)) = X2 >= X2 = plus(X1,active(X2)) active(times(X1,X2)) = X1 >= X1 = times(active(X1),X2) active(times(X1,X2)) = X1 >= X1 = times(X1,active(X2)) active(square(X)) = X >= X = square(active(X)) s(mark(X)) = X >= X = mark(s(X)) posrecip(mark(X)) = X >= X = mark(posrecip(X)) negrecip(mark(X)) = X >= X = mark(negrecip(X)) cons(mark(X1),X2) = X1 >= X1 = mark(cons(X1,X2)) rcons(mark(X1),X2) = X2 >= X2 = mark(rcons(X1,X2)) rcons(X1,mark(X2)) = X2 >= X2 = mark(rcons(X1,X2)) from(mark(X)) = X >= X = mark(from(X)) 2ndspos(mark(X1),X2) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndspos(X1,mark(X2)) = X1 >= X1 = mark(2ndspos(X1,X2)) 2ndsneg(mark(X1),X2) = X1 >= X1 = mark(2ndsneg(X1,X2)) 2ndsneg(X1,mark(X2)) = X1 >= X1 = mark(2ndsneg(X1,X2)) pi(mark(X)) = X + 1 >= X + 1 = mark(pi(X)) plus(mark(X1),X2) = X2 >= X2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X2 >= X2 = mark(plus(X1,X2)) times(mark(X1),X2) = X1 >= X1 = mark(times(X1,X2)) times(X1,mark(X2)) = X1 >= X1 = mark(times(X1,X2)) square(mark(X)) = X >= X = mark(square(X)) proper(0()) = 2 >= 2 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(posrecip(X)) = X + 1 >= X + 1 = posrecip(proper(X)) proper(negrecip(X)) = X + 1 >= X + 1 = negrecip(proper(X)) proper(nil()) = 1 >= 1 = ok(nil()) proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2)) proper(rnil()) = 1 >= 1 = ok(rnil()) proper(rcons(X1,X2)) = X2 + 1 >= X2 + 1 = rcons(proper(X1),proper(X2)) proper(from(X)) = X + 1 >= X + 1 = from(proper(X)) proper(2ndspos(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndspos(proper(X1),proper(X2)) proper(2ndsneg(X1,X2)) = X1 + 1 >= X1 + 1 = 2ndsneg(proper(X1),proper(X2)) proper(pi(X)) = X + 2 >= X + 2 = pi(proper(X)) proper(plus(X1,X2)) = X2 + 1 >= X2 + 1 = plus(proper(X1),proper(X2)) proper(times(X1,X2)) = X1 + 1 >= X1 + 1 = times(proper(X1),proper(X2)) proper(square(X)) = X + 1 >= X + 1 = square(proper(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) posrecip(ok(X)) = X + 1 >= X + 1 = ok(posrecip(X)) negrecip(ok(X)) = X + 1 >= X + 1 = ok(negrecip(X)) cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2)) rcons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(rcons(X1,X2)) from(ok(X)) = X + 1 >= X + 1 = ok(from(X)) 2ndspos(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndspos(X1,X2)) 2ndsneg(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(2ndsneg(X1,X2)) pi(ok(X)) = X + 2 >= X + 2 = ok(pi(X)) plus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(plus(X1,X2)) times(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(times(X1,X2)) square(ok(X)) = X + 1 >= X + 1 = ok(square(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: square#(mark(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,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z))) active(2ndsneg(0(),Z)) -> mark(rnil()) active(2ndsneg(s(N),cons(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(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)) 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(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)) 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