KILLED
proof of input_bU7VLmT06Y.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) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
        (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 6 ms]
        (12) typed CpxTrs
        (13) OrderProof [LOWER BOUND(ID), 0 ms]
        (14) typed CpxTrs
    (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
    (16) TRS for Loop Detection
(17) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(18) CdtProblem
    (19) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (20) CdtProblem
    (21) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CdtProblem
    (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
        (25) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
        (26) CpxTRS
        (27) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
        (28) CpxWeightedTrs
            (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
            (30) CpxTypedWeightedTrs
            (31) CompletionProof [UPPER BOUND(ID), 0 ms]
            (32) CpxTypedWeightedCompleteTrs
                (33) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
                (34) CpxTypedWeightedCompleteTrs
                (35) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (36) CpxRNTS
                (37) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
                (38) CpxRNTS
                (39) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
                (40) CpxRNTS
                (41) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (42) CpxRNTS
                (43) IntTrsBoundProof [UPPER BOUND(ID), 599 ms]
                (44) CpxRNTS
                (45) IntTrsBoundProof [UPPER BOUND(ID), 69 ms]
                (46) CpxRNTS
                (47) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (48) CpxRNTS
                (49) IntTrsBoundProof [UPPER BOUND(ID), 272 ms]
                (50) CpxRNTS
                (51) IntTrsBoundProof [UPPER BOUND(ID), 57 ms]
                (52) CpxRNTS
                (53) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (54) CpxRNTS
                (55) IntTrsBoundProof [UPPER BOUND(ID), 97 ms]
                (56) CpxRNTS
                (57) IntTrsBoundProof [UPPER BOUND(ID), 22 ms]
                (58) CpxRNTS
            (59) CompletionProof [UPPER BOUND(ID), 0 ms]
            (60) CpxTypedWeightedCompleteTrs
                (61) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (62) CpxRNTS
    (63) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (64) CdtProblem
        (65) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (66) CdtProblem
        (67) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (68) CdtProblem
        (69) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (70) CdtProblem
        (71) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (72) CdtProblem
        (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (74) CdtProblem
(75) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(76) CpxWeightedTrs
    (77) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (78) CpxTypedWeightedTrs
    (79) CompletionProof [UPPER BOUND(ID), 0 ms]
    (80) CpxTypedWeightedCompleteTrs
        (81) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (82) CpxTypedWeightedCompleteTrs
        (83) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (84) CpxRNTS
        (85) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (86) CpxRNTS
        (87) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (88) CpxRNTS
        (89) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (90) CpxRNTS
        (91) IntTrsBoundProof [UPPER BOUND(ID), 665 ms]
        (92) CpxRNTS
        (93) IntTrsBoundProof [UPPER BOUND(ID), 96 ms]
        (94) CpxRNTS
        (95) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (96) CpxRNTS
        (97) IntTrsBoundProof [UPPER BOUND(ID), 130 ms]
        (98) CpxRNTS
        (99) IntTrsBoundProof [UPPER BOUND(ID), 12 ms]
        (100) CpxRNTS
        (101) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (102) CpxRNTS
        (103) IntTrsBoundProof [UPPER BOUND(ID), 186 ms]
        (104) CpxRNTS
        (105) IntTrsBoundProof [UPPER BOUND(ID), 32 ms]
        (106) CpxRNTS
    (107) CompletionProof [UPPER BOUND(ID), 0 ms]
    (108) CpxTypedWeightedCompleteTrs
        (109) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (110) CpxRNTS


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

(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) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

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


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

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

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


The TRS R consists of the following rules:

   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

The (relative) TRS S consists of the following 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

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

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

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


The TRS R consists of the following rules:

   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

The (relative) TRS S consists of the following 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

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

(11) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(12)
Obligation:
Innermost TRS:
Rules:
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
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

Types:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3:c4 -> c1 -> c2
INCR :: cons:n__incr -> c3:c4
pairs :: cons:n__incr
cons :: 0':s -> cons:n__incr -> cons:n__incr
c3 :: c7:c8 -> c3:c4
ACTIVATE :: cons:n__incr -> c7:c8
c4 :: c3:c4
HEAD :: cons:n__incr -> c5
c5 :: c5
TAIL :: cons:n__incr -> c6
c6 :: c7:c8 -> c6
n__incr :: cons:n__incr -> cons:n__incr
c7 :: c3:c4 -> c7:c8
c8 :: c7:c8
nats :: cons:n__incr
0' :: 0':s
odds :: cons:n__incr
incr :: cons:n__incr -> cons:n__incr
s :: 0':s -> 0':s
activate :: cons:n__incr -> cons:n__incr
head :: cons:n__incr -> 0':s
tail :: cons:n__incr -> cons:n__incr
hole_c1_9 :: c
hole_c12_9 :: c1
hole_c23_9 :: c2
hole_c3:c44_9 :: c3:c4
hole_cons:n__incr5_9 :: cons:n__incr
hole_0':s6_9 :: 0':s
hole_c7:c87_9 :: c7:c8
hole_c58_9 :: c5
hole_c69_9 :: c6
gen_c10_9 :: Nat -> c
gen_cons:n__incr11_9 :: Nat -> cons:n__incr
gen_0':s12_9 :: Nat -> 0':s

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
NATS, PAIRS, ODDS, INCR, pairs, ACTIVATE, nats, odds, incr, activate

They will be analysed ascendingly in the following order:
PAIRS = ODDS
INCR < ODDS
pairs < ODDS
INCR = ACTIVATE
pairs = odds
incr < odds
incr = activate

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

(14)
Obligation:
Innermost TRS:
Rules:
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
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

Types:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3:c4 -> c1 -> c2
INCR :: cons:n__incr -> c3:c4
pairs :: cons:n__incr
cons :: 0':s -> cons:n__incr -> cons:n__incr
c3 :: c7:c8 -> c3:c4
ACTIVATE :: cons:n__incr -> c7:c8
c4 :: c3:c4
HEAD :: cons:n__incr -> c5
c5 :: c5
TAIL :: cons:n__incr -> c6
c6 :: c7:c8 -> c6
n__incr :: cons:n__incr -> cons:n__incr
c7 :: c3:c4 -> c7:c8
c8 :: c7:c8
nats :: cons:n__incr
0' :: 0':s
odds :: cons:n__incr
incr :: cons:n__incr -> cons:n__incr
s :: 0':s -> 0':s
activate :: cons:n__incr -> cons:n__incr
head :: cons:n__incr -> 0':s
tail :: cons:n__incr -> cons:n__incr
hole_c1_9 :: c
hole_c12_9 :: c1
hole_c23_9 :: c2
hole_c3:c44_9 :: c3:c4
hole_cons:n__incr5_9 :: cons:n__incr
hole_0':s6_9 :: 0':s
hole_c7:c87_9 :: c7:c8
hole_c58_9 :: c5
hole_c69_9 :: c6
gen_c10_9 :: Nat -> c
gen_cons:n__incr11_9 :: Nat -> cons:n__incr
gen_0':s12_9 :: Nat -> 0':s


Generator Equations:
gen_c10_9(0) <=> hole_c1_9
gen_c10_9(+(x, 1)) <=> c(gen_c10_9(x))
gen_cons:n__incr11_9(0) <=> hole_cons:n__incr5_9
gen_cons:n__incr11_9(+(x, 1)) <=> cons(0', gen_cons:n__incr11_9(x))
gen_0':s12_9(0) <=> 0'
gen_0':s12_9(+(x, 1)) <=> s(gen_0':s12_9(x))


The following defined symbols remain to be analysed:
NATS, PAIRS, ODDS, INCR, pairs, ACTIVATE, nats, odds, incr, activate

They will be analysed ascendingly in the following order:
PAIRS = ODDS
INCR < ODDS
pairs < ODDS
INCR = ACTIVATE
pairs = odds
incr < odds
incr = activate

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

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

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

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


The TRS R consists of the following rules:

   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

The (relative) TRS S consists of the following 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

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

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

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


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

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

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

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


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

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

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

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


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

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

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


The TRS R consists of the following rules:

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

The (relative) TRS S consists of the following 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

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

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

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


The TRS R consists of the following rules:

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

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

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

(28)
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 -> c(NATS) [1]
   PAIRS -> c1(ODDS) [1]
   ODDS -> c2(INCR(pairs), PAIRS) [1]
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) [1]
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) [1]
   pairs -> cons(0, n__incr(odds)) [0]
   odds -> incr(pairs) [0]
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1))) [0]
   incr(z0) -> n__incr(z0) [0]
   activate(n__incr(z0)) -> incr(z0) [0]
   activate(z0) -> z0 [0]

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

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

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

   NATS -> c(NATS) [1]
   PAIRS -> c1(ODDS) [1]
   ODDS -> c2(INCR(pairs), PAIRS) [1]
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) [1]
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) [1]
   pairs -> cons(0, n__incr(odds)) [0]
   odds -> incr(pairs) [0]
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1))) [0]
   incr(z0) -> n__incr(z0) [0]
   activate(n__incr(z0)) -> incr(z0) [0]
   activate(z0) -> z0 [0]

