YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(c(a(x0)))	→	Wait(Right1(x0))
Begin(a(x0))	→	Wait(Right2(x0))
Begin(a(x0))	→	Wait(Right3(x0))
Right1(b(End(x0)))	→	Left(a(b(a(b(End(x0))))))
Right2(b(c(End(x0))))	→	Left(a(b(a(b(End(x0))))))
Right3(a(End(x0)))	→	Left(a(c(b(a(End(x0))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right1(c(x0))	→	Ac(Right1(x0))
Right2(c(x0))	→	Ac(Right2(x0))
Right3(c(x0))	→	Ac(Right3(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Ab(Left(x0))	→	Left(b(x0))
Ac(Left(x0))	→	Left(c(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(c(a(x0)))	→	a(b(a(b(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(c(b(a(x0))))

Proof

1 String Reversal

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

a(c(Begin(x0)))	→	Right1(Wait(x0))
a(Begin(x0))	→	Right2(Wait(x0))
a(Begin(x0))	→	Right3(Wait(x0))
End(b(Right1(x0)))	→	End(b(a(b(a(Left(x0))))))
End(c(b(Right2(x0))))	→	End(b(a(b(a(Left(x0))))))
End(a(Right3(x0)))	→	End(a(b(c(a(Left(x0))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
c(Right1(x0))	→	Right1(Ac(x0))
c(Right2(x0))	→	Right2(Ac(x0))
c(Right3(x0))	→	Right3(Ac(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Ac(x0))	→	c(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
a(c(b(x0)))	→	b(a(b(a(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(b(c(a(x0))))

1.1 Rule Removal

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

[Wait(x₁)]

1	0	0
1	1	1
0	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

[b(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[c(x₁)]

1	0	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[a(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[End(x₁)]

1	0	1
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Ac(x₁)]

1	0	0
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	1	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	0
1	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

the rules

a(c(Begin(x0)))	→	Right1(Wait(x0))
a(Begin(x0))	→	Right2(Wait(x0))
a(Begin(x0))	→	Right3(Wait(x0))
End(b(Right1(x0)))	→	End(b(a(b(a(Left(x0))))))
End(a(Right3(x0)))	→	End(a(b(c(a(Left(x0))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
c(Right1(x0))	→	Right1(Ac(x0))
c(Right2(x0))	→	Right2(Ac(x0))
c(Right3(x0))	→	Right3(Ac(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Ac(x0))	→	c(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
a(c(b(x0)))	→	b(a(b(a(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(b(c(a(x0))))

remain.

1.1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	4 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	4 · x₁ + -∞
[Right3(x₁)]	=	4 · x₁ + -∞
[Begin(x₁)]	=	4 · x₁ + -∞

the rules

a(c(Begin(x0)))	→	Right1(Wait(x0))
a(Begin(x0))	→	Right3(Wait(x0))
End(b(Right1(x0)))	→	End(b(a(b(a(Left(x0))))))
End(a(Right3(x0)))	→	End(a(b(c(a(Left(x0))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
c(Right1(x0))	→	Right1(Ac(x0))
c(Right2(x0))	→	Right2(Ac(x0))
c(Right3(x0))	→	Right3(Ac(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Ac(x0))	→	c(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
a(c(b(x0)))	→	b(a(b(a(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(b(c(a(x0))))

remain.

1.1.1.1 Rule Removal

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

[Wait(x₁)]

1	1	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[b(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[c(x₁)]

1	0	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

1	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

1	0	1
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Aa(x₁)]

1	1	0
0	0	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Ac(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	1	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

the rules

a(c(Begin(x0)))	→	Right1(Wait(x0))
a(Begin(x0))	→	Right3(Wait(x0))
End(a(Right3(x0)))	→	End(a(b(c(a(Left(x0))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
c(Right1(x0))	→	Right1(Ac(x0))
c(Right2(x0))	→	Right2(Ac(x0))
c(Right3(x0))	→	Right3(Ac(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Ac(x0))	→	c(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
a(c(b(x0)))	→	b(a(b(a(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(b(c(a(x0))))

remain.

1.1.1.1.1 Rule Removal

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

[Wait(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	0 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	1 · x₁ + -∞
[Right3(x₁)]	=	1 · x₁ + -∞
[Begin(x₁)]	=	1 · x₁ + -∞

the rules

a(Begin(x0))	→	Right3(Wait(x0))
End(a(Right3(x0)))	→	End(a(b(c(a(Left(x0))))))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
c(Right1(x0))	→	Right1(Ac(x0))
c(Right2(x0))	→	Right2(Ac(x0))
c(Right3(x0))	→	Right3(Ac(x0))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Ac(x0))	→	c(Left(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Wait(x0))	→	Begin(x0)
a(c(b(x0)))	→	b(a(b(a(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(b(c(a(x0))))

remain.

1.1.1.1.1.1 String Reversal

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

Begin(a(x0))	→	Wait(Right3(x0))
Right3(a(End(x0)))	→	Left(a(c(b(a(End(x0))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right1(c(x0))	→	Ac(Right1(x0))
Right2(c(x0))	→	Ac(Right2(x0))
Right3(c(x0))	→	Ac(Right3(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Ab(Left(x0))	→	Left(b(x0))
Ac(Left(x0))	→	Left(c(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(c(a(x0)))	→	a(b(a(b(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(c(b(a(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

[Wait(x₁)]

1	0	1
1	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	0
0	0	1
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[c(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right1(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
1	0	0

[Right2(x₁)]

1	0	0
1	0	1
1	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
1	0	0
0	1	0

· x₁ +

0	0	0
1	0	0
0	0	0

[a(x₁)]

1	0	0
0	1	0
1	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[End(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

1	0	0
1	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[Ac(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Left(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	1	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

the rules

Begin(a(x0))	→	Wait(Right3(x0))
Right3(a(End(x0)))	→	Left(a(c(b(a(End(x0))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right1(c(x0))	→	Ac(Right1(x0))
Right2(c(x0))	→	Ac(Right2(x0))
Right3(c(x0))	→	Ac(Right3(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Ab(Left(x0))	→	Left(b(x0))
Ac(Left(x0))	→	Left(c(x0))
Aa(Left(x0))	→	Left(a(x0))
b(c(a(x0)))	→	a(b(a(b(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(c(b(a(x0))))

remain.

1.1.1.1.1.1.1.1 Rule Removal

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

[Wait(x₁)]	=	4 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	6 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	2 · x₁ + -∞
[Right3(x₁)]	=	2 · x₁ + -∞
[Begin(x₁)]	=	15 · x₁ + -∞

the rules

Right3(a(End(x0)))	→	Left(a(c(b(a(End(x0))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right1(c(x0))	→	Ac(Right1(x0))
Right2(c(x0))	→	Ac(Right2(x0))
Right3(c(x0))	→	Ac(Right3(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Ab(Left(x0))	→	Left(b(x0))
Ac(Left(x0))	→	Left(c(x0))
Aa(Left(x0))	→	Left(a(x0))
b(c(a(x0)))	→	a(b(a(b(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(c(b(a(x0))))

remain.

1.1.1.1.1.1.1.1.1 Rule Removal

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

[b(x₁)]	=	0 · x₁ + -∞
[c(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	0 · x₁ + -∞
[Right2(x₁)]	=	0 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[Ac(x₁)]	=	0 · x₁ + -∞
[Left(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	2 · x₁ + -∞

the rules

Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right1(c(x0))	→	Ac(Right1(x0))
Right2(c(x0))	→	Ac(Right2(x0))
Right3(c(x0))	→	Ac(Right3(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Ab(Left(x0))	→	Left(b(x0))
Ac(Left(x0))	→	Left(c(x0))
Aa(Left(x0))	→	Left(a(x0))
b(c(a(x0)))	→	a(b(a(b(x0))))
b(x0)	→	c(c(x0))
a(a(x0))	→	a(c(b(a(x0))))

remain.

1.1.1.1.1.1.1.1.1.1 Bounds

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

final states:

{24, 23, 20, 18, 16, 14, 13, 12, 11, 10, 9, 8, 6, 4, 1}

transitions:

32 → 15

10 → 7

57 → 47

9 → 5

20 → 15

49 → 42

49 → 21

1 → 3

8 → 3

13 → 7

44 → 22

21 → 42

6 → 7

22 → 45

2 → 30

11 → 3

4 → 5

12 → 5

46 → 55

35 → 25

24 → 33

24 → 19

19 → 33

c₀(17) → 23

c₀(25) → 26

c₀(2) → 17

b₀(19) → 25

b₀(2) → 15

b₀(21) → 22

Right2₀(2) → 5

b₁(46) → 47

Ac₀(7) → 10

Ac₀(5) → 9

Ac₀(3) → 8

Right3₀(2) → 7

c₁(30) → 31

c₁(34) → 35

c₁(47) → 48

c₁(31) → 32

c₁(33) → 34

c₁(43) → 44

c₁(42) → 43

f13₀ → 2

Ab₀(7) → 6

Ab₀(3) → 1

Ab₀(5) → 4

Right1₀(2) → 3

a₀(26) → 24

a₀(2) → 19

a₀(15) → 21

a₀(22) → 20

Left₀(15) → 14

Left₀(19) → 18

Left₀(17) → 16

c₂(56) → 57

c₂(55) → 56

Aa₀(7) → 13

Aa₀(3) → 11

Aa₀(5) → 12

a₁(48) → 49

a₁(45) → 46

32	→	15
10	→	7
57	→	47
9	→	5
20	→	15
49	→	42
49	→	21
1	→	3
8	→	3
13	→	7
44	→	22
21	→	42
6	→	7
22	→	45
2	→	30
11	→	3
4	→	5
12	→	5
46	→	55
35	→	25
24	→	33
24	→	19
19	→	33
c₀(17)	→	23
c₀(25)	→	26
c₀(2)	→	17
b₀(19)	→	25
b₀(2)	→	15
b₀(21)	→	22
Right2₀(2)	→	5
b₁(46)	→	47
Ac₀(7)	→	10
Ac₀(5)	→	9
Ac₀(3)	→	8
Right3₀(2)	→	7
c₁(30)	→	31
c₁(34)	→	35
c₁(47)	→	48
c₁(31)	→	32
c₁(33)	→	34
c₁(43)	→	44
c₁(42)	→	43
f13₀	→	2
Ab₀(7)	→	6
Ab₀(3)	→	1
Ab₀(5)	→	4
Right1₀(2)	→	3
a₀(26)	→	24
a₀(2)	→	19
a₀(15)	→	21
a₀(22)	→	20
Left₀(15)	→	14
Left₀(19)	→	18
Left₀(17)	→	16
c₂(56)	→	57
c₂(55)	→	56
Aa₀(7)	→	13
Aa₀(3)	→	11
Aa₀(5)	→	12
a₁(48)	→	49
a₁(45)	→	46