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

(0) Obligation:

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


The TRS R consists of the following rules:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(x, leaf) → false
less_leaves(leaf, cons(w, z)) → true
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))

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^3).


The TRS R consists of the following rules:

minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
app(nil, y) → y [1]
app(add(n, x), y) → add(n, app(x, y)) [1]
reverse(nil) → nil [1]
reverse(add(n, x)) → app(reverse(x), add(n, nil)) [1]
shuffle(nil) → nil [1]
shuffle(add(n, x)) → add(n, shuffle(reverse(x))) [1]
concat(leaf, y) → y [1]
concat(cons(u, v), y) → cons(u, concat(v, y)) [1]
less_leaves(x, leaf) → false [1]
less_leaves(leaf, cons(w, z)) → true [1]
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z)) [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:

minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
app(nil, y) → y [1]
app(add(n, x), y) → add(n, app(x, y)) [1]
reverse(nil) → nil [1]
reverse(add(n, x)) → app(reverse(x), add(n, nil)) [1]
shuffle(nil) → nil [1]
shuffle(add(n, x)) → add(n, shuffle(reverse(x))) [1]
concat(leaf, y) → y [1]
concat(cons(u, v), y) → cons(u, concat(v, y)) [1]
less_leaves(x, leaf) → false [1]
less_leaves(leaf, cons(w, z)) → true [1]
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z)) [1]

The TRS has the following type information:

minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s quot :: 0:s → 0:s → 0:s app :: nil:add → nil:add → nil:add nil :: nil:add add :: a → nil:add → nil:add reverse :: nil:add → nil:add shuffle :: nil:add → nil:add concat :: leaf:cons → leaf:cons → leaf:cons leaf :: leaf:cons cons :: leaf:cons → leaf:cons → leaf:cons less_leaves :: leaf:cons → leaf:cons → false:true false :: false:true true :: false:true

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:

quot
shuffle
less_leaves

(c) The following functions are completely defined:

minus
reverse
concat
app

Due to the following rules being added:

minus(v0, v1) → 0 [0]

And the following fresh constants:

const

(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: minus(x, 0) → x [1] minus(s(x), s(y)) → minus(x, y) [1] quot(0, s(y)) → 0 [1] quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1] app(nil, y) → y [1] app(add(n, x), y) → add(n, app(x, y)) [1] reverse(nil) → nil [1] reverse(add(n, x)) → app(reverse(x), add(n, nil)) [1] shuffle(nil) → nil [1] shuffle(add(n, x)) → add(n, shuffle(reverse(x))) [1] concat(leaf, y) → y [1] concat(cons(u, v), y) → cons(u, concat(v, y)) [1] less_leaves(x, leaf) → false [1] less_leaves(leaf, cons(w, z)) → true [1] less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z)) [1] minus(v0, v1) → 0 [0] The TRS has the following type information: minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s quot :: 0:s → 0:s → 0:s app :: nil:add → nil:add → nil:add nil :: nil:add add :: a → nil:add → nil:add reverse :: nil:add → nil:add shuffle :: nil:add → nil:add concat :: leaf:cons → leaf:cons → leaf:cons leaf :: leaf:cons cons :: leaf:cons → leaf:cons → leaf:cons less_leaves :: leaf:cons → leaf:cons → false:true false :: false:true true :: false:true const :: a 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: minus(x, 0) → x [1] minus(s(x), s(y)) → minus(x, y) [1] quot(0, s(y)) → 0 [1] quot(s(x), s(0)) → s(quot(x, s(0))) [2] quot(s(s(x')), s(s(y'))) → s(quot(minus(x', y'), s(s(y')))) [2] quot(s(x), s(y)) → s(quot(0, s(y))) [1] app(nil, y) → y [1] app(add(n, x), y) → add(n, app(x, y)) [1] reverse(nil) → nil [1] reverse(add(n, nil)) → app(nil, add(n, nil)) [2] reverse(add(n, add(n', x''))) → app(app(reverse(x''), add(n', nil)), add(n, nil)) [2] shuffle(nil) → nil [1] shuffle(add(n, nil)) → add(n, shuffle(nil)) [2] shuffle(add(n, add(n'', x1))) → add(n, shuffle(app(reverse(x1), add(n'', nil)))) [2] concat(leaf, y) → y [1] concat(cons(u, v), y) → cons(u, concat(v, y)) [1] less_leaves(x, leaf) → false [1] less_leaves(leaf, cons(w, z)) → true [1] less_leaves(cons(leaf, v), cons(leaf, z)) → less_leaves(v, z) [3] less_leaves(cons(leaf, v), cons(cons(u'', v''), z)) → less_leaves(v, cons(u'', concat(v'', z))) [3] less_leaves(cons(cons(u', v'), v), cons(leaf, z)) → less_leaves(cons(u', concat(v', v)), z) [3] less_leaves(cons(cons(u', v'), v), cons(cons(u1, v2), z)) → less_leaves(cons(u', concat(v', v)), cons(u1, concat(v2, z))) [3] minus(v0, v1) → 0 [0] The TRS has the following type information: minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s quot :: 0:s → 0:s → 0:s app :: nil:add → nil:add → nil:add nil :: nil:add add :: a → nil:add → nil:add reverse :: nil:add → nil:add shuffle :: nil:add → nil:add concat :: leaf:cons → leaf:cons → leaf:cons leaf :: leaf:cons cons :: leaf:cons → leaf:cons → leaf:cons less_leaves :: leaf:cons → leaf:cons → false:true false :: false:true true :: false:true const :: a 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:

0 => 0
nil => 0
leaf => 0
false => 0
true => 1
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, y) :|: n >= 0, z'' = y, z' = 1 + n + x, x >= 0, y >= 0
concat(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, y) :|: v >= 0, z' = 1 + u + v, z'' = y, y >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(v, z) :|: v >= 0, z >= 0, z' = 1 + 0 + v, z'' = 1 + 0 + z
less_leaves(z', z'') -{ 3 }→ less_leaves(v, 1 + u'' + concat(v'', z)) :|: v >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, z' = 1 + 0 + v, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + 0 + z
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ minus(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
minus(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
quot(z', z'') -{ 1 }→ 0 :|: y >= 0, z'' = 1 + y, z' = 0
quot(z', z'') -{ 2 }→ 1 + quot(x, 1 + 0) :|: z' = 1 + x, x >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 }→ 1 + quot(minus(x', y'), 1 + (1 + y')) :|: z' = 1 + (1 + x'), x' >= 0, z'' = 1 + (1 + y'), y' >= 0
quot(z', z'') -{ 1 }→ 1 + quot(0, 1 + y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + n + 0) :|: n >= 0, z' = 1 + n + 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + n + shuffle(0) :|: n >= 0, z' = 1 + n + 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:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

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

Found the following analysis order by SCC decomposition:

{ minus } { concat } { app } { quot } { less_leaves } { reverse } { shuffle }

(14) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {minus}, {concat}, {app}, {quot}, {less_leaves}, {reverse}, {shuffle}

(15) 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'

(16) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {minus}, {concat}, {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

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

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

(18) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {concat}, {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {concat}, {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

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

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

(22) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {concat}, {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

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

Computed RUNTIME bound using CoFloCo for: concat
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:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 1 }→ 1 + u + concat(v, z'') :|: v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, 1 + u'' + concat(v'', z)) :|: z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), z'' - 1) :|: v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 3 }→ less_leaves(1 + u' + concat(v', v), 1 + u1 + concat(v2, z)) :|: v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

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

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

(28) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {app}, {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

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

Computed RUNTIME bound using CoFloCo for: app
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:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 1 }→ 1 + n + app(x, z'') :|: n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 2 }→ app(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

(33) 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'

(34) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {quot}, {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

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

(35) 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''

(36) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 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'') -{ 1 }→ 1 + quot(0, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0
quot(z', z'') -{ 2 }→ 1 + quot(z' - 1, 1 + 0) :|: z' - 1 >= 0, z'' = 1 + 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·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:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z']

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

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

(40) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {less_leaves}, {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: ?, size: O(1) [1]

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 }→ less_leaves(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 4 + v'' }→ less_leaves(z' - 1, 1 + u'' + s1) :|: s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 4 + v' }→ less_leaves(1 + u' + s2, z'' - 1) :|: s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 5 + v' + v2 }→ less_leaves(1 + u' + s3, 1 + u1 + s4) :|: s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1]

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1]

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

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed: {reverse}, {shuffle}
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1] reverse: runtime: ?, size: O(n1) [z']

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 2 }→ app(app(reverse(x''), 1 + n' + 0), 1 + n + 0) :|: n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 2 }→ 1 + n + shuffle(app(reverse(x1), 1 + n'' + 0)) :|: n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

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

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1] reverse: runtime: O(n2) [4 + 3·z' + 2·z'2], 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:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 8 + s14 + s15 + 3·x'' + 2·x''² }→ s16 :|: s14 >= 0, s14 <= 1 * x'', s15 >= 0, s15 <= 1 * s14 + 1 * (1 + n' + 0), s16 >= 0, s16 <= 1 * s15 + 1 * (1 + n + 0), n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 7 + s17 + 3·x1 + 2·x1² }→ 1 + n + shuffle(s18) :|: s17 >= 0, s17 <= 1 * x1, s18 >= 0, s18 <= 1 * s17 + 1 * (1 + n'' + 0), n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

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

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1] reverse: runtime: O(n2) [4 + 3·z' + 2·z'2], size: O(n1) [z']

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

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

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 8 + s14 + s15 + 3·x'' + 2·x''² }→ s16 :|: s14 >= 0, s14 <= 1 * x'', s15 >= 0, s15 <= 1 * s14 + 1 * (1 + n' + 0), s16 >= 0, s16 <= 1 * s15 + 1 * (1 + n + 0), n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 7 + s17 + 3·x1 + 2·x1² }→ 1 + n + shuffle(s18) :|: s17 >= 0, s17 <= 1 * x1, s18 >= 0, s18 <= 1 * s17 + 1 * (1 + n'' + 0), n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

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

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1] reverse: runtime: O(n2) [4 + 3·z' + 2·z'2], size: O(n1) [z'] shuffle: runtime: ?, size: O(n1) [z']

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

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

app(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
app(z', z'') -{ 2 + x }→ 1 + n + s5 :|: s5 >= 0, s5 <= 1 * x + 1 * z'', n >= 0, z' = 1 + n + x, x >= 0, z'' >= 0
concat(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
concat(z', z'') -{ 2 + v }→ 1 + u + s'' :|: s'' >= 0, s'' <= 1 * v + 1 * z'', v >= 0, z' = 1 + u + v, z'' >= 0, u >= 0
less_leaves(z', z'') -{ 3 + z'·z'' + z'² + -1·z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
less_leaves(z', z'') -{ 2 + -1·s1 + s1·z' + -1·u'' + u''·z' + v'' + 2·z' + z'² }→ s11 :|: s11 >= 0, s11 <= 1, s1 >= 0, s1 <= 1 * v'' + 1 * z, z' - 1 >= 0, z >= 0, z'' = 1 + (1 + u'' + v'') + z, u'' >= 0, v'' >= 0
less_leaves(z', z'') -{ 8 + 4·s2 + 2·s2·u' + s2·z'' + s2² + 4·u' + u'·z'' + u'² + v' + z'' }→ s12 :|: s12 >= 0, s12 <= 1, s2 >= 0, s2 <= 1 * v' + 1 * v, v >= 0, z'' - 1 >= 0, u' >= 0, v' >= 0, z' = 1 + (1 + u' + v') + v
less_leaves(z', z'') -{ 11 + 6·s3 + s3·s4 + 2·s3·u' + s3·u1 + s3² + s4 + s4·u' + 6·u' + u'·u1 + u'² + u1 + v' + v2 }→ s13 :|: s13 >= 0, s13 <= 1, s3 >= 0, s3 <= 1 * v' + 1 * v, s4 >= 0, s4 <= 1 * v2 + 1 * z, v >= 0, z >= 0, u' >= 0, v' >= 0, u1 >= 0, z' = 1 + (1 + u' + v') + v, z'' = 1 + (1 + u1 + v2) + z, v2 >= 0
less_leaves(z', z'') -{ 1 }→ 1 :|: z >= 0, z'' = 1 + w + z, w >= 0, z' = 0
less_leaves(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 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'') -{ 0 }→ 0 :|: z' >= 0, z'' >= 0
quot(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
quot(z', z'') -{ 3·z' }→ 1 + s7 :|: s7 >= 0, s7 <= 1 * (z' - 1), z' - 1 >= 0, z'' = 1 + 0
quot(z', z'') -{ 2 + 2·s' + s'·z'' + z'' }→ 1 + s8 :|: s8 >= 0, s8 <= 1 * s', s' >= 0, s' <= 1 * (z' - 2), z' - 2 >= 0, z'' - 2 >= 0
quot(z', z'') -{ 2 }→ 1 + s9 :|: s9 >= 0, s9 <= 1 * 0, z' - 1 >= 0, z'' - 1 >= 0
reverse(z') -{ 8 + s14 + s15 + 3·x'' + 2·x''² }→ s16 :|: s14 >= 0, s14 <= 1 * x'', s15 >= 0, s15 <= 1 * s14 + 1 * (1 + n' + 0), s16 >= 0, s16 <= 1 * s15 + 1 * (1 + n + 0), n >= 0, n' >= 0, z' = 1 + n + (1 + n' + x''), x'' >= 0
reverse(z') -{ 3 }→ s6 :|: s6 >= 0, s6 <= 1 * 0 + 1 * (1 + (z' - 1) + 0), z' - 1 >= 0
reverse(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 1 }→ 0 :|: z' = 0
shuffle(z') -{ 7 + s17 + 3·x1 + 2·x1² }→ 1 + n + shuffle(s18) :|: s17 >= 0, s17 <= 1 * x1, s18 >= 0, s18 <= 1 * s17 + 1 * (1 + n'' + 0), n >= 0, x1 >= 0, n'' >= 0, z' = 1 + n + (1 + n'' + x1)
shuffle(z') -{ 2 }→ 1 + (z' - 1) + shuffle(0) :|: z' - 1 >= 0

Function symbols to be analyzed:
Previous analysis results are:

minus: runtime: O(n1) [1 + z''], size: O(n1) [z'] concat: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] app: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] quot: runtime: O(n2) [1 + 2·z' + z'·z''], size: O(n1) [z'] less_leaves: runtime: O(n2) [1 + 3·z' + z'·z'' + z'2], size: O(1) [1] reverse: runtime: O(n2) [4 + 3·z' + 2·z'2], size: O(n1) [z'] shuffle: runtime: O(n3) [1 + 9·z' + 4·z'2 + 2·z'3], size: O(n1) [z']

(55) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(56) BOUNDS(1, n^3)