Runtime Complexity (innermost) proof of /tmp/tmpeWMvue/times.xml

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

0 CpxTRS

↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxWeightedTrs

↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CpxTypedWeightedTrs

↳5 CompletionProof (UPPER BOUND(ID), 0 ms)

↳6 CpxTypedWeightedCompleteTrs

↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CpxTypedWeightedCompleteTrs

↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)

↳10 CpxRNTS

↳11 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 CpxRNTS

↳13 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CpxRNTS

↳15 IntTrsBoundProof (UPPER BOUND(ID), 545 ms)

↳16 CpxRNTS

↳17 IntTrsBoundProof (UPPER BOUND(ID), 97 ms)

↳18 CpxRNTS

↳19 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳20 CpxRNTS

↳21 IntTrsBoundProof (UPPER BOUND(ID), 146 ms)

↳22 CpxRNTS

↳23 IntTrsBoundProof (UPPER BOUND(ID), 49 ms)

↳24 CpxRNTS

↳25 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳26 CpxRNTS

↳27 IntTrsBoundProof (UPPER BOUND(ID), 370 ms)

↳28 CpxRNTS

↳29 IntTrsBoundProof (UPPER BOUND(ID), 78 ms)

↳30 CpxRNTS

↳31 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳32 CpxRNTS

↳33 IntTrsBoundProof (UPPER BOUND(ID), 480 ms)

↳34 CpxRNTS

↳35 IntTrsBoundProof (UPPER BOUND(ID), 191 ms)

↳36 CpxRNTS

↳37 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳38 CpxRNTS

↳39 IntTrsBoundProof (UPPER BOUND(ID), 1043 ms)

↳40 CpxRNTS

↳41 IntTrsBoundProof (UPPER BOUND(ID), 533 ms)

↳42 CpxRNTS

↳43 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳44 CpxRNTS

↳45 IntTrsBoundProof (UPPER BOUND(ID), 1569 ms)

↳46 CpxRNTS

↳47 IntTrsBoundProof (UPPER BOUND(ID), 197 ms)

↳48 CpxRNTS

↳49 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳50 CpxRNTS

↳51 IntTrsBoundProof (UPPER BOUND(ID), 182 ms)

↳52 CpxRNTS

↳53 IntTrsBoundProof (UPPER BOUND(ID), 4 ms)

↳54 CpxRNTS

↳55 FinalProof (⇔, 0 ms)

↳56 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:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

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:

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [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:

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [1]

The TRS has the following type information:

inc :: s:0 → s:0
s :: s:0 → s:0
0 :: s:0
plus :: s:0 → s:0 → s:0
ifPlus :: false:true → s:0 → s:0 → s:0 → s:0
eq :: s:0 → s:0 → false:true
minus :: s:0 → s:0 → s:0
false :: false:true
true :: false:true
times :: s:0 → s:0 → s:0
timesIter :: s:0 → s:0 → s:0 → s:0
ifTimes :: false:true → s:0 → s:0 → s:0 → s:0 → s:0
f :: g:h
g :: g:h
h :: g:h

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:

times
timesIter
ifTimes
f

eq
minus
inc
plus
ifPlus

Due to the following rules being added:
none

And the following fresh constants: none

(6) Obligation:

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

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

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [1]

The TRS has the following type information:

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:

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(s(x'), y) → ifPlus(false, minus(x', 0), s(x'), s(inc(x'))) [4]
plus(s(0), y) → ifPlus(false, 0, s(0), s(inc(0))) [4]
plus(0, y) → ifPlus(true, 0, 0, s(0)) [4]
plus(0, y) → ifPlus(true, 0, 0, s(0)) [4]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(s(x''), y, z) → ifTimes(false, minus(x'', 0), y, z, ifPlus(eq(y, 0), minus(y, s(0)), y, inc(y))) [4]
timesIter(s(0), y, z) → ifTimes(false, 0, y, z, ifPlus(eq(y, 0), minus(y, s(0)), y, inc(y))) [4]
timesIter(0, y, z) → ifTimes(true, 0, y, z, ifPlus(eq(y, 0), minus(y, s(0)), y, inc(y))) [4]
timesIter(0, y, z) → ifTimes(true, 0, y, z, ifPlus(eq(y, 0), minus(y, s(0)), y, inc(y))) [4]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [1]

The TRS has the following type information:

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
false => 0
true => 1
g => 0
h => 1

