YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

1 → 5

1 → 3

22 → 5

7 → 12

a₀(11) → 1

a₀(8) → 9

a₀(4) → 5

a₀(2) → 3

a₀(5) → 6

b₀(7) → 8

b₀(9) → 10

b₀(10) → 11

b₀(6) → 7

b₀(3) → 4

f2₀ → 2

b₁(19) → 20

b₁(16) → 17

b₁(20) → 21

b₁(13) → 14

b₁(17) → 18

a₁(15) → 16

a₁(14) → 15

a₁(18) → 19

a₁(12) → 13

a₁(21) → 22

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