KILLED
proof of input_FgJxE2nIET.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CpxTRS
(3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(4) CpxTRS
(5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(6) CpxWeightedTrs
    (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTypedWeightedTrs
    (9) CompletionProof [UPPER BOUND(ID), 0 ms]
    (10) CpxTypedWeightedCompleteTrs
        (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (12) CpxTypedWeightedCompleteTrs
        (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (14) CpxRNTS
        (15) SimplificationProof [BOTH BOUNDS(ID, ID), 2 ms]
        (16) CpxRNTS
        (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (18) CpxRNTS
        (19) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (20) CpxRNTS
        (21) IntTrsBoundProof [UPPER BOUND(ID), 559 ms]
        (22) CpxRNTS
        (23) IntTrsBoundProof [UPPER BOUND(ID), 175 ms]
        (24) CpxRNTS
        (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (26) CpxRNTS
        (27) IntTrsBoundProof [UPPER BOUND(ID), 133 ms]
        (28) CpxRNTS
        (29) IntTrsBoundProof [UPPER BOUND(ID), 56 ms]
        (30) CpxRNTS
        (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (32) CpxRNTS
        (33) IntTrsBoundProof [UPPER BOUND(ID), 137 ms]
        (34) CpxRNTS
        (35) IntTrsBoundProof [UPPER BOUND(ID), 12 ms]
        (36) CpxRNTS
    (37) CompletionProof [UPPER BOUND(ID), 0 ms]
    (38) CpxTypedWeightedCompleteTrs
        (39) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (40) CpxRNTS
(41) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(42) CdtProblem
    (43) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (44) CdtProblem
    (45) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (46) CdtProblem
    (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (48) CdtProblem
    (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (50) CdtProblem
    (51) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (52) CdtProblem
    (53) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (54) CdtProblem
    (55) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (56) CdtProblem
    (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (58) CdtProblem


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

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


The TRS R consists of the following rules:

   nats -> cons(0, n__incr(nats))
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS)))
   head(cons(X, XS)) -> X
   tail(cons(X, XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   activate(n__incr(X)) -> incr(X)
   activate(X) -> X

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

(1) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   nats -> cons(0', n__incr(nats))
   pairs -> cons(0', n__incr(odds))
   odds -> incr(pairs)
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS)))
   head(cons(X, XS)) -> X
   tail(cons(X, XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   activate(n__incr(X)) -> incr(X)
   activate(X) -> X

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

(3) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(4)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   nats -> cons(0, n__incr(nats))
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS)))
   head(cons(X, XS)) -> X
   tail(cons(X, XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   activate(n__incr(X)) -> incr(X)
   activate(X) -> X

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

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

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


The TRS R consists of the following rules:

   nats -> cons(0, n__incr(nats)) [1]
   pairs -> cons(0, n__incr(odds)) [1]
   odds -> incr(pairs) [1]
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) [1]
   head(cons(X, XS)) -> X [1]
   tail(cons(X, XS)) -> activate(XS) [1]
   incr(X) -> n__incr(X) [1]
   activate(n__incr(X)) -> incr(X) [1]
   activate(X) -> X [1]

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:

   nats -> cons(0, n__incr(nats)) [1]
   pairs -> cons(0, n__incr(odds)) [1]
   odds -> incr(pairs) [1]
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) [1]
   head(cons(X, XS)) -> X [1]
   tail(cons(X, XS)) -> activate(XS) [1]
   incr(X) -> n__incr(X) [1]
   activate(n__incr(X)) -> incr(X) [1]
   activate(X) -> X [1]

The TRS has the following type information:
nats :: n__incr:cons
cons :: 0:s -> n__incr:cons -> n__incr:cons
0 :: 0:s
n__incr :: n__incr:cons -> n__incr:cons
pairs :: n__incr:cons
odds :: n__incr:cons
incr :: n__incr:cons -> n__incr:cons
s :: 0:s -> 0:s
activate :: n__incr:cons -> n__incr:cons
head :: n__incr:cons -> 0:s
tail :: n__incr:cons -> n__incr:cons

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:

   nats
   head_1
   tail_1

(c) The following functions are completely defined:

   pairs
   odds
   incr_1
   activate_1

Due to the following rules being added:
none

And the following fresh constants:    const

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

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

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

   nats -> cons(0, n__incr(nats)) [1]
   pairs -> cons(0, n__incr(odds)) [1]
   odds -> incr(pairs) [1]
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) [1]
   head(cons(X, XS)) -> X [1]
   tail(cons(X, XS)) -> activate(XS) [1]
   incr(X) -> n__incr(X) [1]
   activate(n__incr(X)) -> incr(X) [1]
   activate(X) -> X [1]

The TRS has the following type information:
nats :: n__incr:cons
cons :: 0:s -> n__incr:cons -> n__incr:cons
0 :: 0:s
n__incr :: n__incr:cons -> n__incr:cons
pairs :: n__incr:cons
odds :: n__incr:cons
incr :: n__incr:cons -> n__incr:cons
s :: 0:s -> 0:s
activate :: n__incr:cons -> n__incr:cons
head :: n__incr:cons -> 0:s
tail :: n__incr:cons -> n__incr:cons
const :: n__incr:cons

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:

   nats -> cons(0, n__incr(nats)) [1]
   pairs -> cons(0, n__incr(odds)) [1]
   odds -> incr(cons(0, n__incr(odds))) [2]
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) [1]
   head(cons(X, XS)) -> X [1]
   tail(cons(X, XS)) -> activate(XS) [1]
   incr(X) -> n__incr(X) [1]
   activate(n__incr(X)) -> incr(X) [1]
   activate(X) -> X [1]

The TRS has the following type information:
nats :: n__incr:cons
cons :: 0:s -> n__incr:cons -> n__incr:cons
0 :: 0:s
n__incr :: n__incr:cons -> n__incr:cons
pairs :: n__incr:cons
odds :: n__incr:cons
incr :: n__incr:cons -> n__incr:cons
s :: 0:s -> 0:s
activate :: n__incr:cons -> n__incr:cons
head :: n__incr:cons -> 0:s
tail :: n__incr:cons -> n__incr:cons
const :: n__incr:cons

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
   const => 0

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

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

   activate(z) -{ 1 }-> X :|: X >= 0, z = X
   activate(z) -{ 1 }-> incr(X) :|: z = 1 + X, X >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + X :|: X >= 0, z = X
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0


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

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

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

   activate(z) -{ 1 }-> z :|: z >= 0
   activate(z) -{ 1 }-> incr(z - 1) :|: z - 1 >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0


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

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

   { activate, incr }
   { head }
   { nats }
   { odds }
   { tail }
   { pairs }

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

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

   activate(z) -{ 1 }-> z :|: z >= 0
   activate(z) -{ 1 }-> incr(z - 1) :|: z - 1 >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {activate,incr}, {head}, {nats}, {odds}, {tail}, {pairs}

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

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

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

   activate(z) -{ 1 }-> z :|: z >= 0
   activate(z) -{ 1 }-> incr(z - 1) :|: z - 1 >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {activate,incr}, {head}, {nats}, {odds}, {tail}, {pairs}

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

(21) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   activate(z) -{ 1 }-> z :|: z >= 0
   activate(z) -{ 1 }-> incr(z - 1) :|: z - 1 >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {activate,incr}, {head}, {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: ?, size: O(n^1) [3*z]
  incr: runtime: ?, size: O(n^1) [1 + 3*z]

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

(23) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   activate(z) -{ 1 }-> z :|: z >= 0
   activate(z) -{ 1 }-> incr(z - 1) :|: z - 1 >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {head}, {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {head}, {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]

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

(27) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {head}, {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]
  head: runtime: ?, size: O(n^1) [z]

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]
  head: runtime: O(1) [1], size: O(n^1) [z]

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]
  head: runtime: O(1) [1], size: O(n^1) [z]

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

(33) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]
  head: runtime: O(1) [1], size: O(n^1) [z]
  nats: runtime: ?, size: O(1) [0]

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   activate(z) -{ 2*z }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 1 }-> z :|: z >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   incr(z) -{ 1 }-> 1 + z :|: z >= 0
   incr(z) -{ 3 + 2*XS }-> 1 + (1 + X) + (1 + s) :|: s >= 0, s <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 2 }-> incr(1 + 0 + (1 + odds)) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 3 + 2*XS }-> s' :|: s' >= 0, s' <= 3 * XS, z = 1 + X + XS, X >= 0, XS >= 0

Function symbols to be analyzed: {nats}, {odds}, {tail}, {pairs}
Previous analysis results are:
  activate: runtime: O(n^1) [2 + 2*z], size: O(n^1) [3*z]
  incr: runtime: O(n^1) [1 + 2*z], size: O(n^1) [1 + 3*z]
  head: runtime: O(1) [1], size: O(n^1) [z]
  nats: runtime: INF, size: O(1) [0]

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

(37) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   head(v0) -> null_head [0]
   tail(v0) -> null_tail [0]

And the following fresh constants:    null_head, null_tail

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

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

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

   nats -> cons(0, n__incr(nats)) [1]
   pairs -> cons(0, n__incr(odds)) [1]
   odds -> incr(pairs) [1]
   incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) [1]
   head(cons(X, XS)) -> X [1]
   tail(cons(X, XS)) -> activate(XS) [1]
   incr(X) -> n__incr(X) [1]
   activate(n__incr(X)) -> incr(X) [1]
   activate(X) -> X [1]
   head(v0) -> null_head [0]
   tail(v0) -> null_tail [0]

The TRS has the following type information:
nats :: n__incr:cons:null_tail
cons :: 0:s:null_head -> n__incr:cons:null_tail -> n__incr:cons:null_tail
0 :: 0:s:null_head
n__incr :: n__incr:cons:null_tail -> n__incr:cons:null_tail
pairs :: n__incr:cons:null_tail
odds :: n__incr:cons:null_tail
incr :: n__incr:cons:null_tail -> n__incr:cons:null_tail
s :: 0:s:null_head -> 0:s:null_head
activate :: n__incr:cons:null_tail -> n__incr:cons:null_tail
head :: n__incr:cons:null_tail -> 0:s:null_head
tail :: n__incr:cons:null_tail -> n__incr:cons:null_tail
null_head :: 0:s:null_head
null_tail :: n__incr:cons:null_tail

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

(39) 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
   null_head => 0
   null_tail => 0

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

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

   activate(z) -{ 1 }-> X :|: X >= 0, z = X
   activate(z) -{ 1 }-> incr(X) :|: z = 1 + X, X >= 0
   head(z) -{ 1 }-> X :|: z = 1 + X + XS, X >= 0, XS >= 0
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   incr(z) -{ 1 }-> 1 + X :|: X >= 0, z = X
   incr(z) -{ 1 }-> 1 + (1 + X) + (1 + activate(XS)) :|: z = 1 + X + XS, X >= 0, XS >= 0
   nats -{ 1 }-> 1 + 0 + (1 + nats) :|: 
   odds -{ 1 }-> incr(pairs) :|: 
   pairs -{ 1 }-> 1 + 0 + (1 + odds) :|: 
   tail(z) -{ 1 }-> activate(XS) :|: z = 1 + X + XS, X >= 0, XS >= 0
   tail(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

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

(42)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   nats -> cons(0, n__incr(nats))
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   INCR(z0) -> c4
   HEAD(cons(z0, z1)) -> c5
   TAIL(cons(z0, z1)) -> c6(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ACTIVATE(z0) -> c8
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   INCR(z0) -> c4
   HEAD(cons(z0, z1)) -> c5
   TAIL(cons(z0, z1)) -> c6(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ACTIVATE(z0) -> c8
K tuples:none
Defined Rule Symbols:   nats, pairs, odds, incr_1, head_1, tail_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, INCR_1, HEAD_1, TAIL_1, ACTIVATE_1

Compound Symbols:   c_1, c1_1, c2_2, c3_1, c4, c5, c6_1, c7_1, c8


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

(43) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   TAIL(cons(z0, z1)) -> c6(ACTIVATE(z1))
Removed 3 trailing nodes:
   HEAD(cons(z0, z1)) -> c5
   INCR(z0) -> c4
   ACTIVATE(z0) -> c8

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

(44)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   nats -> cons(0, n__incr(nats))
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
K tuples:none
Defined Rule Symbols:   nats, pairs, odds, incr_1, head_1, tail_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, INCR_1, ACTIVATE_1

Compound Symbols:   c_1, c1_1, c2_2, c3_1, c7_1


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

(45) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   nats -> cons(0, n__incr(nats))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)

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

(46)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(pairs), PAIRS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, INCR_1, ACTIVATE_1

Compound Symbols:   c_1, c1_1, c2_2, c3_1, c7_1


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

(47) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace ODDS -> c2(INCR(pairs), PAIRS) by 
   ODDS -> c2(INCR(cons(0, n__incr(odds))), PAIRS)

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

(48)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(odds))), PAIRS)
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(odds))), PAIRS)
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, INCR_1, ACTIVATE_1, ODDS

