YES Problem: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U11(tt())) -> U12#(tt()) active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U11(X)) -> active#(X) active#(U11(X)) -> U11#(active(X)) active#(U12(X)) -> active#(X) active#(U12(X)) -> U12#(active(X)) active#(isNePal(X)) -> active#(X) active#(isNePal(X)) -> isNePal#(active(X)) __#(mark(X1),X2) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) U11#(mark(X)) -> U11#(X) U12#(mark(X)) -> U12#(X) isNePal#(mark(X)) -> isNePal#(X) proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U11(X)) -> proper#(X) proper#(U11(X)) -> U11#(proper(X)) proper#(U12(X)) -> proper#(X) proper#(U12(X)) -> U12#(proper(X)) proper#(isNePal(X)) -> proper#(X) proper#(isNePal(X)) -> isNePal#(proper(X)) __#(ok(X1),ok(X2)) -> __#(X1,X2) U11#(ok(X)) -> U11#(X) U12#(ok(X)) -> U12#(X) isNePal#(ok(X)) -> isNePal#(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(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U11(tt())) -> U12#(tt()) active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U11(X)) -> active#(X) active#(U11(X)) -> U11#(active(X)) active#(U12(X)) -> active#(X) active#(U12(X)) -> U12#(active(X)) active#(isNePal(X)) -> active#(X) active#(isNePal(X)) -> isNePal#(active(X)) __#(mark(X1),X2) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) U11#(mark(X)) -> U11#(X) U12#(mark(X)) -> U12#(X) isNePal#(mark(X)) -> isNePal#(X) proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U11(X)) -> proper#(X) proper#(U11(X)) -> U11#(proper(X)) proper#(U12(X)) -> proper#(X) proper#(U12(X)) -> U12#(proper(X)) proper#(isNePal(X)) -> proper#(X) proper#(isNePal(X)) -> isNePal#(proper(X)) __#(ok(X1),ok(X2)) -> __#(X1,X2) U11#(ok(X)) -> U11#(X) U12#(ok(X)) -> U12#(X) isNePal#(ok(X)) -> isNePal#(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(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) top#(ok(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) top#(ok(X)) -> active#(X) -> active#(U12(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) top#(ok(X)) -> active#(X) -> active#(U11(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) top#(ok(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) top#(ok(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) top#(ok(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(isNePal(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(isNePal(X)) -> isNePal#(proper(X)) -> isNePal#(ok(X)) -> isNePal#(X) proper#(isNePal(X)) -> isNePal#(proper(X)) -> isNePal#(mark(X)) -> isNePal#(X) proper#(U12(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(U12(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(U12(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(U12(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(U12(X)) -> U12#(proper(X)) -> U12#(ok(X)) -> U12#(X) proper#(U12(X)) -> U12#(proper(X)) -> U12#(mark(X)) -> U12#(X) proper#(U11(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(U11(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(U11(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(U11(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(U11(X)) -> U11#(proper(X)) -> U11#(ok(X)) -> U11#(X) proper#(U11(X)) -> U11#(proper(X)) -> U11#(mark(X)) -> U11#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(isNePal(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U12(X)) -> U12#(proper(X)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U12(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U11(X)) -> U11#(proper(X)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U11(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X1) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(isNePal(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U12(X)) -> U12#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U12(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U11(X)) -> U11#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U11(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(X1,mark(X2)) -> __#(X1,X2) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(mark(X1),X2) -> __#(X1,X2) isNePal#(ok(X)) -> isNePal#(X) -> isNePal#(ok(X)) -> isNePal#(X) isNePal#(ok(X)) -> isNePal#(X) -> isNePal#(mark(X)) -> isNePal#(X) isNePal#(mark(X)) -> isNePal#(X) -> isNePal#(ok(X)) -> isNePal#(X) isNePal#(mark(X)) -> isNePal#(X) -> isNePal#(mark(X)) -> isNePal#(X) U11#(ok(X)) -> U11#(X) -> U11#(ok(X)) -> U11#(X) U11#(ok(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X) U11#(mark(X)) -> U11#(X) -> U11#(ok(X)) -> U11#(X) U11#(mark(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X) U12#(ok(X)) -> U12#(X) -> U12#(ok(X)) -> U12#(X) U12#(ok(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X) U12#(mark(X)) -> U12#(X) -> U12#(ok(X)) -> U12#(X) U12#(mark(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) -> U11#(ok(X)) -> U11#(X) active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) -> U11#(mark(X)) -> U11#(X) active#(isNePal(X)) -> isNePal#(active(X)) -> isNePal#(ok(X)) -> isNePal#(X) active#(isNePal(X)) -> isNePal#(active(X)) -> isNePal#(mark(X)) -> isNePal#(X) active#(isNePal(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(isNePal(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(isNePal(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(isNePal(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(isNePal(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(isNePal(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(isNePal(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(isNePal(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(U12(X)) -> U12#(active(X)) -> U12#(ok(X)) -> U12#(X) active#(U12(X)) -> U12#(active(X)) -> U12#(mark(X)) -> U12#(X) active#(U12(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(U12(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(U12(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(U12(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(U12(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(U12(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(U12(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U12(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(U11(tt())) -> U12#(tt()) -> U12#(ok(X)) -> U12#(X) active#(U11(tt())) -> U12#(tt()) -> U12#(mark(X)) -> U12#(X) active#(U11(X)) -> U11#(active(X)) -> U11#(ok(X)) -> U11#(X) active#(U11(X)) -> U11#(active(X)) -> U11#(mark(X)) -> U11#(X) active#(U11(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(U11(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(U11(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(U11(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(U11(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(U11(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(U11(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U11(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(U12(X)) -> U12#(active(X)) active#(__(X1,X2)) -> active#(X2) -> active#(U12(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(U11(X)) -> U11#(active(X)) active#(__(X1,X2)) -> active#(X2) -> active#(U11(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X2) -> active#(U11(tt())) -> U12#(tt()) active#(__(X1,X2)) -> active#(X2) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(__(X1,X2)) -> active#(X2) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(U12(X)) -> U12#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(U12(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(U11(X)) -> U11#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(U11(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X1) -> active#(U11(tt())) -> U12#(tt()) active#(__(X1,X2)) -> active#(X1) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(__(X1,X2)) -> active#(X1) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) EDG Processor: DPs: active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U11(tt())) -> U12#(tt()) active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U11(X)) -> active#(X) active#(U11(X)) -> U11#(active(X)) active#(U12(X)) -> active#(X) active#(U12(X)) -> U12#(active(X)) active#(isNePal(X)) -> active#(X) active#(isNePal(X)) -> isNePal#(active(X)) __#(mark(X1),X2) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) U11#(mark(X)) -> U11#(X) U12#(mark(X)) -> U12#(X) isNePal#(mark(X)) -> isNePal#(X) proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U11(X)) -> proper#(X) proper#(U11(X)) -> U11#(proper(X)) proper#(U12(X)) -> proper#(X) proper#(U12(X)) -> U12#(proper(X)) proper#(isNePal(X)) -> proper#(X) proper#(isNePal(X)) -> isNePal#(proper(X)) __#(ok(X1),ok(X2)) -> __#(X1,X2) U11#(ok(X)) -> U11#(X) U12#(ok(X)) -> U12#(X) isNePal#(ok(X)) -> isNePal#(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(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) top#(ok(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) top#(ok(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) top#(ok(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(U11(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) top#(ok(X)) -> active#(X) -> active#(U12(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) top#(ok(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(isNePal(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(isNePal(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(isNePal(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(isNePal(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(isNePal(X)) -> isNePal#(proper(X)) -> isNePal#(mark(X)) -> isNePal#(X) proper#(isNePal(X)) -> isNePal#(proper(X)) -> isNePal#(ok(X)) -> isNePal#(X) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(U12(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U12(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(U12(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(U12(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(U12(X)) -> U12#(proper(X)) -> U12#(mark(X)) -> U12#(X) proper#(U12(X)) -> U12#(proper(X)) -> U12#(ok(X)) -> U12#(X) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X2) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> proper#(X1) proper#(U11(X)) -> proper#(X) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(U11(X)) -> proper#(X) -> proper#(U11(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(U11(X)) -> U11#(proper(X)) proper#(U11(X)) -> proper#(X) -> proper#(U12(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(U12(X)) -> U12#(proper(X)) proper#(U11(X)) -> proper#(X) -> proper#(isNePal(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(U11(X)) -> U11#(proper(X)) -> U11#(mark(X)) -> U11#(X) proper#(U11(X)) -> U11#(proper(X)) -> U11#(ok(X)) -> U11#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> proper#(X2) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U11(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U11(X)) -> U11#(proper(X)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U12(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(U12(X)) -> U12#(proper(X)) proper#(__(X1,X2)) -> proper#(X2) -> proper#(isNePal(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X2) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> proper#(X2) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> proper#(X1) -> proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U11(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U11(X)) -> U11#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U12(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(U12(X)) -> U12#(proper(X)) proper#(__(X1,X2)) -> proper#(X1) -> proper#(isNePal(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) -> proper#(isNePal(X)) -> isNePal#(proper(X)) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(mark(X1),X2) -> __#(X1,X2) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(X1,mark(X2)) -> __#(X1,X2) proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) isNePal#(ok(X)) -> isNePal#(X) -> isNePal#(mark(X)) -> isNePal#(X) isNePal#(ok(X)) -> isNePal#(X) -> isNePal#(ok(X)) -> isNePal#(X) isNePal#(mark(X)) -> isNePal#(X) -> isNePal#(mark(X)) -> isNePal#(X) isNePal#(mark(X)) -> isNePal#(X) -> isNePal#(ok(X)) -> isNePal#(X) U11#(ok(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X) U11#(ok(X)) -> U11#(X) -> U11#(ok(X)) -> U11#(X) U11#(mark(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X) U11#(mark(X)) -> U11#(X) -> U11#(ok(X)) -> U11#(X) U12#(ok(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X) U12#(ok(X)) -> U12#(X) -> U12#(ok(X)) -> U12#(X) U12#(mark(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X) U12#(mark(X)) -> U12#(X) -> U12#(ok(X)) -> U12#(X) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(ok(X1),ok(X2)) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(mark(X1),X2) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(X1,mark(X2)) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(isNePal(X)) -> isNePal#(active(X)) -> isNePal#(mark(X)) -> isNePal#(X) active#(isNePal(X)) -> isNePal#(active(X)) -> isNePal#(ok(X)) -> isNePal#(X) active#(isNePal(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(isNePal(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(isNePal(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(isNePal(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(isNePal(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(isNePal(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(isNePal(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(isNePal(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(isNePal(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(U12(X)) -> U12#(active(X)) -> U12#(mark(X)) -> U12#(X) active#(U12(X)) -> U12#(active(X)) -> U12#(ok(X)) -> U12#(X) active#(U12(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(U12(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U12(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(U12(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(U12(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U12(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(U12(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(U12(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(U12(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(U11(X)) -> U11#(active(X)) -> U11#(mark(X)) -> U11#(X) active#(U11(X)) -> U11#(active(X)) -> U11#(ok(X)) -> U11#(X) active#(U11(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(U11(X)) -> active#(X) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(U11(X)) -> active#(X) -> active#(U11(tt())) -> U12#(tt()) active#(U11(X)) -> active#(X) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X1) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> active#(X2) active#(U11(X)) -> active#(X) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(U11(X)) -> active#(X) -> active#(U11(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(U11(X)) -> U11#(active(X)) active#(U11(X)) -> active#(X) -> active#(U12(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(U12(X)) -> U12#(active(X)) active#(U11(X)) -> active#(X) -> active#(isNePal(X)) -> active#(X) active#(U11(X)) -> active#(X) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(Y,Z) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(active(X1),X2) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(mark(X1),X2) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(X1,mark(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> __#(X1,active(X2)) -> __#(ok(X1),ok(X2)) -> __#(X1,X2) active#(__(X1,X2)) -> active#(X2) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(X1,X2)) -> active#(X2) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(__(X1,X2)) -> active#(X2) -> active#(U11(tt())) -> U12#(tt()) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> active#(X2) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(__(X1,X2)) -> active#(X2) -> active#(U11(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(U11(X)) -> U11#(active(X)) active#(__(X1,X2)) -> active#(X2) -> active#(U12(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(U12(X)) -> U12#(active(X)) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) -> active#(isNePal(X)) -> isNePal#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(__(__(X,Y),Z)) -> __#(Y,Z) active#(__(X1,X2)) -> active#(X1) -> active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) active#(__(X1,X2)) -> active#(X1) -> active#(U11(tt())) -> U12#(tt()) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(__(I,__(P,I)))) -> U11#(tt()) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> active#(X1) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> __#(active(X1),X2) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> active#(X1) -> active#(__(X1,X2)) -> __#(X1,active(X2)) active#(__(X1,X2)) -> active#(X1) -> active#(U11(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(U11(X)) -> U11#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(U12(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(U12(X)) -> U12#(active(X)) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(X)) -> active#(X) active#(__(X1,X2)) -> active#(X1) -> active#(isNePal(X)) -> isNePal#(active(X)) SCC Processor: #sccs: 7 #rules: 21 #arcs: 194/1296 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=2 interpretation: [top#](x0) = [1 2]x0, [0] [top](x0) = [0], [2 0] [1] [ok](x0) = [2 1]x0 + [0], [0 0] [2] [proper](x0) = [0 1]x0 + [0], [0] [isNePal](x0) = x0 + [3], [1 0] [U12](x0) = [0 3]x0, [1 0] [0] [U11](x0) = [0 2]x0 + [3], [0] [tt] = [1], [0] [nil] = [0], [0 0] [0] [mark](x0) = [0 1]x0 + [2], [active](x0) = x0, [0 0] [0] [__](x0, x1) = [0 2]x0 + x1 + [2] orientation: top#(ok(X)) = [6 2]X + [1] >= [1 2]X = top#(active(X)) top#(mark(X)) = [0 2]X + [4] >= [0 2]X + [2] = top#(proper(X)) [0 0] [0 0] [0] [0 0] [0 0] [0 0] [0] active(__(__(X,Y),Z)) = [0 4]X + [0 2]Y + Z + [6] >= [0 2]X + [0 2]Y + [0 1]Z + [6] = mark(__(X,__(Y,Z))) [0 0] [0] [0 0] [0] active(__(X,nil())) = [0 2]X + [2] >= [0 1]X + [2] = mark(X) [0] [0 0] [0] active(__(nil(),X)) = X + [2] >= [0 1]X + [2] = mark(X) [0] [0] active(U11(tt())) = [5] >= [5] = mark(U12(tt())) [0] [0] active(U12(tt())) = [3] >= [3] = mark(tt()) [1 0] [0 0] [0] [0] active(isNePal(__(I,__(P,I)))) = [0 3]I + [0 2]P + [7] >= [7] = mark(U11(tt())) [0 0] [0] [0 0] [0] active(__(X1,X2)) = [0 2]X1 + X2 + [2] >= [0 2]X1 + X2 + [2] = __(active(X1),X2) [0 0] [0] [0 0] [0] active(__(X1,X2)) = [0 2]X1 + X2 + [2] >= [0 2]X1 + X2 + [2] = __(X1,active(X2)) [1 0] [0] [1 0] [0] active(U11(X)) = [0 2]X + [3] >= [0 2]X + [3] = U11(active(X)) [1 0] [1 0] active(U12(X)) = [0 3]X >= [0 3]X = U12(active(X)) [0] [0] active(isNePal(X)) = X + [3] >= X + [3] = isNePal(active(X)) [0 0] [0] [0 0] [0 0] [0] __(mark(X1),X2) = [0 2]X1 + X2 + [6] >= [0 2]X1 + [0 1]X2 + [4] = mark(__(X1,X2)) [0 0] [0 0] [0] [0 0] [0 0] [0] __(X1,mark(X2)) = [0 2]X1 + [0 1]X2 + [4] >= [0 2]X1 + [0 1]X2 + [4] = mark(__(X1,X2)) [0 0] [0] [0 0] [0] U11(mark(X)) = [0 2]X + [7] >= [0 2]X + [5] = mark(U11(X)) [0 0] [0] [0 0] [0] U12(mark(X)) = [0 3]X + [6] >= [0 3]X + [2] = mark(U12(X)) [0 0] [0] [0 0] [0] isNePal(mark(X)) = [0 1]X + [5] >= [0 1]X + [5] = mark(isNePal(X)) [0 0] [0 0] [2] [0 0] [0 0] [2] proper(__(X1,X2)) = [0 2]X1 + [0 1]X2 + [2] >= [0 2]X1 + [0 1]X2 + [2] = __(proper(X1),proper(X2)) [2] [1] proper(nil()) = [0] >= [0] = ok(nil()) [0 0] [2] [0 0] [2] proper(U11(X)) = [0 2]X + [3] >= [0 2]X + [3] = U11(proper(X)) [2] [1] proper(tt()) = [1] >= [1] = ok(tt()) [0 0] [2] [0 0] [2] proper(U12(X)) = [0 3]X + [0] >= [0 3]X + [0] = U12(proper(X)) [0 0] [2] [0 0] [2] proper(isNePal(X)) = [0 1]X + [3] >= [0 1]X + [3] = isNePal(proper(X)) [0 0] [2 0] [1] [0 0] [2 0] [1] __(ok(X1),ok(X2)) = [4 2]X1 + [2 1]X2 + [2] >= [0 2]X1 + [2 1]X2 + [2] = ok(__(X1,X2)) [2 0] [1] [2 0] [1] U11(ok(X)) = [4 2]X + [3] >= [2 2]X + [3] = ok(U11(X)) [2 0] [1] [2 0] [1] U12(ok(X)) = [6 3]X + [0] >= [2 3]X + [0] = ok(U12(X)) [2 0] [1] [2 0] [1] isNePal(ok(X)) = [2 1]X + [3] >= [2 1]X + [3] = ok(isNePal(X)) [0] [0] top(mark(X)) = [0] >= [0] = top(proper(X)) [0] [0] top(ok(X)) = [0] >= [0] = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(isNePal(X)) -> proper#(X) proper#(U12(X)) -> proper#(X) proper#(U11(X)) -> proper#(X) proper#(__(X1,X2)) -> proper#(X1) proper#(__(X1,X2)) -> proper#(X2) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [proper#](x0) = 5x0 + 2, [top](x0) = 4, [ok](x0) = x0 + 4, [proper](x0) = 2x0, [isNePal](x0) = x0 + 1, [U12](x0) = x0 + 5, [U11](x0) = x0 + 1, [tt] = 4, [nil] = 6, [mark](x0) = x0, [active](x0) = 2x0, [__](x0, x1) = 2x0 + 2x1 + 2 orientation: proper#(isNePal(X)) = 5X + 7 >= 5X + 2 = proper#(X) proper#(U12(X)) = 5X + 27 >= 5X + 2 = proper#(X) proper#(U11(X)) = 5X + 7 >= 5X + 2 = proper#(X) proper#(__(X1,X2)) = 10X1 + 10X2 + 12 >= 5X1 + 2 = proper#(X1) proper#(__(X1,X2)) = 10X1 + 10X2 + 12 >= 5X2 + 2 = proper#(X2) active(__(__(X,Y),Z)) = 8X + 8Y + 4Z + 12 >= 2X + 4Y + 4Z + 6 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 4X + 28 >= X = mark(X) active(__(nil(),X)) = 4X + 28 >= X = mark(X) active(U11(tt())) = 10 >= 9 = mark(U12(tt())) active(U12(tt())) = 18 >= 4 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 12I + 8P + 14 >= 5 = mark(U11(tt())) active(__(X1,X2)) = 4X1 + 4X2 + 4 >= 4X1 + 2X2 + 2 = __(active(X1),X2) active(__(X1,X2)) = 4X1 + 4X2 + 4 >= 2X1 + 4X2 + 2 = __(X1,active(X2)) active(U11(X)) = 2X + 2 >= 2X + 1 = U11(active(X)) active(U12(X)) = 2X + 10 >= 2X + 5 = U12(active(X)) active(isNePal(X)) = 2X + 2 >= 2X + 1 = isNePal(active(X)) __(mark(X1),X2) = 2X1 + 2X2 + 2 >= 2X1 + 2X2 + 2 = mark(__(X1,X2)) __(X1,mark(X2)) = 2X1 + 2X2 + 2 >= 2X1 + 2X2 + 2 = mark(__(X1,X2)) U11(mark(X)) = X + 1 >= X + 1 = mark(U11(X)) U12(mark(X)) = X + 5 >= X + 5 = mark(U12(X)) isNePal(mark(X)) = X + 1 >= X + 1 = mark(isNePal(X)) proper(__(X1,X2)) = 4X1 + 4X2 + 4 >= 4X1 + 4X2 + 2 = __(proper(X1),proper(X2)) proper(nil()) = 12 >= 10 = ok(nil()) proper(U11(X)) = 2X + 2 >= 2X + 1 = U11(proper(X)) proper(tt()) = 8 >= 8 = ok(tt()) proper(U12(X)) = 2X + 10 >= 2X + 5 = U12(proper(X)) proper(isNePal(X)) = 2X + 2 >= 2X + 1 = isNePal(proper(X)) __(ok(X1),ok(X2)) = 2X1 + 2X2 + 18 >= 2X1 + 2X2 + 6 = ok(__(X1,X2)) U11(ok(X)) = X + 5 >= X + 5 = ok(U11(X)) U12(ok(X)) = X + 9 >= X + 9 = ok(U12(X)) isNePal(ok(X)) = X + 5 >= X + 5 = ok(isNePal(X)) top(mark(X)) = 4 >= 4 = top(proper(X)) top(ok(X)) = 4 >= 4 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: active#(isNePal(X)) -> active#(X) active#(U12(X)) -> active#(X) active#(U11(X)) -> active#(X) active#(__(X1,X2)) -> active#(X2) active#(__(X1,X2)) -> active#(X1) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [active#](x0) = 2x0, [top](x0) = 4, [ok](x0) = 0, [proper](x0) = x0, [isNePal](x0) = x0 + 5, [U12](x0) = x0 + 2, [U11](x0) = 2x0 + 1, [tt] = 3, [nil] = 2, [mark](x0) = 0, [active](x0) = 2x0, [__](x0, x1) = x0 + 4x1 + 1 orientation: active#(isNePal(X)) = 2X + 10 >= 2X = active#(X) active#(U12(X)) = 2X + 4 >= 2X = active#(X) active#(U11(X)) = 4X + 2 >= 2X = active#(X) active#(__(X1,X2)) = 2X1 + 8X2 + 2 >= 2X2 = active#(X2) active#(__(X1,X2)) = 2X1 + 8X2 + 2 >= 2X1 = active#(X1) active(__(__(X,Y),Z)) = 2X + 8Y + 8Z + 4 >= 0 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 2X + 18 >= 0 = mark(X) active(__(nil(),X)) = 8X + 6 >= 0 = mark(X) active(U11(tt())) = 14 >= 0 = mark(U12(tt())) active(U12(tt())) = 10 >= 0 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 34I + 8P + 20 >= 0 = mark(U11(tt())) active(__(X1,X2)) = 2X1 + 8X2 + 2 >= 2X1 + 4X2 + 1 = __(active(X1),X2) active(__(X1,X2)) = 2X1 + 8X2 + 2 >= X1 + 8X2 + 1 = __(X1,active(X2)) active(U11(X)) = 4X + 2 >= 4X + 1 = U11(active(X)) active(U12(X)) = 2X + 4 >= 2X + 2 = U12(active(X)) active(isNePal(X)) = 2X + 10 >= 2X + 5 = isNePal(active(X)) __(mark(X1),X2) = 4X2 + 1 >= 0 = mark(__(X1,X2)) __(X1,mark(X2)) = X1 + 1 >= 0 = mark(__(X1,X2)) U11(mark(X)) = 1 >= 0 = mark(U11(X)) U12(mark(X)) = 2 >= 0 = mark(U12(X)) isNePal(mark(X)) = 5 >= 0 = mark(isNePal(X)) proper(__(X1,X2)) = X1 + 4X2 + 1 >= X1 + 4X2 + 1 = __(proper(X1),proper(X2)) proper(nil()) = 2 >= 0 = ok(nil()) proper(U11(X)) = 2X + 1 >= 2X + 1 = U11(proper(X)) proper(tt()) = 3 >= 0 = ok(tt()) proper(U12(X)) = X + 2 >= X + 2 = U12(proper(X)) proper(isNePal(X)) = X + 5 >= X + 5 = isNePal(proper(X)) __(ok(X1),ok(X2)) = 1 >= 0 = ok(__(X1,X2)) U11(ok(X)) = 1 >= 0 = ok(U11(X)) U12(ok(X)) = 2 >= 0 = ok(U12(X)) isNePal(ok(X)) = 5 >= 0 = ok(isNePal(X)) top(mark(X)) = 4 >= 4 = top(proper(X)) top(ok(X)) = 4 >= 4 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: __#(ok(X1),ok(X2)) -> __#(X1,X2) __#(X1,mark(X2)) -> __#(X1,X2) __#(mark(X1),X2) -> __#(X1,X2) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [__#](x0, x1) = x0 + x1, [top](x0) = 1, [ok](x0) = x0 + 1/2, [proper](x0) = 2x0 + 1/2, [isNePal](x0) = x0, [U12](x0) = 3x0 + 2, [U11](x0) = 2x0 + 2, [tt] = 0, [nil] = 1, [mark](x0) = x0 + 1, [active](x0) = 3/2x0, [__](x0, x1) = x0 + x1 + 1 orientation: __#(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 = __#(X1,X2) __#(X1,mark(X2)) = X1 + X2 + 1 >= X1 + X2 = __#(X1,X2) __#(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 = __#(X1,X2) active(__(__(X,Y),Z)) = 3/2X + 3/2Y + 3/2Z + 3 >= X + Y + Z + 3 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 3/2X + 3 >= X + 1 = mark(X) active(__(nil(),X)) = 3/2X + 3 >= X + 1 = mark(X) active(U11(tt())) = 3 >= 3 = mark(U12(tt())) active(U12(tt())) = 3 >= 1 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 3I + 3/2P + 3 >= 3 = mark(U11(tt())) active(__(X1,X2)) = 3/2X1 + 3/2X2 + 3/2 >= 3/2X1 + X2 + 1 = __(active(X1),X2) active(__(X1,X2)) = 3/2X1 + 3/2X2 + 3/2 >= X1 + 3/2X2 + 1 = __(X1,active(X2)) active(U11(X)) = 3X + 3 >= 3X + 2 = U11(active(X)) active(U12(X)) = 9/2X + 3 >= 9/2X + 2 = U12(active(X)) active(isNePal(X)) = 3/2X >= 3/2X = isNePal(active(X)) __(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 2 = mark(__(X1,X2)) __(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = mark(__(X1,X2)) U11(mark(X)) = 2X + 4 >= 2X + 3 = mark(U11(X)) U12(mark(X)) = 3X + 5 >= 3X + 3 = mark(U12(X)) isNePal(mark(X)) = X + 1 >= X + 1 = mark(isNePal(X)) proper(__(X1,X2)) = 2X1 + 2X2 + 5/2 >= 2X1 + 2X2 + 2 = __(proper(X1),proper(X2)) proper(nil()) = 5/2 >= 3/2 = ok(nil()) proper(U11(X)) = 4X + 9/2 >= 4X + 3 = U11(proper(X)) proper(tt()) = 1/2 >= 1/2 = ok(tt()) proper(U12(X)) = 6X + 9/2 >= 6X + 7/2 = U12(proper(X)) proper(isNePal(X)) = 2X + 1/2 >= 2X + 1/2 = isNePal(proper(X)) __(ok(X1),ok(X2)) = X1 + X2 + 2 >= X1 + X2 + 3/2 = ok(__(X1,X2)) U11(ok(X)) = 2X + 3 >= 2X + 5/2 = ok(U11(X)) U12(ok(X)) = 3X + 7/2 >= 3X + 5/2 = ok(U12(X)) isNePal(ok(X)) = X + 1/2 >= X + 1/2 = ok(isNePal(X)) top(mark(X)) = 1 >= 1 = top(proper(X)) top(ok(X)) = 1 >= 1 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: U11#(ok(X)) -> U11#(X) U11#(mark(X)) -> U11#(X) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [U11#](x0) = 1/2x0, [top](x0) = 1, [ok](x0) = x0 + 2, [proper](x0) = 2x0, [isNePal](x0) = 2x0 + 3/2, [U12](x0) = x0 + 2, [U11](x0) = x0, [tt] = 2, [nil] = 2, [mark](x0) = x0 + 2, [active](x0) = 3x0, [__](x0, x1) = 2x0 + x1 + 3/2 orientation: U11#(ok(X)) = 1/2X + 1 >= 1/2X = U11#(X) U11#(mark(X)) = 1/2X + 1 >= 1/2X = U11#(X) active(__(__(X,Y),Z)) = 12X + 6Y + 3Z + 27/2 >= 2X + 2Y + Z + 5 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 6X + 21/2 >= X + 2 = mark(X) active(__(nil(),X)) = 3X + 33/2 >= X + 2 = mark(X) active(U11(tt())) = 6 >= 6 = mark(U12(tt())) active(U12(tt())) = 12 >= 4 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 18I + 12P + 45/2 >= 4 = mark(U11(tt())) active(__(X1,X2)) = 6X1 + 3X2 + 9/2 >= 6X1 + X2 + 3/2 = __(active(X1),X2) active(__(X1,X2)) = 6X1 + 3X2 + 9/2 >= 2X1 + 3X2 + 3/2 = __(X1,active(X2)) active(U11(X)) = 3X >= 3X = U11(active(X)) active(U12(X)) = 3X + 6 >= 3X + 2 = U12(active(X)) active(isNePal(X)) = 6X + 9/2 >= 6X + 3/2 = isNePal(active(X)) __(mark(X1),X2) = 2X1 + X2 + 11/2 >= 2X1 + X2 + 7/2 = mark(__(X1,X2)) __(X1,mark(X2)) = 2X1 + X2 + 7/2 >= 2X1 + X2 + 7/2 = mark(__(X1,X2)) U11(mark(X)) = X + 2 >= X + 2 = mark(U11(X)) U12(mark(X)) = X + 4 >= X + 4 = mark(U12(X)) isNePal(mark(X)) = 2X + 11/2 >= 2X + 7/2 = mark(isNePal(X)) proper(__(X1,X2)) = 4X1 + 2X2 + 3 >= 4X1 + 2X2 + 3/2 = __(proper(X1),proper(X2)) proper(nil()) = 4 >= 4 = ok(nil()) proper(U11(X)) = 2X >= 2X = U11(proper(X)) proper(tt()) = 4 >= 4 = ok(tt()) proper(U12(X)) = 2X + 4 >= 2X + 2 = U12(proper(X)) proper(isNePal(X)) = 4X + 3 >= 4X + 3/2 = isNePal(proper(X)) __(ok(X1),ok(X2)) = 2X1 + X2 + 15/2 >= 2X1 + X2 + 7/2 = ok(__(X1,X2)) U11(ok(X)) = X + 2 >= X + 2 = ok(U11(X)) U12(ok(X)) = X + 4 >= X + 4 = ok(U12(X)) isNePal(ok(X)) = 2X + 11/2 >= 2X + 7/2 = ok(isNePal(X)) top(mark(X)) = 1 >= 1 = top(proper(X)) top(ok(X)) = 1 >= 1 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: U12#(ok(X)) -> U12#(X) U12#(mark(X)) -> U12#(X) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [U12#](x0) = x0, [top](x0) = 0, [ok](x0) = 2x0 + 1, [proper](x0) = 4x0, [isNePal](x0) = x0, [U12](x0) = 2x0, [U11](x0) = 3x0, [tt] = 1, [nil] = 1, [mark](x0) = x0 + 1, [active](x0) = x0, [__](x0, x1) = 2x0 + x1 + 2 orientation: U12#(ok(X)) = 2X + 1 >= X = U12#(X) U12#(mark(X)) = X + 1 >= X = U12#(X) active(__(__(X,Y),Z)) = 4X + 2Y + Z + 6 >= 2X + 2Y + Z + 5 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 2X + 3 >= X + 1 = mark(X) active(__(nil(),X)) = X + 4 >= X + 1 = mark(X) active(U11(tt())) = 3 >= 3 = mark(U12(tt())) active(U12(tt())) = 2 >= 2 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 3I + 2P + 4 >= 4 = mark(U11(tt())) active(__(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = __(active(X1),X2) active(__(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = __(X1,active(X2)) active(U11(X)) = 3X >= 3X = U11(active(X)) active(U12(X)) = 2X >= 2X = U12(active(X)) active(isNePal(X)) = X >= X = isNePal(active(X)) __(mark(X1),X2) = 2X1 + X2 + 4 >= 2X1 + X2 + 3 = mark(__(X1,X2)) __(X1,mark(X2)) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = mark(__(X1,X2)) U11(mark(X)) = 3X + 3 >= 3X + 1 = mark(U11(X)) U12(mark(X)) = 2X + 2 >= 2X + 1 = mark(U12(X)) isNePal(mark(X)) = X + 1 >= X + 1 = mark(isNePal(X)) proper(__(X1,X2)) = 8X1 + 4X2 + 8 >= 8X1 + 4X2 + 2 = __(proper(X1),proper(X2)) proper(nil()) = 4 >= 3 = ok(nil()) proper(U11(X)) = 12X >= 12X = U11(proper(X)) proper(tt()) = 4 >= 3 = ok(tt()) proper(U12(X)) = 8X >= 8X = U12(proper(X)) proper(isNePal(X)) = 4X >= 4X = isNePal(proper(X)) __(ok(X1),ok(X2)) = 4X1 + 2X2 + 5 >= 4X1 + 2X2 + 5 = ok(__(X1,X2)) U11(ok(X)) = 6X + 3 >= 6X + 1 = ok(U11(X)) U12(ok(X)) = 4X + 2 >= 4X + 1 = ok(U12(X)) isNePal(ok(X)) = 2X + 1 >= 2X + 1 = ok(isNePal(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: isNePal#(ok(X)) -> isNePal#(X) isNePal#(mark(X)) -> isNePal#(X) TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [isNePal#](x0) = x0, [top](x0) = 0, [ok](x0) = 2x0 + 1, [proper](x0) = 4x0, [isNePal](x0) = x0, [U12](x0) = 2x0, [U11](x0) = 3x0, [tt] = 1, [nil] = 1, [mark](x0) = x0 + 1, [active](x0) = x0, [__](x0, x1) = 2x0 + x1 + 2 orientation: isNePal#(ok(X)) = 2X + 1 >= X = isNePal#(X) isNePal#(mark(X)) = X + 1 >= X = isNePal#(X) active(__(__(X,Y),Z)) = 4X + 2Y + Z + 6 >= 2X + 2Y + Z + 5 = mark(__(X,__(Y,Z))) active(__(X,nil())) = 2X + 3 >= X + 1 = mark(X) active(__(nil(),X)) = X + 4 >= X + 1 = mark(X) active(U11(tt())) = 3 >= 3 = mark(U12(tt())) active(U12(tt())) = 2 >= 2 = mark(tt()) active(isNePal(__(I,__(P,I)))) = 3I + 2P + 4 >= 4 = mark(U11(tt())) active(__(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = __(active(X1),X2) active(__(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = __(X1,active(X2)) active(U11(X)) = 3X >= 3X = U11(active(X)) active(U12(X)) = 2X >= 2X = U12(active(X)) active(isNePal(X)) = X >= X = isNePal(active(X)) __(mark(X1),X2) = 2X1 + X2 + 4 >= 2X1 + X2 + 3 = mark(__(X1,X2)) __(X1,mark(X2)) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = mark(__(X1,X2)) U11(mark(X)) = 3X + 3 >= 3X + 1 = mark(U11(X)) U12(mark(X)) = 2X + 2 >= 2X + 1 = mark(U12(X)) isNePal(mark(X)) = X + 1 >= X + 1 = mark(isNePal(X)) proper(__(X1,X2)) = 8X1 + 4X2 + 8 >= 8X1 + 4X2 + 2 = __(proper(X1),proper(X2)) proper(nil()) = 4 >= 3 = ok(nil()) proper(U11(X)) = 12X >= 12X = U11(proper(X)) proper(tt()) = 4 >= 3 = ok(tt()) proper(U12(X)) = 8X >= 8X = U12(proper(X)) proper(isNePal(X)) = 4X >= 4X = isNePal(proper(X)) __(ok(X1),ok(X2)) = 4X1 + 2X2 + 5 >= 4X1 + 2X2 + 5 = ok(__(X1,X2)) U11(ok(X)) = 6X + 3 >= 6X + 1 = ok(U11(X)) U12(ok(X)) = 4X + 2 >= 4X + 1 = ok(U12(X)) isNePal(ok(X)) = 2X + 1 >= 2X + 1 = ok(isNePal(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed