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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 270 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 46.2 s]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 385 ms]
        (20) typed CpxTrs


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

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


The TRS R consists of the following rules:

   incr(nil) -> nil
   incr(cons(X, L)) -> cons(s(X), incr(L))
   adx(nil) -> nil
   adx(cons(X, L)) -> incr(cons(X, adx(L)))
   nats -> adx(zeros)
   zeros -> cons(0, zeros)
   head(cons(X, L)) -> X
   tail(cons(X, L)) -> L

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

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   incr(nil) -> nil
   incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
   adx(nil) -> nil
   adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
   nats -> adx(zeros)
   zeros -> cons(0, zeros)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   INCR(nil) -> c
   INCR(cons(z0, z1)) -> c1(INCR(z1))
   ADX(nil) -> c2
   ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
   NATS -> c4(ADX(zeros), ZEROS)
   ZEROS -> c5(ZEROS)
   HEAD(cons(z0, z1)) -> c6
   TAIL(cons(z0, z1)) -> c7
S tuples:
   INCR(nil) -> c
   INCR(cons(z0, z1)) -> c1(INCR(z1))
   ADX(nil) -> c2
   ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
   NATS -> c4(ADX(zeros), ZEROS)
   ZEROS -> c5(ZEROS)
   HEAD(cons(z0, z1)) -> c6
   TAIL(cons(z0, z1)) -> c7
K tuples:none
Defined Rule Symbols:   incr_1, adx_1, nats, zeros, head_1, tail_1

Defined Pair Symbols:   INCR_1, ADX_1, NATS, ZEROS, HEAD_1, TAIL_1

Compound Symbols:   c, c1_1, c2, c3_2, c4_2, c5_1, c6, c7


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

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

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


The TRS R consists of the following rules:

   INCR(nil) -> c
   INCR(cons(z0, z1)) -> c1(INCR(z1))
   ADX(nil) -> c2
   ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
   NATS -> c4(ADX(zeros), ZEROS)
   ZEROS -> c5(ZEROS)
   HEAD(cons(z0, z1)) -> c6
   TAIL(cons(z0, z1)) -> c7

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

   incr(nil) -> nil
   incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
   adx(nil) -> nil
   adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
   nats -> adx(zeros)
   zeros -> cons(0, zeros)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1

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

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

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


