WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c16() A__AND(tt(),z0) -> c15(MARK(z0)) A__ISNAT(z0) -> c20() A__ISNAT(0()) -> c17() A__ISNAT(plus(z0,z1)) -> c18(A__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatKind(z1)) ,A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c19(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c24() A__ISNATKIND(0()) -> c21() A__ISNATKIND(plus(z0,z1)) -> c22(A__AND(a__isNatKind(z0),isNatKind(z1)),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c23(A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c27() A__PLUS(z0,0()) -> c25(A__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) ,A__AND(a__isNat(z0),isNatKind(z0)) ,A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c26(A__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,z1 ,z0) ,A__AND(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNat(z1),isNatKind(z1)) ,A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNat(z0),z1),A__ISNAT(z0)) A__U12(z0,z1) -> c3() A__U12(tt(),z0) -> c2(A__U13(a__isNat(z0)),A__ISNAT(z0)) A__U13(z0) -> c5() A__U13(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(MARK(z0)) A__U41(z0,z1,z2) -> c14() A__U41(tt(),z0,z1) -> c12(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U41(tt(),z0,z1) -> c13(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c42() MARK(U11(z0,z1,z2)) -> c28(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1)) -> c29(A__U12(mark(z0),z1),MARK(z0)) MARK(U13(z0)) -> c31(A__U13(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c32(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c33(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c34(A__U31(mark(z0),z1),MARK(z0)) MARK(U41(z0,z1,z2)) -> c35(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c38(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c30(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c39(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c36(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c37(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(tt()) -> c40() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNat(z0),z1) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> a__U13(a__isNat(z0)) a__U13(z0) -> U13(z0) a__U13(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(plus(z0,z1)) -> a__and(a__isNatKind(z0),isNatKind(z1)) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) a__plus(z0,s(z1)) -> a__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U13(z0)) -> a__U13(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/2,A__U13/1,A__U21/2,A__U22/1,A__U31/2,A__U41/3 ,MARK/1,a__U11/3,a__U12/2,a__U13/1,a__U21/2,a__U22/1,a__U31/2,a__U41/3,a__and/2,a__isNat/1,a__isNatKind/1 ,a__plus/2,mark/1} / {0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,and/2,c/2,c1/0,c10/1,c11/0,c12/2,c13/2 ,c14/0,c15/1,c16/0,c17/0,c18/3,c19/2,c2/2,c20/0,c21/0,c22/2,c23/1,c24/0,c25/3,c26/4,c27/0,c28/2,c29/2,c3/0 ,c30/1,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2,c37/2,c38/2,c39/1,c4/0,c40/0,c41/1,c42/0,c5/0,c6/2,c7/0,c8/0,c9/0 ,isNat/1,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13 ,A__U21,A__U22,A__U31,A__U41,MARK,a__U11,a__U12,a__U13,a__U21,a__U22,a__U31,a__U41,a__and,a__isNat ,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U21,U22,U31,U41,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c5,c6,c7,c8,c9,isNat,isNatKind,plus,s,tt} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c16() A__AND(tt(),z0) -> c15(MARK(z0)) A__ISNAT(z0) -> c20() A__ISNAT(0()) -> c17() A__ISNAT(plus(z0,z1)) -> c18(A__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatKind(z1)) ,A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c19(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c24() A__ISNATKIND(0()) -> c21() A__ISNATKIND(plus(z0,z1)) -> c22(A__AND(a__isNatKind(z0),isNatKind(z1)),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c23(A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c27() A__PLUS(z0,0()) -> c25(A__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) ,A__AND(a__isNat(z0),isNatKind(z0)) ,A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c26(A__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,z1 ,z0) ,A__AND(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNat(z1),isNatKind(z1)) ,A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNat(z0),z1),A__ISNAT(z0)) A__U12(z0,z1) -> c3() A__U12(tt(),z0) -> c2(A__U13(a__isNat(z0)),A__ISNAT(z0)) A__U13(z0) -> c5() A__U13(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(MARK(z0)) A__U41(z0,z1,z2) -> c14() A__U41(tt(),z0,z1) -> c12(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U41(tt(),z0,z1) -> c13(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c42() MARK(U11(z0,z1,z2)) -> c28(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1)) -> c29(A__U12(mark(z0),z1),MARK(z0)) MARK(U13(z0)) -> c31(A__U13(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c32(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c33(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c34(A__U31(mark(z0),z1),MARK(z0)) MARK(U41(z0,z1,z2)) -> c35(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c38(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c30(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c39(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c36(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c37(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(tt()) -> c40() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNat(z0),z1) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> a__U13(a__isNat(z0)) a__U13(z0) -> U13(z0) a__U13(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(plus(z0,z1)) -> a__and(a__isNatKind(z0),isNatKind(z1)) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) a__plus(z0,s(z1)) -> a__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U13(z0)) -> a__U13(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/2,A__U13/1,A__U21/2,A__U22/1,A__U31/2,A__U41/3 ,MARK/1,a__U11/3,a__U12/2,a__U13/1,a__U21/2,a__U22/1,a__U31/2,a__U41/3,a__and/2,a__isNat/1,a__isNatKind/1 ,a__plus/2,mark/1} / {0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,and/2,c/2,c1/0,c10/1,c11/0,c12/2,c13/2 ,c14/0,c15/1,c16/0,c17/0,c18/3,c19/2,c2/2,c20/0,c21/0,c22/2,c23/1,c24/0,c25/3,c26/4,c27/0,c28/2,c29/2,c3/0 ,c30/1,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2,c37/2,c38/2,c39/1,c4/0,c40/0,c41/1,c42/0,c5/0,c6/2,c7/0,c8/0,c9/0 ,isNat/1,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13 ,A__U21,A__U22,A__U31,A__U41,MARK,a__U11,a__U12,a__U13,a__U21,a__U22,a__U31,a__U41,a__and,a__isNat ,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U21,U22,U31,U41,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c5,c6,c7,c8,c9,isNat,isNatKind,plus,s,tt} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c16() A__AND(tt(),z0) -> c15(MARK(z0)) A__ISNAT(z0) -> c20() A__ISNAT(0()) -> c17() A__ISNAT(plus(z0,z1)) -> c18(A__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatKind(z1)) ,A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c19(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c24() A__ISNATKIND(0()) -> c21() A__ISNATKIND(plus(z0,z1)) -> c22(A__AND(a__isNatKind(z0),isNatKind(z1)),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c23(A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c27() A__PLUS(z0,0()) -> c25(A__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) ,A__AND(a__isNat(z0),isNatKind(z0)) ,A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c26(A__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,z1 ,z0) ,A__AND(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNat(z1),isNatKind(z1)) ,A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNat(z0),z1),A__ISNAT(z0)) A__U12(z0,z1) -> c3() A__U12(tt(),z0) -> c2(A__U13(a__isNat(z0)),A__ISNAT(z0)) A__U13(z0) -> c5() A__U13(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(MARK(z0)) A__U41(z0,z1,z2) -> c14() A__U41(tt(),z0,z1) -> c12(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U41(tt(),z0,z1) -> c13(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c42() MARK(U11(z0,z1,z2)) -> c28(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1)) -> c29(A__U12(mark(z0),z1),MARK(z0)) MARK(U13(z0)) -> c31(A__U13(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c32(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c33(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c34(A__U31(mark(z0),z1),MARK(z0)) MARK(U41(z0,z1,z2)) -> c35(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c38(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c30(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c39(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c36(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c37(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(tt()) -> c40() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNat(z0),z1) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> a__U13(a__isNat(z0)) a__U13(z0) -> U13(z0) a__U13(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__and(a__isNatKind(z0),isNatKind(z1)),z0,z1) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(plus(z0,z1)) -> a__and(a__isNatKind(z0),isNatKind(z1)) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U31(a__and(a__isNat(z0),isNatKind(z0)),z0) a__plus(z0,s(z1)) -> a__U41(a__and(a__and(a__isNat(z1),isNatKind(z1)),and(isNat(z0),isNatKind(z0))),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U13(z0)) -> a__U13(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/2,A__U13/1,A__U21/2,A__U22/1,A__U31/2,A__U41/3 ,MARK/1,a__U11/3,a__U12/2,a__U13/1,a__U21/2,a__U22/1,a__U31/2,a__U41/3,a__and/2,a__isNat/1,a__isNatKind/1 ,a__plus/2,mark/1} / {0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,and/2,c/2,c1/0,c10/1,c11/0,c12/2,c13/2 ,c14/0,c15/1,c16/0,c17/0,c18/3,c19/2,c2/2,c20/0,c21/0,c22/2,c23/1,c24/0,c25/3,c26/4,c27/0,c28/2,c29/2,c3/0 ,c30/1,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2,c37/2,c38/2,c39/1,c4/0,c40/0,c41/1,c42/0,c5/0,c6/2,c7/0,c8/0,c9/0 ,isNat/1,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13 ,A__U21,A__U22,A__U31,A__U41,MARK,a__U11,a__U12,a__U13,a__U21,a__U22,a__U31,a__U41,a__and,a__isNat ,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U21,U22,U31,U41,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c5,c6,c7,c8,c9,isNat,isNatKind,plus,s,tt} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISNATKIND(x){x -> plus(x,y)} = A__ISNATKIND(plus(x,y)) ->^+ c22(A__AND(a__isNatKind(x),isNatKind(y)),A__ISNATKIND(x)) = C[A__ISNATKIND(x) = A__ISNATKIND(x){}] WORST_CASE(Omega(n^1),?)