YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(x0)))	→	0(2(1(1(x0))))
0(1(2(x0)))	→	0(2(1(3(x0))))
0(1(2(x0)))	→	0(2(1(1(3(x0)))))
0(1(2(x0)))	→	0(2(4(1(1(x0)))))
0(1(2(x0)))	→	0(2(4(1(3(x0)))))
0(3(2(x0)))	→	0(2(1(3(x0))))
0(3(2(x0)))	→	0(2(1(1(3(x0)))))
0(3(2(x0)))	→	0(0(2(1(1(3(x0))))))
0(1(1(2(x0))))	→	0(2(1(1(3(x0)))))
0(1(2(2(x0))))	→	0(2(2(1(1(x0)))))
0(1(2(2(x0))))	→	0(2(3(2(1(x0)))))
0(1(3(2(x0))))	→	0(2(1(4(3(x0)))))
0(1(3(2(x0))))	→	3(3(0(2(1(x0)))))
0(1(3(2(x0))))	→	3(0(2(4(1(1(x0))))))
0(1(5(2(x0))))	→	5(0(2(1(1(x0)))))
0(3(2(2(x0))))	→	0(0(2(3(2(x0)))))
0(3(2(2(x0))))	→	0(0(4(2(3(2(x0))))))
2(0(3(2(x0))))	→	1(3(0(2(2(x0)))))
3(0(3(2(x0))))	→	3(0(0(0(2(3(x0))))))
3(1(5(2(x0))))	→	0(2(1(5(3(x0)))))
3(3(5(2(x0))))	→	3(0(2(1(5(3(x0))))))
4(5(2(2(x0))))	→	2(5(0(2(4(1(x0))))))
5(0(1(2(x0))))	→	0(2(1(3(4(5(x0))))))
5(0(2(2(x0))))	→	2(0(2(4(1(5(x0))))))
5(0(3(2(x0))))	→	3(0(2(1(4(5(x0))))))
5(1(2(2(x0))))	→	0(2(1(5(2(1(x0))))))
5(1(2(2(x0))))	→	2(1(5(2(1(1(x0))))))
0(1(2(4(2(x0)))))	→	4(2(1(0(2(1(x0))))))
0(1(2(5(2(x0)))))	→	2(0(2(1(5(4(x0))))))
0(1(5(1(2(x0)))))	→	1(0(2(1(1(5(x0))))))
0(1(5(5(2(x0)))))	→	0(2(1(5(5(1(x0))))))
0(5(0(1(2(x0)))))	→	0(4(5(0(2(1(x0))))))
0(5(0(3(2(x0)))))	→	0(5(0(0(2(3(x0))))))
0(5(5(2(2(x0)))))	→	0(2(1(5(5(2(x0))))))
3(0(3(1(2(x0)))))	→	1(3(3(0(2(3(x0))))))
3(0(3(4(2(x0)))))	→	1(3(4(0(2(3(x0))))))
4(5(1(4(2(x0)))))	→	2(4(4(4(1(5(x0))))))
5(0(1(3(2(x0)))))	→	3(5(0(2(1(3(x0))))))
5(0(3(1(2(x0)))))	→	0(2(1(4(3(5(x0))))))
5(0(4(2(2(x0)))))	→	2(0(2(4(1(5(x0))))))
5(1(0(3(2(x0)))))	→	0(4(3(5(1(2(x0))))))
5(1(0(3(2(x0)))))	→	5(3(1(1(0(2(x0))))))
5(1(0(5(2(x0)))))	→	3(5(5(0(2(1(x0))))))
5(1(0(5(2(x0)))))	→	5(0(2(1(5(5(x0))))))
5(2(0(3(2(x0)))))	→	0(2(5(2(3(1(x0))))))

Proof

1 Bounds

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

final states:

{145, 140, 138, 133, 128, 123, 121, 118, 115, 112, 107, 105, 102, 97, 93, 87, 84, 81, 77, 73, 68, 62, 57, 56, 52, 47, 43, 40, 35, 34, 33, 30, 26, 22, 20, 19, 16, 13, 10, 6, 1}

transitions:

128 → 98

128 → 63

81 → 130

81 → 98

81 → 63

145 → 108

145 → 63

133 → 98

133 → 63

57 → 64

57 → 88

62 → 63

123 → 63

73 → 63