The TRS has the following type information:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3 -> c1 -> c2
INCR :: cons:n__incr -> c3
pairs :: cons:n__incr
cons :: 0:s -> cons:n__incr -> cons:n__incr
c3 :: c7 -> c3
ACTIVATE :: cons:n__incr -> c7
n__incr :: cons:n__incr -> cons:n__incr
c7 :: c3 -> c7
0 :: 0:s
odds :: cons:n__incr
incr :: cons:n__incr -> cons:n__incr
s :: 0:s -> 0:s
activate :: cons:n__incr -> cons:n__incr

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

(31) 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
   PAIRS
   ODDS
   INCR_1
   ACTIVATE_1

(c) The following functions are completely defined:

   pairs
   odds
   incr_1
   activate_1

Due to the following rules being added:

   pairs -> const4 [0]
   odds -> const4 [0]
   incr(v0) -> const4 [0]
   activate(v0) -> const4 [0]

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

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

(32)
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 -> c(NATS) [1]
   PAIRS -> c1(ODDS) [1]
   ODDS -> c2(INCR(pairs), PAIRS) [1]
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) [1]
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) [1]
   pairs -> cons(0, n__incr(odds)) [0]
   odds -> incr(pairs) [0]
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1))) [0]
   incr(z0) -> n__incr(z0) [0]
   activate(n__incr(z0)) -> incr(z0) [0]
   activate(z0) -> z0 [0]
   pairs -> const4 [0]
   odds -> const4 [0]
   incr(v0) -> const4 [0]
   activate(v0) -> const4 [0]

