YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

v(s(x0))	→	s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x0))))))))))))))))))))
v(0(x0))	→	p(p(s(s(0(p(p(s(s(s(s(s(x0))))))))))))
w(s(x0))	→	s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x0))))))))))))))))))))
w(0(x0))	→	p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x0)))))))))))))))))))
p(p(s(x0)))	→	p(x0)
p(s(x0))	→	x0
p(0(x0))	→	0(s(s(s(s(s(s(s(p(s(x0))))))))))

Proof

1 Bounds

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

final states:

{66, 2, 65, 51, 33, 22, 1}

transitions:

279 → 63

33 → 11

33 → 118

111 → 113

25 → 95

25 → 27

29 → 82

80 → 21

98 → 40

51 → 11

51 → 118

181 → 183

96 → 28

129 → 104

129 → 41

18 → 79

18 → 20

41 → 45

41 → 104

3 → 73

3 → 34

213 → 60

225 → 227

108 → 58

37 → 97

37 → 39

90 → 10

125 → 177

125 → 127

235 → 61

269 → 271

36 → 40

36 → 98

161 → 58

161 → 108

178 → 128

257 → 62

6 → 90

109 → 111

88 → 57

54 → 87

54 → 56

52 → 151

124 → 178

174 → 117

82 → 22

53 → 107

53 → 88

2 → 4

2 → 35

2 → 74

2 → 65

4 → 6

212 → 225

66 → 65

114 → 173

114 → 116

63 → 51

104 → 45

7 → 89

7 → 9

234 → 247

113 → 117

113 → 174

30 → 81

30 → 32

42 → 103

42 → 44

35 → 109

256 → 269

17 → 80

160 → 181

190 → 203

203 → 205

74 → 35

24 → 28

24 → 96

151 → 153

191 → 59

247 → 249

w₁(117) → 118

0₀(52) → 53

0₀(72) → 66

0₀(28) → 29

v₀(40) → 41

w₀(10) → 11

p₁(87) → 88

p₁(112) → 113

p₁(97) → 98

p₁(152) → 153

p₁(226) → 227

p₁(270) → 271

p₁(107) → 108

p₁(248) → 249

p₁(89) → 90

p₁(116) → 117

p₁(182) → 183

p₁(103) → 104

p₁(81) → 82

p₁(95) → 96

p₁(110) → 111

p₁(79) → 80

p₁(126) → 127

p₁(115) → 116

p₁(127) → 128

p₁(204) → 205

p₁(73) → 74

0₁(278) → 279

0₁(190) → 191

0₁(212) → 213

0₁(256) → 257

0₁(234) → 235

0₁(160) → 161

s₀(11) → 12

s₀(37) → 38

s₀(14) → 15

s₀(50) → 33

s₀(3) → 23

s₀(18) → 19

s₀(15) → 16

s₀(70) → 71

s₀(5) → 67

s₀(7) → 8

s₀(23) → 24

s₀(24) → 25

s₀(26) → 52

s₀(29) → 30

s₀(16) → 17

s₀(54) → 55

s₀(63) → 64

s₀(53) → 54

s₀(49) → 50

s₀(2) → 3

s₀(4) → 5

s₀(45) → 46

s₀(25) → 26

s₀(48) → 49

s₀(42) → 43

s₀(47) → 48

s₀(12) → 13

s₀(46) → 47

s₀(35) → 36

s₀(71) → 72

s₀(13) → 14

s₀(36) → 37

s₀(69) → 70

s₀(17) → 18

s₀(67) → 68

s₀(30) → 31

s₀(6) → 7

s₀(68) → 69

s₀(21) → 1

s₀(41) → 42

p₀(2) → 65

p₀(56) → 57

p₀(9) → 10

p₀(64) → 51

p₀(19) → 20

p₀(55) → 56

p₀(43) → 44

p₀(8) → 9

p₀(61) → 62

