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

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 InnermostUnusableRulesProof (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), 0 ms)
↳12 CpxTypedWeightedCompleteTrs
↳13 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳14 CpxRNTS
↳15 InliningProof (UPPER BOUND(ID), 163 ms)
↳16 CpxRNTS
↳17 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 237 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 21 ms)
↳24 CpxRNTS
↳25 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 181 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 45 ms)
↳30 CpxRNTS
↳31 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 23 ms)
↳34 CpxRNTS
↳35 IntTrsBoundProof (UPPER BOUND(ID), 5 ms)
↳36 CpxRNTS
↳37 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 76 ms)
↳40 CpxRNTS
↳41 IntTrsBoundProof (UPPER BOUND(ID), 74 ms)
↳42 CpxRNTS
↳43 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳44 CpxRNTS
↳45 IntTrsBoundProof (UPPER BOUND(ID), 269 ms)
↳46 CpxRNTS
↳47 IntTrsBoundProof (UPPER BOUND(ID), 48 ms)
↳48 CpxRNTS
↳49 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳50 CpxRNTS
↳51 IntTrsBoundProof (UPPER BOUND(ID), 104 ms)
↳52 CpxRNTS
↳53 IntTrsBoundProof (UPPER BOUND(ID), 5 ms)
↳54 CpxRNTS
↳55 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳56 CpxRNTS
↳57 IntTrsBoundProof (UPPER BOUND(ID), 4412 ms)
↳58 CpxRNTS
↳59 IntTrsBoundProof (UPPER BOUND(ID), 1804 ms)
↳60 CpxRNTS
↳61 FinalProof (⇔, 0 ms)
↳62 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:

t(N) → cs(r(q(N)), nt(ns(N)))
q(0) → 0
q(s(X)) → s(p(q(X), d(X)))
d(0) → 0
d(s(X)) → s(s(d(X)))
p(0, X) → X
p(X, 0) → X
p(s(X), s(Y)) → s(s(p(X, Y)))
f(0, X) → nil
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z)))
t(X) → nt(X)
s(X) → ns(X)
f(X1, X2) → nf(X1, X2)
a(nt(X)) → t(a(X))
a(ns(X)) → s(a(X))
a(nf(X1, X2)) → f(a(X1), a(X2))
a(X) → X

Rewrite Strategy: INNERMOST

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

The following defined symbols can occur below the 0th argument of t: s, a, p, q, d, t, f
The following defined symbols can occur below the 0th argument of a: s, a, p, q, d, t, f
The following defined symbols can occur below the 0th argument of q: s, a, p, q, d, t, f
The following defined symbols can occur below the 0th argument of s: s, a, p, q, d, t, f
The following defined symbols can occur below the 0th argument of f: s, a, p, q, d, t, f
The following defined symbols can occur below the 1th argument of f: s, a, p, q, d, t, f
The following defined symbols can occur below the 0th argument of p: s, a, p, q, d, t, f
The following defined symbols can occur below the 1th argument of p: d

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
d(s(X)) → s(s(d(X)))
p(s(X), s(Y)) → s(s(p(X, Y)))

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

t(N) → cs(r(q(N)), nt(ns(N)))
t(X) → nt(X)
a(ns(X)) → s(a(X))
q(s(X)) → s(p(q(X), d(X)))
a(X) → X
a(nf(X1, X2)) → f(a(X1), a(X2))
d(0) → 0
f(0, X) → nil
f(X1, X2) → nf(X1, X2)
q(0) → 0
p(0, X) → X
p(X, 0) → X
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z)))
s(X) → ns(X)
a(nt(X)) → t(a(X))

Rewrite Strategy: INNERMOST

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

Transformed TRS to weighted TRS

(4) Obligation:

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


The TRS R consists of the following rules:

t(N) → cs(r(q(N)), nt(ns(N))) [1]
t(X) → nt(X) [1]
a(ns(X)) → s(a(X)) [1]
q(s(X)) → s(p(q(X), d(X))) [1]
a(X) → X [1]
a(nf(X1, X2)) → f(a(X1), a(X2)) [1]
d(0) → 0 [1]
f(0, X) → nil [1]
f(X1, X2) → nf(X1, X2) [1]
q(0) → 0 [1]
p(0, X) → X [1]
p(X, 0) → X [1]
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z))) [1]
s(X) → ns(X) [1]
a(nt(X)) → t(a(X)) [1]

