Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann14)

The rewrite relation of the following TRS is considered.

empty(nil) true (1)
empty(cons(x,y)) false (2)
tail(nil) nil (3)
tail(cons(x,y)) y (4)
head(cons(x,y)) x (5)
zero(0) true (6)
zero(s(x)) false (7)
p(0) 0 (8)
p(s(0)) 0 (9)
p(s(s(x))) s(p(s(x))) (10)
intlist(x) if_intlist(empty(x),x) (11)
if_intlist(true,x) nil (12)
if_intlist(false,x) cons(s(head(x)),intlist(tail(x))) (13)
int(x,y) if_int(zero(x),zero(y),x,y) (14)
if_int(true,b,x,y) if1(b,x,y) (15)
if_int(false,b,x,y) if2(b,x,y) (16)
if1(true,x,y) cons(0,nil) (17)
if1(false,x,y) cons(0,int(s(0),y)) (18)
if2(true,x,y) nil (19)
if2(false,x,y) intlist(int(p(x),p(y))) (20)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
p#(s(s(x))) p#(s(x)) (21)
intlist#(x) if_intlist#(empty(x),x) (22)
intlist#(x) empty#(x) (23)
if_intlist#(false,x) head#(x) (24)
if_intlist#(false,x) intlist#(tail(x)) (25)
if_intlist#(false,x) tail#(x) (26)
int#(x,y) if_int#(zero(x),zero(y),x,y) (27)
int#(x,y) zero#(x) (28)
int#(x,y) zero#(y) (29)
if_int#(true,b,x,y) if1#(b,x,y) (30)
if_int#(false,b,x,y) if2#(b,x,y) (31)
if1#(false,x,y) int#(s(0),y) (32)
if2#(false,x,y) intlist#(int(p(x),p(y))) (33)
if2#(false,x,y) int#(p(x),p(y)) (34)
if2#(false,x,y) p#(x) (35)
if2#(false,x,y) p#(y) (36)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.