Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/aprove00)

The rewrite relation of the following TRS is considered.

a(s(x1)) s(s(s(p(s(b(p(p(s(s(x1)))))))))) (1)
b(s(x1)) s(s(s(p(p(s(s(c(p(s(p(s(x1)))))))))))) (2)
c(s(x1)) p(s(p(s(a(p(s(p(s(x1))))))))) (3)
p(p(s(x1))) p(x1) (4)
p(s(x1)) x1 (5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a#(s(x1)) p#(s(b(p(p(s(s(x1))))))) (6)
a#(s(x1)) b#(p(p(s(s(x1))))) (7)
a#(s(x1)) p#(p(s(s(x1)))) (8)
a#(s(x1)) p#(s(s(x1))) (9)
b#(s(x1)) p#(p(s(s(c(p(s(p(s(x1))))))))) (10)
b#(s(x1)) p#(s(s(c(p(s(p(s(x1)))))))) (11)
b#(s(x1)) c#(p(s(p(s(x1))))) (12)
b#(s(x1)) p#(s(p(s(x1)))) (13)
b#(s(x1)) p#(s(x1)) (14)
c#(s(x1)) p#(s(p(s(a(p(s(p(s(x1))))))))) (15)
c#(s(x1)) p#(s(a(p(s(p(s(x1))))))) (16)
c#(s(x1)) a#(p(s(p(s(x1))))) (17)
c#(s(x1)) p#(s(p(s(x1)))) (18)
c#(s(x1)) p#(s(x1)) (19)
p#(p(s(x1))) p#(x1) (20)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.