WORST_CASE(Omega(n^1),O(n^3))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 523 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [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), 4 ms]
    (10) CpxTypedWeightedCompleteTrs
    (11) NarrowingProof [BOTH BOUNDS(ID, ID), 83 ms]
    (12) CpxTypedWeightedCompleteTrs
    (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (14) CpxRNTS
    (15) InliningProof [UPPER BOUND(ID), 0 ms]
    (16) CpxRNTS
    (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxRNTS
    (19) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 2 ms]
    (20) CpxRNTS
    (21) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (22) CpxRNTS
    (23) IntTrsBoundProof [UPPER BOUND(ID), 243 ms]
    (24) CpxRNTS
    (25) IntTrsBoundProof [UPPER BOUND(ID), 75 ms]
    (26) CpxRNTS
    (27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (28) CpxRNTS
    (29) IntTrsBoundProof [UPPER BOUND(ID), 332 ms]
    (30) CpxRNTS
    (31) IntTrsBoundProof [UPPER BOUND(ID), 125 ms]
    (32) CpxRNTS
    (33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (34) CpxRNTS
    (35) IntTrsBoundProof [UPPER BOUND(ID), 362 ms]
    (36) CpxRNTS
    (37) IntTrsBoundProof [UPPER BOUND(ID), 166 ms]
    (38) CpxRNTS
    (39) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (40) CpxRNTS
    (41) IntTrsBoundProof [UPPER BOUND(ID), 180 ms]
    (42) CpxRNTS
    (43) IntTrsBoundProof [UPPER BOUND(ID), 62 ms]
    (44) CpxRNTS
    (45) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (46) CpxRNTS
    (47) IntTrsBoundProof [UPPER BOUND(ID), 210 ms]
    (48) CpxRNTS
    (49) IntTrsBoundProof [UPPER BOUND(ID), 6 ms]
    (50) CpxRNTS
    (51) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (52) CpxRNTS
    (53) IntTrsBoundProof [UPPER BOUND(ID), 249 ms]
    (54) CpxRNTS
    (55) IntTrsBoundProof [UPPER BOUND(ID), 33 ms]
    (56) CpxRNTS
    (57) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (58) CpxRNTS
    (59) IntTrsBoundProof [UPPER BOUND(ID), 2120 ms]
    (60) CpxRNTS
    (61) IntTrsBoundProof [UPPER BOUND(ID), 688 ms]
    (62) CpxRNTS
    (63) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (64) CpxRNTS
    (65) IntTrsBoundProof [UPPER BOUND(ID), 4403 ms]
    (66) CpxRNTS
    (67) IntTrsBoundProof [UPPER BOUND(ID), 794 ms]
    (68) CpxRNTS
    (69) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (70) CpxRNTS
    (71) IntTrsBoundProof [UPPER BOUND(ID), 638 ms]
    (72) CpxRNTS
    (73) IntTrsBoundProof [UPPER BOUND(ID), 52 ms]
    (74) CpxRNTS
    (75) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
    (76) CpxRNTS
    (77) IntTrsBoundProof [UPPER BOUND(ID), 570 ms]
    (78) CpxRNTS
    (79) IntTrsBoundProof [UPPER BOUND(ID), 3 ms]
    (80) CpxRNTS
    (81) FinalProof [FINISHED, 0 ms]
    (82) BOUNDS(1, n^3)
(83) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(84) TRS for Loop Detection
    (85) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (86) BEST
        (87) proven lower bound
            (88) LowerBoundPropagationProof [FINISHED, 0 ms]
            (89) BOUNDS(n^1, INF)
        (90) TRS for Loop Detection


----------------------------------------

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   <='(0, z0) -> c2
   <='(s(z0), 0) -> c3
   <='(s(z0), s(z1)) -> c4(<='(z0, z1))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6
   PERFECTP(0) -> c7
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c9
   F(0, z0, s(z1), z2) -> c10
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0)))
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1))
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0))
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3))

The (relative) TRS S consists of the following rules:

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   <=(0, z0) -> true
   <=(s(z0), 0) -> false
   <=(s(z0), s(z1)) -> <=(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   <='(0, z0) -> c2
   <='(s(z0), 0) -> c3
   <='(s(z0), s(z1)) -> c4(<='(z0, z1))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6
   PERFECTP(0) -> c7
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c9
   F(0, z0, s(z1), z2) -> c10
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0)))
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1))
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0))
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3))

