WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ISNAT(z0) -> c29() A__ISNAT(0()) -> c25() A__ISNAT(plus(z0,z1)) -> c26(A__U11(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c27(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNAT(x(z0,z1)) -> c28(A__U31(a__isNat(z0),z1),A__ISNAT(z0)) A__PLUS(z0,z1) -> c32() A__PLUS(z0,0()) -> c30(A__U41(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c31(A__U51(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(A__U12(a__isNat(z0)),A__ISNAT(z0)) A__U12(z0) -> c3() A__U12(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1) -> c7() A__U31(tt(),z0) -> c6(A__U32(a__isNat(z0)),A__ISNAT(z0)) A__U32(z0) -> c9() A__U32(tt()) -> c8() A__U41(z0,z1) -> c11() A__U41(tt(),z0) -> c10(MARK(z0)) A__U51(z0,z1,z2) -> c13() A__U51(tt(),z0,z1) -> c12(A__U52(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U52(z0,z1,z2) -> c16() A__U52(tt(),z0,z1) -> c14(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U52(tt(),z0,z1) -> c15(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U61(z0) -> c18() A__U61(tt()) -> c17() A__U71(z0,z1,z2) -> c20() A__U71(tt(),z0,z1) -> c19(A__U72(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U72(z0,z1,z2) -> c24() A__U72(tt(),z0,z1) -> c21(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U72(tt(),z0,z1) -> c22(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U72(tt(),z0,z1) -> c23(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c35() A__X(z0,0()) -> c33(A__U61(a__isNat(z0)),A__ISNAT(z0)) A__X(z0,s(z1)) -> c34(A__U71(a__isNat(z1),z1,z0),A__ISNAT(z1)) MARK(0()) -> c54() MARK(U11(z0,z1)) -> c36(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c37(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c39(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c40(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c41(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c42(A__U41(mark(z0),z1),MARK(z0)) MARK(U51(z0,z1,z2)) -> c43(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1,z2)) -> c44(A__U52(mark(z0),z1,z2),MARK(z0)) MARK(U61(z0)) -> c47(A__U61(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c48(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1,z2)) -> c49(A__U72(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c38(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c45(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c46(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c53(MARK(z0)) MARK(tt()) -> c52() MARK(x(z0,z1)) -> c50(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c51(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNat(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNat(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> mark(z0) a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z1),z0,z1) a__U52(z0,z1,z2) -> U52(z0,z1,z2) a__U52(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U61(z0) -> U61(z0) a__U61(tt()) -> 0() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0,z1) a__U72(z0,z1,z2) -> U72(z0,z1,z2) a__U72(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNat(z0),z1) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(x(z0,z1)) -> a__U31(a__isNat(z0),z1) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U41(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U51(a__isNat(z1),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> a__U61(a__isNat(z0)) a__x(z0,s(z1)) -> a__U71(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1,z2)) -> a__U52(mark(z0),z1,z2) mark(U61(z0)) -> a__U61(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1,z2)) -> a__U72(mark(z0),z1,z2) mark(isNat(z0)) -> a__isNat(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__ISNAT/1,A__PLUS/2,A__U11/2,A__U12/1,A__U21/1,A__U31/2,A__U32/1,A__U41/2,A__U51/3,A__U52/3,A__U61/1 ,A__U71/3,A__U72/3,A__X/2,MARK/1,a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3 ,a__U61/1,a__U71/3,a__U72/3,a__isNat/1,a__plus/2,a__x/2,mark/1} / {0/0,U11/2,U12/1,U21/1,U31/2,U32/1,U41/2 ,U51/3,U52/3,U61/1,U71/3,U72/3,c/2,c1/0,c10/1,c11/0,c12/2,c13/0,c14/2,c15/2,c16/0,c17/0,c18/0,c19/2,c2/0 ,c20/0,c21/3,c22/3,c23/2,c24/0,c25/0,c26/2,c27/2,c28/2,c29/0,c3/0,c30/2,c31/2,c32/0,c33/2,c34/2,c35/0,c36/2 ,c37/2,c38/1,c39/2,c4/0,c40/2,c41/2,c42/2,c43/2,c44/2,c45/2,c46/2,c47/2,c48/2,c49/2,c5/0,c50/2,c51/2,c52/0 ,c53/1,c54/0,c6/2,c7/0,c8/0,c9/0,isNat/1,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__PLUS,A__U11,A__U12,A__U21,A__U31,A__U32 ,A__U41,A__U51,A__U52,A__U61,A__U71,A__U72,A__X,MARK,a__U11,a__U12,a__U21,a__U31,a__U32,a__U41,a__U51,a__U52 ,a__U61,a__U71,a__U72,a__isNat,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U31,U32,U41,U51,U52,U61 ,U71,U72,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,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c6,c7,c8 ,c9,isNat,plus,s,tt,x} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ISNAT(z0) -> c29() A__ISNAT(0()) -> c25() A__ISNAT(plus(z0,z1)) -> c26(A__U11(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c27(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNAT(x(z0,z1)) -> c28(A__U31(a__isNat(z0),z1),A__ISNAT(z0)) A__PLUS(z0,z1) -> c32() A__PLUS(z0,0()) -> c30(A__U41(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c31(A__U51(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(A__U12(a__isNat(z0)),A__ISNAT(z0)) A__U12(z0) -> c3() A__U12(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1) -> c7() A__U31(tt(),z0) -> c6(A__U32(a__isNat(z0)),A__ISNAT(z0)) A__U32(z0) -> c9() A__U32(tt()) -> c8() A__U41(z0,z1) -> c11() A__U41(tt(),z0) -> c10(MARK(z0)) A__U51(z0,z1,z2) -> c13() A__U51(tt(),z0,z1) -> c12(A__U52(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U52(z0,z1,z2) -> c16() A__U52(tt(),z0,z1) -> c14(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U52(tt(),z0,z1) -> c15(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U61(z0) -> c18() A__U61(tt()) -> c17() A__U71(z0,z1,z2) -> c20() A__U71(tt(),z0,z1) -> c19(A__U72(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U72(z0,z1,z2) -> c24() A__U72(tt(),z0,z1) -> c21(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U72(tt(),z0,z1) -> c22(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U72(tt(),z0,z1) -> c23(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c35() A__X(z0,0()) -> c33(A__U61(a__isNat(z0)),A__ISNAT(z0)) A__X(z0,s(z1)) -> c34(A__U71(a__isNat(z1),z1,z0),A__ISNAT(z1)) MARK(0()) -> c54() MARK(U11(z0,z1)) -> c36(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c37(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c39(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c40(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c41(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c42(A__U41(mark(z0),z1),MARK(z0)) MARK(U51(z0,z1,z2)) -> c43(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1,z2)) -> c44(A__U52(mark(z0),z1,z2),MARK(z0)) MARK(U61(z0)) -> c47(A__U61(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c48(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1,z2)) -> c49(A__U72(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c38(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c45(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c46(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c53(MARK(z0)) MARK(tt()) -> c52() MARK(x(z0,z1)) -> c50(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c51(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNat(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNat(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> mark(z0) a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z1),z0,z1) a__U52(z0,z1,z2) -> U52(z0,z1,z2) a__U52(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U61(z0) -> U61(z0) a__U61(tt()) -> 0() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0,z1) a__U72(z0,z1,z2) -> U72(z0,z1,z2) a__U72(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNat(z0),z1) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(x(z0,z1)) -> a__U31(a__isNat(z0),z1) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U41(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U51(a__isNat(z1),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> a__U61(a__isNat(z0)) a__x(z0,s(z1)) -> a__U71(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1,z2)) -> a__U52(mark(z0),z1,z2) mark(U61(z0)) -> a__U61(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1,z2)) -> a__U72(mark(z0),z1,z2) mark(isNat(z0)) -> a__isNat(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__ISNAT/1,A__PLUS/2,A__U11/2,A__U12/1,A__U21/1,A__U31/2,A__U32/1,A__U41/2,A__U51/3,A__U52/3,A__U61/1 ,A__U71/3,A__U72/3,A__X/2,MARK/1,a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3 ,a__U61/1,a__U71/3,a__U72/3,a__isNat/1,a__plus/2,a__x/2,mark/1} / {0/0,U11/2,U12/1,U21/1,U31/2,U32/1,U41/2 ,U51/3,U52/3,U61/1,U71/3,U72/3,c/2,c1/0,c10/1,c11/0,c12/2,c13/0,c14/2,c15/2,c16/0,c17/0,c18/0,c19/2,c2/0 ,c20/0,c21/3,c22/3,c23/2,c24/0,c25/0,c26/2,c27/2,c28/2,c29/0,c3/0,c30/2,c31/2,c32/0,c33/2,c34/2,c35/0,c36/2 ,c37/2,c38/1,c39/2,c4/0,c40/2,c41/2,c42/2,c43/2,c44/2,c45/2,c46/2,c47/2,c48/2,c49/2,c5/0,c50/2,c51/2,c52/0 ,c53/1,c54/0,c6/2,c7/0,c8/0,c9/0,isNat/1,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__PLUS,A__U11,A__U12,A__U21,A__U31,A__U32 ,A__U41,A__U51,A__U52,A__U61,A__U71,A__U72,A__X,MARK,a__U11,a__U12,a__U21,a__U31,a__U32,a__U41,a__U51,a__U52 ,a__U61,a__U71,a__U72,a__isNat,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U31,U32,U41,U51,U52,U61 ,U71,U72,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,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c6,c7,c8 ,c9,isNat,plus,s,tt,x} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ISNAT(z0) -> c29() A__ISNAT(0()) -> c25() A__ISNAT(plus(z0,z1)) -> c26(A__U11(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c27(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNAT(x(z0,z1)) -> c28(A__U31(a__isNat(z0),z1),A__ISNAT(z0)) A__PLUS(z0,z1) -> c32() A__PLUS(z0,0()) -> c30(A__U41(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c31(A__U51(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(A__U12(a__isNat(z0)),A__ISNAT(z0)) A__U12(z0) -> c3() A__U12(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1) -> c7() A__U31(tt(),z0) -> c6(A__U32(a__isNat(z0)),A__ISNAT(z0)) A__U32(z0) -> c9() A__U32(tt()) -> c8() A__U41(z0,z1) -> c11() A__U41(tt(),z0) -> c10(MARK(z0)) A__U51(z0,z1,z2) -> c13() A__U51(tt(),z0,z1) -> c12(A__U52(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U52(z0,z1,z2) -> c16() A__U52(tt(),z0,z1) -> c14(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U52(tt(),z0,z1) -> c15(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U61(z0) -> c18() A__U61(tt()) -> c17() A__U71(z0,z1,z2) -> c20() A__U71(tt(),z0,z1) -> c19(A__U72(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U72(z0,z1,z2) -> c24() A__U72(tt(),z0,z1) -> c21(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U72(tt(),z0,z1) -> c22(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U72(tt(),z0,z1) -> c23(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c35() A__X(z0,0()) -> c33(A__U61(a__isNat(z0)),A__ISNAT(z0)) A__X(z0,s(z1)) -> c34(A__U71(a__isNat(z1),z1,z0),A__ISNAT(z1)) MARK(0()) -> c54() MARK(U11(z0,z1)) -> c36(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c37(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c39(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c40(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c41(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c42(A__U41(mark(z0),z1),MARK(z0)) MARK(U51(z0,z1,z2)) -> c43(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1,z2)) -> c44(A__U52(mark(z0),z1,z2),MARK(z0)) MARK(U61(z0)) -> c47(A__U61(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c48(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1,z2)) -> c49(A__U72(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c38(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c45(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c46(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c53(MARK(z0)) MARK(tt()) -> c52() MARK(x(z0,z1)) -> c50(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c51(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNat(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNat(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> mark(z0) a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z1),z0,z1) a__U52(z0,z1,z2) -> U52(z0,z1,z2) a__U52(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U61(z0) -> U61(z0) a__U61(tt()) -> 0() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0,z1) a__U72(z0,z1,z2) -> U72(z0,z1,z2) a__U72(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNat(z0),z1) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(x(z0,z1)) -> a__U31(a__isNat(z0),z1) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U41(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U51(a__isNat(z1),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> a__U61(a__isNat(z0)) a__x(z0,s(z1)) -> a__U71(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1,z2)) -> a__U52(mark(z0),z1,z2) mark(U61(z0)) -> a__U61(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1,z2)) -> a__U72(mark(z0),z1,z2) mark(isNat(z0)) -> a__isNat(z0) mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(tt()) -> tt() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__ISNAT/1,A__PLUS/2,A__U11/2,A__U12/1,A__U21/1,A__U31/2,A__U32/1,A__U41/2,A__U51/3,A__U52/3,A__U61/1 ,A__U71/3,A__U72/3,A__X/2,MARK/1,a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3 ,a__U61/1,a__U71/3,a__U72/3,a__isNat/1,a__plus/2,a__x/2,mark/1} / {0/0,U11/2,U12/1,U21/1,U31/2,U32/1,U41/2 ,U51/3,U52/3,U61/1,U71/3,U72/3,c/2,c1/0,c10/1,c11/0,c12/2,c13/0,c14/2,c15/2,c16/0,c17/0,c18/0,c19/2,c2/0 ,c20/0,c21/3,c22/3,c23/2,c24/0,c25/0,c26/2,c27/2,c28/2,c29/0,c3/0,c30/2,c31/2,c32/0,c33/2,c34/2,c35/0,c36/2 ,c37/2,c38/1,c39/2,c4/0,c40/2,c41/2,c42/2,c43/2,c44/2,c45/2,c46/2,c47/2,c48/2,c49/2,c5/0,c50/2,c51/2,c52/0 ,c53/1,c54/0,c6/2,c7/0,c8/0,c9/0,isNat/1,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__PLUS,A__U11,A__U12,A__U21,A__U31,A__U32 ,A__U41,A__U51,A__U52,A__U61,A__U71,A__U72,A__X,MARK,a__U11,a__U12,a__U21,a__U31,a__U32,a__U41,a__U51,a__U52 ,a__U61,a__U71,a__U72,a__isNat,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U31,U32,U41,U51,U52,U61 ,U71,U72,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,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c6,c7,c8 ,c9,isNat,plus,s,tt,x} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISNAT(x){x -> plus(x,y)} = A__ISNAT(plus(x,y)) ->^+ c26(A__U11(a__isNat(x),y),A__ISNAT(x)) = C[A__ISNAT(x) = A__ISNAT(x){}] WORST_CASE(Omega(n^1),?)