YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

A(b(x0))	→	b(a(B(A(x0))))
B(a(x0))	→	a(b(A(B(x0))))
A(a(x0))	→	x0
B(b(x0))	→	x0

Proof

1 String Reversal

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

b(A(x0))	→	A(B(a(b(x0))))
a(B(x0))	→	B(A(b(a(x0))))
a(A(x0))	→	x0
b(B(x0))	→	x0

1.1 Bounds

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

final states:

{2, 6, 1}

transitions:

9 → 8

5 → 4

1 → 3

1 → 8

6 → 7

6 → 4

2 → 7

2 → 3

2 → 4

2 → 8

B₀(9) → 6

B₀(4) → 5

f4₀ → 2

b₀(7) → 8

b₀(2) → 3

a₀(2) → 7

a₀(3) → 4

A₀(8) → 9

A₀(5) → 1

9	→	8
5	→	4
1	→	3
1	→	8
6	→	7
6	→	4
2	→	7
2	→	3
2	→	4
2	→	8
B₀(9)	→	6
B₀(4)	→	5
f4₀	→	2
b₀(7)	→	8
b₀(2)	→	3
a₀(2)	→	7
a₀(3)	→	4
A₀(8)	→	9
A₀(5)	→	1