Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_DLMMU04_GM)

The rewrite relation of the following TRS is considered.

a__pairNs → cons(0,incr(oddNs)) (1)
a__oddNs → a__incr(a__pairNs) (2)
a__incr(cons(X,XS)) → cons(s(mark(X)),incr(XS)) (3)
a__take(0,XS) → nil (4)
a__take(s(N),cons(X,XS)) → cons(mark(X),take(N,XS)) (5)
a__zip(nil,XS) → nil (6)
a__zip(X,nil) → nil (7)
a__zip(cons(X,XS),cons(Y,YS)) → cons(pair(mark(X),mark(Y)),zip(XS,YS)) (8)
a__tail(cons(X,XS)) → mark(XS) (9)
a__repItems(nil) → nil (10)
a__repItems(cons(X,XS)) → cons(mark(X),cons(X,repItems(XS))) (11)
mark(pairNs) → a__pairNs (12)
mark(incr(X)) → a__incr(mark(X)) (13)
mark(oddNs) → a__oddNs (14)
mark(take(X1,X2)) → a__take(mark(X1),mark(X2)) (15)
mark(zip(X1,X2)) → a__zip(mark(X1),mark(X2)) (16)
mark(tail(X)) → a__tail(mark(X)) (17)
mark(repItems(X)) → a__repItems(mark(X)) (18)
mark(cons(X1,X2)) → cons(mark(X1),X2) (19)
mark(0) → 0 (20)
mark(s(X)) → s(mark(X)) (21)
mark(nil) → nil (22)
mark(pair(X1,X2)) → pair(mark(X1),mark(X2)) (23)
a__pairNs → pairNs (24)
a__incr(X) → incr(X) (25)
a__oddNs → oddNs (26)
a__take(X1,X2) → take(X1,X2) (27)
a__zip(X1,X2) → zip(X1,X2) (28)
a__tail(X) → tail(X) (29)
a__repItems(X) → repItems(X) (30)

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__pairNs] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[incr(x1)] = 2 · x1
[oddNs] = 0
[a__oddNs] = 0
[a__incr(x1)] = 2 · x1
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[a__take(x1, x2)] = 1 · x1 + 2 · x2
[nil] = 0
[take(x1, x2)] = 1 · x1 + 2 · x2
[a__zip(x1, x2)] = 1 · x1 + 2 · x2
[pair(x1, x2)] = 1 · x1 + 2 · x2
[zip(x1, x2)] = 1 · x1 + 2 · x2
[a__tail(x1)] = 2 · x1
[a__repItems(x1)] = 1 + 2 · x1
[repItems(x1)] = 1 + 2 · x1
[pairNs] = 0
[tail(x1)] = 2 · x1
all of the following rules can be deleted.
a__repItems(nil) → nil (10)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__pairNs] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[incr(x1)] = 1 · x1
[oddNs] = 0
[a__oddNs] = 0
[a__incr(x1)] = 1 · x1
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[a__take(x1, x2)] = 2 · x1 + 1 · x2
[nil] = 0
[take(x1, x2)] = 2 · x1 + 1 · x2
[a__zip(x1, x2)] = 1 · x1 + 2 · x2
[pair(x1, x2)] = 1 · x1 + 2 · x2
[zip(x1, x2)] = 1 · x1 + 2 · x2
[a__tail(x1)] = 1 + 1 · x1
[a__repItems(x1)] = 2 · x1
[repItems(x1)] = 2 · x1
[pairNs] = 0
[tail(x1)] = 1 + 1 · x1
all of the following rules can be deleted.
a__tail(cons(X,XS)) → mark(XS) (9)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__pairNs] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[incr(x1)] = 2 · x1
[oddNs] = 0
[a__oddNs] = 0
[a__incr(x1)] = 2 · x1
[s(x1)] = 2 · x1
[mark(x1)] = 1 · x1
[a__take(x1, x2)] = 2 · x1 + 1 · x2
[nil] = 0
[take(x1, x2)] = 2 · x1 + 1 · x2
[a__zip(x1, x2)] = 2 + 2 · x1 + 1 · x2
[pair(x1, x2)] = 2 · x1 + 1 · x2
[zip(x1, x2)] = 2 + 2 · x1 + 1 · x2
[a__repItems(x1)] = 2 · x1
[repItems(x1)] = 2 · x1
[pairNs] = 0
[tail(x1)] = 1 · x1
[a__tail(x1)] = 1 · x1
all of the following rules can be deleted.
a__zip(nil,XS) → nil (6)
a__zip(X,nil) → nil (7)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__pairNs] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[incr(x1)] = 1 · x1
[oddNs] = 0
[a__oddNs] = 0
[a__incr(x1)] = 1 · x1
[s(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[a__take(x1, x2)] = 1 + 1 · x1 + 1 · x2
[nil] = 0
[take(x1, x2)] = 1 + 1 · x1 + 1 · x2
[a__zip(x1, x2)] = 1 · x1 + 2 · x2
[pair(x1, x2)] = 1 · x1 + 2 · x2
[zip(x1, x2)] = 1 · x1 + 2 · x2
[a__repItems(x1)] = 2 · x1
[repItems(x1)] = 2 · x1
[pairNs] = 0
[tail(x1)] = 1 · x1
[a__tail(x1)] = 1 · x1
all of the following rules can be deleted.
a__take(0,XS) → nil (4)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a__oddNs# → a__incr#(a__pairNs) (31)
a__oddNs# → a__pairNs# (32)
a__incr#(cons(X,XS)) → mark#(X) (33)
a__take#(s(N),cons(X,XS)) → mark#(X) (34)
a__zip#(cons(X,XS),cons(Y,YS)) → mark#(X) (35)
a__zip#(cons(X,XS),cons(Y,YS)) → mark#(Y) (36)
a__repItems#(cons(X,XS)) → mark#(X) (37)
mark#(pairNs) → a__pairNs# (38)
mark#(incr(X)) → a__incr#(mark(X)) (39)
mark#(incr(X)) → mark#(X) (40)
mark#(oddNs) → a__oddNs# (41)
mark#(take(X1,X2)) → a__take#(mark(X1),mark(X2)) (42)
mark#(take(X1,X2)) → mark#(X1) (43)
mark#(take(X1,X2)) → mark#(X2) (44)
mark#(zip(X1,X2)) → a__zip#(mark(X1),mark(X2)) (45)
mark#(zip(X1,X2)) → mark#(X1) (46)
mark#(zip(X1,X2)) → mark#(X2) (47)
mark#(tail(X)) → a__tail#(mark(X)) (48)
mark#(tail(X)) → mark#(X) (49)
mark#(repItems(X)) → a__repItems#(mark(X)) (50)
mark#(repItems(X)) → mark#(X) (51)
mark#(cons(X1,X2)) → mark#(X1) (52)
mark#(s(X)) → mark#(X) (53)
mark#(pair(X1,X2)) → mark#(X1) (54)
mark#(pair(X1,X2)) → mark#(X2) (55)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.