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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(tt()) -> tt() U41(tt(),N) -> activate(N) U51(tt(),M,N) -> s(plus(activate(N),activate(M))) U61(tt()) -> 0() U71(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) 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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) plus(N,0()) -> U41(and(isNat(N),n__isNatKind(N)),N) plus(N,s(M)) -> U51(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) x(N,0()) -> U61(and(isNat(N),n__isNatKind(N))) x(N,s(M)) -> U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N) x(X1,X2) -> n__x(X1,X2) - Signature: {0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2} / {n__0/0,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,n__x/2,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U12,U13,U21,U22,U31,U32,U33,U41,U51,U61,U71 ,activate,and,isNat,isNatKind,plus,s,x} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,n__x,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. plus(N,0()) -> U41(and(isNat(N),n__isNatKind(N)),N) plus(N,s(M)) -> U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N) x(N,0()) -> U61(and(isNat(N),n__isNatKind(N))) x(N,s(M)) -> U71(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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(tt()) -> tt() U41(tt(),N) -> activate(N) U51(tt(),M,N) -> s(plus(activate(N),activate(M))) U61(tt()) -> 0() U71(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) 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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2} / {n__0/0,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,n__x/2,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U12,U13,U21,U22,U31,U32,U33,U41,U51,U61,U71 ,activate,and,isNat,isNatKind,plus,s,x} and constructors {n__0,n__and,n__isNatKind,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(),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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U33#(tt()) -> c_9() U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U61#(tt()) -> c_12(0#()) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_14() activate#(n__0()) -> c_15(0#()) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(X1,X2) -> c_21() and#(tt(),X) -> c_22(activate#(X)) isNat#(n__0()) -> c_23() isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U33#(tt()) -> c_9() U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U61#(tt()) -> c_12(0#()) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_14() activate#(n__0()) -> c_15(0#()) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(X1,X2) -> c_21() and#(tt(),X) -> c_22(activate#(X)) isNat#(n__0()) -> c_23() isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(tt()) -> tt() U41(tt(),N) -> activate(N) U51(tt(),M,N) -> s(plus(activate(N),activate(M))) U61(tt()) -> 0() U71(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) 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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/4,c_8/3,c_9/0,c_10/1,c_11/4,c_12/1 ,c_13/5,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,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() U31(tt(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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(),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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U33#(tt()) -> c_9() U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U61#(tt()) -> c_12(0#()) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_14() activate#(n__0()) -> c_15(0#()) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(X1,X2) -> c_21() and#(tt(),X) -> c_22(activate#(X)) isNat#(n__0()) -> c_23() isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() * 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U33#(tt()) -> c_9() U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U61#(tt()) -> c_12(0#()) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(X) -> c_14() activate#(n__0()) -> c_15(0#()) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(X1,X2) -> c_21() and#(tt(),X) -> c_22(activate#(X)) isNat#(n__0()) -> c_23() isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/4,c_8/3,c_9/0,c_10/1,c_11/4,c_12/1 ,c_13/5,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,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,4,6,9,14,21,23,27,28,32,33,34} by application of Pre({1,4,6,9,14,21,23,27,28,32,33,34}) = {2,3,5,7,8,10,11,12,13,15,16,17,18,19,20,22,24,25,26,29,30,31}. 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 8: U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) 9: U33#(tt()) -> c_9() 10: U41#(tt(),N) -> c_10(activate#(N)) 11: U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) 12: U61#(tt()) -> c_12(0#()) 13: U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) 14: activate#(X) -> c_14() 15: activate#(n__0()) -> c_15(0#()) 16: activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) 17: activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) 18: activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) 19: activate#(n__s(X)) -> c_19(s#(X)) 20: activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) 21: and#(X1,X2) -> c_21() 22: and#(tt(),X) -> c_22(activate#(X)) 23: isNat#(n__0()) -> c_23() 24: isNat#(n__plus(V1,V2)) -> c_24(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)) 25: isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) 26: isNat#(n__x(V1,V2)) -> c_26(U31#(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)) 27: isNatKind#(X) -> c_27() 28: isNatKind#(n__0()) -> c_28() 29: isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) 30: isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) 31: isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) 32: plus#(X1,X2) -> c_32() 33: s#(X) -> c_33() 34: x#(X1,X2) -> c_34() * 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U61#(tt()) -> c_12(0#()) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__0()) -> c_15(0#()) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(tt(),X) -> c_22(activate#(X)) isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() U13#(tt()) -> c_4() U22#(tt()) -> c_6() U33#(tt()) -> c_9() activate#(X) -> c_14() and#(X1,X2) -> c_21() isNat#(n__0()) -> c_23() isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/4,c_8/3,c_9/0,c_10/1,c_11/4,c_12/1 ,c_13/5,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {8,10,13,14,15} by application of Pre({8,10,13,14,15}) = {1,2,3,4,5,6,7,9,16,17,18,19,20,21,22}. 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 5: U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) 6: U41#(tt(),N) -> c_10(activate#(N)) 7: U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) 8: U61#(tt()) -> c_12(0#()) 9: U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) 10: activate#(n__0()) -> c_15(0#()) 11: activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) 12: activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) 13: activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) 14: activate#(n__s(X)) -> c_19(s#(X)) 15: activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) 16: and#(tt(),X) -> c_22(activate#(X)) 17: isNat#(n__plus(V1,V2)) -> c_24(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)) 18: isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) 19: isNat#(n__x(V1,V2)) -> c_26(U31#(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)) 20: isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) 21: isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) 22: isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) 23: 0#() -> c_1() 24: U13#(tt()) -> c_4() 25: U22#(tt()) -> c_6() 26: U33#(tt()) -> c_9() 27: activate#(X) -> c_14() 28: and#(X1,X2) -> c_21() 29: isNat#(n__0()) -> c_23() 30: isNatKind#(X) -> c_27() 31: isNatKind#(n__0()) -> c_28() 32: plus#(X1,X2) -> c_32() 33: s#(X) -> c_33() 34: x#(X1,X2) -> c_34() * 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) and#(tt(),X) -> c_22(activate#(X)) isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() U13#(tt()) -> c_4() U22#(tt()) -> c_6() U33#(tt()) -> c_9() U61#(tt()) -> c_12(0#()) activate#(X) -> c_14() activate#(n__0()) -> c_15(0#()) activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) activate#(n__s(X)) -> c_19(s#(X)) activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) and#(X1,X2) -> c_21() isNat#(n__0()) -> c_23() isNatKind#(X) -> c_27() isNatKind#(n__0()) -> c_28() plus#(X1,X2) -> c_32() s#(X) -> c_33() x#(X1,X2) -> c_34() - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/4,c_8/3,c_9/0,c_10/1,c_11/4,c_12/1 ,c_13/5,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,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__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):2 -->_2 isNat#(n__0()) -> c_23():29 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 2:S:U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_2 isNat#(n__0()) -> c_23():29 -->_3 activate#(X) -> c_14():23 -->_1 U13#(tt()) -> c_4():19 3:S:U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)) -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_2 isNat#(n__0()) -> c_23():29 -->_3 activate#(X) -> c_14():23 -->_1 U22#(tt()) -> c_6():20 4:S:U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):5 -->_2 isNat#(n__0()) -> c_23():29 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 5:S:U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_2 isNat#(n__0()) -> c_23():29 -->_3 activate#(X) -> c_14():23 -->_1 U33#(tt()) -> c_9():21 6:S:U41#(tt(),N) -> c_10(activate#(N)) -->_1 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_1 activate#(n__s(X)) -> c_19(s#(X)):26 -->_1 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_1 activate#(n__0()) -> c_15(0#()):24 -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 activate#(X) -> c_14():23 7:S:U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 s#(X) -> c_33():33 -->_2 plus#(X1,X2) -> c_32():32 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 8:S:U71#(tt(),M,N) -> c_13(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_20(x#(X1,X2)):27 -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_5 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_5 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_5 activate#(n__0()) -> c_15(0#()):24 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_2 x#(X1,X2) -> c_34():34 -->_1 plus#(X1,X2) -> c_32():32 -->_5 activate#(X) -> c_14():23 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 9:S:activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_1 and#(X1,X2) -> c_21():28 10:S:activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 isNatKind#(n__0()) -> c_28():31 -->_1 isNatKind#(X) -> c_27():30 11:S:and#(tt(),X) -> c_22(activate#(X)) -->_1 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_1 activate#(n__s(X)) -> c_19(s#(X)):26 -->_1 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_1 activate#(n__0()) -> c_15(0#()):24 -->_1 activate#(X) -> c_14():23 -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 12:S:isNat#(n__plus(V1,V2)) -> c_24(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__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_6 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_5 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_7 activate#(n__s(X)) -> c_19(s#(X)):26 -->_6 activate#(n__s(X)) -> c_19(s#(X)):26 -->_5 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_7 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_6 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_5 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_7 activate#(n__0()) -> c_15(0#()):24 -->_6 activate#(n__0()) -> c_15(0#()):24 -->_5 activate#(n__0()) -> c_15(0#()):24 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_3 isNatKind#(n__0()) -> c_28():31 -->_3 isNatKind#(X) -> c_27():30 -->_2 and#(X1,X2) -> c_21():28 -->_7 activate#(X) -> c_14():23 -->_6 activate#(X) -> c_14():23 -->_5 activate#(X) -> c_14():23 -->_4 activate#(X) -> c_14():23 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):1 13:S:isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 isNatKind#(n__0()) -> c_28():31 -->_2 isNatKind#(X) -> c_27():30 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):3 14:S:isNat#(n__x(V1,V2)) -> c_26(U31#(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__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_6 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_5 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_7 activate#(n__s(X)) -> c_19(s#(X)):26 -->_6 activate#(n__s(X)) -> c_19(s#(X)):26 -->_5 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_7 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_6 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_5 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_7 activate#(n__0()) -> c_15(0#()):24 -->_6 activate#(n__0()) -> c_15(0#()):24 -->_5 activate#(n__0()) -> c_15(0#()):24 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_3 isNatKind#(n__0()) -> c_28():31 -->_3 isNatKind#(X) -> c_27():30 -->_2 and#(X1,X2) -> c_21():28 -->_7 activate#(X) -> c_14():23 -->_6 activate#(X) -> c_14():23 -->_5 activate#(X) -> c_14():23 -->_4 activate#(X) -> c_14():23 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):4 15:S:isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__0()) -> c_28():31 -->_2 isNatKind#(X) -> c_27():30 -->_1 and#(X1,X2) -> c_21():28 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 16:S:isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) -->_2 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_2 activate#(n__s(X)) -> c_19(s#(X)):26 -->_2 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_2 activate#(n__0()) -> c_15(0#()):24 -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__0()) -> c_28():31 -->_1 isNatKind#(X) -> c_27():30 -->_2 activate#(X) -> c_14():23 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 17:S:isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_3 activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)):27 -->_4 activate#(n__s(X)) -> c_19(s#(X)):26 -->_3 activate#(n__s(X)) -> c_19(s#(X)):26 -->_4 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_3 activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)):25 -->_4 activate#(n__0()) -> c_15(0#()):24 -->_3 activate#(n__0()) -> c_15(0#()):24 -->_2 isNatKind#(n__0()) -> c_28():31 -->_2 isNatKind#(X) -> c_27():30 -->_1 and#(X1,X2) -> c_21():28 -->_4 activate#(X) -> c_14():23 -->_3 activate#(X) -> c_14():23 -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 18:W:0#() -> c_1() 19:W:U13#(tt()) -> c_4() 20:W:U22#(tt()) -> c_6() 21:W:U33#(tt()) -> c_9() 22:W:U61#(tt()) -> c_12(0#()) -->_1 0#() -> c_1():18 23:W:activate#(X) -> c_14() 24:W:activate#(n__0()) -> c_15(0#()) -->_1 0#() -> c_1():18 25:W:activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) -->_1 plus#(X1,X2) -> c_32():32 26:W:activate#(n__s(X)) -> c_19(s#(X)) -->_1 s#(X) -> c_33():33 27:W:activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) -->_1 x#(X1,X2) -> c_34():34 28:W:and#(X1,X2) -> c_21() 29:W:isNat#(n__0()) -> c_23() 30:W:isNatKind#(X) -> c_27() 31:W:isNatKind#(n__0()) -> c_28() 32:W:plus#(X1,X2) -> c_32() 33:W:s#(X) -> c_33() 34:W:x#(X1,X2) -> c_34() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 22: U61#(tt()) -> c_12(0#()) 19: U13#(tt()) -> c_4() 21: U33#(tt()) -> c_9() 20: U22#(tt()) -> c_6() 29: isNat#(n__0()) -> c_23() 23: activate#(X) -> c_14() 28: and#(X1,X2) -> c_21() 30: isNatKind#(X) -> c_27() 31: isNatKind#(n__0()) -> c_28() 24: activate#(n__0()) -> c_15(0#()) 18: 0#() -> c_1() 25: activate#(n__plus(X1,X2)) -> c_18(plus#(X1,X2)) 32: plus#(X1,X2) -> c_32() 26: activate#(n__s(X)) -> c_19(s#(X)) 33: s#(X) -> c_33() 27: activate#(n__x(X1,X2)) -> c_20(x#(X1,X2)) 34: x#(X1,X2) -> c_34() * 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) and#(tt(),X) -> c_22(activate#(X)) isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/4,c_8/3,c_9/0,c_10/1,c_11/4,c_12/1 ,c_13/5,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,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__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_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__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 3:S:U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)) -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 4:S:U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):5 5:S:U32#(tt(),V2) -> c_8(U33#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 6:S:U41#(tt(),N) -> c_10(activate#(N)) -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 7:S:U51#(tt(),M,N) -> c_11(s#(plus(activate(N),activate(M))) ,plus#(activate(N),activate(M)) ,activate#(N) ,activate#(M)) -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 8:S:U71#(tt(),M,N) -> c_13(plus#(x(activate(N),activate(M)),activate(N)) ,x#(activate(N),activate(M)) ,activate#(N) ,activate#(M) ,activate#(N)) -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 9:S:activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) -->_1 and#(tt(),X) -> c_22(activate#(X)):11 10:S:activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 11:S:and#(tt(),X) -> c_22(activate#(X)) -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 12:S:isNat#(n__plus(V1,V2)) -> c_24(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__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):1 13:S:isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):3 14:S:isNat#(n__x(V1,V2)) -> c_26(U31#(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__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):4 15:S:isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 16:S:isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 17:S:isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 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)) U32#(tt(),V2) -> c_8(isNat#(activate(V2)),activate#(V2)) U51#(tt(),M,N) -> c_11(activate#(N),activate#(M)) U71#(tt(),M,N) -> c_13(activate#(N),activate#(M),activate#(N)) * 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(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(isNat#(activate(V2)),activate#(V2)) U41#(tt(),N) -> c_10(activate#(N)) U51#(tt(),M,N) -> c_11(activate#(N),activate#(M)) U71#(tt(),M,N) -> c_13(activate#(N),activate#(M),activate#(N)) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) and#(tt(),X) -> c_22(activate#(X)) isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/2,c_4/0,c_5/2,c_6/0,c_7/4,c_8/2,c_9/0,c_10/1,c_11/2,c_12/1 ,c_13/3,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,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__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_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__x(V1,V2)) -> c_26(U31#(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)):14 -->_1 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_1 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 3:S:U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_1 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_1 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 4:S:U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_2 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_2 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U32#(tt(),V2) -> c_8(isNat#(activate(V2)),activate#(V2)):5 5:S:U32#(tt(),V2) -> c_8(isNat#(activate(V2)),activate#(V2)) -->_1 isNat#(n__x(V1,V2)) -> c_26(U31#(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)):14 -->_1 isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)):13 -->_1 isNat#(n__plus(V1,V2)) -> c_24(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)):12 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 6:S:U41#(tt(),N) -> c_10(activate#(N)) -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 7:S:U51#(tt(),M,N) -> c_11(activate#(N),activate#(M)) -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 8:S:U71#(tt(),M,N) -> c_13(activate#(N),activate#(M),activate#(N)) -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 9:S:activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) -->_1 and#(tt(),X) -> c_22(activate#(X)):11 10:S:activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 11:S:and#(tt(),X) -> c_22(activate#(X)) -->_1 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_1 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 12:S:isNat#(n__plus(V1,V2)) -> c_24(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__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):1 13:S:isNat#(n__s(V1)) -> c_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1)):3 14:S:isNat#(n__x(V1,V2)) -> c_26(U31#(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__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_3 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_3 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 and#(tt(),X) -> c_22(activate#(X)):11 -->_7 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_6 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_5 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_7 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_6 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_5 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_1 U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):4 15:S:isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 16:S:isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) -->_1 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_1 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_1 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_2 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_2 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 17:S:isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):17 -->_2 isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)):16 -->_2 isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)):15 -->_1 and#(tt(),X) -> c_22(activate#(X)):11 -->_4 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_3 activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)):10 -->_4 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 -->_3 activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)):9 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). [(6,U41#(tt(),N) -> c_10(activate#(N))) ,(7,U51#(tt(),M,N) -> c_11(activate#(N),activate#(M))) ,(8,U71#(tt(),M,N) -> c_13(activate#(N),activate#(M),activate#(N)))] * 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)) U31#(tt(),V1,V2) -> c_7(U32#(isNat(activate(V1)),activate(V2)) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) U32#(tt(),V2) -> c_8(isNat#(activate(V2)),activate#(V2)) activate#(n__and(X1,X2)) -> c_16(and#(X1,X2)) activate#(n__isNatKind(X)) -> c_17(isNatKind#(X)) and#(tt(),X) -> c_22(activate#(X)) isNat#(n__plus(V1,V2)) -> c_24(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_25(U21#(isNatKind(activate(V1)),activate(V1)) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V1)) isNat#(n__x(V1,V2)) -> c_26(U31#(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)) isNatKind#(n__plus(V1,V2)) -> c_29(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatKind#(n__s(V1)) -> c_30(isNatKind#(activate(V1)),activate#(V1)) isNatKind#(n__x(V1,V2)) -> c_31(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2))) ,isNatKind#(activate(V1)) ,activate#(V1) ,activate#(V2)) - 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(),V1,V2) -> U32(isNat(activate(V1)),activate(V2)) U32(tt(),V2) -> U33(isNat(activate(V2))) U33(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) activate(n__x(X1,X2)) -> x(X1,X2) 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)) isNat(n__x(V1,V2)) -> U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) 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)) isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(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/3,U12/2,U13/1,U21/2,U22/1,U31/3,U32/2,U33/1,U41/2,U51/3,U61/1,U71/3,activate/1,and/2,isNat/1 ,isNatKind/1,plus/2,s/1,x/2,0#/0,U11#/3,U12#/2,U13#/1,U21#/2,U22#/1,U31#/3,U32#/2,U33#/1,U41#/2,U51#/3 ,U61#/1,U71#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1,x#/2} / {n__0/0,n__and/2,n__isNatKind/1 ,n__plus/2,n__s/1,n__x/2,tt/0,c_1/0,c_2/4,c_3/2,c_4/0,c_5/2,c_6/0,c_7/4,c_8/2,c_9/0,c_10/1,c_11/2,c_12/1 ,c_13/3,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/0,c_22/1,c_23/0,c_24/7,c_25/4,c_26/7,c_27/0 ,c_28/0,c_29/4,c_30/2,c_31/4,c_32/0,c_33/0,c_34/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U32#,U33#,U41#,U51#,U61# ,U71#,activate#,and#,isNat#,isNatKind#,plus#,s#,x#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s ,n__x,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE