YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{6, 1}

transitions:

157 → 11

111 → 90

89 → 94

98 → 66

98 → 93

97 → 128

97 → 152

129 → 71

167 → 66

145 → 95

133 → 144

39 → 20

39 → 4

39 → 24

134 → 90

134 → 116

37 → 65

37 → 112

59 → 21

59 → 44

110 → 122

65 → 70

175 → 131

20 → 35

107 → 36

1 → 3

1 → 11

1 → 56

40 → 55

123 → 95

13 → 156

13 → 160

44 → 21

44 → 90

73 → 106

58 → 82

161 → 38

177 → 71

6 → 7

6 → 41

116 → 90

153 → 131

82 → 110

143 → 90

2 → 10

2 → 40

4 → 20

106 → 142

14 → 6

93 → 66

93 → 113

112 → 130

169 → 113

69 → 21

35 → 89

83 → 36

160 → 166

160 → 168

168 → 174

142 → 150

74 → 21

74 → 69

24 → 4

24 → 12

24 → 57

166 → 176

151 → 95

a₃(115) → 116

a₃(92) → 93

a₃(91) → 92

a₃(114) → 115

a₃(128) → 129

a₃(113) → 114

a₃(70) → 71

a₃(72) → 73

a₃(90) → 91

a₃(176) → 177

b₃(73) → 74

b₃(71) → 72

b₃(110) → 111

b₃(112) → 113

b₃(89) → 90

b₃(168) → 169

b₃(142) → 143

a₂(106) → 107

a₂(160) → 161

a₂(37) → 38

a₂(35) → 36

a₂(55) → 56

a₂(82) → 83

a₂(57) → 58

a₂(67) → 68

a₂(68) → 69

a₂(66) → 67

b₀(3) → 4

b₀(2) → 7

b₀(5) → 1

a₀(7) → 8

a₀(9) → 6

a₀(8) → 9

a₀(2) → 3

a₀(4) → 5

b₄(97) → 98

b₄(133) → 134

b₄(95) → 96

b₄(131) → 132

a₄(132) → 133

a₄(96) → 97

a₄(152) → 153

a₄(94) → 95

a₄(130) → 131

a₄(144) → 145

a₄(174) → 175

a₄(122) → 123

a₄(150) → 151

f2₀ → 2

a₁(22) → 23

a₁(23) → 24

a₁(156) → 157

a₁(10) → 11

a₁(43) → 44

a₁(42) → 43

a₁(12) → 13

a₁(21) → 22

a₁(41) → 42

b₂(56) → 57

b₂(65) → 66

b₂(166) → 167

b₂(36) → 37

b₂(38) → 39

b₂(58) → 59

b₁(13) → 14

b₁(20) → 21

b₁(11) → 12

b₁(40) → 41

157	→	11
111	→	90
89	→	94
98	→	66
98	→	93
97	→	128
97	→	152
129	→	71
167	→	66
145	→	95
133	→	144
39	→	20
39	→	4
39	→	24
134	→	90
134	→	116
37	→	65
37	→	112
59	→	21
59	→	44
110	→	122
65	→	70
175	→	131
20	→	35
107	→	36
1	→	3
1	→	11
1	→	56
40	→	55
123	→	95
13	→	156
13	→	160
44	→	21
44	→	90
73	→	106
58	→	82
161	→	38
177	→	71
6	→	7
6	→	41
116	→	90
153	→	131
82	→	110
143	→	90
2	→	10
2	→	40
4	→	20
106	→	142
14	→	6
93	→	66
93	→	113
112	→	130
169	→	113
69	→	21
35	→	89
83	→	36
160	→	166
160	→	168
168	→	174
142	→	150
74	→	21
74	→	69
24	→	4
24	→	12
24	→	57
166	→	176
151	→	95
a₃(115)	→	116
a₃(92)	→	93
a₃(91)	→	92
a₃(114)	→	115
a₃(128)	→	129
a₃(113)	→	114
a₃(70)	→	71
a₃(72)	→	73
a₃(90)	→	91
a₃(176)	→	177
b₃(73)	→	74
b₃(71)	→	72
b₃(110)	→	111
b₃(112)	→	113
b₃(89)	→	90
b₃(168)	→	169
b₃(142)	→	143
a₂(106)	→	107
a₂(160)	→	161
a₂(37)	→	38
a₂(35)	→	36
a₂(55)	→	56
a₂(82)	→	83
a₂(57)	→	58
a₂(67)	→	68
a₂(68)	→	69
a₂(66)	→	67
b₀(3)	→	4
b₀(2)	→	7
b₀(5)	→	1
a₀(7)	→	8
a₀(9)	→	6
a₀(8)	→	9
a₀(2)	→	3
a₀(4)	→	5
b₄(97)	→	98
b₄(133)	→	134
b₄(95)	→	96
b₄(131)	→	132
a₄(132)	→	133
a₄(96)	→	97
a₄(152)	→	153
a₄(94)	→	95
a₄(130)	→	131
a₄(144)	→	145
a₄(174)	→	175
a₄(122)	→	123
a₄(150)	→	151
f2₀	→	2
a₁(22)	→	23
a₁(23)	→	24
a₁(156)	→	157
a₁(10)	→	11
a₁(43)	→	44
a₁(42)	→	43
a₁(12)	→	13
a₁(21)	→	22
a₁(41)	→	42
b₂(56)	→	57
b₂(65)	→	66
b₂(166)	→	167
b₂(36)	→	37
b₂(38)	→	39
b₂(58)	→	59
b₁(13)	→	14
b₁(20)	→	21
b₁(11)	→	12
b₁(40)	→	41