WORST_CASE(?,O(n^1)) * Step 1: 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)) 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: 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) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(appendAll) = [2] x1 + [3] p(appendAll#1) = [2] x1 + [0] p(appendAll2) = [2] x1 + [1] p(appendAll2#1) = [2] x1 + [1] p(appendAll3) = [4] x1 + [1] p(appendAll3#1) = [4] x1 + [1] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [0] Following rules are strictly oriented: appendAll(l) = [2] l + [3] > [2] l + [0] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [4] > [1] l1 + [2] ls + [3] = append(l1,appendAll(ls)) appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [5] > [2] l1 + [2] ls + [4] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [1] > [0] = nil() appendAll3#1(cons(l1,ls)) = [4] l1 + [4] ls + [9] > [2] l1 + [4] ls + [2] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [1] > [0] = nil() Following rules are (at-least) weakly oriented: append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [2] >= [1] l2 + [1] x + [1] xs + [2] = cons(x,append(xs,l2)) append#1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 appendAll#1(nil()) = [0] >= [0] = nil() appendAll2(l) = [2] l + [1] >= [2] l + [1] = appendAll2#1(l) appendAll3(l) = [4] l + [1] >= [4] l + [1] = 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)) append#1(nil(),l2) -> l2 appendAll#1(nil()) -> nil() appendAll2(l) -> appendAll2#1(l) appendAll3(l) -> appendAll3#1(l) - Weak TRS: appendAll(l) -> appendAll#1(l) appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls)) 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) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(appendAll) = [1] x1 + [0] p(appendAll#1) = [1] x1 + [0] p(appendAll2) = [1] x1 + [8] p(appendAll2#1) = [1] x1 + [0] p(appendAll3) = [1] x1 + [4] p(appendAll3#1) = [1] x1 + [4] p(cons) = [1] x1 + [1] x2 + [9] p(nil) = [0] Following rules are strictly oriented: appendAll2(l) = [1] l + [8] > [1] l + [0] = appendAll2#1(l) Following rules are (at-least) weakly oriented: append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [9] >= [1] l2 + [1] x + [1] xs + [9] = cons(x,append(xs,l2)) append#1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 appendAll(l) = [1] l + [0] >= [1] l + [0] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [1] l1 + [1] ls + [9] >= [1] l1 + [1] ls + [0] = append(l1,appendAll(ls)) appendAll#1(nil()) = [0] >= [0] = nil() appendAll2#1(cons(l1,ls)) = [1] l1 + [1] ls + [9] >= [1] l1 + [1] ls + [8] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [0] >= [0] = nil() appendAll3(l) = [1] l + [4] >= [1] l + [4] = appendAll3#1(l) appendAll3#1(cons(l1,ls)) = [1] l1 + [1] ls + [13] >= [1] l1 + [1] ls + [12] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [4] >= [0] = nil() * Step 3: 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)) append#1(nil(),l2) -> l2 appendAll#1(nil()) -> nil() appendAll3(l) -> appendAll3#1(l) - Weak TRS: appendAll(l) -> appendAll#1(l) 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) = [1] x1 + [1] x2 + [12] p(append#1) = [1] x1 + [1] x2 + [12] p(appendAll) = [2] x1 + [0] p(appendAll#1) = [2] x1 + [0] p(appendAll2) = [2] x1 + [0] p(appendAll2#1) = [2] x1 + [0] p(appendAll3) = [2] x1 + [0] p(appendAll3#1) = [2] x1 + [0] p(cons) = [1] x1 + [1] x2 + [6] p(nil) = [0] Following rules are strictly oriented: append#1(nil(),l2) = [1] l2 + [12] > [1] l2 + [0] = l2 Following rules are (at-least) weakly oriented: append(l1,l2) = [1] l1 + [1] l2 + [12] >= [1] l1 + [1] l2 + [12] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [18] >= [1] l2 + [1] x + [1] xs + [18] = cons(x,append(xs,l2)) appendAll(l) = [2] l + [0] >= [2] l + [0] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [12] >= [1] l1 + [2] ls + [12] = append(l1,appendAll(ls)) appendAll#1(nil()) = [0] >= [0] = nil() appendAll2(l) = [2] l + [0] >= [2] l + [0] = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [12] >= [2] l1 + [2] ls + [12] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [0] >= [0] = nil() appendAll3(l) = [2] l + [0] >= [2] l + [0] = appendAll3#1(l) appendAll3#1(cons(l1,ls)) = [2] l1 + [2] ls + [12] >= [2] l1 + [2] ls + [12] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [0] >= [0] = nil() * Step 4: 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#1(nil()) -> nil() appendAll3(l) -> appendAll3#1(l) - Weak TRS: append#1(nil(),l2) -> l2 appendAll(l) -> appendAll#1(l) 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 + [0] p(append#1) = [2] x1 + [1] x2 + [0] p(appendAll) = [2] x1 + [0] p(appendAll#1) = [2] x1 + [0] p(appendAll2) = [4] x1 + [0] p(appendAll2#1) = [4] x1 + [0] p(appendAll3) = [8] x1 + [9] p(appendAll3#1) = [8] x1 + [9] p(cons) = [1] x1 + [1] x2 + [0] p(nil) = [1] Following rules are strictly oriented: appendAll#1(nil()) = [2] > [1] = nil() Following rules are (at-least) weakly oriented: append(l1,l2) = [2] l1 + [1] l2 + [0] >= [2] l1 + [1] l2 + [0] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [2] x + [2] xs + [0] >= [1] l2 + [1] x + [2] xs + [0] = cons(x,append(xs,l2)) append#1(nil(),l2) = [1] l2 + [2] >= [1] l2 + [0] = l2 appendAll(l) = [2] l + [0] >= [2] l + [0] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [0] >= [2] l1 + [2] ls + [0] = append(l1,appendAll(ls)) appendAll2(l) = [4] l + [0] >= [4] l + [0] = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = [4] l1 + [4] ls + [0] >= [4] l1 + [4] ls + [0] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [4] >= [1] = nil() appendAll3(l) = [8] l + [9] >= [8] l + [9] = appendAll3#1(l) appendAll3#1(cons(l1,ls)) = [8] l1 + [8] ls + [9] >= [8] l1 + [8] ls + [9] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [17] >= [1] = nil() * Step 5: 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)) appendAll3(l) -> appendAll3#1(l) - Weak TRS: 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#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) = [1] x1 + [1] x2 + [1] p(append#1) = [1] x1 + [1] x2 + [1] p(appendAll) = [1] x1 + [0] p(appendAll#1) = [1] x1 + [0] p(appendAll2) = [2] x1 + [9] p(appendAll2#1) = [2] x1 + [6] p(appendAll3) = [8] x1 + [6] p(appendAll3#1) = [8] x1 + [0] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [1] Following rules are strictly oriented: appendAll3(l) = [8] l + [6] > [8] l + [0] = appendAll3#1(l) Following rules are (at-least) weakly oriented: append(l1,l2) = [1] l1 + [1] l2 + [1] >= [1] l1 + [1] l2 + [1] = append#1(l1,l2) append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [3] >= [1] l2 + [1] x + [1] xs + [3] = cons(x,append(xs,l2)) append#1(nil(),l2) = [1] l2 + [2] >= [1] l2 + [0] = l2 appendAll(l) = [1] l + [0] >= [1] l + [0] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [1] l1 + [1] ls + [2] >= [1] l1 + [1] ls + [1] = append(l1,appendAll(ls)) appendAll#1(nil()) = [1] >= [1] = nil() appendAll2(l) = [2] l + [9] >= [2] l + [6] = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [10] >= [1] l1 + [2] ls + [10] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [8] >= [1] = nil() appendAll3#1(cons(l1,ls)) = [8] l1 + [8] ls + [16] >= [2] l1 + [8] ls + [16] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [8] >= [1] = nil() * Step 6: 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)) - Weak TRS: 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) = 2*x1 + x2 p(append#1) = 2*x1 + x2 p(appendAll) = 3*x1 p(appendAll#1) = 3*x1 p(appendAll2) = 1 + 7*x1 p(appendAll2#1) = 1 + 7*x1 p(appendAll3) = 5 + 14*x1 p(appendAll3#1) = 4 + 14*x1 p(cons) = 1 + x1 + x2 p(nil) = 0 Following rules are strictly oriented: append#1(cons(x,xs),l2) = 2 + l2 + 2*x + 2*xs > 1 + l2 + x + 2*xs = cons(x,append(xs,l2)) Following rules are (at-least) weakly oriented: append(l1,l2) = 2*l1 + l2 >= 2*l1 + l2 = append#1(l1,l2) append#1(nil(),l2) = l2 >= l2 = l2 appendAll(l) = 3*l >= 3*l = appendAll#1(l) appendAll#1(cons(l1,ls)) = 3 + 3*l1 + 3*ls >= 2*l1 + 3*ls = append(l1,appendAll(ls)) appendAll#1(nil()) = 0 >= 0 = nil() appendAll2(l) = 1 + 7*l >= 1 + 7*l = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = 8 + 7*l1 + 7*ls >= 1 + 6*l1 + 7*ls = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = 1 >= 0 = nil() appendAll3(l) = 5 + 14*l >= 4 + 14*l = appendAll3#1(l) appendAll3#1(cons(l1,ls)) = 18 + 14*l1 + 14*ls >= 7 + 14*l1 + 14*ls = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = 4 >= 0 = nil() * Step 7: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(l1,l2) -> append#1(l1,l2) - Weak TRS: 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: 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 + [4] p(append#1) = [2] x1 + [1] x2 + [3] p(appendAll) = [2] x1 + [2] p(appendAll#1) = [2] x1 + [2] p(appendAll2) = [4] x1 + [0] p(appendAll2#1) = [4] x1 + [0] p(appendAll3) = [11] x1 + [2] p(appendAll3#1) = [11] x1 + [1] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [0] Following rules are strictly oriented: append(l1,l2) = [2] l1 + [1] l2 + [4] > [2] l1 + [1] l2 + [3] = append#1(l1,l2) Following rules are (at-least) weakly oriented: append#1(cons(x,xs),l2) = [1] l2 + [2] x + [2] xs + [7] >= [1] l2 + [1] x + [2] xs + [6] = cons(x,append(xs,l2)) append#1(nil(),l2) = [1] l2 + [3] >= [1] l2 + [0] = l2 appendAll(l) = [2] l + [2] >= [2] l + [2] = appendAll#1(l) appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [6] >= [2] l1 + [2] ls + [6] = append(l1,appendAll(ls)) appendAll#1(nil()) = [2] >= [0] = nil() appendAll2(l) = [4] l + [0] >= [4] l + [0] = appendAll2#1(l) appendAll2#1(cons(l1,ls)) = [4] l1 + [4] ls + [8] >= [4] l1 + [4] ls + [8] = append(appendAll(l1),appendAll2(ls)) appendAll2#1(nil()) = [0] >= [0] = nil() appendAll3(l) = [11] l + [2] >= [11] l + [1] = appendAll3#1(l) appendAll3#1(cons(l1,ls)) = [11] l1 + [11] ls + [23] >= [8] l1 + [11] ls + [6] = append(appendAll2(l1),appendAll3(ls)) appendAll3#1(nil()) = [1] >= [0] = nil() * Step 8: 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))