Certification Problem

Input (TPDB TRS_Standard/SK90/2.51)

The rewrite relation of the following TRS is considered.

ack(0,y)	→	s(y)	(1)
ack(s(x),0)	→	ack(x,s(0))	(2)
ack(s(x),s(y))	→	ack(x,ack(s(x),y))	(3)

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^#(s(x),s(y))	→	ack^#(x,ack(s(x),y))	(4)
ack^#(s(x),s(y))	→	ack^#(s(x),y)	(5)
ack^#(s(x),0)	→	ack^#(x,s(0))	(6)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

ack^#(s(x),0) → ack^#(x,s(0)) (6)

ack^#(s(x),s(y)) → ack^#(s(x),y) (5)

ack^#(s(x),s(y)) → ack^#(x,ack(s(x),y)) (4)

1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation

[s(x₁)] = x₁ + 1

[ack(x₁, x₂)] = x₂ + 2

[0] = 1

[ack^#(x₁, x₂)] = x₁ + 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

ack^#(s(x),0) → ack^#(x,s(0)) (6)

ack^#(s(x),s(y)) → ack^#(x,ack(s(x),y)) (4)

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^#(s(x),s(y)) → ack^#(s(x),y) (5)
  
  1.1.1.1.1 Reduction Pair Processor with Usable Rules
  Using the Max-polynomial interpretation
  
  [s(x₁)] = x₁ + 1
  
  [ack(x₁, x₂)] = max(0)
  
  [0] = 0
  
  [ack^#(x₁, x₂)] = max(x₂ + 1, 0)
  
  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair
  ack^#(s(x),s(y)) → ack^#(s(x),y) (5)
  could be deleted.
  1.1.1.1.1.1 Dependency Graph Processor
  
  The dependency pairs are split into 0 components.