The TRS has the following type information:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3 -> c1 -> c2
INCR :: cons:n__incr:const4 -> c3
pairs :: cons:n__incr:const4
cons :: 0:s -> cons:n__incr:const4 -> cons:n__incr:const4
c3 :: c7 -> c3
ACTIVATE :: cons:n__incr:const4 -> c7
n__incr :: cons:n__incr:const4 -> cons:n__incr:const4
c7 :: c3 -> c7
0 :: 0:s
odds :: cons:n__incr:const4
incr :: cons:n__incr:const4 -> cons:n__incr:const4
s :: 0:s -> 0:s
activate :: cons:n__incr:const4 -> cons:n__incr:const4
const4 :: cons:n__incr:const4
const :: c
const1 :: c1
const2 :: c2
const3 :: c3
const5 :: c7

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

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

(34)
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 -> c(NATS) [1]
   PAIRS -> c1(ODDS) [1]
   ODDS -> c2(INCR(cons(0, n__incr(odds))), PAIRS) [1]
   ODDS -> c2(INCR(const4), PAIRS) [1]
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) [1]
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) [1]
   pairs -> cons(0, n__incr(odds)) [0]
   odds -> incr(cons(0, n__incr(odds))) [0]
   odds -> incr(const4) [0]
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1))) [0]
   incr(z0) -> n__incr(z0) [0]
   activate(n__incr(z0)) -> incr(z0) [0]
   activate(z0) -> z0 [0]
   pairs -> const4 [0]
   odds -> const4 [0]
   incr(v0) -> const4 [0]
   activate(v0) -> const4 [0]

The TRS has the following type information:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3 -> c1 -> c2
INCR :: cons:n__incr:const4 -> c3
pairs :: cons:n__incr:const4
cons :: 0:s -> cons:n__incr:const4 -> cons:n__incr:const4
c3 :: c7 -> c3
ACTIVATE :: cons:n__incr:const4 -> c7
n__incr :: cons:n__incr:const4 -> cons:n__incr:const4
c7 :: c3 -> c7
0 :: 0:s
odds :: cons:n__incr:const4
incr :: cons:n__incr:const4 -> cons:n__incr:const4
s :: 0:s -> 0:s
activate :: cons:n__incr:const4 -> cons:n__incr:const4
const4 :: cons:n__incr:const4
const :: c
const1 :: c1
const2 :: c2
const3 :: c3
const5 :: c7

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

