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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 126 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
(5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CdtProblem
(11) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxTRS
(13) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxWeightedTrs
(15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CpxTypedWeightedTrs
(17) CompletionProof [UPPER BOUND(ID), 0 ms]
(18) CpxTypedWeightedCompleteTrs
(19) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CpxTypedWeightedCompleteTrs
(21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(22) CpxRNTS
(23) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CpxRNTS
(25) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(26) CpxRNTS
(27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(28) CpxRNTS
(29) IntTrsBoundProof [UPPER BOUND(ID), 304 ms]
(30) CpxRNTS
(31) IntTrsBoundProof [UPPER BOUND(ID), 76 ms]
(32) CpxRNTS
(33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(34) CpxRNTS
(35) IntTrsBoundProof [UPPER BOUND(ID), 231 ms]
(36) CpxRNTS
(37) IntTrsBoundProof [UPPER BOUND(ID), 115 ms]
(38) CpxRNTS
(39) FinalProof [FINISHED, 0 ms]
(40) BOUNDS(1, n^1)


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

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


The TRS R consists of the following rules:

   a(C(x1, x2), y, z) -> C(a(x1, y, z), a(x2, y, y))
   a(Z, y, z) -> Z
   eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2))
   eqZList(C(x1, x2), Z) -> False
   eqZList(Z, C(y1, y2)) -> False
   eqZList(Z, Z) -> True
   second(C(x1, x2)) -> x2
   first(C(x1, x2)) -> x1

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

   a(C(x1, x2), y, z) -> C(a(x1, y, z), a(x2, y, y))
   a(Z, y, z) -> Z
   eqZList(C(x1, x2), C(y1, y2)) -> and(eqZList(x1, y1), eqZList(x2, y2))
   eqZList(C(x1, x2), Z) -> False
   eqZList(Z, C(y1, y2)) -> False
   eqZList(Z, Z) -> True
   second(C(x1, x2)) -> x2
   first(C(x1, x2)) -> x1

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   a(C(z0, z1), z2, z3) -> C(a(z0, z2, z3), a(z1, z2, z2))
   a(Z, z0, z1) -> Z
   eqZList(C(z0, z1), C(z2, z3)) -> and(eqZList(z0, z2), eqZList(z1, z3))
   eqZList(C(z0, z1), Z) -> False
   eqZList(Z, C(z0, z1)) -> False
   eqZList(Z, Z) -> True
   second(C(z0, z1)) -> z1
   first(C(z0, z1)) -> z0
Tuples:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   A(Z, z0, z1) -> c6
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z1, z3))
   EQZLIST(C(z0, z1), Z) -> c9
   EQZLIST(Z, C(z0, z1)) -> c10
   EQZLIST(Z, Z) -> c11
   SECOND(C(z0, z1)) -> c12
   FIRST(C(z0, z1)) -> c13
S tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   A(Z, z0, z1) -> c6
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z1, z3))
   EQZLIST(C(z0, z1), Z) -> c9
   EQZLIST(Z, C(z0, z1)) -> c10
   EQZLIST(Z, Z) -> c11
   SECOND(C(z0, z1)) -> c12
   FIRST(C(z0, z1)) -> c13
K tuples:none
Defined Rule Symbols:   a_3, eqZList_2, second_1, first_1, and_2

Defined Pair Symbols:   AND_2, A_3, EQZLIST_2, SECOND_1, FIRST_1

Compound Symbols:   c, c1, c2, c3, c4_1, c5_1, c6, c7_2, c8_2, c9, c10, c11, c12, c13


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 10 trailing nodes:
   EQZLIST(Z, C(z0, z1)) -> c10
   FIRST(C(z0, z1)) -> c13
   EQZLIST(Z, Z) -> c11
   AND(False, True) -> c2
   AND(False, False) -> c
   EQZLIST(C(z0, z1), Z) -> c9
   A(Z, z0, z1) -> c6
   AND(True, True) -> c3
   SECOND(C(z0, z1)) -> c12
   AND(True, False) -> c1

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   a(C(z0, z1), z2, z3) -> C(a(z0, z2, z3), a(z1, z2, z2))
   a(Z, z0, z1) -> Z
   eqZList(C(z0, z1), C(z2, z3)) -> and(eqZList(z0, z2), eqZList(z1, z3))
   eqZList(C(z0, z1), Z) -> False
   eqZList(Z, C(z0, z1)) -> False
   eqZList(Z, Z) -> True
   second(C(z0, z1)) -> z1
   first(C(z0, z1)) -> z0
Tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z1, z3))
S tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:   a_3, eqZList_2, second_1, first_1, and_2

Defined Pair Symbols:   A_3, EQZLIST_2

