Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann37)

The rewrite relation of the following TRS is considered.

eq(0,0) → true (1)
eq(0,s(x)) → false (2)
eq(s(x),0) → false (3)
eq(s(x),s(y)) → eq(x,y) (4)
or(true,y) → true (5)
or(false,y) → y (6)
and(true,y) → y (7)
and(false,y) → false (8)
size(empty) → 0 (9)
size(edge(x,y,i)) → s(size(i)) (10)
le(0,y) → true (11)
le(s(x),0) → false (12)
le(s(x),s(y)) → le(x,y) (13)
reachable(x,y,i) → reach(x,y,0,i,i) (14)
reach(x,y,c,i,j) → if1(eq(x,y),x,y,c,i,j) (15)
if1(true,x,y,c,i,j) → true (16)
if1(false,x,y,c,i,j) → if2(le(c,size(j)),x,y,c,i,j) (17)
if2(false,x,y,c,i,j) → false (18)
if2(true,x,y,c,empty,j) → false (19)
if2(true,x,y,c,edge(u,v,i),j) → or(if2(true,x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j))) (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.
eq#(s(x),s(y)) → eq#(x,y) (21)
size#(edge(x,y,i)) → size#(i) (22)
le#(s(x),s(y)) → le#(x,y) (23)
reachable#(x,y,i) → reach#(x,y,0,i,i) (24)
reach#(x,y,c,i,j) → if1#(eq(x,y),x,y,c,i,j) (25)
reach#(x,y,c,i,j) → eq#(x,y) (26)
if1#(false,x,y,c,i,j) → if2#(le(c,size(j)),x,y,c,i,j) (27)
if1#(false,x,y,c,i,j) → le#(c,size(j)) (28)
if1#(false,x,y,c,i,j) → size#(j) (29)
if2#(true,x,y,c,edge(u,v,i),j) → or#(if2(true,x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j))) (30)
if2#(true,x,y,c,edge(u,v,i),j) → if2#(true,x,y,c,i,j) (31)
if2#(true,x,y,c,edge(u,v,i),j) → and#(eq(x,u),reach(v,y,s(c),j,j)) (32)
if2#(true,x,y,c,edge(u,v,i),j) → eq#(x,u) (33)
if2#(true,x,y,c,edge(u,v,i),j) → reach#(v,y,s(c),j,j) (34)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.