138 → 98

138 → 63

121 → 63

52 → 146

52 → 7

118 → 64

118 → 88

112 → 7

77 → 130

77 → 98

77 → 63

140 → 98

140 → 63

115 → 7

47 → 7

68 → 63

43 → 36

56 → 7

f6₀ → 2

5₀(31) → 103

5₀(147) → 148

5₀(60) → 61

5₀(137) → 133

5₀(88) → 89

5₀(98) → 99

5₀(7) → 53

5₀(23) → 78

5₀(50) → 106

5₀(5) → 82

5₀(6) → 122

5₀(144) → 140

5₀(63) → 141

5₀(2) → 63

5₀(3) → 98

5₀(36) → 108

5₀(129) → 130

5₀(1) → 34

5₀(103) → 139

5₀(108) → 109

2₀(126) → 127

2₀(148) → 149

2₀(100) → 101

2₀(70) → 71

2₀(14) → 15

2₀(37) → 38

2₀(142) → 143

2₀(85) → 86

2₀(7) → 48

2₀(58) → 59

2₀(8) → 9

2₀(11) → 12

2₀(79) → 80

2₀(110) → 111

2₀(120) → 118

2₀(92) → 87

2₀(90) → 91

2₀(36) → 44

2₀(28) → 29

2₀(3) → 23

2₀(54) → 55

2₀(146) → 147

2₀(94) → 95

2₀(61) → 57

2₀(72) → 68

2₀(83) → 81

2₀(74) → 75

2₀(5) → 21

2₀(17) → 18

2₀(2) → 36

2₀(4) → 5

2₀(24) → 25

2₀(66) → 67

1₀(31) → 85

1₀(65) → 66

1₀(53) → 54

1₀(46) → 43

1₀(78) → 79

1₀(141) → 142

1₀(3) → 4

1₀(7) → 8

1₀(125) → 126

1₀(8) → 11

1₀(135) → 136

1₀(134) → 135

1₀(89) → 90

1₀(114) → 112

1₀(64) → 74

1₀(82) → 83

1₀(99) → 100

1₀(27) → 28

1₀(96) → 93

1₀(109) → 110

1₀(63) → 69

1₀(117) → 115

1₀(36) → 129

1₀(2) → 3

1₀(69) → 94

3₀(2) → 7

3₀(31) → 32

3₀(45) → 46

3₀(113) → 114

3₀(51) → 47

3₀(32) → 30

3₀(136) → 137

3₀(76) → 73

3₀(36) → 37

3₀(23) → 24

3₀(64) → 65

3₀(139) → 138

3₀(13) → 33

3₀(63) → 124

3₀(116) → 117

3₀(49) → 113

3₀(130) → 131

3₀(3) → 146

3₀(52) → 56

3₀(122) → 121

0₀(18) → 16

0₀(149) → 145

0₀(91) → 92

0₀(9) → 6

0₀(10) → 19

0₀(49) → 50

0₀(48) → 49

0₀(50) → 51

0₀(95) → 96

0₀(67) → 62

0₀(80) → 77

0₀(36) → 134

0₀(55) → 52

0₀(71) → 72

0₀(25) → 22

0₀(21) → 20

0₀(104) → 102

0₀(38) → 39

0₀(23) → 31

0₀(132) → 128

0₀(111) → 107

0₀(29) → 26

0₀(15) → 13

0₀(101) → 97

0₀(127) → 123

0₀(42) → 40

0₀(75) → 76

0₀(39) → 35

0₀(12) → 10

0₀(143) → 144

0₀(41) → 42

0₀(44) → 45

0₀(59) → 60

0₀(5) → 1

0₀(106) → 105

4₀(8) → 17

4₀(86) → 84

4₀(63) → 64

4₀(69) → 70

4₀(124) → 125

4₀(4) → 14

4₀(7) → 27

4₀(49) → 116

4₀(119) → 120

4₀(103) → 104

4₀(3) → 58

4₀(70) → 119

4₀(131) → 132

4₀(38) → 41

4₀(2) → 88