The (relative) TRS S consists of the following rules:

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   <=(0, z0) -> true
   <=(s(z0), 0) -> false
   <=(s(z0), s(z1)) -> <=(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c [1]
   -'(s(z0), s(z1)) -> c1(-'(z0, z1)) [1]
   <='(0, z0) -> c2 [1]
   <='(s(z0), 0) -> c3 [1]
   <='(s(z0), s(z1)) -> c4(<='(z0, z1)) [1]
   IF(true, z0, z1) -> c5 [1]
   IF(false, z0, z1) -> c6 [1]
   PERFECTP(0) -> c7 [1]
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0))) [1]
   F(0, z0, 0, z1) -> c9 [1]
   F(0, z0, s(z1), z2) -> c10 [1]
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0))) [1]
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1)) [1]
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0)) [1]
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3)) [1]
   -(z0, 0) -> z0 [0]
   -(s(z0), s(z1)) -> -(z0, z1) [0]
   <=(0, z0) -> true [0]
   <=(s(z0), 0) -> false [0]
   <=(s(z0), s(z1)) -> <=(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   perfectp(0) -> false [0]
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0)) [0]
   f(0, z0, 0, z1) -> true [0]
   f(0, z0, s(z1), z2) -> false [0]
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2) [0]
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus
<= => lteq

----------------------------------------

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c [1]
   -'(s(z0), s(z1)) -> c1(-'(z0, z1)) [1]
   <='(0, z0) -> c2 [1]
   <='(s(z0), 0) -> c3 [1]
   <='(s(z0), s(z1)) -> c4(<='(z0, z1)) [1]
   IF(true, z0, z1) -> c5 [1]
   IF(false, z0, z1) -> c6 [1]
   PERFECTP(0) -> c7 [1]
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0))) [1]
   F(0, z0, 0, z1) -> c9 [1]
   F(0, z0, s(z1), z2) -> c10 [1]
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, minus(z1, s(z0)), z2), -'(z1, s(z0))) [1]
   F(s(z0), s(z1), z2, z3) -> c12(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1)) [1]
   F(s(z0), s(z1), z2, z3) -> c13(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), minus(z1, z0), z2, z3), -'(z1, z0)) [1]
   F(s(z0), s(z1), z2, z3) -> c14(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lteq(0, z0) -> true [0]
   lteq(s(z0), 0) -> false [0]
   lteq(s(z0), s(z1)) -> lteq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   perfectp(0) -> false [0]
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0)) [0]
   f(0, z0, 0, z1) -> true [0]
   f(0, z0, s(z1), z2) -> false [0]
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2) [0]
   f(s(z0), s(z1), z2, z3) -> if(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(8)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   -'(z0, 0) -> c [1]
   -'(s(z0), s(z1)) -> c1(-'(z0, z1)) [1]
   <='(0, z0) -> c2 [1]
   <='(s(z0), 0) -> c3 [1]
   <='(s(z0), s(z1)) -> c4(<='(z0, z1)) [1]
   IF(true, z0, z1) -> c5 [1]
   IF(false, z0, z1) -> c6 [1]
   PERFECTP(0) -> c7 [1]
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0))) [1]
   F(0, z0, 0, z1) -> c9 [1]
   F(0, z0, s(z1), z2) -> c10 [1]
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, minus(z1, s(z0)), z2), -'(z1, s(z0))) [1]
   F(s(z0), s(z1), z2, z3) -> c12(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1)) [1]
   F(s(z0), s(z1), z2, z3) -> c13(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), minus(z1, z0), z2, z3), -'(z1, z0)) [1]
   F(s(z0), s(z1), z2, z3) -> c14(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lteq(0, z0) -> true [0]
   lteq(s(z0), 0) -> false [0]
   lteq(s(z0), s(z1)) -> lteq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   perfectp(0) -> false [0]
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0)) [0]
   f(0, z0, 0, z1) -> true [0]
   f(0, z0, s(z1), z2) -> false [0]
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2) [0]
   f(s(z0), s(z1), z2, z3) -> if(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) [0]

The TRS has the following type information:
-' :: 0:s -> 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1 -> c:c1
<=' :: 0:s -> 0:s -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
IF :: true:false -> true:false -> true:false -> c5:c6
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c5:c6
PERFECTP :: 0:s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11:c12:c13:c14 -> c7:c8
F :: 0:s -> 0:s -> 0:s -> 0:s -> c9:c10:c11:c12:c13:c14
c9 :: c9:c10:c11:c12:c13:c14
c10 :: c9:c10:c11:c12:c13:c14
c11 :: c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
minus :: 0:s -> 0:s -> 0:s
c12 :: c5:c6 -> c2:c3:c4 -> c9:c10:c11:c12:c13:c14
lteq :: 0:s -> 0:s -> true:false
f :: 0:s -> 0:s -> 0:s -> 0:s -> true:false
c13 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
c14 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c9:c10:c11:c12:c13:c14
if :: true:false -> true:false -> true:false -> true:false
perfectp :: 0:s -> true:false

Rewrite Strategy: INNERMOST
----------------------------------------

(9) CompletionProof (UPPER BOUND(ID))
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:

   -'_2
   <='_2
   IF_3
   PERFECTP_1
   F_4

(c) The following functions are completely defined:

   minus_2
   lteq_2
   if_3
   perfectp_1
   f_4

Due to the following rules being added:

   minus(v0, v1) -> 0 [0]
   lteq(v0, v1) -> null_lteq [0]
   if(v0, v1, v2) -> null_if [0]
   perfectp(v0) -> null_perfectp [0]
   f(v0, v1, v2, v3) -> null_f [0]

And the following fresh constants:    null_lteq, null_if, null_perfectp, null_f

----------------------------------------

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

   -'(z0, 0) -> c [1]
   -'(s(z0), s(z1)) -> c1(-'(z0, z1)) [1]
   <='(0, z0) -> c2 [1]
   <='(s(z0), 0) -> c3 [1]
   <='(s(z0), s(z1)) -> c4(<='(z0, z1)) [1]
   IF(true, z0, z1) -> c5 [1]
   IF(false, z0, z1) -> c6 [1]
   PERFECTP(0) -> c7 [1]
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0))) [1]
   F(0, z0, 0, z1) -> c9 [1]
   F(0, z0, s(z1), z2) -> c10 [1]
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, minus(z1, s(z0)), z2), -'(z1, s(z0))) [1]
   F(s(z0), s(z1), z2, z3) -> c12(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1)) [1]
   F(s(z0), s(z1), z2, z3) -> c13(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), minus(z1, z0), z2, z3), -'(z1, z0)) [1]
   F(s(z0), s(z1), z2, z3) -> c14(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lteq(0, z0) -> true [0]
   lteq(s(z0), 0) -> false [0]
   lteq(s(z0), s(z1)) -> lteq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   perfectp(0) -> false [0]
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0)) [0]
   f(0, z0, 0, z1) -> true [0]
   f(0, z0, s(z1), z2) -> false [0]
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2) [0]
   f(s(z0), s(z1), z2, z3) -> if(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) [0]
   minus(v0, v1) -> 0 [0]
   lteq(v0, v1) -> null_lteq [0]
   if(v0, v1, v2) -> null_if [0]
   perfectp(v0) -> null_perfectp [0]
   f(v0, v1, v2, v3) -> null_f [0]

The TRS has the following type information:
-' :: 0:s -> 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1 -> c:c1
<=' :: 0:s -> 0:s -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
IF :: true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> c5:c6
true :: true:false:null_lteq:null_if:null_perfectp:null_f
c5 :: c5:c6
false :: true:false:null_lteq:null_if:null_perfectp:null_f
c6 :: c5:c6
PERFECTP :: 0:s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11:c12:c13:c14 -> c7:c8
F :: 0:s -> 0:s -> 0:s -> 0:s -> c9:c10:c11:c12:c13:c14
c9 :: c9:c10:c11:c12:c13:c14
c10 :: c9:c10:c11:c12:c13:c14
c11 :: c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
minus :: 0:s -> 0:s -> 0:s
c12 :: c5:c6 -> c2:c3:c4 -> c9:c10:c11:c12:c13:c14
lteq :: 0:s -> 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
f :: 0:s -> 0:s -> 0:s -> 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
c13 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
c14 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c9:c10:c11:c12:c13:c14
if :: true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f
perfectp :: 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
null_lteq :: true:false:null_lteq:null_if:null_perfectp:null_f
null_if :: true:false:null_lteq:null_if:null_perfectp:null_f
null_perfectp :: true:false:null_lteq:null_if:null_perfectp:null_f
null_f :: true:false:null_lteq:null_if:null_perfectp:null_f