Compound Symbols:   c4_1, c5_1, c7_2, c8_2


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

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   a(C(z0, z1), z2, z3) -> C(a(z0, z2, z3), a(z1, z2, z2))
   a(Z, z0, z1) -> Z
   eqZList(C(z0, z1), C(z2, z3)) -> and(eqZList(z0, z2), eqZList(z1, z3))
   eqZList(C(z0, z1), Z) -> False
   eqZList(Z, C(z0, z1)) -> False
   eqZList(Z, Z) -> True
   second(C(z0, z1)) -> z1
   first(C(z0, z1)) -> z0
Tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3))
S tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:   a_3, eqZList_2, second_1, first_1, and_2

Defined Pair Symbols:   A_3, EQZLIST_2

Compound Symbols:   c4_1, c5_1, c7_1, c8_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   a(C(z0, z1), z2, z3) -> C(a(z0, z2, z3), a(z1, z2, z2))
   a(Z, z0, z1) -> Z
   eqZList(C(z0, z1), C(z2, z3)) -> and(eqZList(z0, z2), eqZList(z1, z3))
   eqZList(C(z0, z1), Z) -> False
   eqZList(Z, C(z0, z1)) -> False
   eqZList(Z, Z) -> True
   second(C(z0, z1)) -> z1
   first(C(z0, z1)) -> z0

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3))
S tuples:
   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   A_3, EQZLIST_2

Compound Symbols:   c4_1, c5_1, c7_1, c8_1


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

(11) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3))
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2))
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3))

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

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

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


The TRS R consists of the following rules:

   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3)) [1]
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3)) [1]

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

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

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

   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3)) [1]
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3)) [1]

The TRS has the following type information:
A :: C -> a -> a -> c4:c5
C :: C -> C -> C
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5 -> c4:c5
EQZLIST :: C -> C -> c7:c8
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8 -> c7:c8

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

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

   A_3
   EQZLIST_2

(c) The following functions are completely defined:
none

Due to the following rules being added:
none

And the following fresh constants:    const, const1, const2, const3

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

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

   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3)) [1]
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3)) [1]

The TRS has the following type information:
A :: C -> a -> a -> c4:c5
C :: C -> C -> C
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5 -> c4:c5
EQZLIST :: C -> C -> c7:c8
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8 -> c7:c8
const :: c4:c5
const1 :: C
const2 :: a
const3 :: c7:c8

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

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

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

   A(C(z0, z1), z2, z3) -> c4(A(z0, z2, z3)) [1]
   A(C(z0, z1), z2, z3) -> c5(A(z1, z2, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c7(EQZLIST(z0, z2)) [1]
   EQZLIST(C(z0, z1), C(z2, z3)) -> c8(EQZLIST(z1, z3)) [1]

The TRS has the following type information:
A :: C -> a -> a -> c4:c5
C :: C -> C -> C
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5 -> c4:c5
EQZLIST :: C -> C -> c7:c8
c7 :: c7:c8 -> c7:c8
c8 :: c7:c8 -> c7:c8
const :: c4:c5
const1 :: C
const2 :: a
const3 :: c7:c8

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

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

   const => 0
   const1 => 0
   const2 => 0
   const3 => 0

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z2, z3) :|: z1 >= 0, z' = z2, z0 >= 0, z'' = z3, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z2, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z'' = z3, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0


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

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0


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

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

   { EQZLIST }
   { A }

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {EQZLIST}, {A}

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {EQZLIST}, {A}

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {EQZLIST}, {A}
Previous analysis results are:
  EQZLIST: runtime: ?, size: O(1) [0]

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 }-> 1 + EQZLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {A}
Previous analysis results are:
  EQZLIST: runtime: O(n^1) [z'], size: O(1) [0]

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 + z2 }-> 1 + s :|: s >= 0, s <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 + z3 }-> 1 + s' :|: s' >= 0, s' <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {A}
Previous analysis results are:
  EQZLIST: runtime: O(n^1) [z'], size: O(1) [0]

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 + z2 }-> 1 + s :|: s >= 0, s <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 + z3 }-> 1 + s' :|: s' >= 0, s' <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: {A}
Previous analysis results are:
  EQZLIST: runtime: O(n^1) [z'], size: O(1) [0]
  A: runtime: ?, size: O(1) [0]

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   A(z, z', z'') -{ 1 }-> 1 + A(z0, z', z'') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   A(z, z', z'') -{ 1 }-> 1 + A(z1, z', z') :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' >= 0, z'' >= 0
   EQZLIST(z, z') -{ 1 + z2 }-> 1 + s :|: s >= 0, s <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   EQZLIST(z, z') -{ 1 + z3 }-> 1 + s' :|: s' >= 0, s' <= 0, z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  EQZLIST: runtime: O(n^1) [z'], size: O(1) [0]
  A: runtime: O(n^1) [z], size: O(1) [0]

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

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

(40)
BOUNDS(1, n^1)