YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

b(a(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:

3 → 31

1 → 5

1 → 3

1 → 34

40 → 22

7 → 21

30 → 6

30 → 32

30 → 35

b₀(3) → 4

b₀(7) → 8

b₀(6) → 7

b₀(10) → 1

a₀(5) → 6

a₀(9) → 10

a₀(8) → 9

a₀(2) → 3

a₀(4) → 5

f2₀ → 2

a₁(28) → 29

a₁(37) → 38

a₁(23) → 24

a₁(24) → 25

a₁(38) → 39

a₁(31) → 32

a₁(34) → 35

a₁(27) → 28

a₁(33) → 34

a₁(21) → 22

b₁(22) → 23

b₁(26) → 27

b₁(29) → 30

b₁(35) → 36

b₁(32) → 33

b₁(36) → 37

b₁(39) → 40

b₁(25) → 26

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