YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(x0))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x0)))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))

Proof

1 Bounds

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

final states:

{26, 19, 12, 1}

transitions:

25 → 141

102 → 107

32 → 145

128 → 133

80 → 15

18 → 137

50 → 55

146 → 45

108 → 100

134 → 126

1 → 5

26 → 5

76 → 81

79 → 96

138 → 45

54 → 8

105 → 122

82 → 74

53 → 70

11 → 44

106 → 22

12 → 5

132 → 29

142 → 45

19 → 5

56 → 48

0₁(46) → 47

0₁(127) → 128

0₁(49) → 50

0₁(98) → 99

0₁(75) → 76

0₁(72) → 73

0₁(101) → 102

0₁(124) → 125

2₁(137) → 138

2₁(73) → 74

2₁(70) → 71

2₁(81) → 82

2₁(78) → 79

2₁(130) → 131

2₁(125) → 126

2₁(99) → 100

2₁(107) → 108

2₁(55) → 56

2₁(47) → 48

2₁(104) → 105

2₁(145) → 146

2₁(96) → 97

2₁(133) → 134

2₁(122) → 123

2₁(141) → 142

2₁(44) → 45

2₁(52) → 53

f3₀ → 2

1₀(20) → 21

1₀(29) → 30

1₀(9) → 10

1₀(8) → 9

1₀(32) → 26

1₀(15) → 16

1₀(18) → 12

1₀(16) → 17

1₀(27) → 28

1₀(25) → 19

1₀(23) → 24

1₀(6) → 7

1₀(30) → 31

1₀(11) → 1

1₀(3) → 4

1₀(13) → 14

1₀(22) → 23

0₀(28) → 29

0₀(14) → 15

0₀(7) → 8

0₀(4) → 5

0₀(21) → 22

1₁(51) → 52

1₁(123) → 124

1₁(128) → 129

1₁(105) → 106

1₁(48) → 49

1₁(50) → 51

1₁(79) → 80

1₁(131) → 132

1₁(71) → 72

1₁(76) → 77

1₁(74) → 75

1₁(100) → 101

1₁(53) → 54

1₁(45) → 46

1₁(129) → 130

1₁(103) → 104

1₁(126) → 127

1₁(97) → 98

1₁(77) → 78

1₁(102) → 103

2₀(22) → 27

2₀(24) → 25

2₀(8) → 13

2₀(10) → 11

2₀(15) → 20

2₀(17) → 18

2₀(5) → 6

2₀(31) → 32

2₀(2) → 3

25	→	141
102	→	107
32	→	145
128	→	133
80	→	15
18	→	137
50	→	55
146	→	45
108	→	100
134	→	126
1	→	5
26	→	5
76	→	81
79	→	96
138	→	45
54	→	8
105	→	122
82	→	74
53	→	70
11	→	44
106	→	22
12	→	5
132	→	29
142	→	45
19	→	5
56	→	48
0₁(46)	→	47
0₁(127)	→	128
0₁(49)	→	50
0₁(98)	→	99
0₁(75)	→	76
0₁(72)	→	73
0₁(101)	→	102
0₁(124)	→	125
2₁(137)	→	138
2₁(73)	→	74
2₁(70)	→	71
2₁(81)	→	82
2₁(78)	→	79
2₁(130)	→	131
2₁(125)	→	126
2₁(99)	→	100
2₁(107)	→	108
2₁(55)	→	56
2₁(47)	→	48
2₁(104)	→	105
2₁(145)	→	146
2₁(96)	→	97
2₁(133)	→	134
2₁(122)	→	123
2₁(141)	→	142
2₁(44)	→	45
2₁(52)	→	53
f3₀	→	2
1₀(20)	→	21
1₀(29)	→	30
1₀(9)	→	10
1₀(8)	→	9
1₀(32)	→	26
1₀(15)	→	16
1₀(18)	→	12
1₀(16)	→	17
1₀(27)	→	28
1₀(25)	→	19
1₀(23)	→	24
1₀(6)	→	7
1₀(30)	→	31
1₀(11)	→	1
1₀(3)	→	4
1₀(13)	→	14
1₀(22)	→	23
0₀(28)	→	29
0₀(14)	→	15
0₀(7)	→	8
0₀(4)	→	5
0₀(21)	→	22
1₁(51)	→	52
1₁(123)	→	124
1₁(128)	→	129
1₁(105)	→	106
1₁(48)	→	49
1₁(50)	→	51
1₁(79)	→	80
1₁(131)	→	132
1₁(71)	→	72
1₁(76)	→	77
1₁(74)	→	75
1₁(100)	→	101
1₁(53)	→	54
1₁(45)	→	46
1₁(129)	→	130
1₁(103)	→	104
1₁(126)	→	127
1₁(97)	→	98
1₁(77)	→	78
1₁(102)	→	103
2₀(22)	→	27
2₀(24)	→	25
2₀(8)	→	13
2₀(10)	→	11
2₀(15)	→	20
2₀(17)	→	18
2₀(5)	→	6
2₀(31)	→	32
2₀(2)	→	3