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