Certification Problem

Input (TPDB TRS_Standard/CiME_04/ack_prolog)

The rewrite relation of the following TRS is considered.

ack_in(0,n) ack_out(s(n)) (1)
ack_in(s(m),0) u11(ack_in(m,s(0))) (2)
u11(ack_out(n)) ack_out(n) (3)
ack_in(s(m),s(n)) u21(ack_in(s(m),n),m) (4)
u21(ack_out(n),m) u22(ack_in(m,n)) (5)
u22(ack_out(n)) ack_out(n) (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.
ack_in#(s(m),0) ack_in#(m,s(0)) (7)
ack_in#(s(m),0) u11#(ack_in(m,s(0))) (8)
ack_in#(s(m),s(n)) ack_in#(s(m),n) (9)
ack_in#(s(m),s(n)) u21#(ack_in(s(m),n),m) (10)
u21#(ack_out(n),m) ack_in#(m,n) (11)
u21#(ack_out(n),m) u22#(ack_in(m,n)) (12)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.