YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{9, 5, 1}

transitions:

32 → 102

145 → 114

145 → 142

122 → 114

122 → 142

9 → 4

9 → 10

9 → 31

9 → 47

9 → 70

5 → 4

5 → 10

5 → 31

5 → 47

5 → 70

95 → 32

95 → 68

95 → 142

95 → 154

59 → 32

1 → 4

1 → 10

1 → 31

1 → 47

1 → 70

44 → 14

73 → 32

26 → 83

26 → 91

26 → 101

86 → 32

86 → 68

86 → 142

86 → 154

88 → 14

54 → 29

105 → 32

105 → 68

105 → 142

105 → 154

124 → 120

53 → 87

53 → 113

53 → 119

53 → 127

53 → 141

2 → 45

2 → 55

2 → 69

28 → 43

28 → 67

28 → 123

28 → 139

28 → 153

16 → 10

16 → 4

16 → 1

114 → 32

140 → 128

7 → 13

7 → 26

7 → 31

30 → 10

30 → 4

30 → 1

30 → 53

35 → 10

35 → 4

35 → 1

47 → 31

154 → 142

68 → 32

131 → 114

131 → 142

c₀(7) → 8

c₀(10) → 11

c₀(2) → 6

c₀(12) → 9

a₂(121) → 122

a₂(120) → 121

a₂(84) → 85

a₂(85) → 86

a₂(101) → 102

a₂(153) → 154

a₂(141) → 142

a₀(2) → 10

a₀(4) → 1

a₀(3) → 4

b₁(33) → 34

b₁(58) → 59

b₁(45) → 46

b₁(43) → 44

b₁(56) → 57

b₁(29) → 30

b₁(87) → 88

b₁(27) → 28

b₁(13) → 14

b₁(71) → 72

a₁(31) → 32

a₁(67) → 68

a₁(46) → 47

a₁(113) → 114

a₁(15) → 16

a₁(14) → 15

a₁(69) → 70

c₂(102) → 103

c₂(129) → 130

c₂(144) → 145

c₂(91) → 92

c₂(93) → 94

c₂(139) → 140

c₂(142) → 143

c₂(127) → 128

c₂(104) → 105

c₁(28) → 29

c₁(55) → 56

c₁(26) → 27

c₁(53) → 54

c₁(70) → 71

c₁(32) → 33

c₁(57) → 58

c₁(34) → 35

c₁(72) → 73

f3₀ → 2

b₂(143) → 144

b₂(123) → 124

b₂(94) → 95

b₂(128) → 129

b₂(92) → 93

b₂(83) → 84

b₂(119) → 120

b₂(103) → 104

b₂(130) → 131

b₀(8) → 5

b₀(6) → 7

b₀(2) → 3

b₀(11) → 12

32	→	102
145	→	114
145	→	142
122	→	114
122	→	142
9	→	4
9	→	10
9	→	31
9	→	47
9	→	70
5	→	4
5	→	10
5	→	31
5	→	47
5	→	70
95	→	32
95	→	68
95	→	142
95	→	154
59	→	32
1	→	4
1	→	10
1	→	31
1	→	47
1	→	70
44	→	14
73	→	32
26	→	83
26	→	91
26	→	101
86	→	32
86	→	68
86	→	142
86	→	154
88	→	14
54	→	29
105	→	32
105	→	68
105	→	142
105	→	154
124	→	120
53	→	87
53	→	113
53	→	119
53	→	127
53	→	141
2	→	45
2	→	55
2	→	69
28	→	43
28	→	67
28	→	123
28	→	139
28	→	153
16	→	10
16	→	4
16	→	1
114	→	32
140	→	128
7	→	13
7	→	26
7	→	31
30	→	10
30	→	4
30	→	1
30	→	53
35	→	10
35	→	4
35	→	1
47	→	31
154	→	142
68	→	32
131	→	114
131	→	142
c₀(7)	→	8
c₀(10)	→	11
c₀(2)	→	6
c₀(12)	→	9
a₂(121)	→	122
a₂(120)	→	121
a₂(84)	→	85
a₂(85)	→	86
a₂(101)	→	102
a₂(153)	→	154
a₂(141)	→	142
a₀(2)	→	10
a₀(4)	→	1
a₀(3)	→	4
b₁(33)	→	34
b₁(58)	→	59
b₁(45)	→	46
b₁(43)	→	44
b₁(56)	→	57
b₁(29)	→	30
b₁(87)	→	88
b₁(27)	→	28
b₁(13)	→	14
b₁(71)	→	72
a₁(31)	→	32
a₁(67)	→	68
a₁(46)	→	47
a₁(113)	→	114
a₁(15)	→	16
a₁(14)	→	15
a₁(69)	→	70
c₂(102)	→	103
c₂(129)	→	130
c₂(144)	→	145
c₂(91)	→	92
c₂(93)	→	94
c₂(139)	→	140
c₂(142)	→	143
c₂(127)	→	128
c₂(104)	→	105
c₁(28)	→	29
c₁(55)	→	56
c₁(26)	→	27
c₁(53)	→	54
c₁(70)	→	71
c₁(32)	→	33
c₁(57)	→	58
c₁(34)	→	35
c₁(72)	→	73
f3₀	→	2
b₂(143)	→	144
b₂(123)	→	124
b₂(94)	→	95
b₂(128)	→	129
b₂(92)	→	93
b₂(83)	→	84
b₂(119)	→	120
b₂(103)	→	104
b₂(130)	→	131
b₀(8)	→	5
b₀(6)	→	7
b₀(2)	→	3
b₀(11)	→	12