Certification Problem

Input (TPDB TRS_Standard/CiME_04/big)

The rewrite relation of the following TRS is considered.

0(#) # (1)
+(x,#) x (2)
+(#,x) x (3)
+(0(x),0(y)) 0(+(x,y)) (4)
+(0(x),1(y)) 1(+(x,y)) (5)
+(1(x),0(y)) 1(+(x,y)) (6)
+(1(x),1(y)) 0(+(+(x,y),1(#))) (7)
+(+(x,y),z) +(x,+(y,z)) (8)
-(#,x) # (9)
-(x,#) x (10)
-(0(x),0(y)) 0(-(x,y)) (11)
-(0(x),1(y)) 1(-(-(x,y),1(#))) (12)
-(1(x),0(y)) 1(-(x,y)) (13)
-(1(x),1(y)) 0(-(x,y)) (14)
not(true) false (15)
not(false) true (16)
if(true,x,y) x (17)
if(false,x,y) y (18)
eq(#,#) true (19)
eq(#,1(y)) false (20)
eq(1(x),#) false (21)
eq(#,0(y)) eq(#,y) (22)
eq(0(x),#) eq(x,#) (23)
eq(1(x),1(y)) eq(x,y) (24)
eq(0(x),1(y)) false (25)
eq(1(x),0(y)) false (26)
eq(0(x),0(y)) eq(x,y) (27)
ge(0(x),0(y)) ge(x,y) (28)
ge(0(x),1(y)) not(ge(y,x)) (29)
ge(1(x),0(y)) ge(x,y) (30)
ge(1(x),1(y)) ge(x,y) (31)
ge(x,#) true (32)
ge(#,0(x)) ge(#,x) (33)
ge(#,1(x)) false (34)
log(x) -(log'(x),1(#)) (35)
log'(#) # (36)
log'(1(x)) +(log'(x),1(#)) (37)
log'(0(x)) if(ge(x,1(#)),+(log'(x),1(#)),#) (38)
*(#,x) # (39)
*(0(x),y) 0(*(x,y)) (40)
*(1(x),y) +(0(*(x,y)),y) (41)
*(*(x,y),z) *(x,*(y,z)) (42)
*(x,+(y,z)) +(*(x,y),*(x,z)) (43)
app(nil,l) l (44)
app(cons(x,l1),l2) cons(x,app(l1,l2)) (45)
sum(nil) 0(#) (46)
sum(cons(x,l)) +(x,sum(l)) (47)
sum(app(l1,l2)) +(sum(l1),sum(l2)) (48)
prod(nil) 1(#) (49)
prod(cons(x,l)) *(x,prod(l)) (50)
prod(app(l1,l2)) *(prod(l1),prod(l2)) (51)
mem(x,nil) false (52)
mem(x,cons(y,l)) if(eq(x,y),true,mem(x,l)) (53)
inter(x,nil) nil (54)
inter(nil,x) nil (55)
inter(app(l1,l2),l3) app(inter(l1,l3),inter(l2,l3)) (56)
inter(l1,app(l2,l3)) app(inter(l1,l2),inter(l1,l3)) (57)
inter(cons(x,l1),l2) ifinter(mem(x,l2),x,l1,l2) (58)
inter(l1,cons(x,l2)) ifinter(mem(x,l1),x,l2,l1) (59)
ifinter(true,x,l1,l2) cons(x,inter(l1,l2)) (60)
ifinter(false,x,l1,l2) inter(l1,l2) (61)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
+#(0(x),0(y)) 0#(+(x,y)) (62)
+#(0(x),0(y)) +#(x,y) (63)
+#(0(x),1(y)) +#(x,y) (64)
+#(1(x),0(y)) +#(x,y) (65)
+#(1(x),1(y)) 0#(+(+(x,y),1(#))) (66)
+#(1(x),1(y)) +#(+(x,y),1(#)) (67)
+#(1(x),1(y)) +#(x,y) (68)
+#(+(x,y),z) +#(x,+(y,z)) (69)
+#(+(x,y),z) +#(y,z) (70)
-#(0(x),0(y)) 0#(-(x,y)) (71)
-#(0(x),0(y)) -#(x,y) (72)
-#(0(x),1(y)) -#(-(x,y),1(#)) (73)
-#(0(x),1(y)) -#(x,y) (74)
-#(1(x),0(y)) -#(x,y) (75)
-#(1(x),1(y)) 0#(-(x,y)) (76)
-#(1(x),1(y)) -#(x,y) (77)
eq#(#,0(y)) eq#(#,y) (78)
eq#(0(x),#) eq#(x,#) (79)
eq#(1(x),1(y)) eq#(x,y) (80)
eq#(0(x),0(y)) eq#(x,y) (81)
ge#(0(x),0(y)) ge#(x,y) (82)
ge#(0(x),1(y)) not#(ge(y,x)) (83)
ge#(0(x),1(y)) ge#(y,x) (84)
ge#(1(x),0(y)) ge#(x,y) (85)
ge#(1(x),1(y)) ge#(x,y) (86)
ge#(#,0(x)) ge#(#,x) (87)
log#(x) -#(log'(x),1(#)) (88)
log#(x) log'#(x) (89)
log'#(1(x)) +#(log'(x),1(#)) (90)
log'#(1(x)) log'#(x) (91)
log'#(0(x)) if#(ge(x,1(#)),+(log'(x),1(#)),#) (92)
log'#(0(x)) ge#(x,1(#)) (93)
log'#(0(x)) +#(log'(x),1(#)) (94)
log'#(0(x)) log'#(x) (95)
*#(0(x),y) 0#(*(x,y)) (96)
*#(0(x),y) *#(x,y) (97)
*#(1(x),y) +#(0(*(x,y)),y) (98)
*#(1(x),y) 0#(*(x,y)) (99)
*#(1(x),y) *#(x,y) (100)
*#(*(x,y),z) *#(x,*(y,z)) (101)
*#(*(x,y),z) *#(y,z) (102)
*#(x,+(y,z)) +#(*(x,y),*(x,z)) (103)
*#(x,+(y,z)) *#(x,y) (104)
*#(x,+(y,z)) *#(x,z) (105)
app#(cons(x,l1),l2) app#(l1,l2) (106)
sum#(nil) 0#(#) (107)
sum#(cons(x,l)) +#(x,sum(l)) (108)
sum#(cons(x,l)) sum#(l) (109)
sum#(app(l1,l2)) +#(sum(l1),sum(l2)) (110)
sum#(app(l1,l2)) sum#(l1) (111)
sum#(app(l1,l2)) sum#(l2) (112)
prod#(cons(x,l)) *#(x,prod(l)) (113)
prod#(cons(x,l)) prod#(l) (114)
prod#(app(l1,l2)) *#(prod(l1),prod(l2)) (115)
prod#(app(l1,l2)) prod#(l1) (116)
prod#(app(l1,l2)) prod#(l2) (117)
mem#(x,cons(y,l)) if#(eq(x,y),true,mem(x,l)) (118)
mem#(x,cons(y,l)) eq#(x,y) (119)
mem#(x,cons(y,l)) mem#(x,l) (120)
inter#(app(l1,l2),l3) app#(inter(l1,l3),inter(l2,l3)) (121)
inter#(app(l1,l2),l3) inter#(l1,l3) (122)
inter#(app(l1,l2),l3) inter#(l2,l3) (123)
inter#(l1,app(l2,l3)) app#(inter(l1,l2),inter(l1,l3)) (124)
inter#(l1,app(l2,l3)) inter#(l1,l2) (125)
inter#(l1,app(l2,l3)) inter#(l1,l3) (126)
inter#(cons(x,l1),l2) ifinter#(mem(x,l2),x,l1,l2) (127)
inter#(cons(x,l1),l2) mem#(x,l2) (128)
inter#(l1,cons(x,l2)) ifinter#(mem(x,l1),x,l2,l1) (129)
inter#(l1,cons(x,l2)) mem#(x,l1) (130)
ifinter#(true,x,l1,l2) inter#(l1,l2) (131)
ifinter#(false,x,l1,l2) inter#(l1,l2) (132)

1.1 Dependency Graph Processor

The dependency pairs are split into 14 components.