Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z125)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
f(x1) → a(n(c(n(x1)))) (7)
f(c(x1)) → c(a(n(f(x1)))) (8)
a(n(x1)) → c(x1) (9)
c(c(x1)) → c(x1) (4)
s(n(x1)) → s(s(f(x1))) (10)
f(n(x1)) → n(f(x1)) (11)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(x1) → c#(n(x1)) (12)
f#(x1) → a#(n(c(n(x1)))) (13)
f#(n(x1)) → f#(x1) (14)
f#(c(x1)) → f#(x1) (15)
f#(c(x1)) → c#(a(n(f(x1)))) (16)
f#(c(x1)) → a#(n(f(x1))) (17)
a#(n(x1)) → c#(x1) (18)
s#(n(x1)) → f#(x1) (19)
s#(n(x1)) → s#(f(x1)) (20)
s#(n(x1)) → s#(s(f(x1))) (21)

1.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 +
0
[f(x1)] = x1 +
0
[c(x1)] = x1 +
0
[a(x1)] = x1 +
0
[s(x1)] = x1 +
0
[f#(x1)] = x1 +
2
[c#(x1)] = x1 +
0
[a#(x1)] = x1 +
1
[s#(x1)] = x1 +
3
together with the usable rules
f(x1) → a(n(c(n(x1)))) (7)
f(c(x1)) → c(a(n(f(x1)))) (8)
a(n(x1)) → c(x1) (9)
c(c(x1)) → c(x1) (4)
s(n(x1)) → s(s(f(x1))) (10)
f(n(x1)) → n(f(x1)) (11)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
f#(x1) → c#(n(x1)) (12)
f#(x1) → a#(n(c(n(x1)))) (13)
f#(c(x1)) → c#(a(n(f(x1)))) (16)
f#(c(x1)) → a#(n(f(x1))) (17)
a#(n(x1)) → c#(x1) (18)
s#(n(x1)) → f#(x1) (19)
and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.