Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/26069)

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)

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

1.1 Bounds

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

final states:

{4}

transitions:

23	→	37
23	→	54
89	→	78
87	→	72
87	→	90
87	→	78
87	→	89
34	→	17
55	→	40
20	→	71
49	→	17
49	→	69
49	→	40
49	→	20
49	→	38
49	→	34
49	→	55
26	→	4
26	→	27
26	→	19
26	→	17
38	→	17
91	→	85
72	→	40
4	→	16
28	→	24
104	→	78
69	→	77
46	→	88
43	→	103
27	→	33
27	→	39
70	→	47
1₂(41)	→	42
1₂(44)	→	45
1₂(71)	→	72
1₂(39)	→	40
1₂(42)	→	43
1₂(47)	→	48
1₂(54)	→	55
0₂(46)	→	47
0₂(69)	→	70
0₂(43)	→	44
2₂(45)	→	46
2₂(40)	→	41
2₂(48)	→	49
2₀(4)	→	4
0₀(4)	→	4
2₃(78)	→	79
2₃(86)	→	87
2₃(83)	→	84
1₃(77)	→	78
1₃(88)	→	89
1₃(79)	→	80
1₃(85)	→	86
1₃(80)	→	81
1₃(82)	→	83
1₃(103)	→	104
1₀(4)	→	4
1₁(19)	→	20
1₁(37)	→	38
1₁(18)	→	19
1₁(24)	→	25
1₁(16)	→	17
1₁(33)	→	34
1₁(21)	→	22
0₁(23)	→	24
0₁(27)	→	28
0₁(20)	→	21
0₃(84)	→	85
0₃(90)	→	91
0₃(81)	→	82
2₁(22)	→	23
2₁(17)	→	18
2₁(25)	→	26

The automaton is closed under rewriting as it is compatible.