WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ISNAT(z0) -> c40() A__ISNAT(0()) -> c37() A__ISNAT(plus(z0,z1)) -> c38(A__U11(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c39(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c44() A__ISNATKIND(0()) -> c41() A__ISNATKIND(plus(z0,z1)) -> c42(A__U31(a__isNatKind(z0),z1),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c43(A__U41(a__isNatKind(z0)),A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c47() A__PLUS(z0,0()) -> c45(A__U51(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c46(A__U61(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U12(z0,z1,z2) -> c3() A__U12(tt(),z0,z1) -> c2(A__U13(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U13(z0,z1,z2) -> c5() A__U13(tt(),z0,z1) -> c4(A__U14(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U14(z0,z1,z2) -> c7() A__U14(tt(),z0,z1) -> c6(A__U15(a__isNat(z0),z1),A__ISNAT(z0)) A__U15(z0,z1) -> c9() A__U15(tt(),z0) -> c8(A__U16(a__isNat(z0)),A__ISNAT(z0)) A__U16(z0) -> c11() A__U16(tt()) -> c10() A__U21(z0,z1) -> c13() A__U21(tt(),z0) -> c12(A__U22(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U22(z0,z1) -> c15() A__U22(tt(),z0) -> c14(A__U23(a__isNat(z0)),A__ISNAT(z0)) A__U23(z0) -> c17() A__U23(tt()) -> c16() A__U31(z0,z1) -> c19() A__U31(tt(),z0) -> c18(A__U32(a__isNatKind(z0)),A__ISNATKIND(z0)) A__U32(z0) -> c21() A__U32(tt()) -> c20() A__U41(z0) -> c23() A__U41(tt()) -> c22() A__U51(z0,z1) -> c25() A__U51(tt(),z0) -> c24(A__U52(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U52(z0,z1) -> c27() A__U52(tt(),z0) -> c26(MARK(z0)) A__U61(z0,z1,z2) -> c29() A__U61(tt(),z0,z1) -> c28(A__U62(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U62(z0,z1,z2) -> c31() A__U62(tt(),z0,z1) -> c30(A__U63(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U63(z0,z1,z2) -> c33() A__U63(tt(),z0,z1) -> c32(A__U64(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U64(z0,z1,z2) -> c36() A__U64(tt(),z0,z1) -> c34(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U64(tt(),z0,z1) -> c35(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c72() MARK(U11(z0,z1,z2)) -> c48(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c49(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U13(z0,z1,z2)) -> c51(A__U13(mark(z0),z1,z2),MARK(z0)) MARK(U14(z0,z1,z2)) -> c52(A__U14(mark(z0),z1,z2),MARK(z0)) MARK(U15(z0,z1)) -> c53(A__U15(mark(z0),z1),MARK(z0)) MARK(U16(z0)) -> c55(A__U16(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c56(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0,z1)) -> c57(A__U22(mark(z0),z1),MARK(z0)) MARK(U23(z0)) -> c58(A__U23(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c59(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c60(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0)) -> c61(A__U41(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c62(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0,z1)) -> c63(A__U52(mark(z0),z1),MARK(z0)) MARK(U61(z0,z1,z2)) -> c64(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1,z2)) -> c65(A__U62(mark(z0),z1,z2),MARK(z0)) MARK(U63(z0,z1,z2)) -> c66(A__U63(mark(z0),z1,z2),MARK(z0)) MARK(U64(z0,z1,z2)) -> c67(A__U64(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c54(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c50(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c68(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c69(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c71(MARK(z0)) MARK(tt()) -> c70() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNatKind(z0),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> a__U13(a__isNatKind(z1),z0,z1) a__U13(z0,z1,z2) -> U13(z0,z1,z2) a__U13(tt(),z0,z1) -> a__U14(a__isNatKind(z1),z0,z1) a__U14(z0,z1,z2) -> U14(z0,z1,z2) a__U14(tt(),z0,z1) -> a__U15(a__isNat(z0),z1) a__U15(z0,z1) -> U15(z0,z1) a__U15(tt(),z0) -> a__U16(a__isNat(z0)) a__U16(z0) -> U16(z0) a__U16(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNatKind(z0),z0) a__U22(z0,z1) -> U22(z0,z1) a__U22(tt(),z0) -> a__U23(a__isNat(z0)) a__U23(z0) -> U23(z0) a__U23(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatKind(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0) -> U41(z0) a__U41(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatKind(z0),z0) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> mark(z0) a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNatKind(z0),z0,z1) a__U62(z0,z1,z2) -> U62(z0,z1,z2) a__U62(tt(),z0,z1) -> a__U63(a__isNat(z1),z0,z1) a__U63(z0,z1,z2) -> U63(z0,z1,z2) a__U63(tt(),z0,z1) -> a__U64(a__isNatKind(z1),z0,z1) a__U64(z0,z1,z2) -> U64(z0,z1,z2) a__U64(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNatKind(z0),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__U31(a__isNatKind(z0),z1) a__isNatKind(s(z0)) -> a__U41(a__isNatKind(z0)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U51(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U61(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U13(z0,z1,z2)) -> a__U13(mark(z0),z1,z2) mark(U14(z0,z1,z2)) -> a__U14(mark(z0),z1,z2) mark(U15(z0,z1)) -> a__U15(mark(z0),z1) mark(U16(z0)) -> a__U16(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0,z1)) -> a__U22(mark(z0),z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0)) -> a__U41(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1,z2)) -> a__U62(mark(z0),z1,z2) mark(U63(z0,z1,z2)) -> a__U63(mark(z0),z1,z2) mark(U64(z0,z1,z2)) -> a__U64(mark(z0),z1,z2) 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__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/3,A__U13/3,A__U14/3,A__U15/2,A__U16/1,A__U21/2,A__U22/2 ,A__U23/1,A__U31/2,A__U32/1,A__U41/1,A__U51/2,A__U52/2,A__U61/3,A__U62/3,A__U63/3,A__U64/3,MARK/1,a__U11/3 ,a__U12/3,a__U13/3,a__U14/3,a__U15/2,a__U16/1,a__U21/2,a__U22/2,a__U23/1,a__U31/2,a__U32/1,a__U41/1,a__U51/2 ,a__U52/2,a__U61/3,a__U62/3,a__U63/3,a__U64/3,a__isNat/1,a__isNatKind/1,a__plus/2,mark/1} / {0/0,U11/3,U12/3 ,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,c/2,c1/0 ,c10/0,c11/0,c12/2,c13/0,c14/2,c15/0,c16/0,c17/0,c18/2,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/2,c25/0,c26/1 ,c27/0,c28/2,c29/0,c3/0,c30/2,c31/0,c32/2,c33/0,c34/2,c35/2,c36/0,c37/0,c38/2,c39/2,c4/2,c40/0,c41/0,c42/2 ,c43/2,c44/0,c45/2,c46/2,c47/0,c48/2,c49/2,c5/0,c50/1,c51/2,c52/2,c53/2,c54/1,c55/2,c56/2,c57/2,c58/2,c59/2 ,c6/2,c60/2,c61/2,c62/2,c63/2,c64/2,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/0,c71/1,c72/0,c8/2,c9/0,isNat/1 ,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13,A__U14 ,A__U15,A__U16,A__U21,A__U22,A__U23,A__U31,A__U32,A__U41,A__U51,A__U52,A__U61,A__U62,A__U63,A__U64,MARK ,a__U11,a__U12,a__U13,a__U14,a__U15,a__U16,a__U21,a__U22,a__U23,a__U31,a__U32,a__U41,a__U51,a__U52,a__U61 ,a__U62,a__U63,a__U64,a__isNat,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U14,U15,U16,U21 ,U22,U23,U31,U32,U41,U51,U52,U61,U62,U63,U64,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,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,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__ISNAT(z0) -> c40() A__ISNAT(0()) -> c37() A__ISNAT(plus(z0,z1)) -> c38(A__U11(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c39(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c44() A__ISNATKIND(0()) -> c41() A__ISNATKIND(plus(z0,z1)) -> c42(A__U31(a__isNatKind(z0),z1),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c43(A__U41(a__isNatKind(z0)),A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c47() A__PLUS(z0,0()) -> c45(A__U51(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c46(A__U61(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U12(z0,z1,z2) -> c3() A__U12(tt(),z0,z1) -> c2(A__U13(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U13(z0,z1,z2) -> c5() A__U13(tt(),z0,z1) -> c4(A__U14(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U14(z0,z1,z2) -> c7() A__U14(tt(),z0,z1) -> c6(A__U15(a__isNat(z0),z1),A__ISNAT(z0)) A__U15(z0,z1) -> c9() A__U15(tt(),z0) -> c8(A__U16(a__isNat(z0)),A__ISNAT(z0)) A__U16(z0) -> c11() A__U16(tt()) -> c10() A__U21(z0,z1) -> c13() A__U21(tt(),z0) -> c12(A__U22(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U22(z0,z1) -> c15() A__U22(tt(),z0) -> c14(A__U23(a__isNat(z0)),A__ISNAT(z0)) A__U23(z0) -> c17() A__U23(tt()) -> c16() A__U31(z0,z1) -> c19() A__U31(tt(),z0) -> c18(A__U32(a__isNatKind(z0)),A__ISNATKIND(z0)) A__U32(z0) -> c21() A__U32(tt()) -> c20() A__U41(z0) -> c23() A__U41(tt()) -> c22() A__U51(z0,z1) -> c25() A__U51(tt(),z0) -> c24(A__U52(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U52(z0,z1) -> c27() A__U52(tt(),z0) -> c26(MARK(z0)) A__U61(z0,z1,z2) -> c29() A__U61(tt(),z0,z1) -> c28(A__U62(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U62(z0,z1,z2) -> c31() A__U62(tt(),z0,z1) -> c30(A__U63(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U63(z0,z1,z2) -> c33() A__U63(tt(),z0,z1) -> c32(A__U64(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U64(z0,z1,z2) -> c36() A__U64(tt(),z0,z1) -> c34(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U64(tt(),z0,z1) -> c35(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c72() MARK(U11(z0,z1,z2)) -> c48(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c49(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U13(z0,z1,z2)) -> c51(A__U13(mark(z0),z1,z2),MARK(z0)) MARK(U14(z0,z1,z2)) -> c52(A__U14(mark(z0),z1,z2),MARK(z0)) MARK(U15(z0,z1)) -> c53(A__U15(mark(z0),z1),MARK(z0)) MARK(U16(z0)) -> c55(A__U16(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c56(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0,z1)) -> c57(A__U22(mark(z0),z1),MARK(z0)) MARK(U23(z0)) -> c58(A__U23(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c59(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c60(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0)) -> c61(A__U41(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c62(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0,z1)) -> c63(A__U52(mark(z0),z1),MARK(z0)) MARK(U61(z0,z1,z2)) -> c64(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1,z2)) -> c65(A__U62(mark(z0),z1,z2),MARK(z0)) MARK(U63(z0,z1,z2)) -> c66(A__U63(mark(z0),z1,z2),MARK(z0)) MARK(U64(z0,z1,z2)) -> c67(A__U64(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c54(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c50(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c68(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c69(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c71(MARK(z0)) MARK(tt()) -> c70() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNatKind(z0),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> a__U13(a__isNatKind(z1),z0,z1) a__U13(z0,z1,z2) -> U13(z0,z1,z2) a__U13(tt(),z0,z1) -> a__U14(a__isNatKind(z1),z0,z1) a__U14(z0,z1,z2) -> U14(z0,z1,z2) a__U14(tt(),z0,z1) -> a__U15(a__isNat(z0),z1) a__U15(z0,z1) -> U15(z0,z1) a__U15(tt(),z0) -> a__U16(a__isNat(z0)) a__U16(z0) -> U16(z0) a__U16(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNatKind(z0),z0) a__U22(z0,z1) -> U22(z0,z1) a__U22(tt(),z0) -> a__U23(a__isNat(z0)) a__U23(z0) -> U23(z0) a__U23(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatKind(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0) -> U41(z0) a__U41(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatKind(z0),z0) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> mark(z0) a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNatKind(z0),z0,z1) a__U62(z0,z1,z2) -> U62(z0,z1,z2) a__U62(tt(),z0,z1) -> a__U63(a__isNat(z1),z0,z1) a__U63(z0,z1,z2) -> U63(z0,z1,z2) a__U63(tt(),z0,z1) -> a__U64(a__isNatKind(z1),z0,z1) a__U64(z0,z1,z2) -> U64(z0,z1,z2) a__U64(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNatKind(z0),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__U31(a__isNatKind(z0),z1) a__isNatKind(s(z0)) -> a__U41(a__isNatKind(z0)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U51(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U61(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U13(z0,z1,z2)) -> a__U13(mark(z0),z1,z2) mark(U14(z0,z1,z2)) -> a__U14(mark(z0),z1,z2) mark(U15(z0,z1)) -> a__U15(mark(z0),z1) mark(U16(z0)) -> a__U16(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0,z1)) -> a__U22(mark(z0),z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0)) -> a__U41(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1,z2)) -> a__U62(mark(z0),z1,z2) mark(U63(z0,z1,z2)) -> a__U63(mark(z0),z1,z2) mark(U64(z0,z1,z2)) -> a__U64(mark(z0),z1,z2) 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__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/3,A__U13/3,A__U14/3,A__U15/2,A__U16/1,A__U21/2,A__U22/2 ,A__U23/1,A__U31/2,A__U32/1,A__U41/1,A__U51/2,A__U52/2,A__U61/3,A__U62/3,A__U63/3,A__U64/3,MARK/1,a__U11/3 ,a__U12/3,a__U13/3,a__U14/3,a__U15/2,a__U16/1,a__U21/2,a__U22/2,a__U23/1,a__U31/2,a__U32/1,a__U41/1,a__U51/2 ,a__U52/2,a__U61/3,a__U62/3,a__U63/3,a__U64/3,a__isNat/1,a__isNatKind/1,a__plus/2,mark/1} / {0/0,U11/3,U12/3 ,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,c/2,c1/0 ,c10/0,c11/0,c12/2,c13/0,c14/2,c15/0,c16/0,c17/0,c18/2,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/2,c25/0,c26/1 ,c27/0,c28/2,c29/0,c3/0,c30/2,c31/0,c32/2,c33/0,c34/2,c35/2,c36/0,c37/0,c38/2,c39/2,c4/2,c40/0,c41/0,c42/2 ,c43/2,c44/0,c45/2,c46/2,c47/0,c48/2,c49/2,c5/0,c50/1,c51/2,c52/2,c53/2,c54/1,c55/2,c56/2,c57/2,c58/2,c59/2 ,c6/2,c60/2,c61/2,c62/2,c63/2,c64/2,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/0,c71/1,c72/0,c8/2,c9/0,isNat/1 ,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13,A__U14 ,A__U15,A__U16,A__U21,A__U22,A__U23,A__U31,A__U32,A__U41,A__U51,A__U52,A__U61,A__U62,A__U63,A__U64,MARK ,a__U11,a__U12,a__U13,a__U14,a__U15,a__U16,a__U21,a__U22,a__U23,a__U31,a__U32,a__U41,a__U51,a__U52,a__U61 ,a__U62,a__U63,a__U64,a__isNat,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U14,U15,U16,U21 ,U22,U23,U31,U32,U41,U51,U52,U61,U62,U63,U64,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,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,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__ISNAT(z0) -> c40() A__ISNAT(0()) -> c37() A__ISNAT(plus(z0,z1)) -> c38(A__U11(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__ISNAT(s(z0)) -> c39(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c44() A__ISNATKIND(0()) -> c41() A__ISNATKIND(plus(z0,z1)) -> c42(A__U31(a__isNatKind(z0),z1),A__ISNATKIND(z0)) A__ISNATKIND(s(z0)) -> c43(A__U41(a__isNatKind(z0)),A__ISNATKIND(z0)) A__PLUS(z0,z1) -> c47() A__PLUS(z0,0()) -> c45(A__U51(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c46(A__U61(a__isNat(z1),z1,z0),A__ISNAT(z1)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U12(z0,z1,z2) -> c3() A__U12(tt(),z0,z1) -> c2(A__U13(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U13(z0,z1,z2) -> c5() A__U13(tt(),z0,z1) -> c4(A__U14(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U14(z0,z1,z2) -> c7() A__U14(tt(),z0,z1) -> c6(A__U15(a__isNat(z0),z1),A__ISNAT(z0)) A__U15(z0,z1) -> c9() A__U15(tt(),z0) -> c8(A__U16(a__isNat(z0)),A__ISNAT(z0)) A__U16(z0) -> c11() A__U16(tt()) -> c10() A__U21(z0,z1) -> c13() A__U21(tt(),z0) -> c12(A__U22(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U22(z0,z1) -> c15() A__U22(tt(),z0) -> c14(A__U23(a__isNat(z0)),A__ISNAT(z0)) A__U23(z0) -> c17() A__U23(tt()) -> c16() A__U31(z0,z1) -> c19() A__U31(tt(),z0) -> c18(A__U32(a__isNatKind(z0)),A__ISNATKIND(z0)) A__U32(z0) -> c21() A__U32(tt()) -> c20() A__U41(z0) -> c23() A__U41(tt()) -> c22() A__U51(z0,z1) -> c25() A__U51(tt(),z0) -> c24(A__U52(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__U52(z0,z1) -> c27() A__U52(tt(),z0) -> c26(MARK(z0)) A__U61(z0,z1,z2) -> c29() A__U61(tt(),z0,z1) -> c28(A__U62(a__isNatKind(z0),z0,z1),A__ISNATKIND(z0)) A__U62(z0,z1,z2) -> c31() A__U62(tt(),z0,z1) -> c30(A__U63(a__isNat(z1),z0,z1),A__ISNAT(z1)) A__U63(z0,z1,z2) -> c33() A__U63(tt(),z0,z1) -> c32(A__U64(a__isNatKind(z1),z0,z1),A__ISNATKIND(z1)) A__U64(z0,z1,z2) -> c36() A__U64(tt(),z0,z1) -> c34(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U64(tt(),z0,z1) -> c35(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c72() MARK(U11(z0,z1,z2)) -> c48(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c49(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U13(z0,z1,z2)) -> c51(A__U13(mark(z0),z1,z2),MARK(z0)) MARK(U14(z0,z1,z2)) -> c52(A__U14(mark(z0),z1,z2),MARK(z0)) MARK(U15(z0,z1)) -> c53(A__U15(mark(z0),z1),MARK(z0)) MARK(U16(z0)) -> c55(A__U16(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c56(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0,z1)) -> c57(A__U22(mark(z0),z1),MARK(z0)) MARK(U23(z0)) -> c58(A__U23(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c59(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c60(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0)) -> c61(A__U41(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c62(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0,z1)) -> c63(A__U52(mark(z0),z1),MARK(z0)) MARK(U61(z0,z1,z2)) -> c64(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1,z2)) -> c65(A__U62(mark(z0),z1,z2),MARK(z0)) MARK(U63(z0,z1,z2)) -> c66(A__U63(mark(z0),z1,z2),MARK(z0)) MARK(U64(z0,z1,z2)) -> c67(A__U64(mark(z0),z1,z2),MARK(z0)) MARK(isNat(z0)) -> c54(A__ISNAT(z0)) MARK(isNatKind(z0)) -> c50(A__ISNATKIND(z0)) MARK(plus(z0,z1)) -> c68(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c69(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c71(MARK(z0)) MARK(tt()) -> c70() - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(a__isNatKind(z0),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> a__U13(a__isNatKind(z1),z0,z1) a__U13(z0,z1,z2) -> U13(z0,z1,z2) a__U13(tt(),z0,z1) -> a__U14(a__isNatKind(z1),z0,z1) a__U14(z0,z1,z2) -> U14(z0,z1,z2) a__U14(tt(),z0,z1) -> a__U15(a__isNat(z0),z1) a__U15(z0,z1) -> U15(z0,z1) a__U15(tt(),z0) -> a__U16(a__isNat(z0)) a__U16(z0) -> U16(z0) a__U16(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNatKind(z0),z0) a__U22(z0,z1) -> U22(z0,z1) a__U22(tt(),z0) -> a__U23(a__isNat(z0)) a__U23(z0) -> U23(z0) a__U23(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatKind(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0) -> U41(z0) a__U41(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatKind(z0),z0) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> mark(z0) a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNatKind(z0),z0,z1) a__U62(z0,z1,z2) -> U62(z0,z1,z2) a__U62(tt(),z0,z1) -> a__U63(a__isNat(z1),z0,z1) a__U63(z0,z1,z2) -> U63(z0,z1,z2) a__U63(tt(),z0,z1) -> a__U64(a__isNatKind(z1),z0,z1) a__U64(z0,z1,z2) -> U64(z0,z1,z2) a__U64(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(plus(z0,z1)) -> a__U11(a__isNatKind(z0),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__U31(a__isNatKind(z0),z1) a__isNatKind(s(z0)) -> a__U41(a__isNatKind(z0)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U51(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U61(a__isNat(z1),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U13(z0,z1,z2)) -> a__U13(mark(z0),z1,z2) mark(U14(z0,z1,z2)) -> a__U14(mark(z0),z1,z2) mark(U15(z0,z1)) -> a__U15(mark(z0),z1) mark(U16(z0)) -> a__U16(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0,z1)) -> a__U22(mark(z0),z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0)) -> a__U41(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1,z2)) -> a__U62(mark(z0),z1,z2) mark(U63(z0,z1,z2)) -> a__U63(mark(z0),z1,z2) mark(U64(z0,z1,z2)) -> a__U64(mark(z0),z1,z2) 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__ISNAT/1,A__ISNATKIND/1,A__PLUS/2,A__U11/3,A__U12/3,A__U13/3,A__U14/3,A__U15/2,A__U16/1,A__U21/2,A__U22/2 ,A__U23/1,A__U31/2,A__U32/1,A__U41/1,A__U51/2,A__U52/2,A__U61/3,A__U62/3,A__U63/3,A__U64/3,MARK/1,a__U11/3 ,a__U12/3,a__U13/3,a__U14/3,a__U15/2,a__U16/1,a__U21/2,a__U22/2,a__U23/1,a__U31/2,a__U32/1,a__U41/1,a__U51/2 ,a__U52/2,a__U61/3,a__U62/3,a__U63/3,a__U64/3,a__isNat/1,a__isNatKind/1,a__plus/2,mark/1} / {0/0,U11/3,U12/3 ,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,c/2,c1/0 ,c10/0,c11/0,c12/2,c13/0,c14/2,c15/0,c16/0,c17/0,c18/2,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/2,c25/0,c26/1 ,c27/0,c28/2,c29/0,c3/0,c30/2,c31/0,c32/2,c33/0,c34/2,c35/2,c36/0,c37/0,c38/2,c39/2,c4/2,c40/0,c41/0,c42/2 ,c43/2,c44/0,c45/2,c46/2,c47/0,c48/2,c49/2,c5/0,c50/1,c51/2,c52/2,c53/2,c54/1,c55/2,c56/2,c57/2,c58/2,c59/2 ,c6/2,c60/2,c61/2,c62/2,c63/2,c64/2,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/0,c71/1,c72/0,c8/2,c9/0,isNat/1 ,isNatKind/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATKIND,A__PLUS,A__U11,A__U12,A__U13,A__U14 ,A__U15,A__U16,A__U21,A__U22,A__U23,A__U31,A__U32,A__U41,A__U51,A__U52,A__U61,A__U62,A__U63,A__U64,MARK ,a__U11,a__U12,a__U13,a__U14,a__U15,a__U16,a__U21,a__U22,a__U23,a__U31,a__U32,a__U41,a__U51,a__U52,a__U61 ,a__U62,a__U63,a__U64,a__isNat,a__isNatKind,a__plus,mark} and constructors {0,U11,U12,U13,U14,U15,U16,U21 ,U22,U23,U31,U32,U41,U51,U52,U61,U62,U63,U64,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,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,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)) ->^+ c42(A__U31(a__isNatKind(x),y),A__ISNATKIND(x)) = C[A__ISNATKIND(x) = A__ISNATKIND(x){}] WORST_CASE(Omega(n^1),?)