Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/26291)

The rewrite relation of the following TRS is considered.

0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(x1))))))))))	(1)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))	(2)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))	(3)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))	(4)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))	(5)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))	(6)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))	(7)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))	(8)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))	(9)
0(1(2(1(x1))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))	(10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

1(2(1(0(x1))))	→	2(1(0(2(1(0(1(1(2(1(x1))))))))))	(11)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))	(12)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))	(13)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))	(14)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))	(15)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))	(16)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))	(17)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))	(18)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))	(19)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))	(20)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

1^#(2(1(0(x1))))	→	1^#(x1)	(21)
1^#(2(1(0(x1))))	→	1^#(2(1(x1)))	(22)
1^#(2(1(0(x1))))	→	1^#(1(2(1(x1))))	(23)
1^#(2(1(0(x1))))	→	1^#(0(1(1(2(1(x1))))))	(24)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(1(1(2(1(x1)))))))))	(25)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))	(26)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))	(27)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))	(28)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))	(29)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))	(30)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))	(31)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))	(32)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))	(33)
1^#(2(1(0(x1))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))	(34)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

1^#(2(1(0(x1))))	→	1^#(2(1(x1)))	(22)
1^#(2(1(0(x1))))	→	1^#(1(2(1(x1))))	(23)
1^#(2(1(0(x1))))	→	1^#(x1)	(21)

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[2(x₁)]	=	-4 · x₁ + 1
[1^#(x₁)]	=	0 · x₁ + 0
[1(x₁)]	=	0 · x₁ + -∞
[0(x₁)]	=	4 · x₁ + 6

together with the usable rules

1(2(1(0(x1))))	→	2(1(0(2(1(0(1(1(2(1(x1))))))))))	(11)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))	(12)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))	(13)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))	(14)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))	(15)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))	(16)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))	(17)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))	(18)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))	(19)
1(2(1(0(x1))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))	(20)

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

1^#(2(1(0(x1))))	→	1^#(2(1(x1)))	(22)
1^#(2(1(0(x1))))	→	1^#(1(2(1(x1))))	(23)

could be deleted.

1.1.1.1.1 Size-Change Termination

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

1^#(2(1(0(x1))))	→	1^#(x1)	(21)

1	>	1

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