WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(0(),z0) -> c() +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(0(),z0) -> c() +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(0(),z0) -> c() +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: *'(x,y){x -> p(x)} = *'(p(x),y) ->^+ c8(+'(*(x,y),minus(y)),*'(x,y)) = C[*'(x,y) = *'(x,y){}] ** Step 1.b:1: Ara. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(0(),z0) -> c() +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "*") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "*'") :: ["A"(2) x "A"(1)] -(1)-> "A"(0) F (TrsFun "+") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "+'") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "0") :: [] -(0)-> "A"(2) F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "MINUS") :: ["A"(1)] -(1)-> "A"(0) F (TrsFun "c") :: [] -(0)-> "A"(0) F (TrsFun "c1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c2") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c3") :: [] -(0)-> "A"(0) F (TrsFun "c4") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c5") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c6") :: [] -(0)-> "A"(0) F (TrsFun "c7") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c8") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c9") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "minus") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "p") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "p") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "p") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "s") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "s") :: ["A"(1)] -(1)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) +'(0(),z0) -> c() MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) 2. Weak: *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) ** Step 1.b:2: Ara. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) +'(0(),z0) -> c() MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "*") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "*'") :: ["A"(1) x "A"(0)] -(0)-> "A"(0) F (TrsFun "+") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "+'") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "MINUS") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c") :: [] -(0)-> "A"(0) F (TrsFun "c1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c2") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c3") :: [] -(0)-> "A"(0) F (TrsFun "c4") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c5") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c6") :: [] -(0)-> "A"(0) F (TrsFun "c7") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c8") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c9") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "minus") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "p") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "p") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "s") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) 2. Weak: +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) ** Step 1.b:3: NaturalPI. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) +'(0(),z0) -> c() MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: NaturalPI {shape = Mixed 3, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(3)): The following argument positions are considered usable: uargs(+) = {1,2}, uargs(+') = {1,2}, uargs(c1) = {1}, uargs(c2) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1,2}, uargs(c8) = {1,2}, uargs(c9) = {1,2}, uargs(p) = {1}, uargs(s) = {1} Following symbols are considered usable: {*,*',+,+',MINUS,minus} TcT has computed the following interpretation: p(*) = x1*x2 p(*') = x1*x2^2 + x1^2*x2 + x2 + x2^2 p(+) = x1 + x2 p(+') = x1 + x2 p(0) = 0 p(MINUS) = 0 p(c) = 0 p(c1) = x1 p(c2) = x1 p(c3) = 0 p(c4) = x1 p(c5) = x1 p(c6) = 0 p(c7) = x1 + x2 p(c8) = x1 + x2 p(c9) = x1 + x2 p(minus) = x1 p(p) = 1 + x1 p(s) = 1 + x1 Following rules are strictly oriented: +'(p(z0),z1) = 1 + z0 + z1 > z0 + z1 = c2(+'(z0,z1)) +'(s(z0),z1) = 1 + z0 + z1 > z0 + z1 = c1(+'(z0,z1)) Following rules are (at-least) weakly oriented: *(0(),z0) = 0 >= 0 = 0() *(p(z0),z1) = z0*z1 + z1 >= z0*z1 + z1 = +(*(z0,z1),minus(z1)) *(s(z0),z1) = z0*z1 + z1 >= z0*z1 + z1 = +(*(z0,z1),z1) *'(0(),z0) = z0 + z0^2 >= 0 = c6() *'(p(z0),z1) = 2*z0*z1 + z0*z1^2 + z0^2*z1 + 2*z1 + 2*z1^2 >= z0*z1 + z0*z1^2 + z0^2*z1 + 2*z1 + z1^2 = c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) = 2*z0*z1 + z0*z1^2 + z0^2*z1 + 2*z1 + 2*z1^2 >= z0*z1 + z1 = c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) = 2*z0*z1 + z0*z1^2 + z0^2*z1 + 2*z1 + 2*z1^2 >= z0*z1 + z0*z1^2 + z0^2*z1 + 2*z1 + z1^2 = c7(+'(*(z0,z1),z1),*'(z0,z1)) +(0(),z0) = z0 >= z0 = z0 +(p(z0),z1) = 1 + z0 + z1 >= 1 + z0 + z1 = p(+(z0,z1)) +(s(z0),z1) = 1 + z0 + z1 >= 1 + z0 + z1 = s(+(z0,z1)) +'(0(),z0) = z0 >= 0 = c() MINUS(0()) = 0 >= 0 = c3() MINUS(p(z0)) = 0 >= 0 = c5(MINUS(z0)) MINUS(s(z0)) = 0 >= 0 = c4(MINUS(z0)) minus(0()) = 0 >= 0 = 0() minus(p(z0)) = 1 + z0 >= 1 + z0 = s(minus(z0)) minus(s(z0)) = 1 + z0 >= 1 + z0 = p(minus(z0)) ** Step 1.b:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(0(),z0) -> 0() *(p(z0),z1) -> +(*(z0,z1),minus(z1)) *(s(z0),z1) -> +(*(z0,z1),z1) *'(0(),z0) -> c6() *'(p(z0),z1) -> c8(+'(*(z0,z1),minus(z1)),*'(z0,z1)) *'(p(z0),z1) -> c9(+'(*(z0,z1),minus(z1)),MINUS(z1)) *'(s(z0),z1) -> c7(+'(*(z0,z1),z1),*'(z0,z1)) +(0(),z0) -> z0 +(p(z0),z1) -> p(+(z0,z1)) +(s(z0),z1) -> s(+(z0,z1)) +'(0(),z0) -> c() +'(p(z0),z1) -> c2(+'(z0,z1)) +'(s(z0),z1) -> c1(+'(z0,z1)) MINUS(0()) -> c3() MINUS(p(z0)) -> c5(MINUS(z0)) MINUS(s(z0)) -> c4(MINUS(z0)) minus(0()) -> 0() minus(p(z0)) -> s(minus(z0)) minus(s(z0)) -> p(minus(z0)) - Signature: {*/2,*'/2,+/2,+'/2,MINUS/1,minus/1} / {0/0,c/0,c1/1,c2/1,c3/0,c4/1,c5/1,c6/0,c7/2,c8/2,c9/2,p/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+,+',MINUS,minus} and constructors {0,c,c1,c2,c3,c4 ,c5,c6,c7,c8,c9,p,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))