(10) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' = x, x >= 0, z'' = x
eq(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = 1 + x, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = 1 + x, x >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ y :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(x, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1, z3 = u, u >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(x, y, u) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z3 = u, z' = 0, u >= 0
inc(z') -{ 1 }→ 1 + inc(x) :|: z' = 1 + x, x >= 0
inc(z') -{ 1 }→ 1 + 0 :|: z' = 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'') -{ 1 }→ 0 :|: x >= 0, z'' = x, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' = x, x >= 0, z'' = x
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' = y, y >= 0, z' = 0
plus(z', z'') -{ 4 }→ ifPlus(0, minus(x', 0), 1 + x', 1 + inc(x')) :|: z' = 1 + x', z'' = y, x' >= 0, y >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' = y, y >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(1, 0, y, z, ifPlus(eq(y, 0), minus(y, 1 + 0), y, inc(y))) :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, minus(x'', 0), y, z, ifPlus(eq(y, 0), minus(y, 1 + 0), y, inc(y))) :|: z1 = z, z >= 0, z' = 1 + x'', z'' = y, y >= 0, x'' >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, 0, y, z, ifPlus(eq(y, 0), minus(y, 1 + 0), y, inc(y))) :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 1 + 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:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 4 }→ ifPlus(0, minus(z' - 1, 0), 1 + (z' - 1), 1 + inc(z' - 1)) :|: z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, minus(z' - 1, 0), z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 1 + 0

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

Found the following analysis order by SCC decomposition:

{ minus }
{ f }
{ inc }
{ eq }
{ plus, ifPlus }
{ timesIter, ifTimes }
{ times }

(14) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 4 }→ ifPlus(0, minus(z' - 1, 0), 1 + (z' - 1), 1 + inc(z' - 1)) :|: z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, minus(z' - 1, 0), z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {minus}, {f}, {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}

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

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 4 }→ ifPlus(0, minus(z' - 1, 0), 1 + (z' - 1), 1 + inc(z' - 1)) :|: z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, minus(z' - 1, 0), z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {minus}, {f}, {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

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

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

(18) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 4 }→ ifPlus(0, minus(z' - 1, 0), 1 + (z' - 1), 1 + inc(z' - 1)) :|: z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, minus(z' - 1, 0), z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 4 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), minus(z'', 1 + 0), z'', inc(z''))) :|: z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {f}, {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

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

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {f}, {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

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

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

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

(22) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {f}, {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: ?, size: O(1) [1]

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]

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

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]

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

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

(28) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {inc}, {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: ?, size: O(n¹) [1 + z']

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

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

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 }→ 1 + inc(z' - 1) :|: z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 }→ ifPlus(0, s, 1 + (z' - 1), 1 + inc(z' - 1)) :|: s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 4 }→ ifPlus(0, 0, 1 + 0, 1 + inc(0)) :|: z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', inc(z''))) :|: s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 7 }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', inc(z''))) :|: s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 6 }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', inc(z''))) :|: s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

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

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', s9)) :|: s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', s7)) :|: s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', s8)) :|: s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: O(n¹) [1 + z'], size: O(n¹) [1 + z']

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

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

(34) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', s9)) :|: s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', s7)) :|: s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', s8)) :|: s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {eq}, {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: O(n¹) [1 + z'], size: O(n¹) [1 + z']
eq: runtime: ?, size: O(1) [1]

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

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

(36) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(eq(z'', 0), s3, z'', s9)) :|: s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(eq(z'', 0), s1, z'', s7)) :|: s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 7 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(eq(z'', 0), s2, z'', s8)) :|: s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: O(n¹) [1 + z'], size: O(n¹) [1 + z']
eq: runtime: O(n¹) [1 + z''], size: O(1) [1]

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

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(s13, s3, z'', s9)) :|: s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 9 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(s11, s1, z'', s7)) :|: s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(s12, s2, z'', s8)) :|: s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: O(n¹) [1 + z'], size: O(n¹) [1 + z']
eq: runtime: O(n¹) [1 + z''], size: O(1) [1]

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

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

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

