Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/26226)

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)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ 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))))))))))	(10)
1(2(1(0(x1))))	→	2(1(0(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(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(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(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(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(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(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(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))	(18)

1.1 Bounds

The given TRS is match-(raise)-bounded by 3. This is shown by the following automaton.

final states:

{0, 1, 2}

transitions:

1₀(0)	→	0
1₀(1)	→	0
1₀(2)	→	0
2₀(0)	→	1
2₀(1)	→	1
2₀(2)	→	1
0₀(0)	→	2
0₀(1)	→	2
0₀(2)	→	2
1₁(0)	→	10
2₁(10)	→	9
1₁(9)	→	8
1₁(8)	→	7
0₁(7)	→	6
1₁(6)	→	3
2₁(3)	→	5
0₁(5)	→	4
1₁(4)	→	3
2₁(3)	→	0
1₁(1)	→	10
1₁(2)	→	10
1₁(7)	→	10
1₁(5)	→	10
1₂(7)	→	18
2₂(18)	→	17
1₂(17)	→	16
1₂(16)	→	15
0₂(15)	→	14
1₂(14)	→	11
2₂(11)	→	13
0₂(13)	→	12
1₂(12)	→	11
2₂(11)	→	10
1₂(5)	→	18
1₂(15)	→	18
1₃(15)	→	26
2₃(26)	→	25
1₃(25)	→	24
1₃(24)	→	23
0₃(23)	→	22
1₃(22)	→	19
2₃(19)	→	21
0₃(21)	→	20
1₃(20)	→	19
2₃(19)	→	18
1₃(13)	→	26
5	→	10
5	→	8
13	→	7
13	→	18
21	→	26