YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(s(s(x0))))	→	s(s(a(a(x0))))
b(b(a(a(b(b(s(s(x0))))))))	→	a(a(b(b(s(s(a(a(x0))))))))
b(b(a(a(b(b(b(b(x0))))))))	→	a(a(b(b(a(a(b(b(x0))))))))
a(a(b(b(a(a(a(a(x0))))))))	→	b(b(a(a(b(b(a(a(x0))))))))

Proof

1 String Reversal

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

s(s(a(a(x0))))	→	a(a(s(s(x0))))
s(s(b(b(a(a(b(b(x0))))))))	→	a(a(s(s(b(b(a(a(x0))))))))
b(b(b(b(a(a(b(b(x0))))))))	→	b(b(a(a(b(b(a(a(x0))))))))
a(a(a(a(b(b(a(a(x0))))))))	→	a(a(b(b(a(a(b(b(x0))))))))

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a(x₁)]	=	1 · x₁ + 1
[s(x₁)]	=	2 · x₁ + 0
[b(x₁)]	=	1 · x₁ + 1

the rules

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

remain.

1.1.1 Bounds

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

final states:

{10, 1}

transitions:

10 → 4

10 → 3

1 → 12

1 → 11

b₀(5) → 6

b₀(9) → 1

b₀(8) → 9

b₀(2) → 11

b₀(15) → 16

b₀(14) → 15

b₀(4) → 5

b₀(11) → 12

f3₀ → 2

a₀(6) → 7

a₀(13) → 14

a₀(17) → 10

a₀(12) → 13

a₀(2) → 3

a₀(3) → 4

a₀(16) → 17

a₀(7) → 8

10	→	4
10	→	3
1	→	12
1	→	11
b₀(5)	→	6
b₀(9)	→	1
b₀(8)	→	9
b₀(2)	→	11
b₀(15)	→	16
b₀(14)	→	15
b₀(4)	→	5
b₀(11)	→	12
f3₀	→	2
a₀(6)	→	7
a₀(13)	→	14
a₀(17)	→	10
a₀(12)	→	13
a₀(2)	→	3
a₀(3)	→	4
a₀(16)	→	17
a₀(7)	→	8