WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(l1,l2) -> append#1(l1,l2) append#1(cons(x,xs),l2) -> cons(x,append(xs,l2)) append#1(nil(),l2) -> l2 appendAll(l) -> appendAll#1(l) appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls)) appendAll#1(nil()) -> nil() appendAll2(l) -> appendAll2#1(l) appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) -> nil() appendAll3(l) -> appendAll3#1(l) appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) -> nil() - Signature: {append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1 ,appendAll3#1/1} / {cons/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil} + 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(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: {append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1} TcT has computed the following interpretation: p(append) = x1 + x2 p(append#1) = x1 + x2 p(appendAll) = x1 p(appendAll#1) = x1 p(appendAll2) = 4 + 8*x1 p(appendAll2#1) = 1 + 8*x1 p(appendAll3) = 1 + 8*x1 p(appendAll3#1) = 1 + 8*x1 p(cons) = 1 + x1 + x2 p(nil) = 1 Following rules are strictly oriented: append#1(nil(),l2) = 1 + l2 > l2 = l2 appendAll#1(cons(l1,ls)) = 1 + l1 + ls > l1 + ls = append(l1,appendAll(ls)) appendAll2(l) = 4 + 8*l > 1 + 8*l = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = 9 + 8*l1 + 8*ls > 4 + l1 + 8*ls = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = 9 > 1 = nil() appendAll3#1(cons(l1,ls)) = 9 + 8*l1 + 8*ls > 5 + 8*l1 + 8*ls = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = 9 > 1 = nil() Following rules are (at-least) weakly oriented: append(l1,l2) = l1 + l2 >= l1 + l2 = append#1(l1,l2) append#1(cons(x,xs),l2) = 1 + l2 + x + xs >= 1 + l2 + x + xs = cons(x,append(xs,l2)) appendAll(l) = l >= l = appendAll#1(l) appendAll#1(nil()) = 1 >= 1 = nil() appendAll3(l) = 1 + 8*l >= 1 + 8*l = appendAll3#1(l) * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(l1,l2) -> append#1(l1,l2) append#1(cons(x,xs),l2) -> cons(x,append(xs,l2)) appendAll(l) -> appendAll#1(l) appendAll#1(nil()) -> nil() appendAll3(l) -> appendAll3#1(l) - Weak TRS: append#1(nil(),l2) -> l2 appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls)) appendAll2(l) -> appendAll2#1(l) appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) -> nil() appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) -> nil() - Signature: {append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1 ,appendAll3#1/1} / {cons/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil} + 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(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: {append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1} TcT has computed the following interpretation: p(append) = [2] x1 + [1] x2 + [1] p(append#1) = [2] x1 + [1] x2 + [0] p(appendAll) = [2] x1 + [2] p(appendAll#1) = [2] x1 + [1] p(appendAll2) = [4] x1 + [0] p(appendAll2#1) = [4] x1 + [0] p(appendAll3) = [9] x1 + [1] p(appendAll3#1) = [9] x1 + [0] p(cons) = [1] x1 + [1] x2 + [3] p(nil) = [2] Following rules are strictly oriented: append(l1,l2) = [2] l1 + [1] l2 + [1] > [2] l1 + [1] l2 + [0] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [2] x + [2] xs + [6] > [1] l2 + [1] x + [2] xs + [4] = cons(x,append(xs,l2)) appendAll(l) = [2] l + [2] > [2] l + [1] = appendAll#1(l) appendAll#1(nil()) = [5] > [2] = nil() appendAll3(l) = [9] l + [1] > [9] l + [0] = appendAll3#1(l) Following rules are (at-least) weakly oriented: append#1(nil(),l2) = [1] l2 + [4] >= [1] l2 + [0] = l2 appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [7] >= [2] l1 + [2] ls + [3] = append(l1,appendAll(ls)) appendAll2(l) = [4] l + [0] >= [4] l + [0] = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = [4] l1 + [4] ls + [12] >= [4] l1 + [4] ls + [5] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [8] >= [2] = nil() appendAll3#1(cons(l1,ls)) = [9] l1 + [9] ls + [27] >= [8] l1 + [9] ls + [2] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [18] >= [2] = nil() * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: append(l1,l2) -> append#1(l1,l2) append#1(cons(x,xs),l2) -> cons(x,append(xs,l2)) append#1(nil(),l2) -> l2 appendAll(l) -> appendAll#1(l) appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls)) appendAll#1(nil()) -> nil() appendAll2(l) -> appendAll2#1(l) appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) -> nil() appendAll3(l) -> appendAll3#1(l) appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) -> nil() - Signature: {append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1 ,appendAll3#1/1} / {cons/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))