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 ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

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

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.