(40) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(s13, s3, z'', s9)) :|: s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 9 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(s11, s1, z'', s7)) :|: s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(s12, s2, z'', s8)) :|: s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {plus,ifPlus}, {timesIter,ifTimes}, {times}
Previous analysis results are:

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

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(z'', z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 4 }→ ifPlus(1, 0, 0, 1 + 0) :|: z'' >= 0, z' = 0
plus(z', z'') -{ 5 + z' }→ ifPlus(0, s, 1 + (z' - 1), 1 + s5) :|: s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 5 }→ ifPlus(0, 0, 1 + 0, 1 + s6) :|: s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(1, 0, z'', z1, ifPlus(s13, s3, z'', s9)) :|: s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 9 + z'' }→ ifTimes(0, s'', z'', z1, ifPlus(s11, s1, z'', s7)) :|: s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 8 + z'' }→ ifTimes(0, 0, z'', z1, ifPlus(s12, s2, z'', s8)) :|: s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {timesIter,ifTimes}, {times}
Previous analysis results are:

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

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 20 + 7·s3 + s3² + z'' }→ ifTimes(1, 0, z'', z1, s20) :|: s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 21 + 7·s1 + s1² + z'' }→ ifTimes(0, s'', z'', z1, s18) :|: s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 20 + 7·s2 + s2² + z'' }→ ifTimes(0, 0, z'', z1, s19) :|: s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {timesIter,ifTimes}, {times}
Previous analysis results are:

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

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

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

(46) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 20 + 7·s3 + s3² + z'' }→ ifTimes(1, 0, z'', z1, s20) :|: s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 21 + 7·s1 + s1² + z'' }→ ifTimes(0, s'', z'', z1, s18) :|: s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 20 + 7·s2 + s2² + z'' }→ ifTimes(0, 0, z'', z1, s19) :|: s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

Function symbols to be analyzed: {timesIter,ifTimes}, {times}
Previous analysis results are:

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

Computed RUNTIME bound using PUBS for: timesIter
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 21 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''²

Computed RUNTIME bound using PUBS for: ifTimes
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 22 + 22·z'' + 8·z''·z1 + z''·z1² + 8·z1 + z1²

