Termination Proof using AProVE

Term Rewriting System R:
[x, y]
nats_active -> add_active(zeros_active)
nats_active -> nats
hd_active(x) -> hd(x)
hd_active(cons(x, y)) -> mark(x)
zeros_active -> cons(0, zeros)
zeros_active -> zeros
tl_active(x) -> tl(x)
tl_active(cons(x, y)) -> mark(y)
incr_active(cons(x, y)) -> cons(s(x), incr(y))
incr_active(x) -> incr(x)
mark(nats) -> nats_active
mark(zeros) -> zeros_active
mark(incr(x)) -> incr_active(mark(x))
mark(add(x)) -> add_active(mark(x))
mark(hd(x)) -> hd_active(mark(x))
mark(tl(x)) -> tl_active(mark(x))
mark(0) -> 0
mark(s(x)) -> s(x)
mark(cons(x, y)) -> cons(x, y)
add_active(cons(x, y)) -> incr_active(cons(x, add(y)))
add_active(x) -> add(x)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

NATS_ACTIVE -> ADD_ACTIVE(zeros_active)
NATS_ACTIVE -> ZEROS_ACTIVE
HD_ACTIVE(cons(x, y)) -> MARK(x)
TL_ACTIVE(cons(x, y)) -> MARK(y)
MARK(nats) -> NATS_ACTIVE
MARK(zeros) -> ZEROS_ACTIVE
MARK(incr(x)) -> INCR_ACTIVE(mark(x))
MARK(incr(x)) -> MARK(x)
MARK(add(x)) -> ADD_ACTIVE(mark(x))
MARK(add(x)) -> MARK(x)
MARK(hd(x)) -> HD_ACTIVE(mark(x))
MARK(hd(x)) -> MARK(x)
MARK(tl(x)) -> TL_ACTIVE(mark(x))
MARK(tl(x)) -> MARK(x)
ADD_ACTIVE(cons(x, y)) -> INCR_ACTIVE(cons(x, add(y)))

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

MARK(tl(x)) -> MARK(x)
TL_ACTIVE(cons(x, y)) -> MARK(y)
MARK(tl(x)) -> TL_ACTIVE(mark(x))
MARK(hd(x)) -> MARK(x)
MARK(hd(x)) -> HD_ACTIVE(mark(x))
MARK(add(x)) -> MARK(x)
MARK(incr(x)) -> MARK(x)
HD_ACTIVE(cons(x, y)) -> MARK(x)

Rules:

nats_active -> add_active(zeros_active)
nats_active -> nats
hd_active(x) -> hd(x)
hd_active(cons(x, y)) -> mark(x)
zeros_active -> cons(0, zeros)
zeros_active -> zeros
tl_active(x) -> tl(x)
tl_active(cons(x, y)) -> mark(y)
incr_active(cons(x, y)) -> cons(s(x), incr(y))
incr_active(x) -> incr(x)
mark(nats) -> nats_active
mark(zeros) -> zeros_active
mark(incr(x)) -> incr_active(mark(x))
mark(add(x)) -> add_active(mark(x))
mark(hd(x)) -> hd_active(mark(x))
mark(tl(x)) -> tl_active(mark(x))
mark(0) -> 0
mark(s(x)) -> s(x)
mark(cons(x, y)) -> cons(x, y)
add_active(cons(x, y)) -> incr_active(cons(x, add(y)))
add_active(x) -> add(x)

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(hd(x)) -> HD_ACTIVE(mark(x))

nine new Dependency Pairs are created:

