Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci01)

The rewrite relation of the following TRS is considered.

active(eq(0,0)) mark(true) (1)
active(eq(s(X),s(Y))) mark(eq(X,Y)) (2)
active(eq(X,Y)) mark(false) (3)
active(inf(X)) mark(cons(X,inf(s(X)))) (4)
active(take(0,X)) mark(nil) (5)
active(take(s(X),cons(Y,L))) mark(cons(Y,take(X,L))) (6)
active(length(nil)) mark(0) (7)
active(length(cons(X,L))) mark(s(length(L))) (8)
active(inf(X)) inf(active(X)) (9)
active(take(X1,X2)) take(active(X1),X2) (10)
active(take(X1,X2)) take(X1,active(X2)) (11)
active(length(X)) length(active(X)) (12)
inf(mark(X)) mark(inf(X)) (13)
take(mark(X1),X2) mark(take(X1,X2)) (14)
take(X1,mark(X2)) mark(take(X1,X2)) (15)
length(mark(X)) mark(length(X)) (16)
proper(eq(X1,X2)) eq(proper(X1),proper(X2)) (17)
proper(0) ok(0) (18)
proper(true) ok(true) (19)
proper(s(X)) s(proper(X)) (20)
proper(false) ok(false) (21)
proper(inf(X)) inf(proper(X)) (22)
proper(cons(any(X1),X2)) cons(any(any(proper(X1))),any(proper(X2))) (23)
proper(take(X1,X2)) take(proper(X1),proper(X2)) (24)
proper(nil) ok(nil) (25)
proper(length(X)) length(proper(X)) (26)
eq(ok(X1),ok(X2)) ok(eq(X1,X2)) (27)
s(ok(X)) ok(s(X)) (28)
inf(ok(X)) ok(inf(X)) (29)
cons(ok(X1),ok(X2)) ok(cons(X1,X2)) (30)
take(ok(X1),ok(X2)) ok(take(X1,X2)) (31)
length(ok(X)) ok(length(X)) (32)
top(mark(X)) top(proper(X)) (33)
top(ok(X)) top(active(X)) (34)
any(X) s(X) (35)
any(proper(X)) any(any(any(X))) (36)

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.
inf#(ok(X)) inf#(X) (37)
any#(proper(X)) any#(any(any(X))) (38)
top#(mark(X)) top#(proper(X)) (39)
top#(ok(X)) active#(X) (40)
length#(mark(X)) length#(X) (41)
proper#(length(X)) proper#(X) (42)
proper#(length(X)) length#(proper(X)) (43)
proper#(eq(X1,X2)) eq#(proper(X1),proper(X2)) (44)
active#(length(cons(X,L))) s#(length(L)) (45)
active#(length(cons(X,L))) length#(L) (46)
proper#(eq(X1,X2)) proper#(X1) (47)
inf#(mark(X)) inf#(X) (48)
length#(ok(X)) length#(X) (49)
active#(inf(X)) inf#(s(X)) (50)
proper#(take(X1,X2)) proper#(X2) (51)
active#(take(X1,X2)) take#(X1,active(X2)) (52)
proper#(take(X1,X2)) take#(proper(X1),proper(X2)) (53)
cons#(ok(X1),ok(X2)) cons#(X1,X2) (54)
take#(mark(X1),X2) take#(X1,X2) (55)
any#(proper(X)) any#(X) (56)
proper#(take(X1,X2)) proper#(X1) (57)
s#(ok(X)) s#(X) (58)
proper#(cons(any(X1),X2)) cons#(any(any(proper(X1))),any(proper(X2))) (59)
top#(mark(X)) proper#(X) (60)
active#(inf(X)) s#(X) (61)
take#(X1,mark(X2)) take#(X1,X2) (62)
proper#(s(X)) s#(proper(X)) (63)
active#(length(X)) length#(active(X)) (64)
active#(inf(X)) inf#(active(X)) (65)
proper#(eq(X1,X2)) proper#(X2) (66)
active#(take(X1,X2)) active#(X2) (67)
proper#(inf(X)) proper#(X) (68)
active#(take(s(X),cons(Y,L))) take#(X,L) (69)
any#(proper(X)) any#(any(X)) (70)
active#(take(X1,X2)) active#(X1) (71)
take#(ok(X1),ok(X2)) take#(X1,X2) (72)
top#(ok(X)) top#(active(X)) (73)
active#(take(X1,X2)) take#(active(X1),X2) (74)
proper#(cons(any(X1),X2)) proper#(X1) (75)
proper#(inf(X)) inf#(proper(X)) (76)
proper#(cons(any(X1),X2)) proper#(X2) (77)
proper#(s(X)) proper#(X) (78)
eq#(ok(X1),ok(X2)) eq#(X1,X2) (79)
active#(length(X)) active#(X) (80)
proper#(cons(any(X1),X2)) any#(proper(X1)) (81)
any#(X) s#(X) (82)
active#(eq(s(X),s(Y))) eq#(X,Y) (83)
active#(inf(X)) active#(X) (84)
proper#(cons(any(X1),X2)) any#(any(proper(X1))) (85)
active#(take(s(X),cons(Y,L))) cons#(Y,take(X,L)) (86)
active#(inf(X)) cons#(X,inf(s(X))) (87)
proper#(cons(any(X1),X2)) any#(proper(X2)) (88)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.