Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/Ex1_Luc04b_GM)

The rewrite relation of the following TRS is considered.

a__nats cons(0,incr(nats)) (1)
a__pairs cons(0,incr(odds)) (2)
a__odds a__incr(a__pairs) (3)
a__incr(cons(X,XS)) cons(s(mark(X)),incr(XS)) (4)
a__head(cons(X,XS)) mark(X) (5)
a__tail(cons(X,XS)) mark(XS) (6)
mark(nats) a__nats (7)
mark(pairs) a__pairs (8)
mark(odds) a__odds (9)
mark(incr(X)) a__incr(mark(X)) (10)
mark(head(X)) a__head(mark(X)) (11)
mark(tail(X)) a__tail(mark(X)) (12)
mark(0) 0 (13)
mark(s(X)) s(mark(X)) (14)
mark(nil) nil (15)
mark(cons(X1,X2)) cons(mark(X1),X2) (16)
a__nats nats (17)
a__pairs pairs (18)
a__odds odds (19)
a__incr(X) incr(X) (20)
a__head(X) head(X) (21)
a__tail(X) tail(X) (22)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
mark#(odds) a__odds# (23)
mark#(tail(X)) mark#(X) (24)
a__odds# a__incr#(a__pairs) (25)
mark#(incr(X)) a__incr#(mark(X)) (26)
a__head#(cons(X,XS)) mark#(X) (27)
mark#(cons(X1,X2)) mark#(X1) (28)
a__odds# a__pairs# (29)
mark#(s(X)) mark#(X) (30)
mark#(incr(X)) mark#(X) (31)
mark#(tail(X)) a__tail#(mark(X)) (32)
a__incr#(cons(X,XS)) mark#(X) (33)
mark#(head(X)) a__head#(mark(X)) (34)
a__tail#(cons(X,XS)) mark#(XS) (35)
mark#(nats) a__nats# (36)
mark#(pairs) a__pairs# (37)
mark#(head(X)) mark#(X) (38)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.