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))) 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)) 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)) 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) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,activate,and,isNat,plus ,s} and constructors {n__0,n__isNat,n__plus,n__s,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) 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))) 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,activate,and,isNat,plus ,s} and constructors {n__0,n__isNat,n__plus,n__s,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)) activate#(X) -> c_4() activate#(n__0()) -> c_5(0#()) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(X) -> c_10() isNat#(n__0()) -> c_11() isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) plus#(X1,X2) -> c_14() s#(X) -> c_15() 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)) activate#(X) -> c_4() activate#(n__0()) -> c_5(0#()) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(X) -> c_10() isNat#(n__0()) -> c_11() isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) plus#(X1,X2) -> c_14() s#(X) -> c_15() - Weak TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/4,c_4/0,c_5/1,c_6/1,c_7/3,c_8/2,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) 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)) activate#(X) -> c_4() activate#(n__0()) -> c_5(0#()) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(X) -> c_10() isNat#(n__0()) -> c_11() isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) plus#(X1,X2) -> c_14() s#(X) -> c_15() * 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)) activate#(X) -> c_4() activate#(n__0()) -> c_5(0#()) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(X) -> c_10() isNat#(n__0()) -> c_11() isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) plus#(X1,X2) -> c_14() s#(X) -> c_15() - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/4,c_4/0,c_5/1,c_6/1,c_7/3,c_8/2,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,10,11,14,15} by application of Pre({1,4,10,11,14,15}) = {2,3,5,6,7,8,9,12,13}. 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: activate#(X) -> c_4() 5: activate#(n__0()) -> c_5(0#()) 6: activate#(n__isNat(X)) -> c_6(isNat#(X)) 7: activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) 9: and#(tt(),X) -> c_9(activate#(X)) 10: isNat#(X) -> c_10() 11: isNat#(n__0()) -> c_11() 12: isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 13: isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) 14: plus#(X1,X2) -> c_14() 15: s#(X) -> c_15() * 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)) activate#(n__0()) -> c_5(0#()) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_4() isNat#(X) -> c_10() isNat#(n__0()) -> c_11() plus#(X1,X2) -> c_14() s#(X) -> c_15() - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/4,c_4/0,c_5/1,c_6/1,c_7/3,c_8/2,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3} by application of Pre({3}) = {1,2,5,6,7,8,9}. 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: activate#(n__0()) -> c_5(0#()) 4: activate#(n__isNat(X)) -> c_6(isNat#(X)) 5: activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) 7: and#(tt(),X) -> c_9(activate#(X)) 8: isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 9: isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) 10: 0#() -> c_1() 11: activate#(X) -> c_4() 12: isNat#(X) -> c_10() 13: isNat#(n__0()) -> c_11() 14: plus#(X1,X2) -> c_14() 15: s#(X) -> c_15() * 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)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_4() activate#(n__0()) -> c_5(0#()) isNat#(X) -> c_10() isNat#(n__0()) -> c_11() plus#(X1,X2) -> c_14() s#(X) -> c_15() - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/4,c_4/0,c_5/1,c_6/1,c_7/3,c_8/2,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__0()) -> c_5(0#()):11 -->_1 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_1 activate#(X) -> c_4():10 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_5(0#()):11 -->_3 activate#(n__0()) -> c_5(0#()):11 -->_4 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_4 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_1 s#(X) -> c_15():15 -->_2 plus#(X1,X2) -> c_14():14 -->_4 activate#(X) -> c_4():10 -->_3 activate#(X) -> c_4():10 3:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_1 isNat#(n__0()) -> c_11():13 -->_1 isNat#(X) -> c_10():12 4:S:activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__0()) -> c_5(0#()):11 -->_2 activate#(n__0()) -> c_5(0#()):11 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_1 plus#(X1,X2) -> c_14():14 -->_3 activate#(X) -> c_4():10 -->_2 activate#(X) -> c_4():10 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 5:S:activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) -->_2 activate#(n__0()) -> c_5(0#()):11 -->_1 s#(X) -> c_15():15 -->_2 activate#(X) -> c_4():10 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 6:S:and#(tt(),X) -> c_9(activate#(X)) -->_1 activate#(n__0()) -> c_5(0#()):11 -->_1 activate#(X) -> c_4():10 -->_1 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 7:S:isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__0()) -> c_5(0#()):11 -->_3 activate#(n__0()) -> c_5(0#()):11 -->_2 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_2 isNat#(n__0()) -> c_11():13 -->_2 isNat#(X) -> c_10():12 -->_4 activate#(X) -> c_4():10 -->_3 activate#(X) -> c_4():10 -->_2 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_1 and#(tt(),X) -> c_9(activate#(X)):6 -->_4 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_4 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 8:S:isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) -->_2 activate#(n__0()) -> c_5(0#()):11 -->_1 isNat#(n__0()) -> c_11():13 -->_1 isNat#(X) -> c_10():12 -->_2 activate#(X) -> c_4():10 -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 9:W:0#() -> c_1() 10:W:activate#(X) -> c_4() 11:W:activate#(n__0()) -> c_5(0#()) -->_1 0#() -> c_1():9 12:W:isNat#(X) -> c_10() 13:W:isNat#(n__0()) -> c_11() 14:W:plus#(X1,X2) -> c_14() 15:W:s#(X) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: isNat#(X) -> c_10() 13: isNat#(n__0()) -> c_11() 14: plus#(X1,X2) -> c_14() 10: activate#(X) -> c_4() 15: s#(X) -> c_15() 11: activate#(n__0()) -> c_5(0#()) 9: 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)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/4,c_4/0,c_5/1,c_6/1,c_7/3,c_8/2,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 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__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_4 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 3:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 4:S:activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 5:S:activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 6:S:and#(tt(),X) -> c_9(activate#(X)) -->_1 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 7:S:isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_2 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_1 and#(tt(),X) -> c_9(activate#(X)):6 -->_4 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_4 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 8:S:isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(plus#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 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)) activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(activate#(X)) * 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)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/1,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:U11#(tt(),N) -> c_2(activate#(N)) -->_1 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 2:S:U21#(tt(),M,N) -> c_3(activate#(N),activate#(M)) -->_2 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_1 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_1 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 3:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 4:S:activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)) -->_2 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_1 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_1 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 5:S:activate#(n__s(X)) -> c_8(activate#(X)) -->_1 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 6:S:and#(tt(),X) -> c_9(activate#(X)) -->_1 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_1 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 7:S:isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_2 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_1 and#(tt(),X) -> c_9(activate#(X)):6 -->_4 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_3 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_4 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_3 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 8:S:isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 activate#(n__s(X)) -> c_8(activate#(X)):5 -->_2 activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)):4 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):3 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)))] * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__plus(X1,X2)) -> c_7(activate#(X1),activate#(X2)) activate#(n__s(X)) -> c_8(activate#(X)) and#(tt(),X) -> c_9(activate#(X)) isNat#(n__plus(V1,V2)) -> c_12(and#(isNat(activate(V1)),n__isNat(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNat#(n__s(V1)) -> c_13(isNat#(activate(V1)),activate#(V1)) - 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)) 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)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1,0#/0,U11#/2,U21#/3,activate#/1,and#/2,isNat#/1,plus#/2 ,s#/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/1,c_9/1 ,c_10/0,c_11/0,c_12/4,c_13/2,c_14/0,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,activate#,and#,isNat#,plus# ,s#} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE