The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

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

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2) [1]
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1]
append#1(nil, @l2) → @l2 [1]
appendAll(@l) → appendAll#1(@l) [1]
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1]
appendAll#1(nil) → nil [1]
appendAll2(@l) → appendAll2#1(@l) [1]
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1]
appendAll2#1(nil) → nil [1]
appendAll3(@l) → appendAll3#1(@l) [1]
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1]
appendAll3#1(nil) → nil [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2) [1]
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1]
append#1(nil, @l2) → @l2 [1]
appendAll(@l) → appendAll#1(@l) [1]
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1]
appendAll#1(nil) → nil [1]
appendAll2(@l) → appendAll2#1(@l) [1]
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1]
appendAll2#1(nil) → nil [1]
appendAll3(@l) → appendAll3#1(@l) [1]
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1]
appendAll3#1(nil) → nil [1]

The TRS has the following type information:

append :: :::nil → :::nil → :::nil append#1 :: :::nil → :::nil → :::nil :: :: :::nil → :::nil → :::nil nil :: :::nil appendAll :: :::nil → :::nil appendAll#1 :: :::nil → :::nil appendAll2 :: :::nil → :::nil appendAll2#1 :: :::nil → :::nil appendAll3 :: :::nil → :::nil appendAll3#1 :: :::nil → :::nil

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none

(c) The following functions are completely defined:

appendAll2
appendAll3
appendAll
appendAll#1
appendAll2#1
append
appendAll3#1
append#1

Due to the following rules being added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: append(@l1, @l2) → append#1(@l1, @l2) [1] append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1] append#1(nil, @l2) → @l2 [1] appendAll(@l) → appendAll#1(@l) [1] appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1] appendAll#1(nil) → nil [1] appendAll2(@l) → appendAll2#1(@l) [1] appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1] appendAll2#1(nil) → nil [1] appendAll3(@l) → appendAll3#1(@l) [1] appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1] appendAll3#1(nil) → nil [1] The TRS has the following type information: append :: :::nil → :::nil → :::nil append#1 :: :::nil → :::nil → :::nil :: :: :::nil → :::nil → :::nil nil :: :::nil appendAll :: :::nil → :::nil appendAll#1 :: :::nil → :::nil appendAll2 :: :::nil → :::nil appendAll2#1 :: :::nil → :::nil appendAll3 :: :::nil → :::nil appendAll3#1 :: :::nil → :::nil Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: append(@l1, @l2) → append#1(@l1, @l2) [1] append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1] append#1(nil, @l2) → @l2 [1] appendAll(@l) → appendAll#1(@l) [1] appendAll#1(::(@l1, @ls)) → append(@l1, appendAll#1(@ls)) [2] appendAll#1(nil) → nil [1] appendAll2(@l) → appendAll2#1(@l) [1] appendAll2#1(::(@l1, @ls)) → append(appendAll#1(@l1), appendAll2#1(@ls)) [3] appendAll2#1(nil) → nil [1] appendAll3(@l) → appendAll3#1(@l) [1] appendAll3#1(::(@l1, @ls)) → append(appendAll2#1(@l1), appendAll3#1(@ls)) [3] appendAll3#1(nil) → nil [1] The TRS has the following type information: append :: :::nil → :::nil → :::nil append#1 :: :::nil → :::nil → :::nil :: :: :::nil → :::nil → :::nil nil :: :::nil appendAll :: :::nil → :::nil appendAll#1 :: :::nil → :::nil appendAll2 :: :::nil → :::nil appendAll2#1 :: :::nil → :::nil appendAll3 :: :::nil → :::nil appendAll3#1 :: :::nil → :::nil Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

nil => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
append#1(z, z') -{ 1 }→ @l2 :|: z' = @l2, @l2 >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, @l2) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(@l) :|: z = @l, @l >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(@l) :|: z = @l, @l >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(@l) :|: z = @l, @l >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(z, z') :|: z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, z') :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ append#1, append } { appendAll#1 } { appendAll } { appendAll2#1 } { appendAll3#1 } { appendAll2 } { appendAll3 }

(14) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(z, z') :|: z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, z') :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {append#1,append}, {appendAll#1}, {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: append#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

Computed SIZE bound using CoFloCo for: append
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(16) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(z, z') :|: z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, z') :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {append#1,append}, {appendAll#1}, {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: ?, size: O(n1) [z + z'] append: runtime: ?, size: O(n1) [z + z']

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: append#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 2·z

Computed RUNTIME bound using CoFloCo for: append
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 2·z

(18) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(z, z') :|: z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, z') :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll#1}, {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z']

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll#1}, {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: appendAll#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(22) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll#1}, {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: ?, size: O(n1) [z]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 4·z

(24) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(z) :|: z >= 0
appendAll#1(z) -{ 2 }→ append(@l1, appendAll#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 3 }→ append(appendAll#1(@l1), appendAll2#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: appendAll
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(28) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll}, {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: ?, size: O(n1) [z]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 4·z

(30) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z]

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: appendAll2#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(34) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2#1}, {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: ?, size: O(n1) [z]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll2#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 6·z

(36) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(z) :|: z >= 0
appendAll2#1(z) -{ 4 + 4·@l1 }→ append(s3, appendAll2#1(@ls)) :|: s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 3 }→ append(appendAll2#1(@l1), appendAll3#1(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 4 + 6·@l1 }→ append(s7, appendAll3#1(@ls)) :|: s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: appendAll3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(40) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 4 + 6·@l1 }→ append(s7, appendAll3#1(@ls)) :|: s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3#1}, {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: ?, size: O(n1) [z]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 8·z

(42) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(z) :|: z >= 0
appendAll3#1(z) -{ 4 + 6·@l1 }→ append(s7, appendAll3#1(@ls)) :|: s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z]

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(44) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z]

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: appendAll2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(46) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll2}, {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z] appendAll2: runtime: ?, size: O(n1) [z]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 6·z

(48) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z] appendAll2: runtime: O(n1) [2 + 6·z], size: O(n1) [z]

(49) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(50) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z] appendAll2: runtime: O(n1) [2 + 6·z], size: O(n1) [z]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: appendAll3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(52) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {appendAll3}
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z] appendAll2: runtime: O(n1) [2 + 6·z], size: O(n1) [z] appendAll3: runtime: ?, size: O(n1) [z]

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendAll3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 8·z

(54) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 2 + 2·z }→ s :|: s >= 0, s <= 1 * z + 1 * z', z >= 0, z' >= 0
append#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
append#1(z, z') -{ 3 + 2·@xs }→ 1 + @x + s' :|: s' >= 0, s' <= 1 * @xs + 1 * z', @x >= 0, z = 1 + @x + @xs, z' >= 0, @xs >= 0
appendAll(z) -{ 2 + 4·z }→ s'' :|: s'' >= 0, s'' <= 1 * z, z >= 0
appendAll#1(z) -{ 5 + 2·@l1 + 4·@ls }→ s2 :|: s1 >= 0, s1 <= 1 * @ls, s2 >= 0, s2 <= 1 * @l1 + 1 * s1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 2 + 6·z }→ s4 :|: s4 >= 0, s4 <= 1 * z, z >= 0
appendAll2#1(z) -{ 7 + 4·@l1 + 6·@ls + 2·s3 }→ s6 :|: s5 >= 0, s5 <= 1 * @ls, s6 >= 0, s6 <= 1 * s3 + 1 * s5, s3 >= 0, s3 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 2 + 8·z }→ s8 :|: s8 >= 0, s8 <= 1 * z, z >= 0
appendAll3#1(z) -{ 7 + 6·@l1 + 8·@ls + 2·s7 }→ s10 :|: s9 >= 0, s9 <= 1 * @ls, s10 >= 0, s10 <= 1 * s7 + 1 * s9, s7 >= 0, s7 <= 1 * @l1, @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed:
Previous analysis results are:

append#1: runtime: O(n1) [1 + 2·z], size: O(n1) [z + z'] append: runtime: O(n1) [2 + 2·z], size: O(n1) [z + z'] appendAll#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] appendAll: runtime: O(n1) [2 + 4·z], size: O(n1) [z] appendAll2#1: runtime: O(n1) [1 + 6·z], size: O(n1) [z] appendAll3#1: runtime: O(n1) [1 + 8·z], size: O(n1) [z] appendAll2: runtime: O(n1) [2 + 6·z], size: O(n1) [z] appendAll3: runtime: O(n1) [2 + 8·z], size: O(n1) [z]

(55) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(56) BOUNDS(1, n^1)