Runtime Complexity (innermost) proof of /tmp/tmpvHDWTv/Ex49_GM04

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

0 CpxTRS

↳1 DependencyGraphProof (BOTH BOUNDS(ID, ID), 4 ms)

↳2 CpxTRS

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

↳4 CpxWeightedTrs

↳5 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CpxWeightedTrs

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

↳8 CpxTypedWeightedTrs

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

↳10 CpxTypedWeightedCompleteTrs

↳11 NarrowingProof (BOTH BOUNDS(ID, ID), 15 ms)

↳12 CpxTypedWeightedCompleteTrs

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

↳14 CpxRNTS

↳15 InliningProof (UPPER BOUND(ID), 701 ms)

↳16 CpxRNTS

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

↳18 CpxRNTS

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

↳20 CpxRNTS

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

↳22 CpxRNTS

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

↳24 CpxRNTS

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

↳26 CpxRNTS

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

↳28 CpxRNTS

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

↳30 CpxRNTS

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

↳32 CpxRNTS

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

↳34 CpxRNTS

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

↳36 CpxRNTS

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

↳38 CpxRNTS

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

↳40 CpxRNTS

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

↳42 CpxRNTS

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

↳44 CpxRNTS

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

↳46 CpxRNTS

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

↳48 CpxRNTS

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

↳50 CpxRNTS

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

↳52 CpxRNTS

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

↳54 CpxRNTS

↳55 FinalProof (⇔, 0 ms)

↳56 BOUNDS(1, n^1)

(0) Obligation:

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

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Rewrite Strategy: INNERMOST

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

The following rules are not reachable from basic terms in the dependency graph and can be removed:
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)

(2) Obligation:

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

The TRS R consists of the following rules:

minus(n__0, Y) → 0
activate(n__0) → 0
geq(X, n__0) → true
if(false, X, Y) → activate(Y)
0 → n__0
if(true, X, Y) → activate(X)
s(X) → n__s(X)
activate(X) → X
activate(n__s(X)) → s(X)
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(n__0, n__s(Y)) → false

Rewrite Strategy: INNERMOST

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

Transformed TRS to weighted TRS

(4) Obligation:

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

The TRS R consists of the following rules:

minus(n__0, Y) → 0 [1]
activate(n__0) → 0 [1]
geq(X, n__0) → true [1]
if(false, X, Y) → activate(Y) [1]
0 → n__0 [1]
if(true, X, Y) → activate(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(X) [1]
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y)) [1]
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y)) [1]
geq(n__0, n__s(Y)) → false [1]

Rewrite Strategy: INNERMOST

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

Renamed defined symbols to avoid conflicts with arithmetic symbols:

0 => 0'

(6) Obligation:

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

The TRS R consists of the following rules:

minus(n__0, Y) → 0' [1]
activate(n__0) → 0' [1]
geq(X, n__0) → true [1]
if(false, X, Y) → activate(Y) [1]
0' → n__0 [1]
if(true, X, Y) → activate(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(X) [1]
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y)) [1]
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y)) [1]
geq(n__0, n__s(Y)) → false [1]

Rewrite Strategy: INNERMOST

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

Infered types.

(8) Obligation:

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

minus(n__0, Y) → 0' [1]
activate(n__0) → 0' [1]
geq(X, n__0) → true [1]
if(false, X, Y) → activate(Y) [1]
0' → n__0 [1]
if(true, X, Y) → activate(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(X) [1]
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y)) [1]
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y)) [1]
geq(n__0, n__s(Y)) → false [1]

The TRS has the following type information:

minus :: n__0:n__s → n__0:n__s → n__0:n__s
n__0 :: n__0:n__s
0' :: n__0:n__s
activate :: n__0:n__s → n__0:n__s
geq :: n__0:n__s → n__0:n__s → true:false
true :: true:false
if :: true:false → n__0:n__s → n__0:n__s → n__0:n__s
false :: true:false
s :: n__0:n__s → n__0:n__s
n__s :: n__0:n__s → n__0:n__s

Rewrite Strategy: INNERMOST

(9) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

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

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

minus
geq
if

activate
0'
s

Due to the following rules being added:
none

And the following fresh constants: none

(10) Obligation:

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

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

minus(n__0, Y) → 0' [1]
activate(n__0) → 0' [1]
geq(X, n__0) → true [1]
if(false, X, Y) → activate(Y) [1]
0' → n__0 [1]
if(true, X, Y) → activate(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(X) [1]
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y)) [1]
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y)) [1]
geq(n__0, n__s(Y)) → false [1]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

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

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

(12) Obligation:

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

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