Rewrite Strategy: INNERMOST
----------------------------------------

(11) NarrowingProof (BOTH BOUNDS(ID, ID))
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:

   -'(z0, 0) -> c [1]
   -'(s(z0), s(z1)) -> c1(-'(z0, z1)) [1]
   <='(0, z0) -> c2 [1]
   <='(s(z0), 0) -> c3 [1]
   <='(s(z0), s(z1)) -> c4(<='(z0, z1)) [1]
   IF(true, z0, z1) -> c5 [1]
   IF(false, z0, z1) -> c6 [1]
   PERFECTP(0) -> c7 [1]
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0))) [1]
   F(0, z0, 0, z1) -> c9 [1]
   F(0, z0, s(z1), z2) -> c10 [1]
   F(s(z0), 0, s(z0'), z2) -> c11(F(z0, z2, minus(z0', z0), z2), -'(s(z0'), s(z0))) [1]
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, 0, z2), -'(z1, s(z0))) [1]
   F(s(z0), s(z1), z2, z3) -> c12(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1)) [1]
   F(s(z0), s(z1), z2, z3) -> c13(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), minus(z1, z0), z2, z3), -'(z1, z0)) [1]
   F(s(z0), s(z1), z2, z3) -> c14(IF(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lteq(0, z0) -> true [0]
   lteq(s(z0), 0) -> false [0]
   lteq(s(z0), s(z1)) -> lteq(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   perfectp(0) -> false [0]
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0)) [0]
   f(0, z0, 0, z1) -> true [0]
   f(0, z0, s(z1), z2) -> false [0]
   f(s(z0), 0, s(z018), z2) -> f(z0, z2, minus(z018, z0), z2) [0]
   f(s(z0), 0, z1, z2) -> f(z0, z2, 0, z2) [0]
   f(s(z0), s(z1), z2, z3) -> if(lteq(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) [0]
   minus(v0, v1) -> 0 [0]
   lteq(v0, v1) -> null_lteq [0]
   if(v0, v1, v2) -> null_if [0]
   perfectp(v0) -> null_perfectp [0]
   f(v0, v1, v2, v3) -> null_f [0]

The TRS has the following type information:
-' :: 0:s -> 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1 -> c:c1
<=' :: 0:s -> 0:s -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
IF :: true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> c5:c6
true :: true:false:null_lteq:null_if:null_perfectp:null_f
c5 :: c5:c6
false :: true:false:null_lteq:null_if:null_perfectp:null_f
c6 :: c5:c6
PERFECTP :: 0:s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11:c12:c13:c14 -> c7:c8
F :: 0:s -> 0:s -> 0:s -> 0:s -> c9:c10:c11:c12:c13:c14
c9 :: c9:c10:c11:c12:c13:c14
c10 :: c9:c10:c11:c12:c13:c14
c11 :: c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
minus :: 0:s -> 0:s -> 0:s
c12 :: c5:c6 -> c2:c3:c4 -> c9:c10:c11:c12:c13:c14
lteq :: 0:s -> 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
f :: 0:s -> 0:s -> 0:s -> 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
c13 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c:c1 -> c9:c10:c11:c12:c13:c14
c14 :: c5:c6 -> c9:c10:c11:c12:c13:c14 -> c9:c10:c11:c12:c13:c14
if :: true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f -> true:false:null_lteq:null_if:null_perfectp:null_f
perfectp :: 0:s -> true:false:null_lteq:null_if:null_perfectp:null_f
null_lteq :: true:false:null_lteq:null_if:null_perfectp:null_f
null_if :: true:false:null_lteq:null_if:null_perfectp:null_f
null_perfectp :: true:false:null_lteq:null_if:null_perfectp:null_f
null_f :: true:false:null_lteq:null_if:null_perfectp:null_f

Rewrite Strategy: INNERMOST
----------------------------------------

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

   0 => 0
   c => 0
   c2 => 0
   c3 => 1
   true => 2
   c5 => 0
   false => 1
   c6 => 1
   c7 => 0
   c9 => 1
   c10 => 0
   null_lteq => 0
   null_if => 0
   null_perfectp => 0
   null_f => 0

----------------------------------------

(14)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   <='(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   <='(z, z') -{ 1 }-> 1 + <='(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z1 >= 0, z0 >= 0, z = 0, z4 = z1, z' = z0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z'' = 1 + z1, z = 0, z' = z0, z2 >= 0, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + F(z0, z3, z2, z3) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + <='(z0, z1) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z0, z2, minus(z0', z0), z2) + -'(1 + z0', 1 + z0) :|: z0' >= 0, z = 1 + z0, z0 >= 0, z'' = 1 + z0', z2 >= 0, z' = 0, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z0, z2, 0, z2) + -'(z1, 1 + z0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0, z'' = z1, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + F(1 + z0, minus(z1, z0), z2, z3) + -'(z1, z0) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z0, 1 + 0, 1 + z0, 1 + z0) :|: z = 1 + z0, z0 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z0, z2, minus(z018, z0), z2) :|: z = 1 + z0, z0 >= 0, z'' = 1 + z018, z018 >= 0, z2 >= 0, z' = 0, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> f(z0, z2, 0, z2) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0, z'' = z1, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z1 >= 0, z0 >= 0, z = 0, z4 = z1, z' = z0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z'' = 1 + z1, z = 0, z' = z0, z2 >= 0, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0
   if(z, z', z'') -{ 0 }-> z0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   lteq(z, z') -{ 0 }-> lteq(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lteq(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   lteq(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   perfectp(z) -{ 0 }-> f(z0, 1 + 0, 1 + z0, 1 + z0) :|: z = 1 + z0, z0 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


----------------------------------------

(15) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0

----------------------------------------

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   <='(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   <='(z, z') -{ 1 }-> 1 + <='(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z1 >= 0, z0 >= 0, z = 0, z4 = z1, z' = z0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z'' = 1 + z1, z = 0, z' = z0, z2 >= 0, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + F(z0, z3, z2, z3) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + <='(z0, z1) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z0, z2, minus(z0', z0), z2) + -'(1 + z0', 1 + z0) :|: z0' >= 0, z = 1 + z0, z0 >= 0, z'' = 1 + z0', z2 >= 0, z' = 0, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z0, z2, 0, z2) + -'(z1, 1 + z0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0, z'' = z1, z4 = z2
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) + F(1 + z0, minus(z1, z0), z2, z3) + -'(z1, z0) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z0, 1 + 0, 1 + z0, 1 + z0) :|: z = 1 + z0, z0 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z0, z1), f(1 + z0, minus(z1, z0), z2, z3), f(z0, z3, z2, z3)) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z4 = z3, z2 >= 0, z3 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z0, z2, minus(z018, z0), z2) :|: z = 1 + z0, z0 >= 0, z'' = 1 + z018, z018 >= 0, z2 >= 0, z' = 0, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> f(z0, z2, 0, z2) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z2 >= 0, z' = 0, z'' = z1, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z1 >= 0, z0 >= 0, z = 0, z4 = z1, z' = z0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z'' = 1 + z1, z = 0, z' = z0, z2 >= 0, z4 = z2
   f(z, z', z'', z4) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0
   if(z, z', z'') -{ 0 }-> z0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   lteq(z, z') -{ 0 }-> lteq(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lteq(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   lteq(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   perfectp(z) -{ 0 }-> f(z0, 1 + 0, 1 + z0, 1 + z0) :|: z = 1 + z0, z0 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


----------------------------------------

(17) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(18)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + -'(1 + (z'' - 1), 1 + (z - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, 0, z4) + -'(z'', 1 + (z - 1)) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + -'(z' - 1, z - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0


----------------------------------------

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { -' }
   { minus }
   { <=' }
   { IF }
   { lteq }
   { if }
   { f }
   { F }
   { perfectp }
   { PERFECTP }

----------------------------------------

(20)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + -'(1 + (z'' - 1), 1 + (z - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, 0, z4) + -'(z'', 1 + (z - 1)) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + -'(z' - 1, z - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {-'}, {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}

----------------------------------------

(21) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + -'(1 + (z'' - 1), 1 + (z - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, 0, z4) + -'(z'', 1 + (z - 1)) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + -'(z' - 1, z - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {-'}, {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}

----------------------------------------

(23) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + -'(1 + (z'' - 1), 1 + (z - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, 0, z4) + -'(z'', 1 + (z - 1)) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + -'(z' - 1, z - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {-'}, {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: ?, size: O(n^1) [z']

----------------------------------------

(25) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 }-> 1 + -'(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + -'(1 + (z'' - 1), 1 + (z - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + F(z - 1, z4, 0, z4) + -'(z'', 1 + (z - 1)) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + -'(z' - 1, z - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']

----------------------------------------

(27) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + s' :|: s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + s1 :|: s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']

----------------------------------------

(29) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + s' :|: s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + s1 :|: s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {minus}, {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: ?, size: O(n^1) [z]

----------------------------------------

(31) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, minus(z'' - 1, z - 1), z4) + s' :|: s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), minus(z' - 1, z - 1), z'', z4) + s1 :|: s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), minus(z' - 1, z - 1), z'', z4), f(z - 1, z4, z'', z4)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, minus(z'' - 1, z - 1), z4) :|: z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(33) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: <='
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {<='}, {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: ?, size: O(n^1) [z]

----------------------------------------

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: <='
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 2 + z'

----------------------------------------

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 1 }-> 1 + <='(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + <='(z - 1, z' - 1) :|: s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]

----------------------------------------

(39) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]

----------------------------------------

(41) IntTrsBoundProof (UPPER BOUND(ID))

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

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {IF}, {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: ?, size: O(1) [1]

----------------------------------------

(43) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(44)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]

----------------------------------------

(45) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(46)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]

----------------------------------------

(47) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(48)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {lteq}, {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: ?, size: O(1) [2]

----------------------------------------

(49) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(50)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(lteq(z - 1, z' - 1), f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(lteq(z - 1, z' - 1), f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> lteq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]

----------------------------------------

(51) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(52)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]

----------------------------------------

(53) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(54)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {if}, {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: ?, size: O(n^1) [z' + z'']

----------------------------------------

(55) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(56)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']

----------------------------------------

(57) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(58)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']

----------------------------------------

(59) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: f
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?

----------------------------------------

(60)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}, {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: ?, size: EXP

----------------------------------------

(61) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(62)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z' }-> 1 + IF(s13, f(1 + (z - 1), s5, z'', z4), f(z - 1, z4, z'', z4)) + s11 :|: s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 + IF(s15, f(1 + (z - 1), s8, z'', z4), f(z - 1, z4, z'', z4)) + F(z - 1, z4, z'', z4) :|: s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 1 + z }-> 1 + IF(s14, f(1 + (z - 1), s6, z'', z4), f(z - 1, z4, z'', z4)) + F(1 + (z - 1), s7, z'', z4) + s1 :|: s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> if(s16, f(1 + (z - 1), s9, z'', z4), f(z - 1, z4, z'', z4)) :|: s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, s4, z4) :|: s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> f(z - 1, z4, 0, z4) :|: z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> f(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP

----------------------------------------

(63) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(64)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 }-> 1 + s28 + F(z - 1, z4, z'', z4) :|: s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + s25 + F(1 + (z - 1), s7, z'', z4) + s1 :|: s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP

----------------------------------------

(65) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: F
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z'

----------------------------------------

(66)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 }-> 1 + s28 + F(z - 1, z4, z'', z4) :|: s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + s25 + F(1 + (z - 1), s7, z'', z4) + s1 :|: s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {F}, {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: ?, size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']

----------------------------------------

(67) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: F
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4

----------------------------------------

(68)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 }-> 1 + s28 + F(z - 1, z4, z'', z4) :|: s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, s2, z4) + s' :|: s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + F(z - 1, z4, 0, z4) + s'' :|: s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 2 + z }-> 1 + s25 + F(1 + (z - 1), s7, z'', z4) + s1 :|: s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 1 }-> 1 + F(z - 1, 1 + 0, 1 + (z - 1), 1 + (z - 1)) :|: z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']

----------------------------------------

(69) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(70)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']

----------------------------------------

(71) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: perfectp
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

----------------------------------------

(72)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {perfectp}, {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']
  perfectp: runtime: ?, size: INF

----------------------------------------

(73) IntTrsBoundProof (UPPER BOUND(ID))

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

----------------------------------------

(74)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']
  perfectp: runtime: O(1) [0], size: INF

----------------------------------------

(75) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(76)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']
  perfectp: runtime: O(1) [0], size: INF

----------------------------------------

(77) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: PERFECTP
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 2 + z + 2*z^2 + 3*z^3

----------------------------------------

(78)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {PERFECTP}
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']
  perfectp: runtime: O(1) [0], size: INF
  PERFECTP: runtime: ?, size: O(n^3) [2 + z + 2*z^2 + 3*z^3]

----------------------------------------

(79) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: PERFECTP
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 5 + 7*z + 4*z^2 + z^3

----------------------------------------

(80)
Obligation:
Complexity RNTS consisting of the following rules:

   -'(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   -'(z, z') -{ 1 + z' }-> 1 + s :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z - 1 >= 0
   <='(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0
   <='(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   <='(z, z') -{ 2 + z' }-> 1 + s10 :|: s10 >= 0, s10 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   F(z, z', z'', z4) -{ 1 }-> 1 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   F(z, z', z'', z4) -{ 1 }-> 0 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + z' }-> 1 + s22 + s11 :|: s20 >= 0, s20 <= inf1, s21 >= 0, s21 <= inf2, s22 >= 0, s22 <= 1, s13 >= 0, s13 <= 2, s11 >= 0, s11 <= z - 1, s5 >= 0, s5 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 5*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s28 + s36 :|: s36 >= 0, s36 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s26 >= 0, s26 <= inf5, s27 >= 0, s27 <= inf6, s28 >= 0, s28 <= 1, s15 >= 0, s15 <= 2, s8 >= 0, s8 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s33 + s' :|: s33 >= 0, s33 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s2 >= 0, s2 <= z'' - 1, s' >= 0, s' <= 1 + (z - 1), z'' - 1 >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 3 + 6*z + 2*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s34 + s'' :|: s34 >= 0, s34 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + z4 * (z - 1) + 3 * (z4 * ((z - 1) * (z - 1))) + 2 * z4 + 6 * (z4 * (z - 1)) + 3, s'' >= 0, s'' <= 1 + (z - 1), z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   F(z, z', z'', z4) -{ 11 + 3*s7 + s7*z + 12*z + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z4 }-> 1 + s25 + s35 + s1 :|: s35 >= 0, s35 <= 2 * ((1 + (z - 1)) * (1 + (z - 1))) + 5 * (1 + (z - 1)) + s7 * (1 + (z - 1)) + 3 * (z4 * ((1 + (z - 1)) * (1 + (z - 1)))) + 2 * s7 + 6 * (z4 * (1 + (z - 1))) + 3, s23 >= 0, s23 <= inf3, s24 >= 0, s24 <= inf4, s25 >= 0, s25 <= 1, s14 >= 0, s14 <= 2, s6 >= 0, s6 <= z' - 1, s7 >= 0, s7 <= z' - 1, s1 >= 0, s1 <= z - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   IF(z, z', z'') -{ 1 }-> 1 :|: z'' >= 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z'' >= 0, z' >= 0
   PERFECTP(z) -{ 1 }-> 0 :|: z = 0
   PERFECTP(z) -{ 4 + 7*z + 4*z^2 + z^3 }-> 1 + s32 :|: s32 >= 0, s32 <= 2 * ((z - 1) * (z - 1)) + 5 * (z - 1) + (1 + 0) * (z - 1) + 3 * ((1 + (z - 1)) * ((z - 1) * (z - 1))) + 2 * (1 + 0) + 6 * ((1 + (z - 1)) * (z - 1)) + 3, z - 1 >= 0
   f(z, z', z'', z4) -{ 0 }-> s18 :|: s18 >= 0, s18 <= inf', s4 >= 0, s4 <= z'' - 1, z - 1 >= 0, z'' - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s19 :|: s19 >= 0, s19 <= inf'', z'' >= 0, z - 1 >= 0, z4 >= 0, z' = 0
   f(z, z', z'', z4) -{ 0 }-> s31 :|: s29 >= 0, s29 <= inf7, s30 >= 0, s30 <= inf8, s31 >= 0, s31 <= s30 + s29, s16 >= 0, s16 <= 2, s9 >= 0, s9 <= z' - 1, z' - 1 >= 0, z - 1 >= 0, z'' >= 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 2 :|: z'' = 0, z4 >= 0, z' >= 0, z = 0
   f(z, z', z'', z4) -{ 0 }-> 1 :|: z'' - 1 >= 0, z' >= 0, z = 0, z4 >= 0
   f(z, z', z'', z4) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z4 >= 0
   if(z, z', z'') -{ 0 }-> z' :|: z = 2, z'' >= 0, z' >= 0
   if(z, z', z'') -{ 0 }-> z'' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   lteq(z, z') -{ 0 }-> s12 :|: s12 >= 0, s12 <= 2, z' - 1 >= 0, z - 1 >= 0
   lteq(z, z') -{ 0 }-> 2 :|: z' >= 0, z = 0
   lteq(z, z') -{ 0 }-> 1 :|: z - 1 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   minus(z, z') -{ 0 }-> s3 :|: s3 >= 0, s3 <= z - 1, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   perfectp(z) -{ 0 }-> s17 :|: s17 >= 0, s17 <= inf, z - 1 >= 0
   perfectp(z) -{ 0 }-> 1 :|: z = 0
   perfectp(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  -': runtime: O(n^1) [1 + z'], size: O(n^1) [z']
  minus: runtime: O(1) [0], size: O(n^1) [z]
  <=': runtime: O(n^1) [2 + z'], size: O(n^1) [z]
  IF: runtime: O(1) [1], size: O(1) [1]
  lteq: runtime: O(1) [0], size: O(1) [2]
  if: runtime: O(1) [0], size: O(n^1) [z' + z'']
  f: runtime: O(1) [0], size: EXP
  F: runtime: O(n^3) [9 + 11*z + z*z' + 3*z*z4 + 3*z^2 + z^2*z4 + 3*z' + 3*z4], size: O(n^3) [3 + 5*z + z*z' + 6*z*z4 + 2*z^2 + 3*z^2*z4 + 2*z']
  perfectp: runtime: O(1) [0], size: INF
  PERFECTP: runtime: O(n^3) [5 + 7*z + 4*z^2 + z^3], size: O(n^3) [2 + z + 2*z^2 + 3*z^3]

----------------------------------------

(81) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(82)
BOUNDS(1, n^3)

----------------------------------------

(83) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(84)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   <='(0, z0) -> c2
   <='(s(z0), 0) -> c3
   <='(s(z0), s(z1)) -> c4(<='(z0, z1))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6
   PERFECTP(0) -> c7
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c9
   F(0, z0, s(z1), z2) -> c10
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0)))
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1))
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0))
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3))

The (relative) TRS S consists of the following rules:

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   <=(0, z0) -> true
   <=(s(z0), 0) -> false
   <=(s(z0), s(z1)) -> <=(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST
----------------------------------------

(85) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

-'(s(z0), s(z1)) ->^+ c1(-'(z0, z1))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z0 / s(z0), z1 / s(z1)].

The result substitution is [ ].




----------------------------------------

(86)
Complex Obligation (BEST)

----------------------------------------

(87)
Obligation:
Proved the lower bound n^1 for the following obligation:

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   <='(0, z0) -> c2
   <='(s(z0), 0) -> c3
   <='(s(z0), s(z1)) -> c4(<='(z0, z1))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6
   PERFECTP(0) -> c7
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c9
   F(0, z0, s(z1), z2) -> c10
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0)))
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1))
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0))
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3))

