WORST_CASE(?,O(n^2))
proof of input_n2d1NVwynU.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxWeightedTrs
(3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxTypedWeightedTrs
(5) CompletionProof [UPPER BOUND(ID), 0 ms]
(6) CpxTypedWeightedCompleteTrs
(7) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxTypedWeightedCompleteTrs
(9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(10) CpxRNTS
(11) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxRNTS
(13) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRNTS
(15) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(16) CpxRNTS
(17) IntTrsBoundProof [UPPER BOUND(ID), 318 ms]
(18) CpxRNTS
(19) IntTrsBoundProof [UPPER BOUND(ID), 131 ms]
(20) CpxRNTS
(21) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(22) CpxRNTS
(23) IntTrsBoundProof [UPPER BOUND(ID), 122 ms]
(24) CpxRNTS
(25) IntTrsBoundProof [UPPER BOUND(ID), 46 ms]
(26) CpxRNTS
(27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(28) CpxRNTS
(29) IntTrsBoundProof [UPPER BOUND(ID), 139 ms]
(30) CpxRNTS
(31) IntTrsBoundProof [UPPER BOUND(ID), 44 ms]
(32) CpxRNTS
(33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(34) CpxRNTS
(35) IntTrsBoundProof [UPPER BOUND(ID), 129 ms]
(36) CpxRNTS
(37) IntTrsBoundProof [UPPER BOUND(ID), 45 ms]
(38) CpxRNTS
(39) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(40) CpxRNTS
(41) IntTrsBoundProof [UPPER BOUND(ID), 275 ms]
(42) CpxRNTS
(43) IntTrsBoundProof [UPPER BOUND(ID), 137 ms]
(44) CpxRNTS
(45) FinalProof [FINISHED, 0 ms]
(46) BOUNDS(1, n^2)


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

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

   rev(nil) -> nil
   rev(.(x, y)) -> ++(rev(y), .(x, nil))
   car(.(x, y)) -> x
   cdr(.(x, y)) -> y
   null(nil) -> true
   null(.(x, y)) -> false
   ++(nil, y) -> y
   ++(.(x, y), z) -> .(x, ++(y, z))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   rev(nil) -> nil [1]
   rev(.(x, y)) -> ++(rev(y), .(x, nil)) [1]
   car(.(x, y)) -> x [1]
   cdr(.(x, y)) -> y [1]
   null(nil) -> true [1]
   null(.(x, y)) -> false [1]
   ++(nil, y) -> y [1]
   ++(.(x, y), z) -> .(x, ++(y, z)) [1]

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

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

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

   rev(nil) -> nil [1]
   rev(.(x, y)) -> ++(rev(y), .(x, nil)) [1]
   car(.(x, y)) -> x [1]
   cdr(.(x, y)) -> y [1]
   null(nil) -> true [1]
   null(.(x, y)) -> false [1]
   ++(nil, y) -> y [1]
   ++(.(x, y), z) -> .(x, ++(y, z)) [1]

The TRS has the following type information:
rev :: nil:. -> nil:.
nil :: nil:.
. :: car -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false

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

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

   car_1
   cdr_1
   null_1

(c) The following functions are completely defined:

   rev_1
   ++_2

Due to the following rules being added:
none

And the following fresh constants:    const

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

(6)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

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

   rev(nil) -> nil [1]
   rev(.(x, y)) -> ++(rev(y), .(x, nil)) [1]
   car(.(x, y)) -> x [1]
   cdr(.(x, y)) -> y [1]
   null(nil) -> true [1]
   null(.(x, y)) -> false [1]
   ++(nil, y) -> y [1]
   ++(.(x, y), z) -> .(x, ++(y, z)) [1]

The TRS has the following type information:
rev :: nil:. -> nil:.
nil :: nil:.
. :: car -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
const :: car

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

(7) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(8)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

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

   rev(nil) -> nil [1]
   rev(.(x, nil)) -> ++(nil, .(x, nil)) [2]
   rev(.(x, .(x', y'))) -> ++(++(rev(y'), .(x', nil)), .(x, nil)) [2]
   car(.(x, y)) -> x [1]
   cdr(.(x, y)) -> y [1]
   null(nil) -> true [1]
   null(.(x, y)) -> false [1]
   ++(nil, y) -> y [1]
   ++(.(x, y), z) -> .(x, ++(y, z)) [1]

The TRS has the following type information:
rev :: nil:. -> nil:.
nil :: nil:.
. :: car -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
car :: nil:. -> car
cdr :: nil:. -> nil:.
null :: nil:. -> true:false
true :: true:false
false :: true:false
const :: car

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

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

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

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

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

   ++(z', z'') -{ 1 }-> y :|: z'' = y, y >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z) :|: z'' = z, z >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + x + 0) :|: x >= 0, z' = 1 + x + 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0


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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0


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

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

   { ++ }
   { null }
   { cdr }
   { car }
   { rev }

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {++}, {null}, {cdr}, {car}, {rev}

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {++}, {null}, {cdr}, {car}, {rev}

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

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {++}, {null}, {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: ?, size: O(n^1) [z' + z'']

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

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 1 }-> 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(0, 1 + (z' - 1) + 0) :|: z' - 1 >= 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {null}, {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']

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

(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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {null}, {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']

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

(23) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {null}, {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: ?, size: O(1) [1]

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

(25) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]

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

(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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: cdr
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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {cdr}, {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: ?, size: O(n^1) [z']

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], 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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: car
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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {car}, {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']
  car: runtime: ?, size: O(n^1) [z']

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']
  car: runtime: O(1) [1], 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 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']
  car: runtime: O(1) [1], size: O(n^1) [z']

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

(41) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: {rev}
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']
  car: runtime: O(1) [1], size: O(n^1) [z']
  rev: runtime: ?, size: O(n^1) [z']

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

(43) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   ++(z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' = 0
   ++(z', z'') -{ 2 + y }-> 1 + x + s' :|: s' >= 0, s' <= y + z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
   car(z') -{ 1 }-> x :|: z' = 1 + x + y, x >= 0, y >= 0
   cdr(z') -{ 1 }-> y :|: z' = 1 + x + y, x >= 0, y >= 0
   null(z') -{ 1 }-> 1 :|: z' = 0
   null(z') -{ 1 }-> 0 :|: z' = 1 + x + y, x >= 0, y >= 0
   rev(z') -{ 3 }-> s :|: s >= 0, s <= 0 + (1 + (z' - 1) + 0), z' - 1 >= 0
   rev(z') -{ 1 }-> 0 :|: z' = 0
   rev(z') -{ 2 }-> ++(++(rev(y'), 1 + x' + 0), 1 + x + 0) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  ++: runtime: O(n^1) [1 + z'], size: O(n^1) [z' + z'']
  null: runtime: O(1) [1], size: O(1) [1]
  cdr: runtime: O(1) [1], size: O(n^1) [z']
  car: runtime: O(1) [1], size: O(n^1) [z']
  rev: runtime: O(n^2) [4 + 3*z' + 2*z'^2], size: O(n^1) [z']

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

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

(46)
BOUNDS(1, n^2)