WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() evenodd(x) -> even(x) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() odd(Cons(x,xs)) -> even(xs) odd(Nil()) -> False() - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + 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: none Following symbols are considered usable: {even,evenodd,notEmpty,odd} TcT has computed the following interpretation: p(Cons) = [0] p(False) = [1] p(Nil) = [0] p(True) = [1] p(even) = [1] p(evenodd) = [5] p(notEmpty) = [1] p(odd) = [1] Following rules are strictly oriented: evenodd(x) = [5] > [1] = even(x) Following rules are (at-least) weakly oriented: even(Cons(x,xs)) = [1] >= [1] = odd(xs) even(Nil()) = [1] >= [1] = True() notEmpty(Cons(x,xs)) = [1] >= [1] = True() notEmpty(Nil()) = [1] >= [1] = False() odd(Cons(x,xs)) = [1] >= [1] = even(xs) odd(Nil()) = [1] >= [1] = False() * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() odd(Cons(x,xs)) -> even(xs) odd(Nil()) -> False() - Weak TRS: evenodd(x) -> even(x) - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + 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: none Following symbols are considered usable: {even,evenodd,notEmpty,odd} TcT has computed the following interpretation: p(Cons) = [8] p(False) = [13] p(Nil) = [0] p(True) = [13] p(even) = [13] p(evenodd) = [13] p(notEmpty) = [14] p(odd) = [13] Following rules are strictly oriented: notEmpty(Cons(x,xs)) = [14] > [13] = True() notEmpty(Nil()) = [14] > [13] = False() Following rules are (at-least) weakly oriented: even(Cons(x,xs)) = [13] >= [13] = odd(xs) even(Nil()) = [13] >= [13] = True() evenodd(x) = [13] >= [13] = even(x) odd(Cons(x,xs)) = [13] >= [13] = even(xs) odd(Nil()) = [13] >= [13] = False() * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() odd(Cons(x,xs)) -> even(xs) odd(Nil()) -> False() - Weak TRS: evenodd(x) -> even(x) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + 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: none Following symbols are considered usable: {even,evenodd,notEmpty,odd} TcT has computed the following interpretation: p(Cons) = [1] x2 + [1] p(False) = [15] p(Nil) = [1] p(True) = [15] p(even) = [2] x1 + [15] p(evenodd) = [2] x1 + [15] p(notEmpty) = [8] x1 + [7] p(odd) = [2] x1 + [13] Following rules are strictly oriented: even(Cons(x,xs)) = [2] xs + [17] > [2] xs + [13] = odd(xs) even(Nil()) = [17] > [15] = True() Following rules are (at-least) weakly oriented: evenodd(x) = [2] x + [15] >= [2] x + [15] = even(x) notEmpty(Cons(x,xs)) = [8] xs + [15] >= [15] = True() notEmpty(Nil()) = [15] >= [15] = False() odd(Cons(x,xs)) = [2] xs + [15] >= [2] xs + [15] = even(xs) odd(Nil()) = [15] >= [15] = False() * Step 4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: odd(Cons(x,xs)) -> even(xs) odd(Nil()) -> False() - Weak TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() evenodd(x) -> even(x) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + 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: none Following symbols are considered usable: {even,evenodd,notEmpty,odd} TcT has computed the following interpretation: p(Cons) = [0] p(False) = [0] p(Nil) = [0] p(True) = [0] p(even) = [1] p(evenodd) = [2] p(notEmpty) = [10] p(odd) = [1] Following rules are strictly oriented: odd(Nil()) = [1] > [0] = False() Following rules are (at-least) weakly oriented: even(Cons(x,xs)) = [1] >= [1] = odd(xs) even(Nil()) = [1] >= [0] = True() evenodd(x) = [2] >= [1] = even(x) notEmpty(Cons(x,xs)) = [10] >= [0] = True() notEmpty(Nil()) = [10] >= [0] = False() odd(Cons(x,xs)) = [1] >= [1] = even(xs) * Step 5: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: odd(Cons(x,xs)) -> even(xs) - Weak TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() evenodd(x) -> even(x) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() odd(Nil()) -> False() - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + 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: none Following symbols are considered usable: {even,evenodd,notEmpty,odd} TcT has computed the following interpretation: p(Cons) = 2 + x2 p(False) = 5 p(Nil) = 1 p(True) = 6 p(even) = 5 + 8*x1 p(evenodd) = 5 + 8*x1 p(notEmpty) = 8 + 2*x1 p(odd) = 2 + 8*x1 Following rules are strictly oriented: odd(Cons(x,xs)) = 18 + 8*xs > 5 + 8*xs = even(xs) Following rules are (at-least) weakly oriented: even(Cons(x,xs)) = 21 + 8*xs >= 2 + 8*xs = odd(xs) even(Nil()) = 13 >= 6 = True() evenodd(x) = 5 + 8*x >= 5 + 8*x = even(x) notEmpty(Cons(x,xs)) = 12 + 2*xs >= 6 = True() notEmpty(Nil()) = 10 >= 5 = False() odd(Nil()) = 10 >= 5 = False() * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: even(Cons(x,xs)) -> odd(xs) even(Nil()) -> True() evenodd(x) -> even(x) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() odd(Cons(x,xs)) -> even(xs) odd(Nil()) -> False() - Signature: {even/1,evenodd/1,notEmpty/1,odd/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {even,evenodd,notEmpty,odd} and constructors {Cons,False ,Nil,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))