YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

1 → 9

1 → 3

a₀(7) → 8

a₀(10) → 11

a₀(13) → 14

b₀(11) → 12

b₀(17) → 18

b₀(16) → 17

b₀(15) → 16

b₀(3) → 4

b₀(19) → 1

b₀(8) → 9

b₀(12) → 13

b₀(14) → 15

b₀(9) → 10

b₀(4) → 5

b₀(18) → 19

b₀(2) → 3

b₀(6) → 7

b₀(5) → 6

f2₀ → 2

1	→	9
1	→	3
a₀(7)	→	8
a₀(10)	→	11
a₀(13)	→	14
b₀(11)	→	12
b₀(17)	→	18
b₀(16)	→	17
b₀(15)	→	16
b₀(3)	→	4
b₀(19)	→	1
b₀(8)	→	9
b₀(12)	→	13
b₀(14)	→	15
b₀(9)	→	10
b₀(4)	→	5
b₀(18)	→	19
b₀(2)	→	3
b₀(6)	→	7
b₀(5)	→	6
f2₀	→	2