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

→

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

Proof

1 String Reversal

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

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

→

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

32 → 21

3 → 49

5 → 25

1 → 6

1 → 4

1 → 53

7 → 17

24 → 8

56 → 29

b₁(28) → 29

b₁(22) → 23

b₁(50) → 51

b₁(18) → 19

b₁(26) → 27

b₁(54) → 55

b₁(52) → 53

b₁(20) → 21

b₁(30) → 31

b₀(5) → 6

b₀(7) → 8

b₀(3) → 4

a₀(8) → 1

a₀(4) → 5

a₀(2) → 3

a₀(6) → 7

f2₀ → 2

a₁(53) → 54

a₁(29) → 30

a₁(17) → 18

a₁(55) → 56

a₁(51) → 52

a₁(31) → 32

a₁(21) → 22

a₁(49) → 50

a₁(27) → 28

a₁(19) → 20

a₁(25) → 26

a₁(23) → 24

32	→	21
3	→	49
5	→	25
1	→	6
1	→	4
1	→	53
7	→	17
24	→	8
56	→	29
b₁(28)	→	29
b₁(22)	→	23
b₁(50)	→	51
b₁(18)	→	19
b₁(26)	→	27
b₁(54)	→	55
b₁(52)	→	53
b₁(20)	→	21
b₁(30)	→	31
b₀(5)	→	6
b₀(7)	→	8
b₀(3)	→	4
a₀(8)	→	1
a₀(4)	→	5
a₀(2)	→	3
a₀(6)	→	7
f2₀	→	2
a₁(53)	→	54
a₁(29)	→	30
a₁(17)	→	18
a₁(55)	→	56
a₁(51)	→	52
a₁(31)	→	32
a₁(21)	→	22
a₁(49)	→	50
a₁(27)	→	28
a₁(19)	→	20
a₁(25)	→	26
a₁(23)	→	24