YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(b(b(x0))))

→

b(b(b(a(a(a(a(a(x0))))))))

Proof

1 String Reversal

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

b(b(a(a(x0))))

→

a(a(a(a(a(b(b(b(x0))))))))

1.1 Bounds

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

final states:

{1}

transitions:

81 → 48

15 → 73

18 → 5

41 → 145

90 → 75

1 → 4

1 → 3

8 → 10

13 → 82

6 → 37

153 → 111

54 → 39

117 → 83

45 → 12

113 → 154

126 → 85

162 → 120

115 → 118

17 → 46

43 → 109

a₃(157) → 158

a₃(158) → 159

a₃(125) → 126

a₃(121) → 122

a₃(123) → 124

a₃(159) → 160

a₃(161) → 162

a₃(124) → 125

a₃(160) → 161

a₃(122) → 123

b₃(155) → 156

b₃(120) → 121

b₃(119) → 120

b₃(154) → 155

b₃(118) → 119

b₃(156) → 157

b₂(73) → 74

b₂(147) → 148

b₂(84) → 85

b₂(110) → 111

b₂(109) → 110

b₂(75) → 76

b₂(82) → 83

b₂(111) → 112

b₂(145) → 146

b₂(146) → 147

b₂(83) → 84

b₂(74) → 75

a₀(8) → 9

a₀(9) → 1

a₀(7) → 8

a₀(6) → 7

a₀(5) → 6

b₀(2) → 3

b₀(4) → 5

b₀(3) → 4

f2₀ → 2

b₁(11) → 12

b₁(37) → 38

b₁(39) → 40

b₁(38) → 39

b₁(10) → 11

b₁(48) → 49

b₁(47) → 48

b₁(12) → 13

b₁(46) → 47

a₂(114) → 115

a₂(149) → 150

a₂(79) → 80

a₂(80) → 81

a₂(113) → 114

a₂(152) → 153

a₂(151) → 152

a₂(76) → 77

a₂(150) → 151

a₂(89) → 90

a₂(86) → 87

a₂(87) → 88

a₂(112) → 113

a₂(85) → 86

a₂(78) → 79

a₂(77) → 78

a₂(88) → 89

a₂(148) → 149

a₂(115) → 116

a₂(116) → 117

a₁(44) → 45

a₁(53) → 54

a₁(41) → 42

a₁(15) → 16

a₁(13) → 14

a₁(17) → 18

a₁(14) → 15

a₁(51) → 52

a₁(42) → 43

a₁(52) → 53

a₁(49) → 50

a₁(43) → 44

a₁(50) → 51

a₁(40) → 41

a₁(16) → 17

81	→	48
15	→	73
18	→	5
41	→	145
90	→	75
1	→	4
1	→	3
8	→	10
13	→	82
6	→	37
153	→	111
54	→	39
117	→	83
45	→	12
113	→	154
126	→	85
162	→	120
115	→	118
17	→	46
43	→	109
a₃(157)	→	158
a₃(158)	→	159
a₃(125)	→	126
a₃(121)	→	122
a₃(123)	→	124
a₃(159)	→	160
a₃(161)	→	162
a₃(124)	→	125
a₃(160)	→	161
a₃(122)	→	123
b₃(155)	→	156
b₃(120)	→	121
b₃(119)	→	120
b₃(154)	→	155
b₃(118)	→	119
b₃(156)	→	157
b₂(73)	→	74
b₂(147)	→	148
b₂(84)	→	85
b₂(110)	→	111
b₂(109)	→	110
b₂(75)	→	76
b₂(82)	→	83
b₂(111)	→	112
b₂(145)	→	146
b₂(146)	→	147
b₂(83)	→	84
b₂(74)	→	75
a₀(8)	→	9
a₀(9)	→	1
a₀(7)	→	8
a₀(6)	→	7
a₀(5)	→	6
b₀(2)	→	3
b₀(4)	→	5
b₀(3)	→	4
f2₀	→	2
b₁(11)	→	12
b₁(37)	→	38
b₁(39)	→	40
b₁(38)	→	39
b₁(10)	→	11
b₁(48)	→	49
b₁(47)	→	48
b₁(12)	→	13
b₁(46)	→	47
a₂(114)	→	115
a₂(149)	→	150
a₂(79)	→	80
a₂(80)	→	81
a₂(113)	→	114
a₂(152)	→	153
a₂(151)	→	152
a₂(76)	→	77
a₂(150)	→	151
a₂(89)	→	90
a₂(86)	→	87
a₂(87)	→	88
a₂(112)	→	113
a₂(85)	→	86
a₂(78)	→	79
a₂(77)	→	78
a₂(88)	→	89
a₂(148)	→	149
a₂(115)	→	116
a₂(116)	→	117
a₁(44)	→	45
a₁(53)	→	54
a₁(41)	→	42
a₁(15)	→	16
a₁(13)	→	14
a₁(17)	→	18
a₁(14)	→	15
a₁(51)	→	52
a₁(42)	→	43
a₁(52)	→	53
a₁(49)	→	50
a₁(43)	→	44
a₁(50)	→	51
a₁(40)	→	41
a₁(16)	→	17