/bin/sh: line 1: 55799 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP55648-90 > /tmp/SMTS55648-91 /bin/sh: line 1: 55832 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP55648-88 > /tmp/SMTS55648-89 /bin/sh: line 1: 55838 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP55648-76 > /tmp/SMTS55648-77 /bin/sh: line 1: 55806 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP55648-47 > /tmp/SMTS55648-49 WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () *** Step 1.a:1.a:1: Ara. MAYBE + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 3, araTimeout = 15, araRuleShifting = Just 1, isBestCase = True, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- 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"(1) F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "main") :: ["A"(1)] -(1)-> "A"(0) F (TrsFun "s") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "sqr") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "sum") :: ["A"(1)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) main(x1) -> sum(x1) 2. Weak: *** Step 1.a:1.b:1: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: sum(x){x -> s(x)} = sum(s(x)) ->^+ +(*(s(x),s(x)),sum(x)) = C[sum(x) = sum(x){}] ** Step 1.b:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(+) = {1,2} Following symbols are considered usable: {sqr,sum} TcT has computed the following interpretation: p(*) = [0] p(+) = [1] x1 + [1] x2 + [0] p(0) = [0] p(s) = [1] x1 + [14] p(sqr) = [0] p(sum) = [1] x1 + [9] Following rules are strictly oriented: sum(0()) = [9] > [0] = 0() sum(s(x)) = [1] x + [23] > [1] x + [9] = +(*(s(x),s(x)),sum(x)) sum(s(x)) = [1] x + [23] > [1] x + [9] = +(sqr(s(x)),sum(x)) Following rules are (at-least) weakly oriented: sqr(x) = [0] >= [0] = *(x,x) ** Step 1.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sqr(x) -> *(x,x) - Weak TRS: sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(+) = {1,2} Following symbols are considered usable: {sqr,sum} TcT has computed the following interpretation: p(*) = [0] p(+) = [1] x1 + [1] x2 + [0] p(0) = [11] p(s) = [1] x1 + [2] p(sqr) = [1] p(sum) = [1] x1 + [6] Following rules are strictly oriented: sqr(x) = [1] > [0] = *(x,x) Following rules are (at-least) weakly oriented: sum(0()) = [17] >= [11] = 0() sum(s(x)) = [1] x + [8] >= [1] x + [6] = +(*(s(x),s(x)),sum(x)) sum(s(x)) = [1] x + [8] >= [1] x + [7] = +(sqr(s(x)),sum(x)) ** Step 1.b:3: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: sqr(x) -> *(x,x) sum(0()) -> 0() sum(s(x)) -> +(*(s(x),s(x)),sum(x)) sum(s(x)) -> +(sqr(s(x)),sum(x)) - Signature: {sqr/1,sum/1} / {*/2,+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sqr,sum} and constructors {*,+,0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))