Certification Problem

Input (TPDB TRS_Standard/Beerendonk_07/6)

The rewrite relation of the following TRS is considered.

cond(true,x) cond(odd(x),p(x)) (1)
odd(0) false (2)
odd(s(0)) true (3)
odd(s(s(x))) odd(x) (4)
p(0) 0 (5)
p(s(x)) x (6)

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.
cond#(true,x) p#(x) (7)
cond#(true,x) odd#(x) (8)
cond#(true,x) cond#(odd(x),p(x)) (9)
odd#(s(s(x))) odd#(x) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.