MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) U31(tt()) -> 0() U41(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(N,0()) -> U11(isNat(N),N) plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(N,0()) -> U31(isNat(N)) x(N,s(M)) -> U41(and(isNat(M),n__isNat(N)),M,N) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1 ,n__x/2,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,U41,activate,and,isNat,plus,s ,x} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. plus(N,0()) -> U11(isNat(N),N) plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N) x(N,0()) -> U31(isNat(N)) x(N,s(M)) -> U41(and(isNat(M),n__isNat(N)),M,N) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) U31(tt()) -> 0() U41(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1 ,n__x/2,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,U41,activate,and,isNat,plus,s ,x} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 0#() -> c_1() U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U31#(tt()) -> c_4(0#()) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_6() activate#(n__0()) -> c_7(0#()) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(X) -> c_13() isNat#(n__0()) -> c_14() isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U31#(tt()) -> c_4(0#()) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_6() activate#(n__0()) -> c_7(0#()) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(X) -> c_13() isNat#(n__0()) -> c_14() isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() - Weak TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) U31(tt()) -> 0() U41(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/4,c_4/1,c_5/5,c_6/0,c_7/1,c_8/1,c_9/3,c_10/2,c_11/3,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) 0#() -> c_1() U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U31#(tt()) -> c_4(0#()) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_6() activate#(n__0()) -> c_7(0#()) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(X) -> c_13() isNat#(n__0()) -> c_14() isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U31#(tt()) -> c_4(0#()) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_6() activate#(n__0()) -> c_7(0#()) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(X) -> c_13() isNat#(n__0()) -> c_14() isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/4,c_4/1,c_5/5,c_6/0,c_7/1,c_8/1,c_9/3,c_10/2,c_11/3,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,13,14,18,19,20} by application of Pre({1,6,13,14,18,19,20}) = {2,3,4,5,7,8,9,10,11,12,15,16,17}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: U11#(tt(),N) -> c_2(activate#(N)) 3: U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) 4: U31#(tt()) -> c_4(0#()) 5: U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) 6: activate#(X) -> c_6() 7: activate#(n__0()) -> c_7(0#()) 8: activate#(n__isNat(X)) -> c_8(isNat#(X)) 9: activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 10: activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) 11: activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 12: and#(tt(),X) -> c_12(activate#(X)) 13: isNat#(X) -> c_13() 14: isNat#(n__0()) -> c_14() 15: isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 16: isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) 17: isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 18: plus#(X1,X2) -> c_18() 19: s#(X) -> c_19() 20: x#(X1,X2) -> c_20() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U31#(tt()) -> c_4(0#()) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__0()) -> c_7(0#()) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_6() isNat#(X) -> c_13() isNat#(n__0()) -> c_14() plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/4,c_4/1,c_5/5,c_6/0,c_7/1,c_8/1,c_9/3,c_10/2,c_11/3,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,5} by application of Pre({3,5}) = {1,2,4,7,8,9,10,11,12,13}. Here rules are labelled as follows: 1: U11#(tt(),N) -> c_2(activate#(N)) 2: U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) 3: U31#(tt()) -> c_4(0#()) 4: U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) 5: activate#(n__0()) -> c_7(0#()) 6: activate#(n__isNat(X)) -> c_8(isNat#(X)) 7: activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) 9: activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 10: and#(tt(),X) -> c_12(activate#(X)) 11: isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 12: isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) 13: isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 14: 0#() -> c_1() 15: activate#(X) -> c_6() 16: isNat#(X) -> c_13() 17: isNat#(n__0()) -> c_14() 18: plus#(X1,X2) -> c_18() 19: s#(X) -> c_19() 20: x#(X1,X2) -> c_20() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() U31#(tt()) -> c_4(0#()) activate#(X) -> c_6() activate#(n__0()) -> c_7(0#()) isNat#(X) -> c_13() isNat#(n__0()) -> c_14() plus#(X1,X2) -> c_18() s#(X) -> c_19() x#(X1,X2) -> c_20() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/4,c_4/1,c_5/5,c_6/0,c_7/1,c_8/1,c_9/3,c_10/2,c_11/3,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__0()) -> c_7(0#()):15 -->_1 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 activate#(X) -> c_6():14 2:S:U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) -->_4 activate#(n__0()) -> c_7(0#()):15 -->_3 activate#(n__0()) -> c_7(0#()):15 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 s#(X) -> c_19():19 -->_2 plus#(X1,X2) -> c_18():18 -->_4 activate#(X) -> c_6():14 -->_3 activate#(X) -> c_6():14 3:S:U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) -->_5 activate#(n__0()) -> c_7(0#()):15 -->_4 activate#(n__0()) -> c_7(0#()):15 -->_3 activate#(n__0()) -> c_7(0#()):15 -->_5 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_5 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_5 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_5 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 x#(X1,X2) -> c_20():20 -->_1 plus#(X1,X2) -> c_18():18 -->_5 activate#(X) -> c_6():14 -->_4 activate#(X) -> c_6():14 -->_3 activate#(X) -> c_6():14 4:S:activate#(n__isNat(X)) -> c_8(isNat#(X)) -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 isNat#(n__0()) -> c_14():17 -->_1 isNat#(X) -> c_13():16 5:S:activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__0()) -> c_7(0#()):15 -->_2 activate#(n__0()) -> c_7(0#()):15 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_1 plus#(X1,X2) -> c_18():18 -->_3 activate#(X) -> c_6():14 -->_2 activate#(X) -> c_6():14 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 6:S:activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) -->_2 activate#(n__0()) -> c_7(0#()):15 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_1 s#(X) -> c_19():19 -->_2 activate#(X) -> c_6():14 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 7:S:activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__0()) -> c_7(0#()):15 -->_2 activate#(n__0()) -> c_7(0#()):15 -->_1 x#(X1,X2) -> c_20():20 -->_3 activate#(X) -> c_6():14 -->_2 activate#(X) -> c_6():14 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 8:S:and#(tt(),X) -> c_12(activate#(X)) -->_1 activate#(n__0()) -> c_7(0#()):15 -->_1 activate#(X) -> c_6():14 -->_1 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 9:S:isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__0()) -> c_7(0#()):15 -->_3 activate#(n__0()) -> c_7(0#()):15 -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__0()) -> c_14():17 -->_2 isNat#(X) -> c_13():16 -->_4 activate#(X) -> c_6():14 -->_3 activate#(X) -> c_6():14 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 10:S:isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) -->_2 activate#(n__0()) -> c_7(0#()):15 -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__0()) -> c_14():17 -->_1 isNat#(X) -> c_13():16 -->_2 activate#(X) -> c_6():14 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 11:S:isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__0()) -> c_7(0#()):15 -->_3 activate#(n__0()) -> c_7(0#()):15 -->_2 isNat#(n__0()) -> c_14():17 -->_2 isNat#(X) -> c_13():16 -->_4 activate#(X) -> c_6():14 -->_3 activate#(X) -> c_6():14 -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 12:W:0#() -> c_1() 13:W:U31#(tt()) -> c_4(0#()) -->_1 0#() -> c_1():12 14:W:activate#(X) -> c_6() 15:W:activate#(n__0()) -> c_7(0#()) -->_1 0#() -> c_1():12 16:W:isNat#(X) -> c_13() 17:W:isNat#(n__0()) -> c_14() 18:W:plus#(X1,X2) -> c_18() 19:W:s#(X) -> c_19() 20:W:x#(X1,X2) -> c_20() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: U31#(tt()) -> c_4(0#()) 16: isNat#(X) -> c_13() 17: isNat#(n__0()) -> c_14() 18: plus#(X1,X2) -> c_18() 19: s#(X) -> c_19() 14: activate#(X) -> c_6() 20: x#(X1,X2) -> c_20() 15: activate#(n__0()) -> c_7(0#()) 12: 0#() -> c_1() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/4,c_4/1,c_5/5,c_6/0,c_7/1,c_8/1,c_9/3,c_10/2,c_11/3,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 2:S:U21#(tt(),M,N) -> c_3(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 3:S:U41#(tt(),M,N) -> c_5(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) -->_5 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_5 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_5 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_5 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 4:S:activate#(n__isNat(X)) -> c_8(isNat#(X)) -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 5:S:activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 6:S:activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)) -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 7:S:activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 8:S:and#(tt(),X) -> c_12(activate#(X)) -->_1 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 9:S:isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 10:S:isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 11:S:isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(x#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(s#(activate(X)),activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: U21#(tt(),M,N) -> c_3(activate#(N),activate#(M)) U41#(tt(),M,N) -> c_5(activate#(N),activate#(M),activate#(N)) activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(activate#(X)) activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)) * Step 8: RemoveHeads MAYBE + Considered Problem: - Strict DPs: U11#(tt(),N) -> c_2(activate#(N)) U21#(tt(),M,N) -> c_3(activate#(N),activate#(M)) U41#(tt(),M,N) -> c_5(activate#(N),activate#(M),activate#(N)) activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(activate#(X)) activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/2,c_4/1,c_5/3,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/2,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 2:S:U21#(tt(),M,N) -> c_3(activate#(N),activate#(M)) -->_2 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 3:S:U41#(tt(),M,N) -> c_5(activate#(N),activate#(M),activate#(N)) -->_3 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_2 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_3 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_2 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_3 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_2 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 4:S:activate#(n__isNat(X)) -> c_8(isNat#(X)) -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 5:S:activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)) -->_2 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 6:S:activate#(n__s(X)) -> c_10(activate#(X)) -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 7:S:activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)) -->_2 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 8:S:and#(tt(),X) -> c_12(activate#(X)) -->_1 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_1 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_1 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_1 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 9:S:isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 10:S:isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_1 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_2 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_2 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_2 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 11:S:isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_2 isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)):10 -->_2 isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 and#(tt(),X) -> c_12(activate#(X)):8 -->_4 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_3 activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)):7 -->_4 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_3 activate#(n__s(X)) -> c_10(activate#(X)):6 -->_4 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_3 activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)):5 -->_4 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_8(isNat#(X)):4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(1,U11#(tt(),N) -> c_2(activate#(N))) ,(2,U21#(tt(),M,N) -> c_3(activate#(N),activate#(M))) ,(3,U41#(tt(),M,N) -> c_5(activate#(N),activate#(M),activate#(N)))] * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__isNat(X)) -> c_8(isNat#(X)) activate#(n__plus(X1,X2)) -> c_9(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_10(activate#(X)) activate#(n__x(X1,X2)) -> c_11(activate#(X1),activate#(X2)) and#(tt(),X) -> c_12(activate#(X)) isNat#(n__plus(V1,V2)) -> c_15(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_16(isNat#(activate(V1)),activate#(V1)) isNat#(n__x(V1,V2)) -> c_17(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(n__x(X1,X2)) -> x(activate(X1),activate(X2)) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) isNat(n__x(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/2,U21/3,U31/1,U41/3,activate/1,and/2,isNat/1,plus/2,s/1,x/2,0#/0,U11#/2,U21#/3,U31#/1,U41#/3 ,activate#/1,and#/2,isNat#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0 ,c_2/1,c_3/2,c_4/1,c_5/3,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/2,c_12/1,c_13/0,c_14/0,c_15/4,c_16/2,c_17/4 ,c_18/0,c_19/0,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,U41#,activate#,and#,isNat#,plus#,s# ,x#} and constructors {n__0,n__isNat,n__plus,n__s,n__x,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE