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

(0) Obligation:

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


The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Rewrite Strategy: INNERMOST

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

The following defined symbols can occur below the 0th argument of +: +
The following defined symbols can occur below the 1th argument of +: +
The following defined symbols can occur below the 0th argument of sum: +
The following defined symbols can occur below the 0th argument of quot: hd, sum, +, -, length
The following defined symbols can occur below the 1th argument of quot: length
The following defined symbols can occur below the 0th argument of hd: sum, +
The following defined symbols can occur below the 0th argument of -: hd, sum, +, -
The following defined symbols can occur below the 1th argument of -: length

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))

(2) Obligation:

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


The TRS R consists of the following rules:

++(:(x, xs), ys) → :(x, ++(xs, ys))
-(s(x), s(y)) → -(x, y)
++(nil, ys) → ys
length(:(x, xs)) → s(length(xs))
quot(0, s(y)) → 0
avg(xs) → quot(hd(sum(xs)), length(xs))
+(s(x), y) → s(+(x, y))
-(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
-(x, 0) → x
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(:(x, nil)) → :(x, nil)
length(nil) → 0
+(0, y) → y
hd(:(x, xs)) → x

Rewrite Strategy: INNERMOST

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

Transformed TRS to weighted TRS

(4) Obligation:

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


The TRS R consists of the following rules:

++(:(x, xs), ys) → :(x, ++(xs, ys)) [1]
-(s(x), s(y)) → -(x, y) [1]
++(nil, ys) → ys [1]
length(:(x, xs)) → s(length(xs)) [1]
quot(0, s(y)) → 0 [1]
avg(xs) → quot(hd(sum(xs)), length(xs)) [1]
+(s(x), y) → s(+(x, y)) [1]
-(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(-(x, y), s(y))) [1]
-(x, 0) → x [1]
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs)) [1]
sum(:(x, nil)) → :(x, nil) [1]
length(nil) → 0 [1]
+(0, y) → y [1]
hd(:(x, xs)) → x [1]

Rewrite Strategy: INNERMOST

(5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

+ => plus

(6) Obligation:

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


The TRS R consists of the following rules:

++(:(x, xs), ys) → :(x, ++(xs, ys)) [1]
minus(s(x), s(y)) → minus(x, y) [1]
++(nil, ys) → ys [1]
length(:(x, xs)) → s(length(xs)) [1]
quot(0, s(y)) → 0 [1]
avg(xs) → quot(hd(sum(xs)), length(xs)) [1]
plus(s(x), y) → s(plus(x, y)) [1]
minus(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
minus(x, 0) → x [1]
sum(:(x, :(y, xs))) → sum(:(plus(x, y), xs)) [1]
sum(:(x, nil)) → :(x, nil) [1]
length(nil) → 0 [1]
plus(0, y) → y [1]
hd(:(x, xs)) → x [1]

Rewrite Strategy: INNERMOST

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

Infered types.

(8) Obligation:

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

++(:(x, xs), ys) → :(x, ++(xs, ys)) [1]
minus(s(x), s(y)) → minus(x, y) [1]
++(nil, ys) → ys [1]
length(:(x, xs)) → s(length(xs)) [1]
quot(0, s(y)) → 0 [1]
avg(xs) → quot(hd(sum(xs)), length(xs)) [1]
plus(s(x), y) → s(plus(x, y)) [1]
minus(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
minus(x, 0) → x [1]
sum(:(x, :(y, xs))) → sum(:(plus(x, y), xs)) [1]
sum(:(x, nil)) → :(x, nil) [1]
length(nil) → 0 [1]
plus(0, y) → y [1]
hd(:(x, xs)) → x [1]

The TRS has the following type information:

++ :: ::nil → ::nil → ::nil : :: s:0 → ::nil → ::nil minus :: s:0 → s:0 → s:0 s :: s:0 → s:0 nil :: ::nil length :: ::nil → s:0 quot :: s:0 → s:0 → s:0 0 :: s:0 avg :: ::nil → s:0 hd :: ::nil → s:0 sum :: ::nil → ::nil plus :: s:0 → s:0 → s:0

Rewrite Strategy: INNERMOST

(9) 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:

++
quot
avg

(c) The following functions are completely defined:

minus
hd
sum
length
plus

Due to the following rules being added:

hd(v0) → 0 [0]
sum(v0) → nil [0]

And the following fresh constants: none

(10) 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: ++(:(x, xs), ys) → :(x, ++(xs, ys)) [1] minus(s(x), s(y)) → minus(x, y) [1] ++(nil, ys) → ys [1] length(:(x, xs)) → s(length(xs)) [1] quot(0, s(y)) → 0 [1] avg(xs) → quot(hd(sum(xs)), length(xs)) [1] plus(s(x), y) → s(plus(x, y)) [1] minus(0, s(y)) → 0 [1] quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1] minus(x, 0) → x [1] sum(:(x, :(y, xs))) → sum(:(plus(x, y), xs)) [1] sum(:(x, nil)) → :(x, nil) [1] length(nil) → 0 [1] plus(0, y) → y [1] hd(:(x, xs)) → x [1] hd(v0) → 0 [0] sum(v0) → nil [0] The TRS has the following type information: ++ :: ::nil → ::nil → ::nil : :: s:0 → ::nil → ::nil minus :: s:0 → s:0 → s:0 s :: s:0 → s:0 nil :: ::nil length :: ::nil → s:0 quot :: s:0 → s:0 → s:0 0 :: s:0 avg :: ::nil → s:0 hd :: ::nil → s:0 sum :: ::nil → ::nil plus :: s:0 → s:0 → s:0 Rewrite Strategy: INNERMOST

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

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

(12) 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: ++(:(x, xs), ys) → :(x, ++(xs, ys)) [1] minus(s(x), s(y)) → minus(x, y) [1] ++(nil, ys) → ys [1] length(:(x, xs)) → s(length(xs)) [1] quot(0, s(y)) → 0 [1] avg(:(x', :(y', xs'))) → quot(hd(sum(:(plus(x', y'), xs'))), s(length(:(y', xs')))) [3] avg(:(x'', nil)) → quot(hd(:(x'', nil)), s(length(nil))) [3] avg(:(x1, xs'')) → quot(hd(nil), s(length(xs''))) [2] avg(nil) → quot(hd(nil), 0) [2] plus(s(x), y) → s(plus(x, y)) [1] minus(0, s(y)) → 0 [1] quot(s(s(x2)), s(s(y''))) → s(quot(minus(x2, y''), s(s(y'')))) [2] quot(s(0), s(s(y1))) → s(quot(0, s(s(y1)))) [2] quot(s(x), s(0)) → s(quot(x, s(0))) [2] minus(x, 0) → x [1] sum(:(s(x3), :(y, xs))) → sum(:(s(plus(x3, y)), xs)) [2] sum(:(0, :(y, xs))) → sum(:(y, xs)) [2] sum(:(x, nil)) → :(x, nil) [1] length(nil) → 0 [1] plus(0, y) → y [1] hd(:(x, xs)) → x [1] hd(v0) → 0 [0] sum(v0) → nil [0] The TRS has the following type information: ++ :: ::nil → ::nil → ::nil : :: s:0 → ::nil → ::nil minus :: s:0 → s:0 → s:0 s :: s:0 → s:0 nil :: ::nil length :: ::nil → s:0 quot :: s:0 → s:0 → s:0 0 :: s:0 avg :: ::nil → s:0 hd :: ::nil → s:0 sum :: ::nil → ::nil plus :: s:0 → s:0 → s:0 Rewrite Strategy: INNERMOST

(13) 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
0 => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ ys :|: z' = ys, ys >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, ys) :|: z = 1 + x + xs, xs >= 0, z' = ys, ys >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(hd(0), 0) :|: z = 0
avg(z) -{ 2 }→ quot(hd(0), 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs''
avg(z) -{ 3 }→ quot(hd(1 + x'' + 0), 1 + length(0)) :|: x'' >= 0, z = 1 + x'' + 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
plus(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
quot(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(x, 1 + 0) :|: x >= 0, z' = 1 + 0, z = 1 + x
quot(z, z') -{ 2 }→ 1 + quot(minus(x2, y''), 1 + (1 + y'')) :|: z' = 1 + (1 + y''), z = 1 + (1 + x2), y'' >= 0, x2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + y1)) :|: y1 >= 0, z' = 1 + (1 + y1), z = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
sum(z) -{ 1 }→ 1 + x + 0 :|: x >= 0, z = 1 + x + 0

(15) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0

(16) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ ys :|: z' = ys, ys >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, ys) :|: z = 1 + x + xs, xs >= 0, z' = ys, ys >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: x'' >= 0, z = 1 + x'' + 0, 1 + x'' + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: x'' >= 0, z = 1 + x'' + 0, v0 >= 0, 1 + x'' + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
plus(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
quot(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(x, 1 + 0) :|: x >= 0, z' = 1 + 0, z = 1 + x
quot(z, z') -{ 2 }→ 1 + quot(minus(x2, y''), 1 + (1 + y'')) :|: z' = 1 + (1 + y''), z = 1 + (1 + x2), y'' >= 0, x2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + y1)) :|: y1 >= 0, z' = 1 + (1 + y1), z = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
sum(z) -{ 1 }→ 1 + x + 0 :|: x >= 0, z = 1 + x + 0

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

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

(18) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ minus(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

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

Found the following analysis order by SCC decomposition:

{ minus } { length } { hd } { ++ } { plus } { quot } { sum } { avg }

(20) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ minus(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {minus}, {length}, {hd}, {++}, {plus}, {quot}, {sum}, {avg}

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

Computed SIZE bound using KoAT for: minus
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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ minus(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {minus}, {length}, {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: ?, size: O(n1) [z]

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ minus(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 2 }→ 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {length}, {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + 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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {length}, {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z]

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

Computed SIZE bound using CoFloCo for: length
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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {length}, {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: ?, size: O(n1) [z]

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

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

(30) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 4 }→ quot(x, 1 + length(0)) :|: z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 3 }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + length(1 + y' + xs')) :|: z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 2 }→ quot(0, 1 + length(xs'')) :|: x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ quot(0, 1 + length(0)) :|: z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + 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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z]

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

Computed SIZE bound using KoAT for: hd
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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {hd}, {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: ?, size: O(n1) [z]

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

Computed RUNTIME bound using CoFloCo for: hd
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(36) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], 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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z]

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

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

(40) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {++}, {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: ?, size: O(n1) [z + z']

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 1 }→ 1 + x + ++(xs, z') :|: z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + 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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z']

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

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

(46) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {plus}, {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: ?, size: O(n1) [z + z']

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 + xs' + y' }→ quot(hd(sum(1 + plus(x', y') + xs')), 1 + s1) :|: s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 2 }→ sum(1 + (1 + plus(x3, y)) + xs) :|: xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + 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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z']

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

Computed SIZE bound using KoAT for: quot
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:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {quot}, {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: ?, size: O(n1) [z]

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

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 5 }→ quot(x, 1 + s2) :|: s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
avg(z) -{ 2 }→ quot(0, 0) :|: z = 0, v0 >= 0, 0 = v0
avg(z) -{ 4 }→ quot(0, 1 + s3) :|: s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 3 + xs'' }→ quot(0, 1 + s4) :|: s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 1 + z' }→ 1 + quot(s', 1 + (1 + (z' - 2))) :|: s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
quot(z, z') -{ 2 }→ 1 + quot(0, 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 2 }→ 1 + quot(z - 1, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z]

(55) ResultPropagationProof (UPPER BOUND(ID) transformation)

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

(56) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z]

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

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

(58) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed: {sum}, {avg}
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z] sum: runtime: ?, size: O(n1) [z]

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

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

(60) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 6 + x' + xs' + y' }→ quot(hd(sum(1 + s8 + xs')), 1 + s1) :|: s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 2 }→ sum(1 + y + xs) :|: xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 3 + x3 }→ sum(1 + (1 + s7) + xs) :|: s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

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

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z] sum: runtime: O(n2) [3 + 2·z + z2], size: O(n1) [z]

(61) ResultPropagationProof (UPPER BOUND(ID) transformation)

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

(62) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 14 + s1·s19 + 3·s19 + 4·s8 + 2·s8·xs' + s8² + x' + 5·xs' + xs'² + y' }→ s20 :|: s18 >= 0, s18 <= 1 * (1 + s8 + xs'), s19 >= 0, s19 <= 1 * s18, s20 >= 0, s20 <= 1 * s19, s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 14 + 6·s7 + 2·s7·xs + s7² + x3 + 6·xs + xs² }→ s16 :|: s16 >= 0, s16 <= 1 * (1 + (1 + s7) + xs), s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 8 + 4·xs + 2·xs·y + xs² + 4·y + y² }→ s17 :|: s17 >= 0, s17 <= 1 * (1 + y + xs), xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

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

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z] sum: runtime: O(n2) [3 + 2·z + z2], size: O(n1) [z]

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

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

(64) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 14 + s1·s19 + 3·s19 + 4·s8 + 2·s8·xs' + s8² + x' + 5·xs' + xs'² + y' }→ s20 :|: s18 >= 0, s18 <= 1 * (1 + s8 + xs'), s19 >= 0, s19 <= 1 * s18, s20 >= 0, s20 <= 1 * s19, s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 14 + 6·s7 + 2·s7·xs + s7² + x3 + 6·xs + xs² }→ s16 :|: s16 >= 0, s16 <= 1 * (1 + (1 + s7) + xs), s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 8 + 4·xs + 2·xs·y + xs² + 4·y + y² }→ s17 :|: s17 >= 0, s17 <= 1 * (1 + y + xs), xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

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

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z] sum: runtime: O(n2) [3 + 2·z + z2], size: O(n1) [z] avg: runtime: ?, size: O(n1) [z]

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: avg
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 32 + 23·z + 11·z²

(66) Obligation:

Complexity RNTS consisting of the following rules:

++(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
++(z, z') -{ 2 + xs }→ 1 + x + s5 :|: s5 >= 0, s5 <= 1 * xs + 1 * z', z = 1 + x + xs, xs >= 0, z' >= 0, x >= 0
avg(z) -{ 6 + s2·x + 3·x }→ s12 :|: s12 >= 0, s12 <= 1 * x, s2 >= 0, s2 <= 1 * 0, z - 1 >= 0, 1 + (z - 1) + 0 = 1 + x + xs, xs >= 0, x >= 0
avg(z) -{ 5 }→ s13 :|: s13 >= 0, s13 <= 1 * 0, s3 >= 0, s3 <= 1 * 0, z - 1 >= 0, v0 >= 0, 1 + (z - 1) + 0 = v0
avg(z) -{ 4 + xs'' }→ s14 :|: s14 >= 0, s14 <= 1 * 0, s4 >= 0, s4 <= 1 * xs'', x1 >= 0, xs'' >= 0, z = 1 + x1 + xs'', v0 >= 0, 0 = v0
avg(z) -{ 3 }→ s15 :|: s15 >= 0, s15 <= 1 * 0, z = 0, v0 >= 0, 0 = v0
avg(z) -{ 14 + s1·s19 + 3·s19 + 4·s8 + 2·s8·xs' + s8² + x' + 5·xs' + xs'² + y' }→ s20 :|: s18 >= 0, s18 <= 1 * (1 + s8 + xs'), s19 >= 0, s19 <= 1 * s18, s20 >= 0, s20 <= 1 * s19, s8 >= 0, s8 <= 1 * x' + 1 * y', s1 >= 0, s1 <= 1 * (1 + y' + xs'), z = 1 + x' + (1 + y' + xs'), x' >= 0, xs' >= 0, y' >= 0
hd(z) -{ 1 }→ x :|: z = 1 + x + xs, xs >= 0, x >= 0
hd(z) -{ 0 }→ 0 :|: z >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 2 + xs }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * xs, z = 1 + x + xs, xs >= 0, x >= 0
minus(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1 * (z - 1), z - 1 >= 0, z' - 1 >= 0
minus(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
minus(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s6 :|: s6 >= 0, s6 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0
quot(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
quot(z, z') -{ 3 }→ 1 + s10 :|: s10 >= 0, s10 <= 1 * 0, z' - 2 >= 0, z = 1 + 0
quot(z, z') -{ 3·z }→ 1 + s11 :|: s11 >= 0, s11 <= 1 * (z - 1), z - 1 >= 0, z' = 1 + 0
quot(z, z') -{ 2 + 2·s' + s'·z' + z' }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * s', s' >= 0, s' <= 1 * (z - 2), z' - 2 >= 0, z - 2 >= 0
sum(z) -{ 14 + 6·s7 + 2·s7·xs + s7² + x3 + 6·xs + xs² }→ s16 :|: s16 >= 0, s16 <= 1 * (1 + (1 + s7) + xs), s7 >= 0, s7 <= 1 * x3 + 1 * y, xs >= 0, y >= 0, z = 1 + (1 + x3) + (1 + y + xs), x3 >= 0
sum(z) -{ 8 + 4·xs + 2·xs·y + xs² + 4·y + y² }→ s17 :|: s17 >= 0, s17 <= 1 * (1 + y + xs), xs >= 0, z = 1 + 0 + (1 + y + xs), y >= 0
sum(z) -{ 0 }→ 0 :|: z >= 0
sum(z) -{ 1 }→ 1 + (z - 1) + 0 :|: z - 1 >= 0

Function symbols to be analyzed:
Previous analysis results are:

minus: runtime: O(n1) [1 + z'], size: O(n1) [z] length: runtime: O(n1) [1 + z], size: O(n1) [z] hd: runtime: O(1) [1], size: O(n1) [z] ++: runtime: O(n1) [1 + z], size: O(n1) [z + z'] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] quot: runtime: O(n2) [1 + 2·z + z·z'], size: O(n1) [z] sum: runtime: O(n2) [3 + 2·z + z2], size: O(n1) [z] avg: runtime: O(n2) [32 + 23·z + 11·z2], size: O(n1) [z]

(67) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(68) BOUNDS(1, n^2)