(48) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(z'', z1, z3) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 1 }→ timesIter(z', z'', 0) :|: z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 20 + 7·s3 + s3² + z'' }→ ifTimes(1, 0, z'', z1, s20) :|: s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0
timesIter(z', z'', z1) -{ 21 + 7·s1 + s1² + z'' }→ ifTimes(0, s'', z'', z1, s18) :|: s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 20 + 7·s2 + s2² + z'' }→ ifTimes(0, 0, z'', z1, s19) :|: s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0

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

minus: runtime: O(n¹) [1 + z''], size: O(n¹) [z']
f: runtime: O(1) [1], size: O(1) [1]
inc: runtime: O(n¹) [1 + z'], size: O(n¹) [1 + z']
eq: runtime: O(n¹) [1 + z''], size: O(1) [1]
plus: runtime: O(n²) [11 + 7·z' + z'²], size: O(1) [0]
ifPlus: runtime: O(n²) [12 + 7·z'' + z''²], size: O(n¹) [z1]
timesIter: runtime: O(n³) [21 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''²], size: O(n¹) [z'' + z1]
ifTimes: runtime: O(n³) [22 + 22·z'' + 8·z''·z1 + z''·z1² + 8·z1 + z1²], size: O(n¹) [z1 + z2 + z3]

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

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 22 + 22·z'' + 8·z''·z1 + z''·z1² + 8·z1 + z1² }→ s25 :|: s25 >= 0, s25 <= 1 * z3 + 1 * z1, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 22 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''² }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * z'', z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 43 + 22·s'' + 8·s''·z'' + s''·z''² + 7·s1 + s1² + 9·z'' + z''² }→ s22 :|: s22 >= 0, s22 <= 1 * z'' + 1 * s18 + 1 * z1, s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 42 + 7·s2 + s2² + 9·z'' + z''² }→ s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * s19 + 1 * z1, s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0
timesIter(z', z'', z1) -{ 42 + 7·s3 + s3² + 9·z'' + z''² }→ s24 :|: s24 >= 0, s24 <= 1 * z'' + 1 * s20 + 1 * z1, s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0

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

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

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

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 22 + 22·z'' + 8·z''·z1 + z''·z1² + 8·z1 + z1² }→ s25 :|: s25 >= 0, s25 <= 1 * z3 + 1 * z1, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 22 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''² }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * z'', z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 43 + 22·s'' + 8·s''·z'' + s''·z''² + 7·s1 + s1² + 9·z'' + z''² }→ s22 :|: s22 >= 0, s22 <= 1 * z'' + 1 * s18 + 1 * z1, s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 42 + 7·s2 + s2² + 9·z'' + z''² }→ s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * s19 + 1 * z1, s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0
timesIter(z', z'', z1) -{ 42 + 7·s3 + s3² + 9·z'' + z''² }→ s24 :|: s24 >= 0, s24 <= 1 * z'' + 1 * s20 + 1 * z1, s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0

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

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

Computed RUNTIME bound using KoAT for: times
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 22 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''²

(54) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 + z'' }→ s10 :|: s10 >= 0, s10 <= 1, z' - 1 >= 0, z'' - 1 >= 0
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' >= 0, z'' = z'
eq(z', z'') -{ 1 }→ 0 :|: z'' - 1 >= 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' - 1 >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 12 + 7·z'' + z''² }→ s17 :|: s17 >= 0, s17 <= 0, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0
ifPlus(z', z'', z1, z2) -{ 1 }→ z1 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1
ifTimes(z', z'', z1, z2, z3) -{ 22 + 22·z'' + 8·z''·z1 + z''·z1² + 8·z1 + z1² }→ s25 :|: s25 >= 0, s25 <= 1 * z3 + 1 * z1, z2 >= 0, z'' >= 0, z1 >= 0, z' = 0, z3 >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z2 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1, z3 >= 0
inc(z') -{ 1 + z' }→ 1 + s4 :|: s4 >= 0, s4 <= 1 * (z' - 1) + 1, z' - 1 >= 0
inc(z') -{ 1 }→ 1 + 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'') -{ 1 }→ 0 :|: z'' >= 0, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' = z'
plus(z', z'') -{ 17 + 7·s + s² + z' }→ s14 :|: s14 >= 0, s14 <= 1 * (1 + (z' - 1)), s5 >= 0, s5 <= 1 * (z' - 1) + 1, s >= 0, s <= 1 * (z' - 1), z' - 1 >= 0, z'' >= 0
plus(z', z'') -{ 17 }→ s15 :|: s15 >= 0, s15 <= 1 * (1 + 0), s6 >= 0, s6 <= 1 * 0 + 1, z'' >= 0, z' = 1 + 0
plus(z', z'') -{ 16 }→ s16 :|: s16 >= 0, s16 <= 1 * 0, z'' >= 0, z' = 0
times(z', z'') -{ 22 + 22·z' + 8·z'·z'' + z'·z''² + 8·z'' + z''² }→ s21 :|: s21 >= 0, s21 <= 1 * 0 + 1 * z'', z' >= 0, z'' >= 0
timesIter(z', z'', z1) -{ 43 + 22·s'' + 8·s''·z'' + s''·z''² + 7·s1 + s1² + 9·z'' + z''² }→ s22 :|: s22 >= 0, s22 <= 1 * z'' + 1 * s18 + 1 * z1, s18 >= 0, s18 <= 1 * z'', s11 >= 0, s11 <= 1, s7 >= 0, s7 <= 1 * z'' + 1, s'' >= 0, s'' <= 1 * (z' - 1), s1 >= 0, s1 <= 1 * z'', z1 >= 0, z'' >= 0, z' - 1 >= 0
timesIter(z', z'', z1) -{ 42 + 7·s2 + s2² + 9·z'' + z''² }→ s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * s19 + 1 * z1, s19 >= 0, s19 <= 1 * z'', s12 >= 0, s12 <= 1, s8 >= 0, s8 <= 1 * z'' + 1, s2 >= 0, s2 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 1 + 0
timesIter(z', z'', z1) -{ 42 + 7·s3 + s3² + 9·z'' + z''² }→ s24 :|: s24 >= 0, s24 <= 1 * z'' + 1 * s20 + 1 * z1, s20 >= 0, s20 <= 1 * z'', s13 >= 0, s13 <= 1, s9 >= 0, s9 <= 1 * z'' + 1, s3 >= 0, s3 <= 1 * z'', z1 >= 0, z'' >= 0, z' = 0

Function symbols to be analyzed:
Previous analysis results are:

(55) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

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

(46) Obligation:

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

(48) Obligation:

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

(50) Obligation:

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

(52) Obligation:

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

(54) Obligation:

(55) FinalProof (EQUIVALENT transformation)

(56) BOUNDS(1, n^3)