MAYBE Problem: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(fact(X)) -> p#(X) active#(fact(X)) -> fact#(p(X)) active#(fact(X)) -> prod#(X,fact(p(X))) active#(fact(X)) -> s#(0()) active#(fact(X)) -> zero#(X) active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(add(s(X),Y)) -> add#(X,Y) active#(add(s(X),Y)) -> s#(add(X,Y)) active#(prod(s(X),Y)) -> prod#(X,Y) active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(fact(X)) -> active#(X) active#(fact(X)) -> fact#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(zero(X)) -> active#(X) active#(zero(X)) -> zero#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(prod(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(prod(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(p(X)) -> active#(X) active#(p(X)) -> p#(active(X)) active#(add(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> add#(active(X1),X2) active#(add(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> add#(X1,active(X2)) fact#(mark(X)) -> fact#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) zero#(mark(X)) -> zero#(X) s#(mark(X)) -> s#(X) prod#(mark(X1),X2) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) p#(mark(X)) -> p#(X) add#(mark(X1),X2) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) proper#(fact(X)) -> proper#(X) proper#(fact(X)) -> fact#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(zero(X)) -> proper#(X) proper#(zero(X)) -> zero#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(p(X)) -> proper#(X) proper#(p(X)) -> p#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) fact#(ok(X)) -> fact#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) zero#(ok(X)) -> zero#(X) s#(ok(X)) -> s#(X) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) p#(ok(X)) -> p#(X) add#(ok(X1),ok(X2)) -> add#(X1,X2) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(fact(X)) -> p#(X) active#(fact(X)) -> fact#(p(X)) active#(fact(X)) -> prod#(X,fact(p(X))) active#(fact(X)) -> s#(0()) active#(fact(X)) -> zero#(X) active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(add(s(X),Y)) -> add#(X,Y) active#(add(s(X),Y)) -> s#(add(X,Y)) active#(prod(s(X),Y)) -> prod#(X,Y) active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(fact(X)) -> active#(X) active#(fact(X)) -> fact#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(zero(X)) -> active#(X) active#(zero(X)) -> zero#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(prod(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(prod(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(p(X)) -> active#(X) active#(p(X)) -> p#(active(X)) active#(add(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> add#(active(X1),X2) active#(add(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> add#(X1,active(X2)) fact#(mark(X)) -> fact#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) zero#(mark(X)) -> zero#(X) s#(mark(X)) -> s#(X) prod#(mark(X1),X2) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) p#(mark(X)) -> p#(X) add#(mark(X1),X2) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) proper#(fact(X)) -> proper#(X) proper#(fact(X)) -> fact#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(zero(X)) -> proper#(X) proper#(zero(X)) -> zero#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(p(X)) -> proper#(X) proper#(p(X)) -> p#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) fact#(ok(X)) -> fact#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) zero#(ok(X)) -> zero#(X) s#(ok(X)) -> s#(X) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) p#(ok(X)) -> p#(X) add#(ok(X1),ok(X2)) -> add#(X1,X2) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) 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#(add(X1,X2)) -> add#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) top#(ok(X)) -> active#(X) -> active#(p(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(zero(X)) -> zero#(active(X)) top#(ok(X)) -> active#(X) -> active#(zero(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> fact#(active(X)) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) top#(ok(X)) -> active#(X) -> active#(prod(s(X),Y)) -> prod#(X,Y) top#(ok(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y)) top#(ok(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> zero#(X) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> s#(0()) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> prod#(X,fact(p(X))) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> fact#(p(X)) top#(ok(X)) -> active#(X) -> active#(fact(X)) -> p#(X) 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#(add(X1,X2)) -> add#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(zero(X)) -> zero#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(zero(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) -> proper#(fact(X)) -> fact#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(fact(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X2) -> proper#(zero(X)) -> zero#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(zero(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(add(X1,X2)) -> proper#(X2) -> proper#(fact(X)) -> fact#(proper(X)) proper#(add(X1,X2)) -> proper#(X2) -> proper#(fact(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X1) -> proper#(zero(X)) -> zero#(proper(X)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(zero(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(add(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(add(X1,X2)) -> proper#(X1) -> proper#(fact(X)) -> fact#(proper(X)) proper#(add(X1,X2)) -> proper#(X1) -> proper#(fact(X)) -> proper#(X) proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) -> add#(X1,mark(X2)) -> add#(X1,X2) proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) -> add#(mark(X1),X2) -> add#(X1,X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(add(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(add(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(zero(X)) -> zero#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(zero(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(fact(X)) -> fact#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(fact(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(zero(X)) -> zero#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(zero(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(fact(X)) -> fact#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(fact(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(zero(X)) -> zero#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(zero(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(fact(X)) -> fact#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(fact(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(add(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(zero(X)) -> zero#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(zero(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(fact(X)) -> fact#(proper(X)) proper#(prod(X1,X2)) -> proper#(X2) -> proper#(fact(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(add(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(zero(X)) -> zero#(proper(X)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(zero(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(fact(X)) -> fact#(proper(X)) proper#(prod(X1,X2)) -> proper#(X1) -> proper#(fact(X)) -> proper#(X) proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) -> prod#(X1,mark(X2)) -> prod#(X1,X2) proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) -> prod#(mark(X1),X2) -> prod#(X1,X2) proper#(p(X)) -> proper#(X) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(p(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1) proper#(p(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2) proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(p(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(p(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(p(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(p(X)) -> proper#(X) -> proper#(zero(X)) -> zero#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(zero(X)) -> proper#(X) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(p(X)) -> proper#(X) -> proper#(fact(X)) -> fact#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(fact(X)) -> proper#(X) proper#(p(X)) -> p#(proper(X)) -> p#(ok(X)) -> p#(X) proper#(p(X)) -> p#(proper(X)) -> p#(mark(X)) -> p#(X) proper#(s(X)) -> proper#(X) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(zero(X)) -> zero#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(zero(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(s(X)) -> proper#(X) -> proper#(fact(X)) -> fact#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(fact(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) proper#(zero(X)) -> proper#(X) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(zero(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1) proper#(zero(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2) proper#(zero(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(zero(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(zero(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(zero(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(zero(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(zero(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(zero(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(zero(X)) -> proper#(X) -> proper#(zero(X)) -> zero#(proper(X)) proper#(zero(X)) -> proper#(X) -> proper#(zero(X)) -> proper#(X) proper#(zero(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(zero(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(zero(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(zero(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(zero(X)) -> proper#(X) -> proper#(fact(X)) -> fact#(proper(X)) proper#(zero(X)) -> proper#(X) -> proper#(fact(X)) -> proper#(X) proper#(zero(X)) -> zero#(proper(X)) -> zero#(ok(X)) -> zero#(X) proper#(zero(X)) -> zero#(proper(X)) -> zero#(mark(X)) -> zero#(X) proper#(fact(X)) -> proper#(X) -> proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) proper#(fact(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1) proper#(fact(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2) proper#(fact(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(fact(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(fact(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> prod#(proper(X1),proper(X2)) proper#(fact(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X1) proper#(fact(X)) -> proper#(X) -> proper#(prod(X1,X2)) -> proper#(X2) proper#(fact(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(fact(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(fact(X)) -> proper#(X) -> proper#(zero(X)) -> zero#(proper(X)) proper#(fact(X)) -> proper#(X) -> proper#(zero(X)) -> proper#(X) proper#(fact(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(fact(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(fact(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(fact(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(fact(X)) -> proper#(X) -> proper#(fact(X)) -> fact#(proper(X)) proper#(fact(X)) -> proper#(X) -> proper#(fact(X)) -> proper#(X) proper#(fact(X)) -> fact#(proper(X)) -> fact#(ok(X)) -> fact#(X) proper#(fact(X)) -> fact#(proper(X)) -> fact#(mark(X)) -> fact#(X) add#(ok(X1),ok(X2)) -> add#(X1,X2) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) add#(ok(X1),ok(X2)) -> add#(X1,X2) -> add#(X1,mark(X2)) -> add#(X1,X2) add#(ok(X1),ok(X2)) -> add#(X1,X2) -> add#(mark(X1),X2) -> add#(X1,X2) add#(mark(X1),X2) -> add#(X1,X2) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) add#(mark(X1),X2) -> add#(X1,X2) -> add#(X1,mark(X2)) -> add#(X1,X2) add#(mark(X1),X2) -> add#(X1,X2) -> add#(mark(X1),X2) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) -> add#(X1,mark(X2)) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) -> add#(mark(X1),X2) -> add#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) zero#(ok(X)) -> zero#(X) -> zero#(ok(X)) -> zero#(X) zero#(ok(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X) zero#(mark(X)) -> zero#(X) -> zero#(ok(X)) -> zero#(X) zero#(mark(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) -> prod#(X1,mark(X2)) -> prod#(X1,X2) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) -> prod#(mark(X1),X2) -> prod#(X1,X2) prod#(mark(X1),X2) -> prod#(X1,X2) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) prod#(mark(X1),X2) -> prod#(X1,X2) -> prod#(X1,mark(X2)) -> prod#(X1,X2) prod#(mark(X1),X2) -> prod#(X1,X2) -> prod#(mark(X1),X2) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) -> prod#(X1,mark(X2)) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) -> prod#(mark(X1),X2) -> prod#(X1,X2) fact#(ok(X)) -> fact#(X) -> fact#(ok(X)) -> fact#(X) fact#(ok(X)) -> fact#(X) -> fact#(mark(X)) -> fact#(X) fact#(mark(X)) -> fact#(X) -> fact#(ok(X)) -> fact#(X) fact#(mark(X)) -> fact#(X) -> fact#(mark(X)) -> fact#(X) p#(ok(X)) -> p#(X) -> p#(ok(X)) -> p#(X) p#(ok(X)) -> p#(X) -> p#(mark(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(ok(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X) active#(add(s(X),Y)) -> add#(X,Y) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) active#(add(s(X),Y)) -> add#(X,Y) -> add#(X1,mark(X2)) -> add#(X1,X2) active#(add(s(X),Y)) -> add#(X,Y) -> add#(mark(X1),X2) -> add#(X1,X2) active#(add(s(X),Y)) -> s#(add(X,Y)) -> s#(ok(X)) -> s#(X) active#(add(s(X),Y)) -> s#(add(X,Y)) -> s#(mark(X)) -> s#(X) active#(add(X1,X2)) -> add#(active(X1),X2) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) active#(add(X1,X2)) -> add#(active(X1),X2) -> add#(X1,mark(X2)) -> add#(X1,X2) active#(add(X1,X2)) -> add#(active(X1),X2) -> add#(mark(X1),X2) -> add#(X1,X2) active#(add(X1,X2)) -> add#(X1,active(X2)) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) active#(add(X1,X2)) -> add#(X1,active(X2)) -> add#(X1,mark(X2)) -> add#(X1,X2) active#(add(X1,X2)) -> add#(X1,active(X2)) -> add#(mark(X1),X2) -> add#(X1,X2) active#(add(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(add(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(add(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> active#(X2) -> active#(p(X)) -> p#(active(X)) active#(add(X1,X2)) -> active#(X2) -> active#(p(X)) -> active#(X) active#(add(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(add(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(add(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(add(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(add(X1,X2)) -> active#(X2) -> active#(zero(X)) -> zero#(active(X)) active#(add(X1,X2)) -> active#(X2) -> active#(zero(X)) -> active#(X) active#(add(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(add(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> active#(X1) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> fact#(active(X)) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> active#(X) active#(add(X1,X2)) -> active#(X2) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(add(X1,X2)) -> active#(X2) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(add(X1,X2)) -> active#(X2) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(add(X1,X2)) -> active#(X2) -> active#(add(s(X),Y)) -> add#(X,Y) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> zero#(X) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> s#(0()) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> fact#(p(X)) active#(add(X1,X2)) -> active#(X2) -> active#(fact(X)) -> p#(X) active#(add(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(add(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(add(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(add(X1,X2)) -> active#(X1) -> active#(p(X)) -> active#(X) active#(add(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(add(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X2) active#(add(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(add(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(add(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(add(X1,X2)) -> active#(X1) -> active#(zero(X)) -> zero#(active(X)) active#(add(X1,X2)) -> active#(X1) -> active#(zero(X)) -> active#(X) active#(add(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(add(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> fact#(active(X)) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> active#(X) active#(add(X1,X2)) -> active#(X1) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(add(X1,X2)) -> active#(X1) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(add(X1,X2)) -> active#(X1) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(add(X1,X2)) -> active#(X1) -> active#(add(s(X),Y)) -> add#(X,Y) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> zero#(X) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> s#(0()) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> fact#(p(X)) active#(add(X1,X2)) -> active#(X1) -> active#(fact(X)) -> p#(X) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(p(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(zero(X)) -> zero#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(zero(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> fact#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(add(s(X),Y)) -> add#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> zero#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> s#(0()) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> fact#(p(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(fact(X)) -> p#(X) active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) -> add#(ok(X1),ok(X2)) -> add#(X1,X2) active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) -> add#(X1,mark(X2)) -> add#(X1,X2) active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) -> add#(mark(X1),X2) -> add#(X1,X2) active#(prod(s(X),Y)) -> prod#(X,Y) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) active#(prod(s(X),Y)) -> prod#(X,Y) -> prod#(X1,mark(X2)) -> prod#(X1,X2) active#(prod(s(X),Y)) -> prod#(X,Y) -> prod#(mark(X1),X2) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(active(X1),X2) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(active(X1),X2) -> prod#(X1,mark(X2)) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(active(X1),X2) -> prod#(mark(X1),X2) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(X1,active(X2)) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(X1,active(X2)) -> prod#(X1,mark(X2)) -> prod#(X1,X2) active#(prod(X1,X2)) -> prod#(X1,active(X2)) -> prod#(mark(X1),X2) -> prod#(X1,X2) active#(prod(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(prod(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(prod(X1,X2)) -> active#(X2) -> active#(add(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> active#(X2) -> active#(p(X)) -> p#(active(X)) active#(prod(X1,X2)) -> active#(X2) -> active#(p(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(prod(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X2) -> active#(zero(X)) -> zero#(active(X)) active#(prod(X1,X2)) -> active#(X2) -> active#(zero(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(prod(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> active#(X1) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> fact#(active(X)) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(prod(X1,X2)) -> active#(X2) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(prod(X1,X2)) -> active#(X2) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(prod(X1,X2)) -> active#(X2) -> active#(add(s(X),Y)) -> add#(X,Y) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> zero#(X) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> s#(0()) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> fact#(p(X)) active#(prod(X1,X2)) -> active#(X2) -> active#(fact(X)) -> p#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(prod(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(prod(X1,X2)) -> active#(X1) -> active#(add(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(prod(X1,X2)) -> active#(X1) -> active#(p(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X2) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(prod(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(zero(X)) -> zero#(active(X)) active#(prod(X1,X2)) -> active#(X1) -> active#(zero(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(prod(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> fact#(active(X)) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(prod(X1,X2)) -> active#(X1) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(prod(X1,X2)) -> active#(X1) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(prod(X1,X2)) -> active#(X1) -> active#(add(s(X),Y)) -> add#(X,Y) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> zero#(X) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> s#(0()) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> fact#(p(X)) active#(prod(X1,X2)) -> active#(X1) -> active#(fact(X)) -> p#(X) active#(p(X)) -> p#(active(X)) -> p#(ok(X)) -> p#(X) active#(p(X)) -> p#(active(X)) -> p#(mark(X)) -> p#(X) active#(p(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(p(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2) active#(p(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(p(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(p(X)) -> active#(X) -> active#(p(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(p(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X2) active#(p(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(p(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(p(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(zero(X)) -> zero#(active(X)) active#(p(X)) -> active#(X) -> active#(zero(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(p(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(fact(X)) -> fact#(active(X)) active#(p(X)) -> active#(X) -> active#(fact(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(p(X)) -> active#(X) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(p(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(p(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y) active#(p(X)) -> active#(X) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(p(X)) -> active#(X) -> active#(fact(X)) -> zero#(X) active#(p(X)) -> active#(X) -> active#(fact(X)) -> s#(0()) active#(p(X)) -> active#(X) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(p(X)) -> active#(X) -> active#(fact(X)) -> fact#(p(X)) active#(p(X)) -> active#(X) -> active#(fact(X)) -> p#(X) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(s(X)) -> active#(X) -> active#(p(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(zero(X)) -> zero#(active(X)) active#(s(X)) -> active#(X) -> active#(zero(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(fact(X)) -> fact#(active(X)) active#(s(X)) -> active#(X) -> active#(fact(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(s(X)) -> active#(X) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(s(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(s(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y) active#(s(X)) -> active#(X) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(s(X)) -> active#(X) -> active#(fact(X)) -> zero#(X) active#(s(X)) -> active#(X) -> active#(fact(X)) -> s#(0()) active#(s(X)) -> active#(X) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(s(X)) -> active#(X) -> active#(fact(X)) -> fact#(p(X)) active#(s(X)) -> active#(X) -> active#(fact(X)) -> p#(X) active#(zero(X)) -> zero#(active(X)) -> zero#(ok(X)) -> zero#(X) active#(zero(X)) -> zero#(active(X)) -> zero#(mark(X)) -> zero#(X) active#(zero(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(zero(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2) active#(zero(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(zero(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1) active#(zero(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(zero(X)) -> active#(X) -> active#(p(X)) -> active#(X) active#(zero(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(zero(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X2) active#(zero(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(zero(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X1) active#(zero(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(zero(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(zero(X)) -> active#(X) -> active#(zero(X)) -> zero#(active(X)) active#(zero(X)) -> active#(X) -> active#(zero(X)) -> active#(X) active#(zero(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(zero(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> fact#(active(X)) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> active#(X) active#(zero(X)) -> active#(X) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(zero(X)) -> active#(X) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(zero(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(zero(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> zero#(X) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> s#(0()) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> fact#(p(X)) active#(zero(X)) -> active#(X) -> active#(fact(X)) -> p#(X) active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(fact(X)) -> zero#(X) -> zero#(ok(X)) -> zero#(X) active#(fact(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X) active#(fact(X)) -> s#(0()) -> s#(ok(X)) -> s#(X) active#(fact(X)) -> s#(0()) -> s#(mark(X)) -> s#(X) active#(fact(X)) -> prod#(X,fact(p(X))) -> prod#(ok(X1),ok(X2)) -> prod#(X1,X2) active#(fact(X)) -> prod#(X,fact(p(X))) -> prod#(X1,mark(X2)) -> prod#(X1,X2) active#(fact(X)) -> prod#(X,fact(p(X))) -> prod#(mark(X1),X2) -> prod#(X1,X2) active#(fact(X)) -> fact#(p(X)) -> fact#(ok(X)) -> fact#(X) active#(fact(X)) -> fact#(p(X)) -> fact#(mark(X)) -> fact#(X) active#(fact(X)) -> fact#(active(X)) -> fact#(ok(X)) -> fact#(X) active#(fact(X)) -> fact#(active(X)) -> fact#(mark(X)) -> fact#(X) active#(fact(X)) -> p#(X) -> p#(ok(X)) -> p#(X) active#(fact(X)) -> p#(X) -> p#(mark(X)) -> p#(X) active#(fact(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(X1,active(X2)) active#(fact(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2) active#(fact(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(active(X1),X2) active#(fact(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1) active#(fact(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(fact(X)) -> active#(X) -> active#(p(X)) -> active#(X) active#(fact(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(X1,active(X2)) active#(fact(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X2) active#(fact(X)) -> active#(X) -> active#(prod(X1,X2)) -> prod#(active(X1),X2) active#(fact(X)) -> active#(X) -> active#(prod(X1,X2)) -> active#(X1) active#(fact(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(fact(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(fact(X)) -> active#(X) -> active#(zero(X)) -> zero#(active(X)) active#(fact(X)) -> active#(X) -> active#(zero(X)) -> active#(X) active#(fact(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(fact(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> fact#(active(X)) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> active#(X) active#(fact(X)) -> active#(X) -> active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) active#(fact(X)) -> active#(X) -> active#(prod(s(X),Y)) -> prod#(X,Y) active#(fact(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y)) active#(fact(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> zero#(X) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> s#(0()) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> prod#(X,fact(p(X))) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> fact#(p(X)) active#(fact(X)) -> active#(X) -> active#(fact(X)) -> p#(X) SCC Processor: #sccs: 10 #rules: 38 #arcs: 604/4356 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Open DPs: active#(fact(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) active#(zero(X)) -> active#(X) active#(s(X)) -> active#(X) active#(prod(X1,X2)) -> active#(X1) active#(prod(X1,X2)) -> active#(X2) active#(p(X)) -> active#(X) active#(add(X1,X2)) -> active#(X1) active#(add(X1,X2)) -> active#(X2) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(active#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(fact(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(zero(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(prod(X1,X2)) -> proper#(X2) proper#(prod(X1,X2)) -> proper#(X1) proper#(p(X)) -> proper#(X) proper#(add(X1,X2)) -> proper#(X2) proper#(add(X1,X2)) -> proper#(X1) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(proper#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: add#(mark(X1),X2) -> add#(X1,X2) add#(X1,mark(X2)) -> add#(X1,X2) add#(ok(X1),ok(X2)) -> add#(X1,X2) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(add#) = 1 problem: DPs: add#(mark(X1),X2) -> add#(X1,X2) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(add#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: p#(mark(X)) -> p#(X) p#(ok(X)) -> p#(X) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(p#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: prod#(mark(X1),X2) -> prod#(X1,X2) prod#(X1,mark(X2)) -> prod#(X1,X2) prod#(ok(X1),ok(X2)) -> prod#(X1,X2) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(prod#) = 1 problem: DPs: prod#(mark(X1),X2) -> prod#(X1,X2) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(prod#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(s#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: zero#(mark(X)) -> zero#(X) zero#(ok(X)) -> zero#(X) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(zero#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(if#) = 2 problem: DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(if#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: fact#(mark(X)) -> fact#(X) fact#(ok(X)) -> fact#(X) TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(fact#) = 0 problem: DPs: TRS: active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X))))) active(add(0(),X)) -> mark(X) active(add(s(X),Y)) -> mark(s(add(X,Y))) active(prod(0(),X)) -> mark(0()) active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(zero(0())) -> mark(true()) active(zero(s(X))) -> mark(false()) active(p(s(X))) -> mark(X) active(fact(X)) -> fact(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(zero(X)) -> zero(active(X)) active(s(X)) -> s(active(X)) active(prod(X1,X2)) -> prod(active(X1),X2) active(prod(X1,X2)) -> prod(X1,active(X2)) active(p(X)) -> p(active(X)) active(add(X1,X2)) -> add(active(X1),X2) active(add(X1,X2)) -> add(X1,active(X2)) fact(mark(X)) -> mark(fact(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) zero(mark(X)) -> mark(zero(X)) s(mark(X)) -> mark(s(X)) prod(mark(X1),X2) -> mark(prod(X1,X2)) prod(X1,mark(X2)) -> mark(prod(X1,X2)) p(mark(X)) -> mark(p(X)) add(mark(X1),X2) -> mark(add(X1,X2)) add(X1,mark(X2)) -> mark(add(X1,X2)) proper(fact(X)) -> fact(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(zero(X)) -> zero(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(prod(X1,X2)) -> prod(proper(X1),proper(X2)) proper(p(X)) -> p(proper(X)) proper(add(X1,X2)) -> add(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) fact(ok(X)) -> ok(fact(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) zero(ok(X)) -> ok(zero(X)) s(ok(X)) -> ok(s(X)) prod(ok(X1),ok(X2)) -> ok(prod(X1,X2)) p(ok(X)) -> ok(p(X)) add(ok(X1),ok(X2)) -> ok(add(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed