MAYBE Problem: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Proof: DP Processor: DPs: fact#(X) -> zero#(X) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add#(s(X),Y) -> add#(X,Y) add#(s(X),Y) -> s#(add(X,Y)) prod#(s(X),Y) -> prod#(X,Y) prod#(s(X),Y) -> add#(Y,prod(X,Y)) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__fact(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> p#(activate(X)) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X TDG Processor: DPs: fact#(X) -> zero#(X) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add#(s(X),Y) -> add#(X,Y) add#(s(X),Y) -> s#(add(X,Y)) prod#(s(X),Y) -> prod#(X,Y) prod#(s(X),Y) -> add#(Y,prod(X,Y)) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__0()) -> 0#() activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__fact(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> p#(activate(X)) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X graph: activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__p(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__fact(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__p(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__fact(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__prod(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) -> prod#(s(X),Y) -> add#(Y,prod(X,Y)) activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) -> prod#(s(X),Y) -> prod#(X,Y) activate#(n__fact(X)) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__fact(X)) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) activate#(n__fact(X)) -> activate#(X) -> activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__fact(X)) -> activate#(X) -> activate#(n__fact(X)) -> activate#(X) activate#(n__fact(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__fact(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__fact(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__fact(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__fact(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__fact(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) -> fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) activate#(n__fact(X)) -> fact#(activate(X)) -> fact#(X) -> zero#(X) activate#(n__p(X)) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__p(X)) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> activate#(X) -> activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__p(X)) -> activate#(X) -> activate#(n__fact(X)) -> activate#(X) activate#(n__p(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__p(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__p(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__p(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__p(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__fact(X)) -> fact#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__fact(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) prod#(s(X),Y) -> prod#(X,Y) -> prod#(s(X),Y) -> add#(Y,prod(X,Y)) prod#(s(X),Y) -> prod#(X,Y) -> prod#(s(X),Y) -> prod#(X,Y) prod#(s(X),Y) -> add#(Y,prod(X,Y)) -> add#(s(X),Y) -> s#(add(X,Y)) prod#(s(X),Y) -> add#(Y,prod(X,Y)) -> add#(s(X),Y) -> add#(X,Y) add#(s(X),Y) -> add#(X,Y) -> add#(s(X),Y) -> s#(add(X,Y)) add#(s(X),Y) -> add#(X,Y) -> add#(s(X),Y) -> add#(X,Y) if#(false(),X,Y) -> activate#(Y) -> activate#(n__p(X)) -> p#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__fact(X)) -> fact#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__fact(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__prod(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__prod(X1,X2)) -> activate#(X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__0()) -> 0#() if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__fact(X)) -> fact#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__fact(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__prod(X1,X2)) -> prod#(activate(X1),activate(X2)) if#(true(),X,Y) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__prod(X1,X2)) -> activate#(X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__0()) -> 0#() if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) -> if#(false(),X,Y) -> activate#(Y) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) -> if#(true(),X,Y) -> activate#(X) SCC Processor: #sccs: 3 #rules: 11 #arcs: 82/324 DPs: activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__fact(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) -> activate#(X) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = x0 + 0, [if#](x0, x1, x2) = x0 + x1 + x2 + 0, [fact#](x0) = 4x0 + 4, [p](x0) = x0 + 0, [false] = 1, [activate](x0) = x0 + 0, [true] = 0, [prod](x0, x1) = x0 + x1 + 0, [s](x0) = x0 + 0, [add](x0, x1) = x0 + x1 + 0, [0] = 1, [if](x0, x1, x2) = x1 + x2 + 0, [n__prod](x0, x1) = x0 + x1 + 0, [n__fact](x0) = 4x0 + 4, [n__p](x0) = x0 + 0, [n__s](x0) = x0 + 0, [n__0] = 1, [zero](x0) = 1, [fact](x0) = 4x0 + 4 orientation: activate#(n__prod(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = activate#(X2) activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__prod(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = activate#(X1) activate#(n__fact(X)) = 4X + 4 >= X + 0 = activate#(X) activate#(n__fact(X)) = 4X + 4 >= 4X + 4 = fact#(activate(X)) fact#(X) = 4X + 4 >= 4X + 4 = if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) = X + Y + 0 >= X + 0 = activate#(X) activate#(n__p(X)) = X + 0 >= X + 0 = activate#(X) if#(false(),X,Y) = X + Y + 1 >= Y + 0 = activate#(Y) fact(X) = 4X + 4 >= 4X + 4 = if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) = X + 1 >= X = X add(s(X),Y) = X + Y + 0 >= X + Y + 0 = s(add(X,Y)) prod(0(),X) = X + 1 >= 1 = 0() prod(s(X),Y) = X + Y + 0 >= X + Y + 0 = add(Y,prod(X,Y)) if(true(),X,Y) = X + Y + 0 >= X + 0 = activate(X) if(false(),X,Y) = X + Y + 0 >= Y + 0 = activate(Y) zero(0()) = 1 >= 0 = true() zero(s(X)) = 1 >= 1 = false() p(s(X)) = X + 0 >= X = X s(X) = X + 0 >= X + 0 = n__s(X) 0() = 1 >= 1 = n__0() prod(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__prod(X1,X2) fact(X) = 4X + 4 >= 4X + 4 = n__fact(X) p(X) = X + 0 >= X + 0 = n__p(X) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__0()) = 1 >= 1 = 0() activate(n__prod(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = prod(activate(X1),activate(X2)) activate(n__fact(X)) = 4X + 4 >= 4X + 4 = fact(activate(X)) activate(n__p(X)) = X + 0 >= X + 0 = p(activate(X)) activate(X) = X + 0 >= X = X problem: DPs: activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__prod(X1,X2)) -> activate#(X1) activate#(n__fact(X)) -> fact#(activate(X)) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) -> activate#(X) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = 6x0, [if#](x0, x1, x2) = 1x0 + 6x1 + 6x2, [fact#](x0) = 7x0 + 6, [p](x0) = x0, [false] = 3, [activate](x0) = x0, [true] = 1, [prod](x0, x1) = 1x0 + x1, [s](x0) = x0 + 0, [add](x0, x1) = x1 + 0, [0] = 0, [if](x0, x1, x2) = x1 + x2, [n__prod](x0, x1) = 1x0 + x1, [n__fact](x0) = 1x0 + 0, [n__p](x0) = x0, [n__s](x0) = x0 + 0, [n__0] = 0, [zero](x0) = 3x0, [fact](x0) = 1x0 + 0 orientation: activate#(n__prod(X1,X2)) = 7X1 + 6X2 >= 6X2 = activate#(X2) activate#(n__s(X)) = 6X + 6 >= 6X = activate#(X) activate#(n__prod(X1,X2)) = 7X1 + 6X2 >= 6X1 = activate#(X1) activate#(n__fact(X)) = 7X + 6 >= 7X + 6 = fact#(activate(X)) fact#(X) = 7X + 6 >= 7X + 6 = if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) = 6X + 6Y + 2 >= 6X = activate#(X) activate#(n__p(X)) = 6X >= 6X = activate#(X) if#(false(),X,Y) = 6X + 6Y + 4 >= 6Y = activate#(Y) fact(X) = 1X + 0 >= 1X + 0 = if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) = X + 0 >= X = X add(s(X),Y) = Y + 0 >= Y + 0 = s(add(X,Y)) prod(0(),X) = X + 1 >= 0 = 0() prod(s(X),Y) = 1X + Y + 1 >= 1X + Y + 0 = add(Y,prod(X,Y)) if(true(),X,Y) = X + Y >= X = activate(X) if(false(),X,Y) = X + Y >= Y = activate(Y) zero(0()) = 3 >= 1 = true() zero(s(X)) = 3X + 3 >= 3 = false() p(s(X)) = X + 0 >= X = X s(X) = X + 0 >= X + 0 = n__s(X) 0() = 0 >= 0 = n__0() prod(X1,X2) = 1X1 + X2 >= 1X1 + X2 = n__prod(X1,X2) fact(X) = 1X + 0 >= 1X + 0 = n__fact(X) p(X) = X >= X = n__p(X) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__0()) = 0 >= 0 = 0() activate(n__prod(X1,X2)) = 1X1 + X2 >= 1X1 + X2 = prod(activate(X1),activate(X2)) activate(n__fact(X)) = 1X + 0 >= 1X + 0 = fact(activate(X)) activate(n__p(X)) = X >= X = p(activate(X)) activate(X) = X >= X = X problem: DPs: activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) -> activate#(X) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = x0 + 0, [if#](x0, x1, x2) = 1x1 + x2 + 1, [fact#](x0) = x0 + 1, [p](x0) = x0, [false] = 0, [activate](x0) = x0, [true] = 0, [prod](x0, x1) = x0 + x1, [s](x0) = x0 + 0, [add](x0, x1) = x0 + x1 + 0, [0] = 0, [if](x0, x1, x2) = x0 + x1 + x2, [n__prod](x0, x1) = x0 + x1, [n__fact](x0) = x0 + 1, [n__p](x0) = x0, [n__s](x0) = x0 + 0, [n__0] = 0, [zero](x0) = x0, [fact](x0) = x0 + 1 orientation: activate#(n__prod(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = activate#(X2) activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__fact(X)) = X + 1 >= X + 1 = fact#(activate(X)) fact#(X) = X + 1 >= X + 1 = if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(true(),X,Y) = 1X + Y + 1 >= X + 0 = activate#(X) activate#(n__p(X)) = X + 0 >= X + 0 = activate#(X) if#(false(),X,Y) = 1X + Y + 1 >= Y + 0 = activate#(Y) fact(X) = X + 1 >= X + 1 = if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) = X + 0 >= X = X add(s(X),Y) = X + Y + 0 >= X + Y + 0 = s(add(X,Y)) prod(0(),X) = X + 0 >= 0 = 0() prod(s(X),Y) = X + Y + 0 >= X + Y + 0 = add(Y,prod(X,Y)) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) zero(0()) = 0 >= 0 = true() zero(s(X)) = X + 0 >= 0 = false() p(s(X)) = X + 0 >= X = X s(X) = X + 0 >= X + 0 = n__s(X) 0() = 0 >= 0 = n__0() prod(X1,X2) = X1 + X2 >= X1 + X2 = n__prod(X1,X2) fact(X) = X + 1 >= X + 1 = n__fact(X) p(X) = X >= X = n__p(X) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__0()) = 0 >= 0 = 0() activate(n__prod(X1,X2)) = X1 + X2 >= X1 + X2 = prod(activate(X1),activate(X2)) activate(n__fact(X)) = X + 1 >= X + 1 = fact(activate(X)) activate(n__p(X)) = X >= X = p(activate(X)) activate(X) = X >= X = X problem: DPs: activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = x0, [if#](x0, x1, x2) = 4x1 + x2, [fact#](x0) = 5, [p](x0) = 7x0, [false] = 0, [activate](x0) = x0, [true] = 0, [prod](x0, x1) = x1 + 0, [s](x0) = x0 + 0, [add](x0, x1) = x0 + x1, [0] = 0, [if](x0, x1, x2) = x1 + x2 + 0, [n__prod](x0, x1) = x1 + 0, [n__fact](x0) = 5, [n__p](x0) = 7x0, [n__s](x0) = x0 + 0, [n__0] = 0, [zero](x0) = x0 + 0, [fact](x0) = 5 orientation: activate#(n__prod(X1,X2)) = X2 + 0 >= X2 = activate#(X2) activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__fact(X)) = 5 >= 5 = fact#(activate(X)) fact#(X) = 5 >= 5 = if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) activate#(n__p(X)) = 7X >= X = activate#(X) if#(false(),X,Y) = 4X + Y >= Y = activate#(Y) fact(X) = 5 >= 5 = if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) = X + 0 >= X = X add(s(X),Y) = X + Y + 0 >= X + Y + 0 = s(add(X,Y)) prod(0(),X) = X + 0 >= 0 = 0() prod(s(X),Y) = Y + 0 >= Y + 0 = add(Y,prod(X,Y)) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) zero(0()) = 0 >= 0 = true() zero(s(X)) = X + 0 >= 0 = false() p(s(X)) = 7X + 7 >= X = X s(X) = X + 0 >= X + 0 = n__s(X) 0() = 0 >= 0 = n__0() prod(X1,X2) = X2 + 0 >= X2 + 0 = n__prod(X1,X2) fact(X) = 5 >= 5 = n__fact(X) p(X) = 7X >= 7X = n__p(X) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__0()) = 0 >= 0 = 0() activate(n__prod(X1,X2)) = X2 + 0 >= X2 + 0 = prod(activate(X1),activate(X2)) activate(n__fact(X)) = 5 >= 5 = fact(activate(X)) activate(n__p(X)) = 7X >= 7X = p(activate(X)) activate(X) = X >= X = X problem: DPs: activate#(n__prod(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__fact(X)) -> fact#(activate(X)) fact#(X) -> if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) if#(false(),X,Y) -> activate#(Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Open DPs: prod#(s(X),Y) -> prod#(X,Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(prod#) = 0 problem: DPs: TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Qed DPs: add#(s(X),Y) -> add#(X,Y) TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(add#) = 0 problem: DPs: TRS: fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) prod(0(),X) -> 0() prod(s(X),Y) -> add(Y,prod(X,Y)) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) zero(0()) -> true() zero(s(X)) -> false() p(s(X)) -> X s(X) -> n__s(X) 0() -> n__0() prod(X1,X2) -> n__prod(X1,X2) fact(X) -> n__fact(X) p(X) -> n__p(X) activate(n__s(X)) -> s(activate(X)) activate(n__0()) -> 0() activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2)) activate(n__fact(X)) -> fact(activate(X)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Qed