Certification Problem

Input (TPDB TRS_Standard/Beerendonk_07/7)

The rewrite relation of the following TRS is considered.

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

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.