The TRS R consists of the following rules:

   INCR(nil) -> c
   INCR(cons(z0, z1)) -> c1(INCR(z1))
   ADX(nil) -> c2
   ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
   NATS -> c4(ADX(zeros), ZEROS)
   ZEROS -> c5(ZEROS)
   HEAD(cons(z0, z1)) -> c6
   TAIL(cons(z0, z1)) -> c7

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

   incr(nil) -> nil
   incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
   adx(nil) -> nil
   adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
   nats -> adx(zeros)
   zeros -> cons(0', zeros)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1

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

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

(8)
Obligation:
Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
INCR, ADX, adx, zeros, ZEROS, incr

They will be analysed ascendingly in the following order:
INCR < ADX
adx < ADX
incr < adx

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

(10)
Obligation:
Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(gen_c:c19_8(x))
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(0', gen_nil:cons10_8(x))
gen_s:0'11_8(0) <=> 0'
gen_s:0'11_8(+(x, 1)) <=> s(gen_s:0'11_8(x))
gen_c2:c312_8(0) <=> c2
gen_c2:c312_8(+(x, 1)) <=> c3(c, gen_c2:c312_8(x))
gen_c513_8(0) <=> hole_c56_8
gen_c513_8(+(x, 1)) <=> c5(gen_c513_8(x))


The following defined symbols remain to be analysed:
INCR, ADX, adx, zeros, ZEROS, incr

They will be analysed ascendingly in the following order:
INCR < ADX
adx < ADX
incr < adx

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INCR(gen_nil:cons10_8(n15_8)) -> gen_c:c19_8(n15_8), rt in Omega(1 + n15_8)

Induction Base:
INCR(gen_nil:cons10_8(0)) ->_R^Omega(1)
c

Induction Step:
INCR(gen_nil:cons10_8(+(n15_8, 1))) ->_R^Omega(1)
c1(INCR(gen_nil:cons10_8(n15_8))) ->_IH
c1(gen_c:c19_8(c16_8))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(gen_c:c19_8(x))
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(0', gen_nil:cons10_8(x))
gen_s:0'11_8(0) <=> 0'
gen_s:0'11_8(+(x, 1)) <=> s(gen_s:0'11_8(x))
gen_c2:c312_8(0) <=> c2
gen_c2:c312_8(+(x, 1)) <=> c3(c, gen_c2:c312_8(x))
gen_c513_8(0) <=> hole_c56_8
gen_c513_8(+(x, 1)) <=> c5(gen_c513_8(x))


The following defined symbols remain to be analysed:
INCR, ADX, adx, zeros, ZEROS, incr

They will be analysed ascendingly in the following order:
INCR < ADX
adx < ADX
incr < adx

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5


Lemmas:
INCR(gen_nil:cons10_8(n15_8)) -> gen_c:c19_8(n15_8), rt in Omega(1 + n15_8)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(gen_c:c19_8(x))
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(0', gen_nil:cons10_8(x))
gen_s:0'11_8(0) <=> 0'
gen_s:0'11_8(+(x, 1)) <=> s(gen_s:0'11_8(x))
gen_c2:c312_8(0) <=> c2
gen_c2:c312_8(+(x, 1)) <=> c3(c, gen_c2:c312_8(x))
gen_c513_8(0) <=> hole_c56_8
gen_c513_8(+(x, 1)) <=> c5(gen_c513_8(x))


The following defined symbols remain to be analysed:
zeros, ADX, adx, ZEROS, incr

They will be analysed ascendingly in the following order:
adx < ADX
incr < adx

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
incr(gen_nil:cons10_8(+(1, n316_8))) -> *14_8, rt in Omega(0)

Induction Base:
incr(gen_nil:cons10_8(+(1, 0)))

Induction Step:
incr(gen_nil:cons10_8(+(1, +(n316_8, 1)))) ->_R^Omega(0)
cons(s(0'), incr(gen_nil:cons10_8(+(1, n316_8)))) ->_IH
cons(s(0'), *14_8)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5


Lemmas:
INCR(gen_nil:cons10_8(n15_8)) -> gen_c:c19_8(n15_8), rt in Omega(1 + n15_8)
incr(gen_nil:cons10_8(+(1, n316_8))) -> *14_8, rt in Omega(0)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(gen_c:c19_8(x))
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(0', gen_nil:cons10_8(x))
gen_s:0'11_8(0) <=> 0'
gen_s:0'11_8(+(x, 1)) <=> s(gen_s:0'11_8(x))
gen_c2:c312_8(0) <=> c2
gen_c2:c312_8(+(x, 1)) <=> c3(c, gen_c2:c312_8(x))
gen_c513_8(0) <=> hole_c56_8
gen_c513_8(+(x, 1)) <=> c5(gen_c513_8(x))


The following defined symbols remain to be analysed:
adx, ADX

They will be analysed ascendingly in the following order:
adx < ADX

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
adx(gen_nil:cons10_8(+(1, n568062_8))) -> *14_8, rt in Omega(0)

Induction Base:
adx(gen_nil:cons10_8(+(1, 0)))

Induction Step:
adx(gen_nil:cons10_8(+(1, +(n568062_8, 1)))) ->_R^Omega(0)
incr(cons(0', adx(gen_nil:cons10_8(+(1, n568062_8))))) ->_IH
incr(cons(0', *14_8))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
INCR(nil) -> c
INCR(cons(z0, z1)) -> c1(INCR(z1))
ADX(nil) -> c2
ADX(cons(z0, z1)) -> c3(INCR(cons(z0, adx(z1))), ADX(z1))
NATS -> c4(ADX(zeros), ZEROS)
ZEROS -> c5(ZEROS)
HEAD(cons(z0, z1)) -> c6
TAIL(cons(z0, z1)) -> c7
incr(nil) -> nil
incr(cons(z0, z1)) -> cons(s(z0), incr(z1))
adx(nil) -> nil
adx(cons(z0, z1)) -> incr(cons(z0, adx(z1)))
nats -> adx(zeros)
zeros -> cons(0', zeros)
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1

Types:
INCR :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: s:0' -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
ADX :: nil:cons -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c2:c3
adx :: nil:cons -> nil:cons
NATS :: c4
c4 :: c2:c3 -> c5 -> c4
zeros :: nil:cons
ZEROS :: c5
c5 :: c5 -> c5
HEAD :: nil:cons -> c6
c6 :: c6
TAIL :: nil:cons -> c7
c7 :: c7
incr :: nil:cons -> nil:cons
s :: s:0' -> s:0'
nats :: nil:cons
0' :: s:0'
head :: nil:cons -> s:0'
tail :: nil:cons -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_s:0'3_8 :: s:0'
hole_c2:c34_8 :: c2:c3
hole_c45_8 :: c4
hole_c56_8 :: c5
hole_c67_8 :: c6
hole_c78_8 :: c7
gen_c:c19_8 :: Nat -> c:c1
gen_nil:cons10_8 :: Nat -> nil:cons
gen_s:0'11_8 :: Nat -> s:0'
gen_c2:c312_8 :: Nat -> c2:c3
gen_c513_8 :: Nat -> c5


Lemmas:
INCR(gen_nil:cons10_8(n15_8)) -> gen_c:c19_8(n15_8), rt in Omega(1 + n15_8)
incr(gen_nil:cons10_8(+(1, n316_8))) -> *14_8, rt in Omega(0)
adx(gen_nil:cons10_8(+(1, n568062_8))) -> *14_8, rt in Omega(0)


Generator Equations:
gen_c:c19_8(0) <=> c
gen_c:c19_8(+(x, 1)) <=> c1(gen_c:c19_8(x))
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(0', gen_nil:cons10_8(x))
gen_s:0'11_8(0) <=> 0'
gen_s:0'11_8(+(x, 1)) <=> s(gen_s:0'11_8(x))
gen_c2:c312_8(0) <=> c2
gen_c2:c312_8(+(x, 1)) <=> c3(c, gen_c2:c312_8(x))
gen_c513_8(0) <=> hole_c56_8
gen_c513_8(+(x, 1)) <=> c5(gen_c513_8(x))


The following defined symbols remain to be analysed:
ADX