YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{8, 1}

transitions:

102 → 80

102 → 42

102 → 99

102 → 27

32 → 25

29 → 59

29 → 81

87 → 26

80 → 25

98 → 40

10 → 79

15 → 61

18 → 8

18 → 80

120 → 99

120 → 27

9 → 37

5 → 15

59 → 109

110 → 44

130 → 84

99 → 127

1 → 10

1 → 3

1 → 38

8 → 5

8 → 9

8 → 74

101 → 111

60 → 8

38 → 25

86 → 119

72 → 62

116 → 42

116 → 99

116 → 27

116 → 64

2 → 73

28 → 97

45 → 25

45 → 38

45 → 63

45 → 26

16 → 39

112 → 83

7 → 31

30 → 10

30 → 55

30 → 25

30 → 38

30 → 26

42 → 113

64 → 27

64 → 42

17 → 25

17 → 71

74 → 25

27 → 99

56 → 41

b₃(115) → 116

b₃(127) → 128

b₃(129) → 130

b₃(113) → 114

a₃(114) → 115

a₃(128) → 129

a₂(100) → 101

a₂(81) → 82

a₂(86) → 87

a₂(85) → 86

a₂(43) → 44

a₂(82) → 83

a₂(40) → 41

a₂(97) → 98

a₂(111) → 112

a₂(62) → 63

a₂(44) → 45

a₂(39) → 40

a₀(3) → 4

a₀(9) → 10

a₀(7) → 1

a₀(2) → 3

a₀(6) → 7

b₀(5) → 6

b₀(10) → 8

b₀(2) → 9

b₀(4) → 5

f2₀ → 2

a₁(28) → 29

a₁(37) → 38

a₁(29) → 30

a₁(16) → 17

a₁(55) → 56

a₁(31) → 32

a₁(25) → 26

b₂(99) → 100

b₂(71) → 72

b₂(63) → 64

b₂(61) → 62

b₂(84) → 85

b₂(83) → 84

b₂(101) → 102

b₂(42) → 43

b₂(41) → 42

b₂(109) → 110

b₂(119) → 120

b₁(26) → 27

b₁(15) → 16

b₁(17) → 18

b₁(73) → 74

b₁(59) → 60

b₁(27) → 28

b₁(79) → 80

102	→	80
102	→	42
102	→	99
102	→	27
32	→	25
29	→	59
29	→	81
87	→	26
80	→	25
98	→	40
10	→	79
15	→	61
18	→	8
18	→	80
120	→	99
120	→	27
9	→	37
5	→	15
59	→	109
110	→	44
130	→	84
99	→	127
1	→	10
1	→	3
1	→	38
8	→	5
8	→	9
8	→	74
101	→	111
60	→	8
38	→	25
86	→	119
72	→	62
116	→	42
116	→	99
116	→	27
116	→	64
2	→	73
28	→	97
45	→	25
45	→	38
45	→	63
45	→	26
16	→	39
112	→	83
7	→	31
30	→	10
30	→	55
30	→	25
30	→	38
30	→	26
42	→	113
64	→	27
64	→	42
17	→	25
17	→	71
74	→	25
27	→	99
56	→	41
b₃(115)	→	116
b₃(127)	→	128
b₃(129)	→	130
b₃(113)	→	114
a₃(114)	→	115
a₃(128)	→	129
a₂(100)	→	101
a₂(81)	→	82
a₂(86)	→	87
a₂(85)	→	86
a₂(43)	→	44
a₂(82)	→	83
a₂(40)	→	41
a₂(97)	→	98
a₂(111)	→	112
a₂(62)	→	63
a₂(44)	→	45
a₂(39)	→	40
a₀(3)	→	4
a₀(9)	→	10
a₀(7)	→	1
a₀(2)	→	3
a₀(6)	→	7
b₀(5)	→	6
b₀(10)	→	8
b₀(2)	→	9
b₀(4)	→	5
f2₀	→	2
a₁(28)	→	29
a₁(37)	→	38
a₁(29)	→	30
a₁(16)	→	17
a₁(55)	→	56
a₁(31)	→	32
a₁(25)	→	26
b₂(99)	→	100
b₂(71)	→	72
b₂(63)	→	64
b₂(61)	→	62
b₂(84)	→	85
b₂(83)	→	84
b₂(101)	→	102
b₂(42)	→	43
b₂(41)	→	42
b₂(109)	→	110
b₂(119)	→	120
b₁(26)	→	27
b₁(15)	→	16
b₁(17)	→	18
b₁(73)	→	74
b₁(59)	→	60
b₁(27)	→	28
b₁(79)	→	80