The (relative) TRS S consists of the following rules:

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   <=(0, z0) -> true
   <=(s(z0), 0) -> false
   <=(s(z0), s(z1)) -> <=(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST
----------------------------------------

(88) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(89)
BOUNDS(n^1, INF)

----------------------------------------

(90)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   <='(0, z0) -> c2
   <='(s(z0), 0) -> c3
   <='(s(z0), s(z1)) -> c4(<='(z0, z1))
   IF(true, z0, z1) -> c5
   IF(false, z0, z1) -> c6
   PERFECTP(0) -> c7
   PERFECTP(s(z0)) -> c8(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c9
   F(0, z0, s(z1), z2) -> c10
   F(s(z0), 0, z1, z2) -> c11(F(z0, z2, -(z1, s(z0)), z2), -'(z1, s(z0)))
   F(s(z0), s(z1), z2, z3) -> c12(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), <='(z0, z1))
   F(s(z0), s(z1), z2, z3) -> c13(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(s(z0), -(z1, z0), z2, z3), -'(z1, z0))
   F(s(z0), s(z1), z2, z3) -> c14(IF(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3)), F(z0, z3, z2, z3))

The (relative) TRS S consists of the following rules:

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   <=(0, z0) -> true
   <=(s(z0), 0) -> false
   <=(s(z0), s(z1)) -> <=(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, -(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(<=(z0, z1), f(s(z0), -(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST