WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(@l1,@l2) -> append#1(@l1,@l2) append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2)) append#1(nil(),@l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1,@ls)) -> append(@l1,appendAll(@ls)) appendAll#1(nil()) -> nil() appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) -> append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) -> nil() appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@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} / {::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {::,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(@l1,@l2) -> append#1(@l1,@l2) append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2)) append#1(nil(),@l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1,@ls)) -> append(@l1,appendAll(@ls)) appendAll#1(nil()) -> nil() appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) -> append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) -> nil() appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@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} / {::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {::,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(::) = {2}, uargs(append) = {1,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(::) = 4 + x1 + x2 p(append) = x1 + x2 p(append#1) = x1 + x2 p(appendAll) = 1 + 2*x1 p(appendAll#1) = 2*x1 p(appendAll2) = 4 + 4*x1 p(appendAll2#1) = 4*x1 p(appendAll3) = 14 + 4*x1 p(appendAll3#1) = 5 + 4*x1 p(nil) = 1 Following rules are strictly oriented: append#1(nil(),@l2) = 1 + @l2 > @l2 = @l2 appendAll(@l) = 1 + 2*@l > 2*@l = appendAll#1(@l) appendAll#1(::(@l1,@ls)) = 8 + 2*@l1 + 2*@ls > 1 + @l1 + 2*@ls = append(@l1,appendAll(@ls)) appendAll#1(nil()) = 2 > 1 = nil() appendAll2(@l) = 4 + 4*@l > 4*@l = appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) = 16 + 4*@l1 + 4*@ls > 5 + 2*@l1 + 4*@ls = append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) = 4 > 1 = nil() appendAll3(@l) = 14 + 4*@l > 5 + 4*@l = appendAll3#1(@l) appendAll3#1(::(@l1,@ls)) = 21 + 4*@l1 + 4*@ls > 18 + 4*@l1 + 4*@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(::(@x,@xs),@l2) = 4 + @l2 + @x + @xs >= 4 + @l2 + @x + @xs = ::(@x,append(@xs,@l2)) * Step 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(@l1,@l2) -> append#1(@l1,@l2) append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2)) - Weak TRS: append#1(nil(),@l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1,@ls)) -> append(@l1,appendAll(@ls)) appendAll#1(nil()) -> nil() appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) -> append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) -> nil() appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@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} / {::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {::,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(::) = {2}, uargs(append) = {1,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(::) = 3 + x1 + x2 p(append) = 2*x1 + x2 p(append#1) = 2*x1 + x2 p(appendAll) = 2*x1 p(appendAll#1) = 2*x1 p(appendAll2) = 13 + 4*x1 p(appendAll2#1) = 10 + 4*x1 p(appendAll3) = 4 + 10*x1 p(appendAll3#1) = 10*x1 p(nil) = 0 Following rules are strictly oriented: append#1(::(@x,@xs),@l2) = 6 + @l2 + 2*@x + 2*@xs > 3 + @l2 + @x + 2*@xs = ::(@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) = 2*@l >= 2*@l = appendAll#1(@l) appendAll#1(::(@l1,@ls)) = 6 + 2*@l1 + 2*@ls >= 2*@l1 + 2*@ls = append(@l1,appendAll(@ls)) appendAll#1(nil()) = 0 >= 0 = nil() appendAll2(@l) = 13 + 4*@l >= 10 + 4*@l = appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) = 22 + 4*@l1 + 4*@ls >= 13 + 4*@l1 + 4*@ls = append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) = 10 >= 0 = nil() appendAll3(@l) = 4 + 10*@l >= 10*@l = appendAll3#1(@l) appendAll3#1(::(@l1,@ls)) = 30 + 10*@l1 + 10*@ls >= 30 + 8*@l1 + 10*@ls = append(appendAll2(@l1),appendAll3(@ls)) appendAll3#1(nil()) = 0 >= 0 = nil() * Step 4: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(@l1,@l2) -> append#1(@l1,@l2) - Weak TRS: append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2)) append#1(nil(),@l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1,@ls)) -> append(@l1,appendAll(@ls)) appendAll#1(nil()) -> nil() appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) -> append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) -> nil() appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@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} / {::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {::,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(::) = {2}, uargs(append) = {1,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(::) = 1 + x1 + x2 p(append) = 1 + 2*x1 + x2 p(append#1) = 2*x1 + x2 p(appendAll) = 2*x1 p(appendAll#1) = 2*x1 p(appendAll2) = 1 + 4*x1 p(appendAll2#1) = 4*x1 p(appendAll3) = 1 + 8*x1 p(appendAll3#1) = 8*x1 p(nil) = 2 Following rules are strictly oriented: append(@l1,@l2) = 1 + 2*@l1 + @l2 > 2*@l1 + @l2 = append#1(@l1,@l2) Following rules are (at-least) weakly oriented: append#1(::(@x,@xs),@l2) = 2 + @l2 + 2*@x + 2*@xs >= 2 + @l2 + @x + 2*@xs = ::(@x,append(@xs,@l2)) append#1(nil(),@l2) = 4 + @l2 >= @l2 = @l2 appendAll(@l) = 2*@l >= 2*@l = appendAll#1(@l) appendAll#1(::(@l1,@ls)) = 2 + 2*@l1 + 2*@ls >= 1 + 2*@l1 + 2*@ls = append(@l1,appendAll(@ls)) appendAll#1(nil()) = 4 >= 2 = nil() appendAll2(@l) = 1 + 4*@l >= 4*@l = appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) = 4 + 4*@l1 + 4*@ls >= 2 + 4*@l1 + 4*@ls = append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) = 8 >= 2 = nil() appendAll3(@l) = 1 + 8*@l >= 8*@l = appendAll3#1(@l) appendAll3#1(::(@l1,@ls)) = 8 + 8*@l1 + 8*@ls >= 4 + 8*@l1 + 8*@ls = append(appendAll2(@l1),appendAll3(@ls)) appendAll3#1(nil()) = 16 >= 2 = nil() * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: append(@l1,@l2) -> append#1(@l1,@l2) append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2)) append#1(nil(),@l2) -> @l2 appendAll(@l) -> appendAll#1(@l) appendAll#1(::(@l1,@ls)) -> append(@l1,appendAll(@ls)) appendAll#1(nil()) -> nil() appendAll2(@l) -> appendAll2#1(@l) appendAll2#1(::(@l1,@ls)) -> append(appendAll(@l1),appendAll2(@ls)) appendAll2#1(nil()) -> nil() appendAll3(@l) -> appendAll3#1(@l) appendAll3#1(::(@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} / {::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2 ,appendAll2#1,appendAll3,appendAll3#1} and constructors {::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))