Rewrite Strategy: INNERMOST

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

Removed the following rules with non-basic left-hand side, as they cannot be used in innermost rewriting:

q(s(X)) → s(p(q(X), d(X))) [1]
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z))) [1]

Due to the following rules that have to be used instead:

s(X) → ns(X) [1]

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

t(N) → cs(r(q(N)), nt(ns(N))) [1]
t(X) → nt(X) [1]
a(ns(X)) → s(a(X)) [1]
a(X) → X [1]
a(nf(X1, X2)) → f(a(X1), a(X2)) [1]
d(0) → 0 [1]
f(0, X) → nil [1]
f(X1, X2) → nf(X1, X2) [1]
q(0) → 0 [1]
p(0, X) → X [1]
p(X, 0) → X [1]
s(X) → ns(X) [1]
a(nt(X)) → t(a(X)) [1]

Rewrite Strategy: INNERMOST

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

Infered types.

(8) Obligation:

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

t(N) → cs(r(q(N)), nt(ns(N))) [1]
t(X) → nt(X) [1]
a(ns(X)) → s(a(X)) [1]
a(X) → X [1]
a(nf(X1, X2)) → f(a(X1), a(X2)) [1]
d(0) → 0 [1]
f(0, X) → nil [1]
f(X1, X2) → nf(X1, X2) [1]
q(0) → 0 [1]
p(0, X) → X [1]
p(X, 0) → X [1]
s(X) → ns(X) [1]
a(nt(X)) → t(a(X)) [1]

The TRS has the following type information:
t :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
cs :: r → ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
r :: ns:nt:cs:nf:0:nil → r
q :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
nt :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
ns :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
a :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
s :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
nf :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
f :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
d :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil
0 :: ns:nt:cs:nf:0:nil
nil :: ns:nt:cs:nf:0:nil
p :: ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil → ns:nt:cs:nf:0:nil

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:


d
p

(c) The following functions are completely defined:

a
s
f
t
q

Due to the following rules being added:

q(v0) → null_q [0]

And the following fresh constants:

null_q, const

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

t(N) → cs(r(q(N)), nt(ns(N))) [1]
t(X) → nt(X) [1]
a(ns(X)) → s(a(X)) [1]
a(X) → X [1]
a(nf(X1, X2)) → f(a(X1), a(X2)) [1]
d(0) → 0 [1]
f(0, X) → nil [1]
f(X1, X2) → nf(X1, X2) [1]
q(0) → 0 [1]
p(0, X) → X [1]
p(X, 0) → X [1]
s(X) → ns(X) [1]
a(nt(X)) → t(a(X)) [1]
q(v0) → null_q [0]

The TRS has the following type information:
t :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
cs :: r → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
r :: ns:nt:cs:nf:0:nil:null_q → r
q :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
nt :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
ns :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
a :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
s :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
nf :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
f :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
d :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
0 :: ns:nt:cs:nf:0:nil:null_q
nil :: ns:nt:cs:nf:0:nil:null_q
p :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
null_q :: ns:nt:cs:nf:0:nil:null_q
const :: r

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:

