Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe12)

The rewrite relation of the following TRS is considered.

g(s(x),s(y)) if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) (1)
n(0,y) 0 (2)
n(x,0) 0 (3)
n(s(x),s(y)) s(n(x,y)) (4)
m(0,y) y (5)
m(x,0) x (6)
m(s(x),s(y)) s(m(x,y)) (7)
k(0,s(y)) 0 (8)
k(s(x),s(y)) s(k(minus(x,y),s(y))) (9)
t(x) p(x,x) (10)
p(s(x),s(y)) s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) (11)
p(s(x),x) p(if(gt(x,x),id(x),id(x)),s(x)) (12)
p(0,y) y (13)
p(id(x),s(y)) s(p(x,if(gt(s(y),y),y,s(y)))) (14)
minus(x,0) x (15)
minus(s(x),s(y)) minus(x,y) (16)
id(x) x (17)
if(true,x,y) x (18)
if(false,x,y) y (19)
not(x) if(x,false,true) (20)
and(x,false) false (21)
and(true,true) true (22)
f(0) true (23)
f(s(x)) h(x) (24)
h(0) false (25)
h(s(x)) f(x) (26)
gt(s(x),0) true (27)
gt(0,y) false (28)
gt(s(x),s(y)) gt(x,y) (29)

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.
g#(s(x),s(y)) g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) (30)
g#(s(x),s(y)) n#(s(x),s(y)) (31)
g#(s(x),s(y)) k#(n(s(x),s(y)),s(s(0))) (32)
g#(s(x),s(y)) n#(x,y) (33)
g#(s(x),s(y)) m#(x,y) (34)
g#(s(x),s(y)) minus#(m(x,y),n(x,y)) (35)
g#(s(x),s(y)) k#(minus(m(x,y),n(x,y)),s(s(0))) (36)
g#(s(x),s(y)) g#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0)))) (37)
g#(s(x),s(y)) t#(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))) (38)
g#(s(x),s(y)) f#(s(y)) (39)
g#(s(x),s(y)) f#(s(x)) (40)
g#(s(x),s(y)) and#(f(s(x)),f(s(y))) (41)
g#(s(x),s(y)) if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) (42)
n#(s(x),s(y)) n#(x,y) (43)
m#(s(x),s(y)) m#(x,y) (44)
k#(s(x),s(y)) minus#(x,y) (45)
k#(s(x),s(y)) k#(minus(x,y),s(y)) (46)
t#(x) p#(x,x) (47)
p#(s(x),s(y)) id#(y) (48)
p#(s(x),s(y)) id#(x) (49)
p#(s(x),s(y)) not#(gt(x,y)) (50)
p#(s(x),s(y)) if#(not(gt(x,y)),id(x),id(y)) (51)
p#(s(x),s(y)) gt#(x,y) (52)
p#(s(x),s(y)) if#(gt(x,y),x,y) (53)
p#(s(x),s(y)) p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) (54)
p#(s(x),x) id#(x) (55)
p#(s(x),x) gt#(x,x) (56)
p#(s(x),x) if#(gt(x,x),id(x),id(x)) (57)
p#(s(x),x) p#(if(gt(x,x),id(x),id(x)),s(x)) (58)
p#(id(x),s(y)) gt#(s(y),y) (59)
p#(id(x),s(y)) if#(gt(s(y),y),y,s(y)) (60)
p#(id(x),s(y)) p#(x,if(gt(s(y),y),y,s(y))) (61)
minus#(s(x),s(y)) minus#(x,y) (62)
not#(x) if#(x,false,true) (63)
f#(s(x)) h#(x) (64)
h#(s(x)) f#(x) (65)
gt#(s(x),s(y)) gt#(x,y) (66)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.