p₀(26) → 27

p₀(38) → 39

p₀(3) → 4

p₀(62) → 63

p₀(23) → 34

p₀(32) → 22

p₀(27) → 28

p₀(20) → 21

p₀(39) → 40

p₀(57) → 58

p₀(60) → 61

p₀(34) → 35

p₀(44) → 45

p₀(59) → 60

p₀(31) → 32

p₀(58) → 59

p₀(5) → 6

p₂(177) → 178

p₂(173) → 174

s₁(232) → 233

s₁(207) → 208

s₁(277) → 278

s₁(271) → 272

s₁(249) → 250

s₁(187) → 188

s₁(211) → 212

s₁(123) → 124

s₁(254) → 255

s₁(154) → 155

s₁(183) → 184

s₁(188) → 189

s₁(255) → 256

s₁(124) → 125

s₁(159) → 160

s₁(111) → 112

s₁(247) → 248

s₁(205) → 206

s₁(203) → 204

s₁(275) → 276

s₁(229) → 230

s₁(122) → 123

s₁(109) → 110

s₁(228) → 229

s₁(252) → 253

s₁(208) → 209

s₁(227) → 228

s₁(269) → 270

s₁(274) → 275

s₁(225) → 226

s₁(156) → 157

s₁(186) → 187

s₁(157) → 158

s₁(185) → 186

s₁(121) → 122

s₁(273) → 274

s₁(125) → 126

s₁(114) → 115

s₁(210) → 211

s₁(118) → 119

s₁(120) → 121

s₁(155) → 156

s₁(158) → 159

s₁(233) → 234

s₁(181) → 182

s₁(151) → 152

s₁(209) → 210

s₁(272) → 273

s₁(276) → 277

s₁(230) → 231

s₁(153) → 154

s₁(250) → 251

s₁(113) → 114

s₁(184) → 185

s₁(251) → 252

s₁(253) → 254

s₁(231) → 232

s₁(119) → 120

s₁(206) → 207

s₁(189) → 190

s₁(128) → 129

f5₀ → 2

