YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{9, 6, 1}

transitions:

33 → 28

111 → 65

89 → 13

81 → 28

81 → 51

103 → 79

10 → 27

15 → 32

129 → 65

129 → 113

41 → 64

41 → 106

39 → 14

3 → 12

3 → 38

107 → 66

31 → 9

101 → 91

44 → 27

44 → 10

44 → 100

44 → 50

44 → 42

121 → 51

6 → 38

6 → 3

6 → 106

6 → 41

54 → 44

67 → 82

67 → 90

67 → 126

53 → 88

53 → 102

53 → 110

53 → 118

2 → 40

16 → 11

93 → 63

93 → 65

93 → 113

63 → 13

113 → 65

42 → 50

42 → 100

83 → 51

68 → 43

43 → 62

43 → 78

43 → 112

c₃(126) → 127

c₃(118) → 119

c₁(38) → 39

b₂(82) → 83

b₂(51) → 52

b₂(110) → 111

b₂(50) → 51

b₂(112) → 113

b₂(80) → 81

b₂(91) → 92

b₂(92) → 93

b₂(64) → 65

b₂(79) → 80

b₂(66) → 67

b₂(52) → 53

b₂(65) → 66

b₁(14) → 15

b₁(32) → 33

b₁(88) → 89

b₁(29) → 30

b₁(28) → 29

b₁(40) → 41

b₁(12) → 13

b₁(27) → 28

b₁(13) → 14

b₁(62) → 63

f3₀ → 2

a₀(5) → 1

a₀(10) → 11

a₀(11) → 9

a₀(3) → 10

c₂(106) → 107

c₂(100) → 101

c₂(78) → 79

c₂(90) → 91

c₂(102) → 103

a₂(53) → 54

a₂(67) → 68

c₀(2) → 7

a₁(30) → 31

a₁(43) → 44

a₁(15) → 16

a₁(42) → 43

a₁(41) → 42

b₃(120) → 121

b₃(127) → 128

b₃(119) → 120

b₃(128) → 129

b₀(8) → 6

b₀(2) → 3

b₀(3) → 4

b₀(4) → 5

b₀(7) → 8

33	→	28
111	→	65
89	→	13
81	→	28
81	→	51
103	→	79
10	→	27
15	→	32
129	→	65
129	→	113
41	→	64
41	→	106
39	→	14
3	→	12
3	→	38
107	→	66
31	→	9
101	→	91
44	→	27
44	→	10
44	→	100
44	→	50
44	→	42
121	→	51
6	→	38
6	→	3
6	→	106
6	→	41
54	→	44
67	→	82
67	→	90
67	→	126
53	→	88
53	→	102
53	→	110
53	→	118
2	→	40
16	→	11
93	→	63
93	→	65
93	→	113
63	→	13
113	→	65
42	→	50
42	→	100
83	→	51
68	→	43
43	→	62
43	→	78
43	→	112
c₃(126)	→	127
c₃(118)	→	119
c₁(38)	→	39
b₂(82)	→	83
b₂(51)	→	52
b₂(110)	→	111
b₂(50)	→	51
b₂(112)	→	113
b₂(80)	→	81
b₂(91)	→	92
b₂(92)	→	93
b₂(64)	→	65
b₂(79)	→	80
b₂(66)	→	67
b₂(52)	→	53
b₂(65)	→	66
b₁(14)	→	15
b₁(32)	→	33
b₁(88)	→	89
b₁(29)	→	30
b₁(28)	→	29
b₁(40)	→	41
b₁(12)	→	13
b₁(27)	→	28
b₁(13)	→	14
b₁(62)	→	63
f3₀	→	2
a₀(5)	→	1
a₀(10)	→	11
a₀(11)	→	9
a₀(3)	→	10
c₂(106)	→	107
c₂(100)	→	101
c₂(78)	→	79
c₂(90)	→	91
c₂(102)	→	103
a₂(53)	→	54
a₂(67)	→	68
c₀(2)	→	7
a₁(30)	→	31
a₁(43)	→	44
a₁(15)	→	16
a₁(42)	→	43
a₁(41)	→	42
b₃(120)	→	121
b₃(127)	→	128
b₃(119)	→	120
b₃(128)	→	129
b₀(8)	→	6
b₀(2)	→	3
b₀(3)	→	4
b₀(4)	→	5
b₀(7)	→	8