Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/ExIntrod_GM01_GM)

The rewrite relation of the following TRS is considered.

a__incr(nil) → nil (1)
a__incr(cons(X,L)) → cons(s(mark(X)),incr(L)) (2)
a__adx(nil) → nil (3)
a__adx(cons(X,L)) → a__incr(cons(mark(X),adx(L))) (4)
a__nats → a__adx(a__zeros) (5)
a__zeros → cons(0,zeros) (6)
a__head(cons(X,L)) → mark(X) (7)
a__tail(cons(X,L)) → mark(L) (8)
mark(incr(X)) → a__incr(mark(X)) (9)
mark(adx(X)) → a__adx(mark(X)) (10)
mark(nats) → a__nats (11)
mark(zeros) → a__zeros (12)
mark(head(X)) → a__head(mark(X)) (13)
mark(tail(X)) → a__tail(mark(X)) (14)
mark(nil) → nil (15)
mark(cons(X1,X2)) → cons(mark(X1),X2) (16)
mark(s(X)) → s(mark(X)) (17)
mark(0) → 0 (18)
a__incr(X) → incr(X) (19)
a__adx(X) → adx(X) (20)
a__nats → nats (21)
a__zeros → zeros (22)
a__head(X) → head(X) (23)
a__tail(X) → tail(X) (24)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__incr(x1)] = 1 · x1
[nil] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[incr(x1)] = 1 · x1
[a__adx(x1)] = 1 · x1
[adx(x1)] = 1 · x1
[a__nats] = 1
[a__zeros] = 0
[0] = 0
[zeros] = 0
[a__head(x1)] = 2 · x1
[a__tail(x1)] = 2 · x1
[nats] = 1
[head(x1)] = 2 · x1
[tail(x1)] = 2 · x1
all of the following rules can be deleted.
a__nats → a__adx(a__zeros) (5)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__incr(x1)] = 1 · x1
[nil] = 0
[cons(x1, x2)] = 1 · x1 + 2 · x2
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[incr(x1)] = 1 · x1
[a__adx(x1)] = 1 · x1
[adx(x1)] = 1 · x1
[a__zeros] = 0
[0] = 0
[zeros] = 0
[a__head(x1)] = 1 + 2 · x1
[a__tail(x1)] = 2 · x1
[nats] = 0
[a__nats] = 0
[head(x1)] = 1 + 2 · x1
[tail(x1)] = 2 · x1
all of the following rules can be deleted.
a__head(cons(X,L)) → mark(X) (7)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__incr(x1)] = 1 · x1
[nil] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[incr(x1)] = 1 · x1
[a__adx(x1)] = 1 + 1 · x1
[adx(x1)] = 1 + 1 · x1
[a__zeros] = 0
[0] = 0
[zeros] = 0
[a__tail(x1)] = 1 · x1
[nats] = 0
[a__nats] = 0
[head(x1)] = 2 · x1
[a__head(x1)] = 2 · x1
[tail(x1)] = 1 · x1
all of the following rules can be deleted.
a__adx(nil) → nil (3)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__incr(x1)] = 1 · x1
[nil] = 0
[cons(x1, x2)] = 1 · x1 + 2 · x2
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[incr(x1)] = 1 · x1
[a__adx(x1)] = 1 · x1
[adx(x1)] = 1 · x1
[a__zeros] = 0
[0] = 0
[zeros] = 0
[a__tail(x1)] = 1 + 2 · x1
[nats] = 0
[a__nats] = 0
[head(x1)] = 1 · x1
[a__head(x1)] = 1 · x1
[tail(x1)] = 1 + 2 · x1
all of the following rules can be deleted.
a__tail(cons(X,L)) → mark(L) (8)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a__incr#(cons(X,L)) → mark#(X) (25)
a__adx#(cons(X,L)) → a__incr#(cons(mark(X),adx(L))) (26)
a__adx#(cons(X,L)) → mark#(X) (27)
mark#(incr(X)) → a__incr#(mark(X)) (28)
mark#(incr(X)) → mark#(X) (29)
mark#(adx(X)) → a__adx#(mark(X)) (30)
mark#(adx(X)) → mark#(X) (31)
mark#(nats) → a__nats# (32)
mark#(zeros) → a__zeros# (33)
mark#(head(X)) → a__head#(mark(X)) (34)
mark#(head(X)) → mark#(X) (35)
mark#(tail(X)) → a__tail#(mark(X)) (36)
mark#(tail(X)) → mark#(X) (37)
mark#(cons(X1,X2)) → mark#(X1) (38)
mark#(s(X)) → mark#(X) (39)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.