t(N) → cs(r(q(N)), nt(ns(N))) [1]
t(X) → nt(X) [1]
a(ns(ns(X'))) → s(s(a(X'))) [2]
a(ns(X)) → s(X) [2]
a(ns(nf(X1', X2'))) → s(f(a(X1'), a(X2'))) [2]
a(ns(nt(X''))) → s(t(a(X''))) [2]
a(X) → X [1]
a(nf(ns(X3), ns(X5))) → f(s(a(X3)), s(a(X5))) [3]
a(nf(ns(X3), X2)) → f(s(a(X3)), X2) [3]
a(nf(ns(X3), nf(X11, X21))) → f(s(a(X3)), f(a(X11), a(X21))) [3]
a(nf(ns(X3), nt(X6))) → f(s(a(X3)), t(a(X6))) [3]
a(nf(X1, ns(X7))) → f(X1, s(a(X7))) [3]
a(nf(X1, X2)) → f(X1, X2) [3]
a(nf(X1, nf(X12, X22))) → f(X1, f(a(X12), a(X22))) [3]
a(nf(X1, nt(X8))) → f(X1, t(a(X8))) [3]
a(nf(nf(X1'', X2''), ns(X9))) → f(f(a(X1''), a(X2'')), s(a(X9))) [3]
a(nf(nf(X1'', X2''), X2)) → f(f(a(X1''), a(X2'')), X2) [3]
a(nf(nf(X1'', X2''), nf(X13, X23))) → f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) [3]
a(nf(nf(X1'', X2''), nt(X10))) → f(f(a(X1''), a(X2'')), t(a(X10))) [3]
a(nf(nt(X4), ns(X14))) → f(t(a(X4)), s(a(X14))) [3]
a(nf(nt(X4), X2)) → f(t(a(X4)), X2) [3]
a(nf(nt(X4), nf(X15, X24))) → f(t(a(X4)), f(a(X15), a(X24))) [3]
a(nf(nt(X4), nt(X16))) → f(t(a(X4)), t(a(X16))) [3]
d(0) → 0 [1]
f(0, X) → nil [1]
f(X1, X2) → nf(X1, X2) [1]
q(0) → 0 [1]
p(0, X) → X [1]
p(X, 0) → X [1]
s(X) → ns(X) [1]
a(nt(ns(X17))) → t(s(a(X17))) [2]
a(nt(X)) → t(X) [2]
a(nt(nf(X18, X25))) → t(f(a(X18), a(X25))) [2]
a(nt(nt(X19))) → t(t(a(X19))) [2]
q(v0) → null_q [0]

The TRS has the following type information:
t :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
cs :: r → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
r :: ns:nt:cs:nf:0:nil:null_q → r
q :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
nt :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
ns :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
a :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
s :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
nf :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
f :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
d :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
0 :: ns:nt:cs:nf:0:nil:null_q
nil :: ns:nt:cs:nf:0:nil:null_q
p :: ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q → ns:nt:cs:nf:0:nil:null_q
null_q :: ns:nt:cs:nf:0:nil:null_q
const :: r

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:

