WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c6() A__AND(tt(),z0) -> c5(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(plus(z0,z1)) -> c8(A__AND(a__isNat(z0),isNat(z1)),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c9(A__ISNAT(z0)) A__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(A__U11(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c12(A__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) ,A__AND(a__isNat(z1),isNat(z0)) ,A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(MARK(z0)) A__U21(z0,z1,z2) -> c4() A__U21(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U21(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c22() MARK(U11(z0,z1)) -> c14(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2)) -> c15(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c18(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c19(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c16(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c17(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c21(MARK(z0)) MARK(tt()) -> c20() - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> mark(z0) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(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__and(a__isNat(z0),isNat(z1)) a__isNat(s(z0)) -> a__isNat(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U11(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) 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() - Signature: {A__AND/2,A__ISNAT/1,A__PLUS/2,A__U11/2,A__U21/3,MARK/1,a__U11/2,a__U21/3,a__and/2,a__isNat/1,a__plus/2 ,mark/1} / {0/0,U11/2,U21/3,and/2,c/1,c1/0,c10/0,c11/2,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/2 ,c20/0,c21/1,c22/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/2,c9/1,isNat/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__PLUS,A__U11,A__U21,MARK,a__U11,a__U21 ,a__and,a__isNat,a__plus,mark} and constructors {0,U11,U21,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,isNat,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) -> c6() A__AND(tt(),z0) -> c5(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(plus(z0,z1)) -> c8(A__AND(a__isNat(z0),isNat(z1)),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c9(A__ISNAT(z0)) A__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(A__U11(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c12(A__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) ,A__AND(a__isNat(z1),isNat(z0)) ,A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(MARK(z0)) A__U21(z0,z1,z2) -> c4() A__U21(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U21(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c22() MARK(U11(z0,z1)) -> c14(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2)) -> c15(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c18(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c19(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c16(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c17(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c21(MARK(z0)) MARK(tt()) -> c20() - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> mark(z0) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(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__and(a__isNat(z0),isNat(z1)) a__isNat(s(z0)) -> a__isNat(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U11(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) 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() - Signature: {A__AND/2,A__ISNAT/1,A__PLUS/2,A__U11/2,A__U21/3,MARK/1,a__U11/2,a__U21/3,a__and/2,a__isNat/1,a__plus/2 ,mark/1} / {0/0,U11/2,U21/3,and/2,c/1,c1/0,c10/0,c11/2,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/2 ,c20/0,c21/1,c22/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/2,c9/1,isNat/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__PLUS,A__U11,A__U21,MARK,a__U11,a__U21 ,a__and,a__isNat,a__plus,mark} and constructors {0,U11,U21,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,isNat,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) -> c6() A__AND(tt(),z0) -> c5(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(plus(z0,z1)) -> c8(A__AND(a__isNat(z0),isNat(z1)),A__ISNAT(z0)) A__ISNAT(s(z0)) -> c9(A__ISNAT(z0)) A__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(A__U11(a__isNat(z0),z0),A__ISNAT(z0)) A__PLUS(z0,s(z1)) -> c12(A__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) ,A__AND(a__isNat(z1),isNat(z0)) ,A__ISNAT(z1)) A__U11(z0,z1) -> c1() A__U11(tt(),z0) -> c(MARK(z0)) A__U21(z0,z1,z2) -> c4() A__U21(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U21(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) MARK(0()) -> c22() MARK(U11(z0,z1)) -> c14(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2)) -> c15(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(and(z0,z1)) -> c18(A__AND(mark(z0),z1),MARK(z0)) MARK(isNat(z0)) -> c19(A__ISNAT(z0)) MARK(plus(z0,z1)) -> c16(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c17(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c21(MARK(z0)) MARK(tt()) -> c20() - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> mark(z0) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(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__and(a__isNat(z0),isNat(z1)) a__isNat(s(z0)) -> a__isNat(z0) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> a__U11(a__isNat(z0),z0) a__plus(z0,s(z1)) -> a__U21(a__and(a__isNat(z1),isNat(z0)),z1,z0) mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(and(z0,z1)) -> a__and(mark(z0),z1) 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() - Signature: {A__AND/2,A__ISNAT/1,A__PLUS/2,A__U11/2,A__U21/3,MARK/1,a__U11/2,a__U21/3,a__and/2,a__isNat/1,a__plus/2 ,mark/1} / {0/0,U11/2,U21/3,and/2,c/1,c1/0,c10/0,c11/2,c12/3,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/1,c2/2 ,c20/0,c21/1,c22/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/2,c9/1,isNat/1,plus/2,s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__PLUS,A__U11,A__U21,MARK,a__U11,a__U21 ,a__and,a__isNat,a__plus,mark} and constructors {0,U11,U21,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19 ,c2,c20,c21,c22,c3,c4,c5,c6,c7,c8,c9,isNat,plus,s,tt} + 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)) ->^+ c8(A__AND(a__isNat(x),isNat(y)),A__ISNAT(x)) = C[A__ISNAT(x) = A__ISNAT(x){}] WORST_CASE(Omega(n^1),?)