Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/25192)

The rewrite relation of the following TRS is considered.

0(x1)	→	1(x1)	(1)
4(5(4(5(x1))))	→	4(4(5(5(x1))))	(2)
5(5(5(5(5(5(4(4(4(4(4(4(x1))))))))))))	→	2(x1)	(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.

4^#(5(4(5(x1))))	→	4^#(5(5(x1)))	(4)
4^#(5(4(5(x1))))	→	5^#(5(x1))	(5)
4^#(5(4(5(x1))))	→	4^#(4(5(5(x1))))	(6)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

4^#(5(4(5(x1)))) → 4^#(4(5(5(x1)))) (6)

4^#(5(4(5(x1)))) → 4^#(5(5(x1))) (4)

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

[0^#(x₁)] = 0

[1(x₁)] = 0

[4(x₁)] = 1

[5(x₁)] = 2439

[4^#(x₁)] = x₁ + 0

[0(x₁)] = 0

[5^#(x₁)] = 0

[2(x₁)] = 0

together with the usable rules

5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) → 2(x1) (3)

4(5(4(5(x1)))) → 4(4(5(5(x1)))) (2)

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