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 NaTT @ 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),s(n))	→	ack_in^#(s(m),n)	(8)
ack_in^#(s(m),s(n))	→	u21^#(ack_in(s(m),n),m)	(9)
u21^#(ack_out(n),m)	→	u22^#(ack_in(m,n))	(10)
ack_in^#(s(m),0)	→	u11^#(ack_in(m,s(0)))	(11)
u21^#(ack_out(n),m)	→	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)	(12)
ack_in^#(s(m),s(n))	→	ack_in^#(s(m),n)	(8)
ack_in^#(s(m),s(n))	→	u21^#(ack_in(s(m),n),m)	(9)
ack_in^#(s(m),0)	→	ack_in^#(m,s(0))	(7)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[u22^#(x₁)]	=	0
[ack_in^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 2
[u21^#(x₁, x₂)]	=	x₂ + 1
[u11^#(x₁)]	=	0
[0]	=	1
[ack_out(x₁)]	=	11298
[u11(x₁)]	=	x₁ + 3
[u21(x₁, x₂)]	=	11296
[u22(x₁)]	=	11297
[ack_in(x₁, x₂)]	=	x₁ + 11293

together with the usable rule

u11(ack_out(n))

→

ack_out(n)

(3)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

ack_in^#(s(m),s(n))

→

ack_in^#(s(m),n)

(8)

1.1.1.1.1 Reduction Pair Processor with Usable Rules