279	→	63
33	→	11
33	→	118
111	→	113
25	→	95
25	→	27
29	→	82
80	→	21
98	→	40
51	→	11
51	→	118
181	→	183
96	→	28
129	→	104
129	→	41
18	→	79
18	→	20
41	→	45
41	→	104
3	→	73
3	→	34
213	→	60
225	→	227
108	→	58
37	→	97
37	→	39
90	→	10
125	→	177
125	→	127
235	→	61
269	→	271
36	→	40
36	→	98
161	→	58
161	→	108
178	→	128
257	→	62
6	→	90
109	→	111
88	→	57
54	→	87
54	→	56
52	→	151
124	→	178
174	→	117
82	→	22
53	→	107
53	→	88
2	→	4
2	→	35
2	→	74
2	→	65
4	→	6
212	→	225
66	→	65
114	→	173
114	→	116
63	→	51
104	→	45
7	→	89
7	→	9
234	→	247
113	→	117
113	→	174
30	→	81
30	→	32
42	→	103
42	→	44
35	→	109
256	→	269
17	→	80
160	→	181
190	→	203
203	→	205
74	→	35
24	→	28
24	→	96
151	→	153
191	→	59
247	→	249
w₁(117)	→	118
0₀(52)	→	53
0₀(72)	→	66
0₀(28)	→	29
v₀(40)	→	41
w₀(10)	→	11
p₁(87)	→	88
p₁(112)	→	113
p₁(97)	→	98
p₁(152)	→	153
p₁(226)	→	227
p₁(270)	→	271
p₁(107)	→	108
p₁(248)	→	249
p₁(89)	→	90
p₁(116)	→	117
p₁(182)	→	183
p₁(103)	→	104
p₁(81)	→	82
p₁(95)	→	96
p₁(110)	→	111
p₁(79)	→	80
p₁(126)	→	127
p₁(115)	→	116
p₁(127)	→	128
p₁(204)	→	205
p₁(73)	→	74
0₁(278)	→	279
0₁(190)	→	191
0₁(212)	→	213
0₁(256)	→	257
0₁(234)	→	235
0₁(160)	→	161
s₀(11)	→	12
s₀(37)	→	38
s₀(14)	→	15
s₀(50)	→	33
s₀(3)	→	23
s₀(18)	→	19
s₀(15)	→	16
s₀(70)	→	71
s₀(5)	→	67
s₀(7)	→	8
s₀(23)	→	24
s₀(24)	→	25
s₀(26)	→	52
s₀(29)	→	30
s₀(16)	→	17
s₀(54)	→	55
s₀(63)	→	64
s₀(53)	→	54
s₀(49)	→	50
s₀(2)	→	3
s₀(4)	→	5
s₀(45)	→	46
s₀(25)	→	26
s₀(48)	→	49
s₀(42)	→	43
s₀(47)	→	48
s₀(12)	→	13
s₀(46)	→	47
s₀(35)	→	36
s₀(71)	→	72
s₀(13)	→	14
s₀(36)	→	37
s₀(69)	→	70
s₀(17)	→	18
s₀(67)	→	68
s₀(30)	→	31
s₀(6)	→	7
s₀(68)	→	69
s₀(21)	→	1
s₀(41)	→	42
p₀(2)	→	65
p₀(56)	→	57
p₀(9)	→	10
p₀(64)	→	51
p₀(19)	→	20
p₀(55)	→	56
p₀(43)	→	44
p₀(8)	→	9
p₀(61)	→	62
p₀(26)	→	27
p₀(38)	→	39
p₀(3)	→	4
p₀(62)	→	63
p₀(23)	→	34
p₀(32)	→	22
p₀(27)	→	28
p₀(20)	→	21
p₀(39)	→	40
p₀(57)	→	58
p₀(60)	→	61
p₀(34)	→	35
p₀(44)	→	45
p₀(59)	→	60
p₀(31)	→	32
p₀(58)	→	59
p₀(5)	→	6
p₂(177)	→	178
p₂(173)	→	174
s₁(232)	→	233
s₁(207)	→	208
s₁(277)	→	278
s₁(271)	→	272
s₁(249)	→	250
s₁(187)	→	188
s₁(211)	→	212
s₁(123)	→	124
s₁(254)	→	255
s₁(154)	→	155
s₁(183)	→	184
s₁(188)	→	189
s₁(255)	→	256
s₁(124)	→	125
s₁(159)	→	160
s₁(111)	→	112
s₁(247)	→	248
s₁(205)	→	206
s₁(203)	→	204
s₁(275)	→	276
s₁(229)	→	230
s₁(122)	→	123
s₁(109)	→	110
s₁(228)	→	229
s₁(252)	→	253
s₁(208)	→	209
s₁(227)	→	228
s₁(269)	→	270
s₁(274)	→	275
s₁(225)	→	226
s₁(156)	→	157
s₁(186)	→	187
s₁(157)	→	158
s₁(185)	→	186
s₁(121)	→	122
s₁(273)	→	274
s₁(125)	→	126
s₁(114)	→	115
s₁(210)	→	211
s₁(118)	→	119
s₁(120)	→	121
s₁(155)	→	156
s₁(158)	→	159
s₁(233)	→	234
s₁(181)	→	182
s₁(151)	→	152
s₁(209)	→	210
s₁(272)	→	273
s₁(276)	→	277
s₁(230)	→	231
s₁(153)	→	154
s₁(250)	→	251
s₁(113)	→	114
s₁(184)	→	185
s₁(251)	→	252
s₁(253)	→	254
s₁(231)	→	232
s₁(119)	→	120
s₁(206)	→	207
s₁(189)	→	190
s₁(128)	→	129
f5₀	→	2