0 => 0
nil => 1
null_q => 0
const => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ X :|: X >= 0, z = X
a(z) -{ 2 }→ t(X) :|: z = 1 + X, X >= 0
a(z) -{ 2 }→ t(t(a(X19))) :|: X19 >= 0, z = 1 + (1 + X19)
a(z) -{ 2 }→ t(s(a(X17))) :|: X17 >= 0, z = 1 + (1 + X17)
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
a(z) -{ 2 }→ s(t(a(X''))) :|: z = 1 + (1 + X''), X'' >= 0
a(z) -{ 2 }→ s(s(a(X'))) :|: X' >= 0, z = 1 + (1 + X')
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
f(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
p(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
p(z, z') -{ 1 }→ X :|: X >= 0, z = X, z' = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
t(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
t(z) -{ 1 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z = N, N >= 0

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

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

f(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
f(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
t(z) -{ 1 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z = N, N >= 0
t(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(16) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ X :|: X >= 0, z = X
a(z) -{ 2 }→ t(t(a(X19))) :|: X19 >= 0, z = 1 + (1 + X19)
a(z) -{ 2 }→ t(s(a(X17))) :|: X17 >= 0, z = 1 + (1 + X17)
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(X''))) :|: z = 1 + (1 + X''), X'' >= 0
a(z) -{ 2 }→ s(s(a(X'))) :|: X' >= 0, z = 1 + (1 + X')
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z = 1 + X, X >= 0, X = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
f(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
p(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
p(z, z') -{ 1 }→ X :|: X >= 0, z = X, z' = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
t(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + N)) :|: z = N, N >= 0, N = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + N)) :|: z = N, N >= 0, v0 >= 0, N = v0

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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

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

Found the following analysis order by SCC decomposition:

{ f }
{ t }
{ d }
{ q }
{ p }
{ s }
{ a }

(20) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {f}, {t}, {d}, {q}, {p}, {s}, {a}

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


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

(22) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {f}, {t}, {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: ?, size: O(n1) [1 + z + z']

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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {t}, {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']

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

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

(26) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {t}, {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']

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


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

(28) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {t}, {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: ?, size: O(n1) [4 + z]

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


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

(30) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + 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:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]

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


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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {d}, {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: ?, size: O(1) [0]

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


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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: 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:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]

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


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

(40) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {q}, {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: ?, size: O(1) [0]

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


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

(42) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 3 }→ 1 + (1 + q(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]

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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]

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


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

(46) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {p}, {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: ?, size: O(n1) [z + z']

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


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

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']

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

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

(50) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']

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


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

(52) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']
s: runtime: ?, size: O(n1) [1 + z]

(53) 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

(54) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']
s: runtime: O(1) [1], size: O(n1) [1 + z]

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

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

(56) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']
s: runtime: O(1) [1], size: O(n1) [1 + z]

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


Computed SIZE bound using KoAT for: a
after applying outer abstraction to obtain an ITS,
resulting in: O(n2) with polynomial bound: 92 + 195·z + 22·z2

(58) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {a}
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']
s: runtime: O(1) [1], size: O(n1) [1 + z]
a: runtime: ?, size: O(n2) [92 + 195·z + 22·z2]

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


Computed RUNTIME bound using KoAT for: a
after applying outer abstraction to obtain an ITS,
resulting in: O(n1) with polynomial bound: 132 + 264·z

(60) Obligation:

Complexity RNTS consisting of the following rules:

a(z) -{ 1 }→ z :|: z >= 0
a(z) -{ 2 }→ t(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ t(f(a(X18), a(X25))) :|: X18 >= 0, z = 1 + (1 + X18 + X25), X25 >= 0
a(z) -{ 2 }→ s(t(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(s(a(z - 2))) :|: z - 2 >= 0
a(z) -{ 2 }→ s(f(a(X1'), a(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
a(z) -{ 3 }→ f(X1, t(a(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
a(z) -{ 3 }→ f(X1, s(a(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
a(z) -{ 3 }→ f(X1, f(a(X12), a(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
a(z) -{ 3 }→ f(t(a(X4)), X2) :|: X4 >= 0, X2 >= 0, z = 1 + (1 + X4) + X2
a(z) -{ 3 }→ f(t(a(X4)), t(a(X16))) :|: X16 >= 0, z = 1 + (1 + X4) + (1 + X16), X4 >= 0
a(z) -{ 3 }→ f(t(a(X4)), s(a(X14))) :|: X4 >= 0, z = 1 + (1 + X4) + (1 + X14), X14 >= 0
a(z) -{ 3 }→ f(t(a(X4)), f(a(X15), a(X24))) :|: z = 1 + (1 + X4) + (1 + X15 + X24), X4 >= 0, X15 >= 0, X24 >= 0
a(z) -{ 3 }→ f(s(a(X3)), X2) :|: z = 1 + (1 + X3) + X2, X3 >= 0, X2 >= 0
a(z) -{ 3 }→ f(s(a(X3)), t(a(X6))) :|: X6 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X6)
a(z) -{ 3 }→ f(s(a(X3)), s(a(X5))) :|: X5 >= 0, X3 >= 0, z = 1 + (1 + X3) + (1 + X5)
a(z) -{ 3 }→ f(s(a(X3)), f(a(X11), a(X21))) :|: X11 >= 0, X21 >= 0, z = 1 + (1 + X3) + (1 + X11 + X21), X3 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), X2) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + X2, X2'' >= 0, X2 >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), t(a(X10))) :|: z = 1 + (1 + X1'' + X2'') + (1 + X10), X1'' >= 0, X10 >= 0, X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), s(a(X9))) :|: X1'' >= 0, X9 >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X9), X2'' >= 0
a(z) -{ 3 }→ f(f(a(X1''), a(X2'')), f(a(X13), a(X23))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2'') + (1 + X13 + X23), X2'' >= 0, X13 >= 0, X23 >= 0
a(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
a(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
a(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
a(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
d(z) -{ 1 }→ 0 :|: z = 0
f(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
f(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
p(z, z') -{ 1 }→ z :|: z >= 0, z' = 0
p(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
q(z) -{ 1 }→ 0 :|: z = 0
q(z) -{ 0 }→ 0 :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 1 }→ 1 + z :|: z >= 0
t(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
t(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed:
Previous analysis results are:
f: runtime: O(1) [1], size: O(n1) [1 + z + z']
t: runtime: O(1) [2], size: O(n1) [4 + z]
d: runtime: O(1) [1], size: O(1) [0]
q: runtime: O(1) [1], size: O(1) [0]
p: runtime: O(1) [1], size: O(n1) [z + z']
s: runtime: O(1) [1], size: O(n1) [1 + z]
a: runtime: O(n1) [132 + 264·z], size: O(n2) [92 + 195·z + 22·z2]

(61) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(62) BOUNDS(1, n^1)