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(b(x0))))))

→

b(b(b(b(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(b(a(a(a(x0))))))

→

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

1.1 Bounds

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

final states:

{1}

transitions:

25 → 28

1 → 5

1 → 4

1 → 3

36 → 22

7 → 19

27 → 6

a₀(8) → 9

a₀(9) → 1

a₀(7) → 8

a₀(6) → 7

b₀(5) → 6

b₀(2) → 3

b₀(4) → 5

b₀(3) → 4

f2₀ → 2

b₁(19) → 20

b₁(28) → 29

b₁(22) → 23

b₁(29) → 30

b₁(31) → 32

b₁(20) → 21

b₁(30) → 31

b₁(21) → 22

a₁(24) → 25

a₁(26) → 27

a₁(33) → 34

a₁(35) → 36

a₁(32) → 33

a₁(25) → 26

a₁(23) → 24

a₁(34) → 35

25	→	28
1	→	5
1	→	4
1	→	3
36	→	22
7	→	19
27	→	6
a₀(8)	→	9
a₀(9)	→	1
a₀(7)	→	8
a₀(6)	→	7
b₀(5)	→	6
b₀(2)	→	3
b₀(4)	→	5
b₀(3)	→	4
f2₀	→	2
b₁(19)	→	20
b₁(28)	→	29
b₁(22)	→	23
b₁(29)	→	30
b₁(31)	→	32
b₁(20)	→	21
b₁(30)	→	31
b₁(21)	→	22
a₁(24)	→	25
a₁(26)	→	27
a₁(33)	→	34
a₁(35)	→	36
a₁(32)	→	33
a₁(25)	→	26
a₁(23)	→	24
a₁(34)	→	35