128	→	98
128	→	63
81	→	130
81	→	98
81	→	63
145	→	108
145	→	63
133	→	98
133	→	63
57	→	64
57	→	88
62	→	63
123	→	63
73	→	63
138	→	98
138	→	63
121	→	63
52	→	146
52	→	7
118	→	64
118	→	88
112	→	7
77	→	130
77	→	98
77	→	63
140	→	98
140	→	63
115	→	7
47	→	7
68	→	63
43	→	36
56	→	7
f6₀	→	2
5₀(31)	→	103
5₀(147)	→	148
5₀(60)	→	61
5₀(137)	→	133
5₀(88)	→	89
5₀(98)	→	99
5₀(7)	→	53
5₀(23)	→	78
5₀(50)	→	106
5₀(5)	→	82
5₀(6)	→	122
5₀(144)	→	140
5₀(63)	→	141
5₀(2)	→	63
5₀(3)	→	98
5₀(36)	→	108
5₀(129)	→	130
5₀(1)	→	34
5₀(103)	→	139
5₀(108)	→	109
2₀(126)	→	127
2₀(148)	→	149
2₀(100)	→	101
2₀(70)	→	71
2₀(14)	→	15
2₀(37)	→	38
2₀(142)	→	143
2₀(85)	→	86
2₀(7)	→	48
2₀(58)	→	59
2₀(8)	→	9
2₀(11)	→	12
2₀(79)	→	80
2₀(110)	→	111
2₀(120)	→	118
2₀(92)	→	87
2₀(90)	→	91
2₀(36)	→	44
2₀(28)	→	29
2₀(3)	→	23
2₀(54)	→	55
2₀(146)	→	147
2₀(94)	→	95
2₀(61)	→	57
2₀(72)	→	68
2₀(83)	→	81
2₀(74)	→	75
2₀(5)	→	21
2₀(17)	→	18
2₀(2)	→	36
2₀(4)	→	5
2₀(24)	→	25
2₀(66)	→	67
1₀(31)	→	85
1₀(65)	→	66
1₀(53)	→	54
1₀(46)	→	43
1₀(78)	→	79
1₀(141)	→	142
1₀(3)	→	4
1₀(7)	→	8
1₀(125)	→	126
1₀(8)	→	11
1₀(135)	→	136
1₀(134)	→	135
1₀(89)	→	90
1₀(114)	→	112
1₀(64)	→	74
1₀(82)	→	83
1₀(99)	→	100
1₀(27)	→	28
1₀(96)	→	93
1₀(109)	→	110
1₀(63)	→	69
1₀(117)	→	115
1₀(36)	→	129
1₀(2)	→	3
1₀(69)	→	94
3₀(2)	→	7
3₀(31)	→	32
3₀(45)	→	46
3₀(113)	→	114
3₀(51)	→	47
3₀(32)	→	30
3₀(136)	→	137
3₀(76)	→	73
3₀(36)	→	37
3₀(23)	→	24
3₀(64)	→	65
3₀(139)	→	138
3₀(13)	→	33
3₀(63)	→	124
3₀(116)	→	117
3₀(49)	→	113
3₀(130)	→	131
3₀(3)	→	146
3₀(52)	→	56
3₀(122)	→	121
0₀(18)	→	16
0₀(149)	→	145
0₀(91)	→	92
0₀(9)	→	6
0₀(10)	→	19
0₀(49)	→	50
0₀(48)	→	49
0₀(50)	→	51
0₀(95)	→	96
0₀(67)	→	62
0₀(80)	→	77
0₀(36)	→	134
0₀(55)	→	52
0₀(71)	→	72
0₀(25)	→	22
0₀(21)	→	20
0₀(104)	→	102
0₀(38)	→	39
0₀(23)	→	31
0₀(132)	→	128
0₀(111)	→	107
0₀(29)	→	26
0₀(15)	→	13
0₀(101)	→	97
0₀(127)	→	123
0₀(42)	→	40
0₀(75)	→	76
0₀(39)	→	35
0₀(12)	→	10
0₀(143)	→	144
0₀(41)	→	42
0₀(44)	→	45
0₀(59)	→	60
0₀(5)	→	1
0₀(106)	→	105
4₀(8)	→	17
4₀(86)	→	84
4₀(63)	→	64
4₀(69)	→	70
4₀(124)	→	125
4₀(4)	→	14
4₀(7)	→	27
4₀(49)	→	116
4₀(119)	→	120
4₀(103)	→	104
4₀(3)	→	58
4₀(70)	→	119
4₀(131)	→	132
4₀(38)	→	41
4₀(2)	→	88