WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: bits(0()) -> 0() bits(s(0())) -> s(0()) bits(s(s(x))) -> s(bits(s(half(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} 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(bits) = {1}, uargs(s) = {1} Following symbols are considered usable: {bits,half} TcT has computed the following interpretation: p(0) = [0] p(bits) = [1] x1 + [4] p(half) = [1] x1 + [0] p(s) = [1] x1 + [0] Following rules are strictly oriented: bits(0()) = [4] > [0] = 0() bits(s(0())) = [4] > [0] = s(0()) Following rules are (at-least) weakly oriented: bits(s(s(x))) = [1] x + [4] >= [1] x + [4] = s(bits(s(half(x)))) half(0()) = [0] >= [0] = 0() half(s(0())) = [0] >= [0] = 0() half(s(s(x))) = [1] x + [0] >= [1] x + [0] = s(half(x)) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: bits(s(s(x))) -> s(bits(s(half(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Weak TRS: bits(0()) -> 0() bits(s(0())) -> s(0()) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} and constructors {0,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(bits) = {1}, uargs(s) = {1} Following symbols are considered usable: {bits,half} TcT has computed the following interpretation: p(0) = 0 p(bits) = 9 + 8*x1 p(half) = x1 p(s) = 1 + x1 Following rules are strictly oriented: bits(s(s(x))) = 25 + 8*x > 18 + 8*x = s(bits(s(half(x)))) half(s(0())) = 1 > 0 = 0() half(s(s(x))) = 2 + x > 1 + x = s(half(x)) Following rules are (at-least) weakly oriented: bits(0()) = 9 >= 0 = 0() bits(s(0())) = 17 >= 1 = s(0()) half(0()) = 0 >= 0 = 0() * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: half(0()) -> 0() - Weak TRS: bits(0()) -> 0() bits(s(0())) -> s(0()) bits(s(s(x))) -> s(bits(s(half(x)))) half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} 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(bits) = {1}, uargs(s) = {1} Following symbols are considered usable: {bits,half} TcT has computed the following interpretation: p(0) = [2] p(bits) = [4] x1 + [6] p(half) = [1] x1 + [1] p(s) = [1] x1 + [3] Following rules are strictly oriented: half(0()) = [3] > [2] = 0() Following rules are (at-least) weakly oriented: bits(0()) = [14] >= [2] = 0() bits(s(0())) = [26] >= [5] = s(0()) bits(s(s(x))) = [4] x + [30] >= [4] x + [25] = s(bits(s(half(x)))) half(s(0())) = [6] >= [2] = 0() half(s(s(x))) = [1] x + [7] >= [1] x + [4] = s(half(x)) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: bits(0()) -> 0() bits(s(0())) -> s(0()) bits(s(s(x))) -> s(bits(s(half(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))