YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

33 → 6

33 → 5

9 → 23

1 → 4

1 → 3

40 → 111

44 → 7

121 → 69

88 → 27

118 → 122

77 → 25

30 → 34

132 → 71

74 → 78

43 → 67

b₂(114) → 115

b₂(124) → 125

b₂(126) → 127

b₂(81) → 82

b₂(123) → 124

b₂(78) → 79

b₂(112) → 113

b₂(125) → 126

b₂(79) → 80

b₂(82) → 83

b₂(113) → 114

b₂(111) → 112

b₂(80) → 81

b₂(115) → 116

b₂(122) → 123

a₀(11) → 1

a₀(8) → 9

a₀(9) → 10

a₀(7) → 8

a₀(10) → 11

b₀(5) → 6

b₀(2) → 3

b₀(6) → 7

b₀(4) → 5

b₀(3) → 4

f2₀ → 2

b₁(37) → 38

b₁(70) → 71

b₁(23) → 24

b₁(24) → 25

b₁(26) → 27

b₁(38) → 39

b₁(25) → 26

b₁(34) → 35

b₁(27) → 28

b₁(35) → 36

b₁(71) → 72

b₁(36) → 37

b₁(69) → 70

b₁(67) → 68

b₁(68) → 69

a₂(117) → 118

a₂(128) → 129

a₂(131) → 132

a₂(84) → 85

a₂(86) → 87

a₂(87) → 88

a₂(83) → 84

a₂(118) → 119

a₂(130) → 131

a₂(129) → 130

a₂(127) → 128

a₂(85) → 86

a₂(120) → 121

a₂(116) → 117

a₂(119) → 120

a₁(75) → 76

a₁(41) → 42

a₁(29) → 30

a₁(76) → 77

a₁(73) → 74

a₁(28) → 29

a₁(74) → 75

a₁(31) → 32

a₁(42) → 43

a₁(72) → 73

a₁(32) → 33

a₁(39) → 40

a₁(43) → 44

a₁(30) → 31

a₁(40) → 41

33	→	6
33	→	5
9	→	23
1	→	4
1	→	3
40	→	111
44	→	7
121	→	69
88	→	27
118	→	122
77	→	25
30	→	34
132	→	71
74	→	78
43	→	67
b₂(114)	→	115
b₂(124)	→	125
b₂(126)	→	127
b₂(81)	→	82
b₂(123)	→	124
b₂(78)	→	79
b₂(112)	→	113
b₂(125)	→	126
b₂(79)	→	80
b₂(82)	→	83
b₂(113)	→	114
b₂(111)	→	112
b₂(80)	→	81
b₂(115)	→	116
b₂(122)	→	123
a₀(11)	→	1
a₀(8)	→	9
a₀(9)	→	10
a₀(7)	→	8
a₀(10)	→	11
b₀(5)	→	6
b₀(2)	→	3
b₀(6)	→	7
b₀(4)	→	5
b₀(3)	→	4
f2₀	→	2
b₁(37)	→	38
b₁(70)	→	71
b₁(23)	→	24
b₁(24)	→	25
b₁(26)	→	27
b₁(38)	→	39
b₁(25)	→	26
b₁(34)	→	35
b₁(27)	→	28
b₁(35)	→	36
b₁(71)	→	72
b₁(36)	→	37
b₁(69)	→	70
b₁(67)	→	68
b₁(68)	→	69
a₂(117)	→	118
a₂(128)	→	129
a₂(131)	→	132
a₂(84)	→	85
a₂(86)	→	87
a₂(87)	→	88
a₂(83)	→	84
a₂(118)	→	119
a₂(130)	→	131
a₂(129)	→	130
a₂(127)	→	128
a₂(85)	→	86
a₂(120)	→	121
a₂(116)	→	117
a₂(119)	→	120
a₁(75)	→	76
a₁(41)	→	42
a₁(29)	→	30
a₁(76)	→	77
a₁(73)	→	74
a₁(28)	→	29
a₁(74)	→	75
a₁(31)	→	32
a₁(42)	→	43
a₁(72)	→	73
a₁(32)	→	33
a₁(39)	→	40
a₁(43)	→	44
a₁(30)	→	31
a₁(40)	→	41