Compound Symbols:   c_1, c1_1, c3_1, c7_1, c2_2


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

(49) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace ODDS -> c2(INCR(cons(0, n__incr(odds))), PAIRS) by 
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)

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

(50)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1))
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, INCR_1, ACTIVATE_1, ODDS

Compound Symbols:   c_1, c1_1, c3_1, c7_1, c2_2


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

(51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) by 
   INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0)))

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

(52)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0)))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0))
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0)))
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ACTIVATE_1, ODDS, INCR_1

Compound Symbols:   c_1, c1_1, c7_1, c2_2, c3_1


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

(53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) by 
   ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1))))

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

(54)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0)))
   ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1))))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0)))
   ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1))))
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, INCR_1, ACTIVATE_1

Compound Symbols:   c_1, c1_1, c2_2, c3_1, c7_1


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

(55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace INCR(cons(z0, n__incr(y0))) -> c3(ACTIVATE(n__incr(y0))) by 
   INCR(cons(z0, n__incr(cons(y0, n__incr(y1))))) -> c3(ACTIVATE(n__incr(cons(y0, n__incr(y1)))))

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

(56)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1))))
   INCR(cons(z0, n__incr(cons(y0, n__incr(y1))))) -> c3(ACTIVATE(n__incr(cons(y0, n__incr(y1)))))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1))))
   INCR(cons(z0, n__incr(cons(y0, n__incr(y1))))) -> c3(ACTIVATE(n__incr(cons(y0, n__incr(y1)))))
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, ACTIVATE_1, INCR_1

