YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

B(x0)	→	W(M(V(x0)))
M(x0)	→	x0
M(V(a(x0)))	→	V(Xa(x0))
M(V(b(x0)))	→	V(Xb(x0))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
Xb(a(x0))	→	a(Xb(x0))
Xb(b(x0))	→	b(Xb(x0))
Xa(E(x0))	→	a(E(x0))
Xb(E(x0))	→	b(E(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

Proof

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[E(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[V(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[W(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Xa(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[R(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[B(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

[Xb(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Yb(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ya(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[L(x₁)]

1	0	0
0	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[D(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[M(x₁)]

1	0	0
1	1	1
0	0	1

· x₁ +

1	0	0
1	0	0
1	0	0

the rules

B(x0)	→	W(M(V(x0)))
M(V(a(x0)))	→	V(Xa(x0))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
Xb(a(x0))	→	a(Xb(x0))
Xb(b(x0))	→	b(Xb(x0))
Xa(E(x0))	→	a(E(x0))
Xb(E(x0))	→	b(E(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[a(x₁)]	=	0 · x₁ + -∞
[E(x₁)]	=	0 · x₁ + -∞
[V(x₁)]	=	0 · x₁ + -∞
[W(x₁)]	=	0 · x₁ + -∞
[Xa(x₁)]	=	0 · x₁ + -∞
[R(x₁)]	=	0 · x₁ + -∞
[B(x₁)]	=	0 · x₁ + -∞
[Xb(x₁)]	=	7 · x₁ + -∞
[Yb(x₁)]	=	0 · x₁ + -∞
[Ya(x₁)]	=	0 · x₁ + -∞
[L(x₁)]	=	0 · x₁ + -∞
[D(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[M(x₁)]	=	0 · x₁ + -∞

the rules

B(x0)	→	W(M(V(x0)))
M(V(a(x0)))	→	V(Xa(x0))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
Xb(a(x0))	→	a(Xb(x0))
Xb(b(x0))	→	b(Xb(x0))
Xa(E(x0))	→	a(E(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

remain.

1.1.1 String Reversal

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

B(x0)	→	V(M(W(x0)))
a(V(M(x0)))	→	Xa(V(x0))
a(Xa(x0))	→	Xa(a(x0))
b(Xa(x0))	→	Xa(b(x0))
a(Xb(x0))	→	Xb(a(x0))
b(Xb(x0))	→	Xb(b(x0))
E(Xa(x0))	→	E(a(x0))
V(W(x0))	→	L(R(x0))
a(L(x0))	→	L(Ya(x0))
b(L(x0))	→	L(Yb(x0))
a(a(L(x0)))	→	a(b(a(D(x0))))
D(Ya(x0))	→	a(D(x0))
D(Yb(x0))	→	b(D(x0))
D(R(x0))	→	B(x0)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a(x₁)]	=	4 · x₁ + 0
[E(x₁)]	=	1 · x₁ + 12
[V(x₁)]	=	1 · x₁ + 1
[W(x₁)]	=	1 · x₁ + 0
[Xa(x₁)]	=	4 · x₁ + 0
[R(x₁)]	=	1 · x₁ + 1
[B(x₁)]	=	1 · x₁ + 1
[Xb(x₁)]	=	6 · x₁ + 1
[Yb(x₁)]	=	1 · x₁ + 0
[Ya(x₁)]	=	4 · x₁ + 0
[L(x₁)]	=	1 · x₁ + 0
[D(x₁)]	=	1 · x₁ + 0
[b(x₁)]	=	1 · x₁ + 0
[M(x₁)]	=	1 · x₁ + 0

the rules

B(x0)	→	V(M(W(x0)))
a(V(M(x0)))	→	Xa(V(x0))
a(Xa(x0))	→	Xa(a(x0))
b(Xa(x0))	→	Xa(b(x0))
b(Xb(x0))	→	Xb(b(x0))
E(Xa(x0))	→	E(a(x0))
V(W(x0))	→	L(R(x0))
a(L(x0))	→	L(Ya(x0))
b(L(x0))	→	L(Yb(x0))
a(a(L(x0)))	→	a(b(a(D(x0))))
D(Ya(x0))	→	a(D(x0))
D(Yb(x0))	→	b(D(x0))
D(R(x0))	→	B(x0)

remain.

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[E(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[V(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[W(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

[Xa(x₁)]

1	0	0
1	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[R(x₁)]

1	0	0
0	0	0
1	1	0

· x₁ +

0	0	0
0	0	0
1	0	0

[B(x₁)]

1	0	0
1	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Xb(x₁)]

1	0	1
1	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[Yb(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Ya(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[L(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[D(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	1
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[M(x₁)]

1	0	0
1	1	1
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

the rules

B(x0)	→	V(M(W(x0)))
a(V(M(x0)))	→	Xa(V(x0))
a(Xa(x0))	→	Xa(a(x0))
b(Xa(x0))	→	Xa(b(x0))
E(Xa(x0))	→	E(a(x0))
V(W(x0))	→	L(R(x0))
a(L(x0))	→	L(Ya(x0))
b(L(x0))	→	L(Yb(x0))
a(a(L(x0)))	→	a(b(a(D(x0))))
D(Ya(x0))	→	a(D(x0))
D(Yb(x0))	→	b(D(x0))
D(R(x0))	→	B(x0)

remain.

1.1.1.1.1.1 String Reversal

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

B(x0)	→	W(M(V(x0)))
M(V(a(x0)))	→	V(Xa(x0))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
Xa(E(x0))	→	a(E(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[E(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[V(x₁)]

1	0	1
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[W(x₁)]

1	0	0
1	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Xa(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

0	0	0
1	0	0
0	0	0

[R(x₁)]

1	1	1
1	1	1
1	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[B(x₁)]

1	1	1
1	1	1
1	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Yb(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ya(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
1	0	0
0	0	0

[L(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[D(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[M(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

the rules

B(x0)	→	W(M(V(x0)))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
Xa(E(x0))	→	a(E(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

remain.

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[a(x₁)]	=	0 · x₁ + -∞
[E(x₁)]	=	0 · x₁ + -∞
[V(x₁)]	=	5 · x₁ + -∞
[W(x₁)]	=	0 · x₁ + -∞
[Xa(x₁)]	=	13 · x₁ + -∞
[R(x₁)]	=	3 · x₁ + -∞
[B(x₁)]	=	5 · x₁ + -∞
[Yb(x₁)]	=	0 · x₁ + -∞
[Ya(x₁)]	=	0 · x₁ + -∞
[L(x₁)]	=	2 · x₁ + -∞
[D(x₁)]	=	2 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[M(x₁)]	=	0 · x₁ + -∞

the rules

B(x0)	→	W(M(V(x0)))
Xa(a(x0))	→	a(Xa(x0))
Xa(b(x0))	→	b(Xa(x0))
W(V(x0))	→	R(L(x0))
L(a(x0))	→	Ya(L(x0))
L(b(x0))	→	Yb(L(x0))
L(a(a(x0)))	→	D(a(b(a(x0))))
Ya(D(x0))	→	D(a(x0))
Yb(D(x0))	→	D(b(x0))
R(D(x0))	→	B(x0)

remain.

1.1.1.1.1.1.1.1.1 String Reversal

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

B(x0)	→	V(M(W(x0)))
a(Xa(x0))	→	Xa(a(x0))
b(Xa(x0))	→	Xa(b(x0))
V(W(x0))	→	L(R(x0))
a(L(x0))	→	L(Ya(x0))
b(L(x0))	→	L(Yb(x0))
a(a(L(x0)))	→	a(b(a(D(x0))))
D(Ya(x0))	→	a(D(x0))
D(Yb(x0))	→	b(D(x0))
D(R(x0))	→	B(x0)

1.1.1.1.1.1.1.1.1.1 Bounds

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

final states:

{20, 19, 17, 15, 13, 11, 9, 7, 5, 1}

transitions:

15 → 6

5 → 6

20 → 16

13 → 8

2 → 21

11 → 6

7 → 8

17 → 16

24 → 20

19 → 16

L₀(10) → 9

L₀(12) → 11

L₀(14) → 13

W₀(2) → 3

Xa₀(6) → 5

Xa₀(8) → 7

M₀(3) → 4

V₁(23) → 24

Yb₀(2) → 14

R₀(2) → 10

W₁(21) → 22

Ya₀(2) → 12

V₀(4) → 1

b₀(2) → 8

b₀(16) → 19

b₀(17) → 18

f14₀ → 2

B₀(2) → 20

D₀(2) → 16

M₁(22) → 23

a₀(2) → 6

a₀(18) → 15

a₀(16) → 17

15	→	6
5	→	6
20	→	16
13	→	8
2	→	21
11	→	6
7	→	8
17	→	16
24	→	20
19	→	16
L₀(10)	→	9
L₀(12)	→	11
L₀(14)	→	13
W₀(2)	→	3
Xa₀(6)	→	5
Xa₀(8)	→	7
M₀(3)	→	4
V₁(23)	→	24
Yb₀(2)	→	14
R₀(2)	→	10
W₁(21)	→	22
Ya₀(2)	→	12
V₀(4)	→	1
b₀(2)	→	8
b₀(16)	→	19
b₀(17)	→	18
f14₀	→	2
B₀(2)	→	20
D₀(2)	→	16
M₁(22)	→	23
a₀(2)	→	6
a₀(18)	→	15
a₀(16)	→	17