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.

The 1^st component contains the pair

u21^#(ack_out(n),m)	→	ack_in^#(m,n)	(11)
ack_in^#(s(m),s(n))	→	u21^#(ack_in(s(m),n),m)	(10)
ack_in^#(s(m),s(n))	→	ack_in^#(s(m),n)	(9)
ack_in^#(s(m),0)	→	ack_in^#(m,s(0))	(7)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

u21^#(ack_out(n),m)	→	ack_in^#(m,n)	(11)

2	≥	1
1	>	2
ack_in^#(s(m),s(n))	→	u21^#(ack_in(s(m),n),m)	(10)

1	>	2
ack_in^#(s(m),s(n))	→	ack_in^#(s(m),n)	(9)

2	>	2
1	≥	1
ack_in^#(s(m),0)	→	ack_in^#(m,s(0))	(7)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.