Compound Symbols:   c_1, c1_1, c2_2, c7_1, c3_1


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

(57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ACTIVATE(n__incr(cons(y0, n__incr(y1)))) -> c7(INCR(cons(y0, n__incr(y1)))) by 
   ACTIVATE(n__incr(cons(z0, n__incr(cons(y1, n__incr(y2)))))) -> c7(INCR(cons(z0, n__incr(cons(y1, n__incr(y2))))))

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

(58)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   pairs -> cons(0, n__incr(odds))
   odds -> incr(pairs)
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1)))
   incr(z0) -> n__incr(z0)
   activate(n__incr(z0)) -> incr(z0)
   activate(z0) -> z0
Tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(cons(y0, n__incr(y1))))) -> c3(ACTIVATE(n__incr(cons(y0, n__incr(y1)))))
   ACTIVATE(n__incr(cons(z0, n__incr(cons(y1, n__incr(y2)))))) -> c7(INCR(cons(z0, n__incr(cons(y1, n__incr(y2))))))
S tuples:
   NATS -> c(NATS)
   PAIRS -> c1(ODDS)
   ODDS -> c2(INCR(cons(0, n__incr(incr(pairs)))), PAIRS)
   INCR(cons(z0, n__incr(cons(y0, n__incr(y1))))) -> c3(ACTIVATE(n__incr(cons(y0, n__incr(y1)))))
   ACTIVATE(n__incr(cons(z0, n__incr(cons(y1, n__incr(y2)))))) -> c7(INCR(cons(z0, n__incr(cons(y1, n__incr(y2))))))
K tuples:none
Defined Rule Symbols:   pairs, odds, incr_1, activate_1

Defined Pair Symbols:   NATS, PAIRS, ODDS, INCR_1, ACTIVATE_1

Compound Symbols:   c_1, c1_1, c2_2, c3_1, c7_1