minus(n__0, Y) → 0' [1]
activate(n__0) → 0' [1]
geq(X, n__0) → true [1]
if(false, X, Y) → activate(Y) [1]
0' → n__0 [1]
if(true, X, Y) → activate(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(X) [1]
geq(n__s(n__0), n__s(n__0)) → geq(0', 0') [3]
geq(n__s(n__0), n__s(Y)) → geq(0', Y) [3]
geq(n__s(n__0), n__s(n__s(X''))) → geq(0', s(X'')) [3]
geq(n__s(X), n__s(n__0)) → geq(X, 0') [3]
geq(n__s(X), n__s(Y)) → geq(X, Y) [3]
geq(n__s(X), n__s(n__s(X1))) → geq(X, s(X1)) [3]
geq(n__s(n__s(X')), n__s(n__0)) → geq(s(X'), 0') [3]
geq(n__s(n__s(X')), n__s(Y)) → geq(s(X'), Y) [3]
geq(n__s(n__s(X')), n__s(n__s(X2))) → geq(s(X'), s(X2)) [3]
minus(n__s(n__0), n__s(n__0)) → minus(0', 0') [3]
minus(n__s(n__0), n__s(Y)) → minus(0', Y) [3]
minus(n__s(n__0), n__s(n__s(X4))) → minus(0', s(X4)) [3]
minus(n__s(X), n__s(n__0)) → minus(X, 0') [3]
minus(n__s(X), n__s(Y)) → minus(X, Y) [3]
minus(n__s(X), n__s(n__s(X5))) → minus(X, s(X5)) [3]
minus(n__s(n__s(X3)), n__s(n__0)) → minus(s(X3), 0') [3]
minus(n__s(n__s(X3)), n__s(Y)) → minus(s(X3), Y) [3]
minus(n__s(n__s(X3)), n__s(n__s(X6))) → minus(s(X3), s(X6)) [3]
geq(n__0, n__s(Y)) → false [1]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

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

n__0 => 0
true => 1
false => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ 0' :|: z = 0
geq(z, z') -{ 3 }→ geq(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
geq(z, z') -{ 3 }→ geq(X, s(X1)) :|: X1 >= 0, z = 1 + X, X >= 0, z' = 1 + (1 + X1)
geq(z, z') -{ 3 }→ geq(X, 0') :|: z = 1 + X, X >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(s(X'), Y) :|: Y >= 0, z' = 1 + Y, X' >= 0, z = 1 + (1 + X')
geq(z, z') -{ 3 }→ geq(s(X'), s(X2)) :|: z' = 1 + (1 + X2), X' >= 0, z = 1 + (1 + X'), X2 >= 0
geq(z, z') -{ 3 }→ geq(s(X'), 0') :|: X' >= 0, z' = 1 + 0, z = 1 + (1 + X')
geq(z, z') -{ 3 }→ geq(0', Y) :|: Y >= 0, z = 1 + 0, z' = 1 + Y
geq(z, z') -{ 3 }→ geq(0', s(X'')) :|: z = 1 + 0, z' = 1 + (1 + X''), X'' >= 0
geq(z, z') -{ 3 }→ geq(0', 0') :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 1 }→ 1 :|: X >= 0, z = X, z' = 0
geq(z, z') -{ 1 }→ 0 :|: Y >= 0, z' = 1 + Y, z = 0
if(z, z', z'') -{ 1 }→ activate(X) :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
if(z, z', z'') -{ 1 }→ activate(Y) :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0
minus(z, z') -{ 3 }→ minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
minus(z, z') -{ 3 }→ minus(X, s(X5)) :|: X5 >= 0, z' = 1 + (1 + X5), z = 1 + X, X >= 0
minus(z, z') -{ 3 }→ minus(X, 0') :|: z = 1 + X, X >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(s(X3), Y) :|: z = 1 + (1 + X3), Y >= 0, z' = 1 + Y, X3 >= 0
minus(z, z') -{ 3 }→ minus(s(X3), s(X6)) :|: z' = 1 + (1 + X6), z = 1 + (1 + X3), X6 >= 0, X3 >= 0
minus(z, z') -{ 3 }→ minus(s(X3), 0') :|: z = 1 + (1 + X3), X3 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(0', Y) :|: Y >= 0, z = 1 + 0, z' = 1 + Y
minus(z, z') -{ 3 }→ minus(0', s(X4)) :|: z' = 1 + (1 + X4), z = 1 + 0, X4 >= 0
minus(z, z') -{ 3 }→ minus(0', 0') :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 1 }→ 0' :|: z' = Y, Y >= 0, z = 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

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

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

0' -{ 1 }→ 0 :|:
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
activate(z) -{ 1 }→ 0' :|: z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ s(X) :|: z = 1 + X, X >= 0

(16) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
geq(z, z') -{ 3 }→ geq(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
geq(z, z') -{ 4 }→ geq(X, 0) :|: z = 1 + X, X >= 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(X, 1 + X') :|: X1 >= 0, z = 1 + X, X >= 0, z' = 1 + (1 + X1), X' >= 0, X1 = X'
geq(z, z') -{ 4 }→ geq(0, Y) :|: Y >= 0, z = 1 + 0, z' = 1 + Y
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' = 1 + (1 + X''), X'' >= 0, X >= 0, X'' = X
geq(z, z') -{ 4 }→ geq(1 + X, Y) :|: Y >= 0, z' = 1 + Y, X' >= 0, z = 1 + (1 + X'), X >= 0, X' = X
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: X' >= 0, z' = 1 + 0, z = 1 + (1 + X'), X >= 0, X' = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z' = 1 + (1 + X2), X' >= 0, z = 1 + (1 + X'), X2 >= 0, X >= 0, X' = X, X'' >= 0, X2 = X''
geq(z, z') -{ 1 }→ 1 :|: X >= 0, z = X, z' = 0
geq(z, z') -{ 1 }→ 0 :|: Y >= 0, z' = 1 + Y, z = 0
if(z, z', z'') -{ 2 }→ X' :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0, X' >= 0, Y = X'
if(z, z', z'') -{ 2 }→ X' :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0, X' >= 0, X = X'
if(z, z', z'') -{ 2 }→ s(X') :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0, Y = 1 + X', X' >= 0
if(z, z', z'') -{ 2 }→ s(X') :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0, X = 1 + X', X' >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0, Y = 0
if(z, z', z'') -{ 2 }→ 0' :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0, X = 0
minus(z, z') -{ 3 }→ minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
minus(z, z') -{ 4 }→ minus(X, 0) :|: z = 1 + X, X >= 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(X, 1 + X') :|: X5 >= 0, z' = 1 + (1 + X5), z = 1 + X, X >= 0, X' >= 0, X5 = X'
minus(z, z') -{ 4 }→ minus(0, Y) :|: Y >= 0, z = 1 + 0, z' = 1 + Y
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z' = 1 + (1 + X4), z = 1 + 0, X4 >= 0, X >= 0, X4 = X
minus(z, z') -{ 4 }→ minus(1 + X, Y) :|: z = 1 + (1 + X3), Y >= 0, z' = 1 + Y, X3 >= 0, X >= 0, X3 = X
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z = 1 + (1 + X3), X3 >= 0, z' = 1 + 0, X >= 0, X3 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' = 1 + (1 + X6), z = 1 + (1 + X3), X6 >= 0, X3 >= 0, X >= 0, X3 = X, X' >= 0, X6 = X'
minus(z, z') -{ 2 }→ 0 :|: z' = Y, Y >= 0, z = 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

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

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

(18) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

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

Found the following analysis order by SCC decomposition:

{ activate }
{ minus }
{ 0' }
{ geq }
{ s }
{ if }

(20) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {activate}, {minus}, {0'}, {geq}, {s}, {if}

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

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

(22) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {activate}, {minus}, {0'}, {geq}, {s}, {if}
Previous analysis results are:

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

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {minus}, {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [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:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {minus}, {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]

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

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

(28) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {minus}, {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: ?, size: O(1) [0]

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

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

(30) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ 5 }→ minus(0, 0) :|: z = 1 + 0, z' = 1 + 0
minus(z, z') -{ 4 }→ minus(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 5 }→ minus(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 4 }→ minus(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 3 }→ minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 4 }→ minus(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ 5 }→ minus(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 4 }→ minus(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 5 }→ minus(1 + X, 1 + X') :|: z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]

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

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]

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

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

(34) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {0'}, {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: ?, size: O(1) [0]

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

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

(36) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 2 }→ 0' :|: z'' >= 0, z = 1, z' >= 0, z' = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]

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

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]

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

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

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {geq}, {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]
geq: runtime: ?, size: O(1) [1]

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 5 }→ geq(0, 0) :|: z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 4 }→ geq(0, z' - 1) :|: z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ 5 }→ geq(0, 1 + X) :|: z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 4 }→ geq(z - 1, 0) :|: z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ 3 }→ geq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 4 }→ geq(z - 1, 1 + X') :|: z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 5 }→ geq(1 + X, 0) :|: z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ 4 }→ geq(1 + X, z' - 1) :|: z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 5 }→ geq(1 + X, 1 + X'') :|: z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]
geq: runtime: O(n¹) [2 + 39·z], 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:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]
geq: runtime: O(n¹) [2 + 39·z], size: O(1) [1]

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

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

(46) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed: {s}, {if}
Previous analysis results are:

activate: runtime: O(1) [5], size: O(n¹) [z]
minus: runtime: O(n¹) [2 + 39·z'], size: O(1) [0]
0': runtime: O(1) [1], size: O(1) [0]
geq: runtime: O(n¹) [2 + 39·z], size: O(1) [1]
s: runtime: ?, size: O(n¹) [1 + z]

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
if(z, z', z'') -{ 2 }→ s(z' - 1) :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 2 }→ s(z'' - 1) :|: z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

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

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

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s18 :|: s18 >= 0, s18 <= 1 * (z'' - 1) + 1, z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 3 }→ s19 :|: s19 >= 0, s19 <= 1 * (z' - 1) + 1, z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

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

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

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

(52) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s18 :|: s18 >= 0, s18 <= 1 * (z'' - 1) + 1, z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 3 }→ s19 :|: s19 >= 0, s19 <= 1 * (z' - 1) + 1, z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

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

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

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

0' -{ 1 }→ 0 :|:
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 0 :|: z = 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
geq(z, z') -{ 7 }→ s10 :|: s10 >= 0, s10 <= 1, z = 1 + 0, z' = 1 + 0
geq(z, z') -{ 6 }→ s11 :|: s11 >= 0, s11 <= 1, z' - 1 >= 0, z = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s12 :|: s12 >= 0, s12 <= 1, z - 1 >= 0, z' = 1 + 0
geq(z, z') -{ -33 + 39·z }→ s13 :|: s13 >= 0, s13 <= 1, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
geq(z, z') -{ 45 + 39·X }→ s14 :|: s14 >= 0, s14 <= 1, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
geq(z, z') -{ 46 + 39·X }→ s15 :|: s15 >= 0, s15 <= 1, z - 2 >= 0, z' - 2 >= 0, X >= 0, z - 2 = X, X'' >= 0, z' - 2 = X''
geq(z, z') -{ 7 }→ s16 :|: s16 >= 0, s16 <= 1, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
geq(z, z') -{ 46 + 39·X }→ s17 :|: s17 >= 0, s17 <= 1, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
geq(z, z') -{ -34 + 39·z }→ s9 :|: s9 >= 0, s9 <= 1, z' - 1 >= 0, z - 1 >= 0
geq(z, z') -{ 1 }→ 1 :|: z >= 0, z' = 0
geq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
if(z, z', z'') -{ 3 }→ s18 :|: s18 >= 0, s18 <= 1 * (z'' - 1) + 1, z'' >= 0, z' >= 0, z = 0, z'' - 1 >= 0
if(z, z', z'') -{ 3 }→ s19 :|: s19 >= 0, s19 <= 1 * (z' - 1) + 1, z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0
if(z, z', z'') -{ 3 }→ s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z' >= 0, z = 0, z'' = 0
if(z, z', z'') -{ 3 }→ s8 :|: s8 >= 0, s8 <= 0, z'' >= 0, z = 1, z' >= 0, z' = 0
if(z, z', z'') -{ 2 }→ z' :|: z'' >= 0, z = 1, z' >= 0
if(z, z', z'') -{ 2 }→ z'' :|: z'' >= 0, z' >= 0, z = 0
minus(z, z') -{ -34 + 39·z' }→ s :|: s >= 0, s <= 0, z' - 1 >= 0, z - 1 >= 0
minus(z, z') -{ 7 }→ s' :|: s' >= 0, s' <= 0, z = 1 + 0, z' = 1 + 0
minus(z, z') -{ -33 + 39·z' }→ s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z = 1 + 0
minus(z, z') -{ 6 }→ s1 :|: s1 >= 0, s1 <= 0, z - 1 >= 0, z' = 1 + 0
minus(z, z') -{ 45 + 39·X' }→ s2 :|: s2 >= 0, s2 <= 0, z' - 2 >= 0, z - 1 >= 0, X' >= 0, z' - 2 = X'
minus(z, z') -{ -33 + 39·z' }→ s3 :|: s3 >= 0, s3 <= 0, z' - 1 >= 0, z - 2 >= 0, X >= 0, z - 2 = X
minus(z, z') -{ 46 + 39·X' }→ s4 :|: s4 >= 0, s4 <= 0, z' - 2 >= 0, z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, z' - 2 = X'
minus(z, z') -{ 46 + 39·X }→ s5 :|: s5 >= 0, s5 <= 0, z = 1 + 0, z' - 2 >= 0, X >= 0, z' - 2 = X
minus(z, z') -{ 7 }→ s6 :|: s6 >= 0, s6 <= 0, z - 2 >= 0, z' = 1 + 0, X >= 0, z - 2 = X
minus(z, z') -{ 2 }→ 0 :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0

Function symbols to be analyzed:
Previous analysis results are:

(55) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CompletionProof (UPPER BOUND(ID) transformation)

(10) Obligation:

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

(12) Obligation:

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, 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^1)