YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

39 → 22

9 → 51

5 → 75

55 → 56

62 → 33

1 → 5

1 → 4

1 → 3

26 → 104

76 → 54

91 → 123

36 → 86

52 → 32

28 → 31

112 → 54

7 → 21

30 → 5

30 → 54

30 → 76

30 → 55

132 → 56

24 → 53

94 → 53

a₃(127) → 128

a₃(129) → 130

a₃(125) → 126

a₃(123) → 124

a₃(131) → 132

a₃(124) → 125

b₃(126) → 127

b₃(128) → 129

b₃(130) → 131

b₂(91) → 92

b₂(58) → 59

b₂(60) → 61

b₂(107) → 108

b₂(109) → 110

b₂(56) → 57

b₂(111) → 112

b₂(93) → 94

b₂(89) → 90

a₀(3) → 4

a₀(8) → 9

a₀(4) → 5

a₀(2) → 3

a₀(6) → 7

a₀(10) → 1

b₀(5) → 6

b₀(7) → 8

b₀(9) → 10

f2₀ → 2

b₁(28) → 29

b₁(24) → 25

b₁(26) → 27

b₁(38) → 39

b₁(34) → 35

b₁(36) → 37

a₂(90) → 91

a₂(105) → 106

a₂(54) → 55

a₂(110) → 111

a₂(55) → 56

a₂(92) → 93

a₂(61) → 62

a₂(104) → 105

a₂(86) → 87

a₂(87) → 88

a₂(53) → 54

a₂(57) → 58

a₂(108) → 109

a₂(59) → 60

a₂(106) → 107

a₂(88) → 89

a₁(22) → 23

a₁(75) → 76

a₁(29) → 30

a₁(33) → 34

a₁(51) → 52

a₁(35) → 36

a₁(31) → 32

a₁(21) → 22

a₁(37) → 38

a₁(32) → 33

a₁(27) → 28

a₁(25) → 26

a₁(23) → 24

39	→	22
9	→	51
5	→	75
55	→	56
62	→	33
1	→	5
1	→	4
1	→	3
26	→	104
76	→	54
91	→	123
36	→	86
52	→	32
28	→	31
112	→	54
7	→	21
30	→	5
30	→	54
30	→	76
30	→	55
132	→	56
24	→	53
94	→	53
a₃(127)	→	128
a₃(129)	→	130
a₃(125)	→	126
a₃(123)	→	124
a₃(131)	→	132
a₃(124)	→	125
b₃(126)	→	127
b₃(128)	→	129
b₃(130)	→	131
b₂(91)	→	92
b₂(58)	→	59
b₂(60)	→	61
b₂(107)	→	108
b₂(109)	→	110
b₂(56)	→	57
b₂(111)	→	112
b₂(93)	→	94
b₂(89)	→	90
a₀(3)	→	4
a₀(8)	→	9
a₀(4)	→	5
a₀(2)	→	3
a₀(6)	→	7
a₀(10)	→	1
b₀(5)	→	6
b₀(7)	→	8
b₀(9)	→	10
f2₀	→	2
b₁(28)	→	29
b₁(24)	→	25
b₁(26)	→	27
b₁(38)	→	39
b₁(34)	→	35
b₁(36)	→	37
a₂(90)	→	91
a₂(105)	→	106
a₂(54)	→	55
a₂(110)	→	111
a₂(55)	→	56
a₂(92)	→	93
a₂(61)	→	62
a₂(104)	→	105
a₂(86)	→	87
a₂(87)	→	88
a₂(53)	→	54
a₂(57)	→	58
a₂(108)	→	109
a₂(59)	→	60
a₂(106)	→	107
a₂(88)	→	89
a₁(22)	→	23
a₁(75)	→	76
a₁(29)	→	30
a₁(33)	→	34
a₁(51)	→	52
a₁(35)	→	36
a₁(31)	→	32
a₁(21)	→	22
a₁(37)	→	38
a₁(32)	→	33
a₁(27)	→	28
a₁(25)	→	26
a₁(23)	→	24