MARK(hd(nats)) -> HD_ACTIVE(nats_active)
MARK(hd(zeros)) -> HD_ACTIVE(zeros_active)
MARK(hd(incr(x''))) -> HD_ACTIVE(incr_active(mark(x'')))
MARK(hd(add(x''))) -> HD_ACTIVE(add_active(mark(x'')))
MARK(hd(hd(x''))) -> HD_ACTIVE(hd_active(mark(x'')))
MARK(hd(tl(x''))) -> HD_ACTIVE(tl_active(mark(x'')))
MARK(hd(0)) -> HD_ACTIVE(0)
MARK(hd(s(x''))) -> HD_ACTIVE(s(x''))
MARK(hd(cons(x'', y'))) -> HD_ACTIVE(cons(x'', y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

MARK(hd(cons(x'', y'))) -> HD_ACTIVE(cons(x'', y'))
MARK(hd(tl(x''))) -> HD_ACTIVE(tl_active(mark(x'')))
MARK(hd(hd(x''))) -> HD_ACTIVE(hd_active(mark(x'')))
MARK(hd(add(x''))) -> HD_ACTIVE(add_active(mark(x'')))
MARK(hd(incr(x''))) -> HD_ACTIVE(incr_active(mark(x'')))
MARK(hd(zeros)) -> HD_ACTIVE(zeros_active)
HD_ACTIVE(cons(x, y)) -> MARK(x)
MARK(hd(nats)) -> HD_ACTIVE(nats_active)
TL_ACTIVE(cons(x, y)) -> MARK(y)
MARK(tl(x)) -> TL_ACTIVE(mark(x))
MARK(hd(x)) -> MARK(x)
MARK(add(x)) -> MARK(x)
MARK(incr(x)) -> MARK(x)
MARK(tl(x)) -> MARK(x)

Rules:

nats_active -> add_active(zeros_active)
nats_active -> nats
hd_active(x) -> hd(x)
hd_active(cons(x, y)) -> mark(x)
zeros_active -> cons(0, zeros)
zeros_active -> zeros
tl_active(x) -> tl(x)
tl_active(cons(x, y)) -> mark(y)
incr_active(cons(x, y)) -> cons(s(x), incr(y))
incr_active(x) -> incr(x)
mark(nats) -> nats_active
mark(zeros) -> zeros_active
mark(incr(x)) -> incr_active(mark(x))
mark(add(x)) -> add_active(mark(x))
mark(hd(x)) -> hd_active(mark(x))
mark(tl(x)) -> tl_active(mark(x))
mark(0) -> 0
mark(s(x)) -> s(x)
mark(cons(x, y)) -> cons(x, y)
add_active(cons(x, y)) -> incr_active(cons(x, add(y)))
add_active(x) -> add(x)

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(tl(x)) -> TL_ACTIVE(mark(x))

nine new Dependency Pairs are created:

MARK(tl(nats)) -> TL_ACTIVE(nats_active)
MARK(tl(zeros)) -> TL_ACTIVE(zeros_active)
MARK(tl(incr(x''))) -> TL_ACTIVE(incr_active(mark(x'')))
MARK(tl(add(x''))) -> TL_ACTIVE(add_active(mark(x'')))
MARK(tl(hd(x''))) -> TL_ACTIVE(hd_active(mark(x'')))
MARK(tl(tl(x''))) -> TL_ACTIVE(tl_active(mark(x'')))
MARK(tl(0)) -> TL_ACTIVE(0)
MARK(tl(s(x''))) -> TL_ACTIVE(s(x''))
MARK(tl(cons(x'', y'))) -> TL_ACTIVE(cons(x'', y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

MARK(tl(cons(x'', y'))) -> TL_ACTIVE(cons(x'', y'))
MARK(tl(tl(x''))) -> TL_ACTIVE(tl_active(mark(x'')))
MARK(tl(hd(x''))) -> TL_ACTIVE(hd_active(mark(x'')))
MARK(tl(add(x''))) -> TL_ACTIVE(add_active(mark(x'')))
MARK(tl(incr(x''))) -> TL_ACTIVE(incr_active(mark(x'')))
MARK(tl(zeros)) -> TL_ACTIVE(zeros_active)
TL_ACTIVE(cons(x, y)) -> MARK(y)
MARK(tl(nats)) -> TL_ACTIVE(nats_active)
MARK(hd(tl(x''))) -> HD_ACTIVE(tl_active(mark(x'')))
MARK(hd(hd(x''))) -> HD_ACTIVE(hd_active(mark(x'')))
MARK(hd(add(x''))) -> HD_ACTIVE(add_active(mark(x'')))
MARK(hd(incr(x''))) -> HD_ACTIVE(incr_active(mark(x'')))
MARK(hd(zeros)) -> HD_ACTIVE(zeros_active)
MARK(hd(nats)) -> HD_ACTIVE(nats_active)
MARK(tl(x)) -> MARK(x)
MARK(hd(x)) -> MARK(x)
MARK(add(x)) -> MARK(x)
MARK(incr(x)) -> MARK(x)
HD_ACTIVE(cons(x, y)) -> MARK(x)
MARK(hd(cons(x'', y'))) -> HD_ACTIVE(cons(x'', y'))

Rules:

nats_active -> add_active(zeros_active)
nats_active -> nats
hd_active(x) -> hd(x)
hd_active(cons(x, y)) -> mark(x)
zeros_active -> cons(0, zeros)
zeros_active -> zeros
tl_active(x) -> tl(x)
tl_active(cons(x, y)) -> mark(y)
incr_active(cons(x, y)) -> cons(s(x), incr(y))
incr_active(x) -> incr(x)
mark(nats) -> nats_active
mark(zeros) -> zeros_active
mark(incr(x)) -> incr_active(mark(x))
mark(add(x)) -> add_active(mark(x))
mark(hd(x)) -> hd_active(mark(x))
mark(tl(x)) -> tl_active(mark(x))
mark(0) -> 0
mark(s(x)) -> s(x)
mark(cons(x, y)) -> cons(x, y)
add_active(cons(x, y)) -> incr_active(cons(x, add(y)))
add_active(x) -> add(x)

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:06 minutes