(35) 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
   const4 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0
   const5 => 0

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z0) :|: z = 1 + z0, z0 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   activate(z) -{ 0 }-> incr(z0) :|: z = 1 + z0, z0 >= 0
   activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   incr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   incr(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 


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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> incr(z - 1) :|: z - 1 >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 


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

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

   { activate, incr }
   { INCR, ACTIVATE }
   { NATS }
   { odds }
   { ODDS, PAIRS }
   { pairs }

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> incr(z - 1) :|: z - 1 >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {activate,incr}, {INCR,ACTIVATE}, {NATS}, {odds}, {ODDS,PAIRS}, {pairs}

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> incr(z - 1) :|: z - 1 >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {activate,incr}, {INCR,ACTIVATE}, {NATS}, {odds}, {ODDS,PAIRS}, {pairs}

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

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> incr(z - 1) :|: z - 1 >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

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

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

(45) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> incr(z - 1) :|: z - 1 >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(0) :|: 
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {INCR,ACTIVATE}, {NATS}, {odds}, {ODDS,PAIRS}, {pairs}
Previous analysis results are:
  activate: runtime: O(1) [0], size: O(n^1) [3*z]
  incr: runtime: O(1) [0], size: O(n^1) [1 + 3*z]

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {INCR,ACTIVATE}, {NATS}, {odds}, {ODDS,PAIRS}, {pairs}
Previous analysis results are:
  activate: runtime: O(1) [0], size: O(n^1) [3*z]
  incr: runtime: O(1) [0], size: O(n^1) [1 + 3*z]

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

(49) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {INCR,ACTIVATE}, {NATS}, {odds}, {ODDS,PAIRS}, {pairs}
Previous analysis results are:
  activate: runtime: O(1) [0], size: O(n^1) [3*z]
  incr: runtime: O(1) [0], size: O(n^1) [1 + 3*z]
  INCR: runtime: ?, size: O(1) [0]
  ACTIVATE: runtime: ?, size: O(1) [1]

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

(51) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   ACTIVATE(z) -{ 1 }-> 1 + INCR(z - 1) :|: z - 1 >= 0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(0) + PAIRS :|: 
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {NATS}, {odds}, {ODDS,PAIRS}, {pairs}
Previous analysis results are:
  activate: runtime: O(1) [0], size: O(n^1) [3*z]
  incr: runtime: O(1) [0], size: O(n^1) [1 + 3*z]
  INCR: runtime: O(n^1) [2*z], size: O(1) [0]
  ACTIVATE: runtime: O(n^1) [2*z], size: O(1) [1]

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

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

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

   ACTIVATE(z) -{ -1 + 2*z }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z - 1 >= 0
   INCR(z) -{ 1 + 2*z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + s1 + PAIRS :|: s1 >= 0, s1 <= 0
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Function symbols to be analyzed: {NATS}, {odds}, {ODDS,PAIRS}, {pairs}
Previous analysis results are:
  activate: runtime: O(1) [0], size: O(n^1) [3*z]
  incr: runtime: O(1) [0], size: O(n^1) [1 + 3*z]
  INCR: runtime: O(n^1) [2*z], size: O(1) [0]
  ACTIVATE: runtime: O(n^1) [2*z], size: O(1) [1]

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

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

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

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

   ACTIVATE(z) -{ -1 + 2*z }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z - 1 >= 0
   INCR(z) -{ 1 + 2*z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + s1 + PAIRS :|: s1 >= 0, s1 <= 0
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

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

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

(57) 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: ?

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

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

   ACTIVATE(z) -{ -1 + 2*z }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z - 1 >= 0
   INCR(z) -{ 1 + 2*z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + s1 + PAIRS :|: s1 >= 0, s1 <= 0
   ODDS -{ 1 }-> 1 + INCR(1 + 0 + (1 + odds)) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= 3 * (z - 1) + 1, z - 1 >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 0 :|: z >= 0
   incr(z) -{ 0 }-> 1 + z :|: z >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + s') :|: s' >= 0, s' <= 3 * z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> s :|: s >= 0, s <= 3 * 0 + 1
   odds -{ 0 }-> incr(1 + 0 + (1 + odds)) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

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

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

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

   pairs -> null_pairs [0]
   odds -> null_odds [0]
   incr(v0) -> null_incr [0]
   activate(v0) -> null_activate [0]
   INCR(v0) -> null_INCR [0]
   ACTIVATE(v0) -> null_ACTIVATE [0]

And the following fresh constants:    null_pairs, null_odds, null_incr, null_activate, null_INCR, null_ACTIVATE, const, const1, const2

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

(60)
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 -> c(NATS) [1]
   PAIRS -> c1(ODDS) [1]
   ODDS -> c2(INCR(pairs), PAIRS) [1]
   INCR(cons(z0, z1)) -> c3(ACTIVATE(z1)) [1]
   ACTIVATE(n__incr(z0)) -> c7(INCR(z0)) [1]
   pairs -> cons(0, n__incr(odds)) [0]
   odds -> incr(pairs) [0]
   incr(cons(z0, z1)) -> cons(s(z0), n__incr(activate(z1))) [0]
   incr(z0) -> n__incr(z0) [0]
   activate(n__incr(z0)) -> incr(z0) [0]
   activate(z0) -> z0 [0]
   pairs -> null_pairs [0]
   odds -> null_odds [0]
   incr(v0) -> null_incr [0]
   activate(v0) -> null_activate [0]
   INCR(v0) -> null_INCR [0]
   ACTIVATE(v0) -> null_ACTIVATE [0]

The TRS has the following type information:
NATS :: c
c :: c -> c
PAIRS :: c1
c1 :: c2 -> c1
ODDS :: c2
c2 :: c3:null_INCR -> c1 -> c2
INCR :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> c3:null_INCR
pairs :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
cons :: 0:s -> cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> cons:n__incr:null_pairs:null_odds:null_incr:null_activate
c3 :: c7:null_ACTIVATE -> c3:null_INCR
ACTIVATE :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> c7:null_ACTIVATE
n__incr :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> cons:n__incr:null_pairs:null_odds:null_incr:null_activate
c7 :: c3:null_INCR -> c7:null_ACTIVATE
0 :: 0:s
odds :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
incr :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> cons:n__incr:null_pairs:null_odds:null_incr:null_activate
s :: 0:s -> 0:s
activate :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate -> cons:n__incr:null_pairs:null_odds:null_incr:null_activate
null_pairs :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
null_odds :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
null_incr :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
null_activate :: cons:n__incr:null_pairs:null_odds:null_incr:null_activate
null_INCR :: c3:null_INCR
null_ACTIVATE :: c7:null_ACTIVATE
const :: c
const1 :: c1
const2 :: c2

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

(61) 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_pairs => 0
   null_odds => 0
   null_incr => 0
   null_activate => 0
   null_INCR => 0
   null_ACTIVATE => 0
   const => 0
   const1 => 0
   const2 => 0

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

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

   ACTIVATE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   ACTIVATE(z) -{ 1 }-> 1 + INCR(z0) :|: z = 1 + z0, z0 >= 0
   INCR(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   INCR(z) -{ 1 }-> 1 + ACTIVATE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NATS -{ 1 }-> 1 + NATS :|: 
   ODDS -{ 1 }-> 1 + INCR(pairs) + PAIRS :|: 
   PAIRS -{ 1 }-> 1 + ODDS :|: 
   activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   activate(z) -{ 0 }-> incr(z0) :|: z = 1 + z0, z0 >= 0
   activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   incr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   incr(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   incr(z) -{ 0 }-> 1 + (1 + z0) + (1 + activate(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   odds -{ 0 }-> incr(pairs) :|: 
   odds -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 0 :|: 
   pairs -{ 0 }-> 1 + 0 + (1 + odds) :|: 

Only complete derivations are relevant for the runtime complexity.

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

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

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

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


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

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

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

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


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

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

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

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


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

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

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

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


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

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

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

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


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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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


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

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

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

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

(88)
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}

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

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

(90)
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}

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

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

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

(92)
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]

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

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

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

(94)
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]

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

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

(96)
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]

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

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

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

(98)
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]

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

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

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

(100)
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]

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

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

(102)
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]

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

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

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

(104)
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]

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

(105) 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: ?

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

(106)
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]

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

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

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

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

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

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

(110)
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.