YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

c(a(b(a(b(b(c(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 → 3

1 → 13

22 → 5

22 → 15

7 → 12

b₀(9) → 10

b₀(3) → 4

b₀(7) → 8

b₀(6) → 7

c₀(5) → 6

c₀(11) → 1

a₁(14) → 15

a₁(18) → 19

a₁(12) → 13

a₁(20) → 21

b₁(16) → 17

b₁(19) → 20

b₁(13) → 14

b₁(17) → 18

c₁(21) → 22

c₁(15) → 16

f3₀ → 2

a₀(8) → 9

a₀(10) → 11

a₀(2) → 3

a₀(4) → 5

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