Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z094)

The rewrite relation of the following TRS is considered.

f(x1) → n(c(c(x1))) (1)
c(f(x1)) → f(c(c(x1))) (2)
c(c(x1)) → c(x1) (3)
n(s(x1)) → f(s(s(x1))) (4)
n(f(x1)) → f(n(x1)) (5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
n#(f(x1)) → n#(x1) (6)
n#(f(x1)) → f#(n(x1)) (7)
n#(s(x1)) → f#(s(s(x1))) (8)
f#(x1) → n#(c(c(x1))) (9)
f#(x1) → c#(x1) (10)
f#(x1) → c#(c(x1)) (11)
c#(f(x1)) → f#(c(c(x1))) (12)
c#(f(x1)) → c#(x1) (13)
c#(f(x1)) → c#(c(x1)) (14)

1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[n(x1)] = x1 +
2
[f(x1)] = x1 +
2
[c(x1)] = x1 +
0
[s(x1)] = x1 +
0
[n#(x1)] = x1 +
2
[f#(x1)] = x1 +
2
[c#(x1)] = x1 +
1
together with the usable rules
f(x1) → n(c(c(x1))) (1)
c(f(x1)) → f(c(c(x1))) (2)
c(c(x1)) → c(x1) (3)
n(s(x1)) → f(s(s(x1))) (4)
n(f(x1)) → f(n(x1)) (5)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
n#(f(x1)) → n#(x1) (6)
f#(x1) → c#(x1) (10)
f#(x1) → c#(c(x1)) (11)
c#(f(x1)) → f#(c(c(x1))) (12)
c#(f(x1)) → c#(x1) (13)
c#(f(x1)) → c#(c(x1)) (14)
and no rules could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.