YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(b(a(a(b(x0)))))	→	Wait(Right2(x0))
Begin(a(a(b(x0))))	→	Wait(Right3(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right2(a(b(End(x0))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right3(a(b(b(End(x0)))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

Proof

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
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Right5(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	1	0
0	1	0
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Right4(x₁)]

1	0	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	1	0
0	1	0
0	0	0

· 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
0	0	0
0	0	0

[End(x₁)]

1	1	0
0	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

[Right3(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

the rules

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(b(a(a(b(x0)))))	→	Wait(Right2(x0))
Begin(a(a(b(x0))))	→	Wait(Right3(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

remain.

1.1 Rule Removal

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

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

the rules

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(a(a(b(x0))))	→	Wait(Right3(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

remain.

1.1.1 Rule Removal

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

[Wait(x₁)]	=	8 · x₁ + -∞
[Right5(x₁)]	=	4 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	4 · x₁ + -∞
[Right2(x₁)]	=	9 · x₁ + -∞
[Left(x₁)]	=	4 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[Right4(x₁)]	=	4 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	4 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	12 · x₁ + -∞

the rules

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

remain.

1.1.1.1 String Reversal

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

b(a(a(b(b(Begin(x0))))))	→	Right1(Wait(x0))
b(a(Begin(x0)))	→	Right4(Wait(x0))
b(Begin(x0))	→	Right5(Wait(x0))
End(a(Right1(x0)))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
End(a(b(b(a(Right4(x0))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
End(a(a(b(b(a(Right5(x0)))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right2(x0))	→	Right2(Ab(x0))
b(Right3(x0))	→	Right3(Ab(x0))
b(Right4(x0))	→	Right4(Ab(x0))
b(Right5(x0))	→	Right5(Ab(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Wait(x0))	→	Begin(x0)
b(a(a(b(b(a(x0))))))	→	a(b(a(b(b(a(a(x0)))))))

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[Wait(x₁)]	=	1 · x₁ + 0
[Right5(x₁)]	=	2 · x₁ + 0
[a(x₁)]	=	1 · x₁ + 0
[Right1(x₁)]	=	8 · x₁ + 0
[Right2(x₁)]	=	1 · x₁ + 0
[Left(x₁)]	=	1 · x₁ + 0
[b(x₁)]	=	2 · x₁ + 0
[Right4(x₁)]	=	2 · x₁ + 0
[Ab(x₁)]	=	2 · x₁ + 0
[Aa(x₁)]	=	1 · x₁ + 0
[End(x₁)]	=	1 · x₁ + 0
[Right3(x₁)]	=	5 · x₁ + 2
[Begin(x₁)]	=	1 · x₁ + 0

the rules

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

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[Wait(x₁)]	=	4 · x₁ + 0
[Right5(x₁)]	=	1 · x₁ + 1
[a(x₁)]	=	1 · x₁ + 0
[Right1(x₁)]	=	1 · x₁ + 3
[Right2(x₁)]	=	8 · x₁ + 7
[Left(x₁)]	=	1 · x₁ + 0
[b(x₁)]	=	1 · x₁ + 1
[Right4(x₁)]	=	1 · x₁ + 1
[Ab(x₁)]	=	1 · x₁ + 1
[Aa(x₁)]	=	1 · x₁ + 0
[End(x₁)]	=	4 · x₁ + 0
[Right3(x₁)]	=	4 · x₁ + 0
[Begin(x₁)]	=	4 · x₁ + 0

the rules

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right1(b(x0))	→	Ab(Right1(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

remain.

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

1.1.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	1	1
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Right5(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right1(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Right4(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

1	0	0
0	1	0
0	1	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Aa(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[Right3(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

[Begin(x₁)]

1	1	1
0	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

the rules

b(a(Begin(x0)))	→	Right4(Wait(x0))
b(Begin(x0))	→	Right5(Wait(x0))
End(a(Right1(x0)))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
End(a(b(b(a(Right4(x0))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
End(a(a(b(b(a(Right5(x0)))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right4(x0))	→	Right4(Ab(x0))
b(Right5(x0))	→	Right5(Ab(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Wait(x0))	→	Begin(x0)
b(a(a(b(b(a(x0))))))	→	a(b(a(b(b(a(a(x0)))))))

remain.

1.1.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₁ + -∞
[Right5(x₁)]	=	1 · x₁ + -∞
[a(x₁)]	=	0 · x₁ + -∞
[Right1(x₁)]	=	4 · x₁ + -∞
[Right2(x₁)]	=	9 · x₁ + -∞
[Left(x₁)]	=	1 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞
[Right4(x₁)]	=	1 · x₁ + -∞
[Ab(x₁)]	=	0 · x₁ + -∞
[Aa(x₁)]	=	0 · x₁ + -∞
[End(x₁)]	=	0 · x₁ + -∞
[Right3(x₁)]	=	0 · x₁ + -∞
[Begin(x₁)]	=	5 · x₁ + -∞

the rules

b(a(Begin(x0)))	→	Right4(Wait(x0))
b(Begin(x0))	→	Right5(Wait(x0))
End(a(b(b(a(Right4(x0))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
End(a(a(b(b(a(Right5(x0)))))))	→	End(a(b(a(b(b(a(a(Left(x0)))))))))
a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))
b(Right1(x0))	→	Right1(Ab(x0))
b(Right4(x0))	→	Right4(Ab(x0))
b(Right5(x0))	→	Right5(Ab(x0))
Left(Aa(x0))	→	a(Left(x0))
Left(Ab(x0))	→	b(Left(x0))
Left(Wait(x0))	→	Begin(x0)
b(a(a(b(b(a(x0))))))	→	a(b(a(b(b(a(a(x0)))))))

remain.

1.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:

{26, 25, 24, 7, 23, 22, 20, 19, 18, 17, 16, 14, 5, 4, 1}

transitions:

111 → 118

176 → 204

176 → 215

25 → 6

205 → 176

263 → 276

271 → 166

80 → 28

103 → 105

152 → 24

152 → 9

152 → 148

152 → 162

214 → 185

289 → 173

15 → 33

167 → 148

167 → 145

167 → 6

167 → 24

167 → 162

167 → 10

119 → 121

122 → 130

260 → 268

260 → 270

260 → 274

18 → 27

226 → 148

226 → 24

226 → 162

226 → 9

226 → 12

120 → 29

225 → 233

225 → 252

225 → 254

146 → 161

134 → 142

209 → 235

95 → 31

59 → 32

34 → 42

34 → 71

34 → 75

34 → 79

34 → 111

275 → 195

185 → 213

185 → 224

241 → 166

55 → 57

255 → 262

293 → 46

107 → 26

123 → 30

287 → 185

44 → 29

135 → 32

26 → 29

261 → 152

76 → 28

297 → 122

253 → 173

269 → 176

79 → 81

91 → 93

58 → 66

177 → 161

177 → 7

177 → 146

177 → 147

177 → 8

177 → 11

177 → 13

248 → 195

186 → 161

186 → 7

186 → 146

186 → 8

186 → 147

186 → 11

186 → 13

72 → 28

173 → 184

173 → 197

277 → 281

6 → 145

237 → 151

174 → 145

174 → 6

174 → 24

174 → 10

283 → 152

67 → 292

264 → 150

82 → 90

143 → 296

2 → 165

188 → 166

106 → 294

16 → 27

14 → 27

112 → 28

104 → 32

236 → 259

282 → 286

282 → 288

282 → 290

7 → 6

295 → 91

217 → 148

217 → 145

217 → 6

217 → 24

217 → 162

217 → 9

217 → 12

234 → 185

216 → 227

216 → 240

216 → 247

46 → 54

162 → 148

35 → 28

278 → 151

256 → 149

83 → 29

198 → 173

47 → 30

17 → 27

68 → 26

132 → 31

131 → 133

92 → 30

195 → 208

24 → 6

19 → 27

144 → 26

43 → 45

210 → 150

166 → 173

166 → 175

166 → 187

166 → 194

56 → 31

94 → 102

228 → 176

291 → 255

196 → 149

Right4₂(176) → 177

Right4₂(209) → 210

Right4₂(216) → 217

Right4₂(260) → 261

Right4₂(236) → 237

Right4₂(195) → 196

Right5₁(111) → 112

Right5₁(173) → 174

Right5₁(122) → 123

Right5₁(119) → 120

Right5₁(143) → 144

Right5₁(131) → 132

Right5₁(134) → 135

Aa₀(2) → 15

a₁(146) → 147

a₁(145) → 146

a₁(151) → 152

a₁(149) → 150

Right1₀(21) → 20

Right1₀(15) → 14

Ab₁(118) → 119

Ab₁(187) → 188

Ab₁(102) → 103

Ab₁(296) → 297

Ab₁(294) → 295

Ab₁(90) → 91

Ab₁(292) → 293

Ab₁(45) → 46

Ab₁(81) → 82

Ab₁(252) → 253

Ab₁(240) → 241

Ab₁(270) → 271

Ab₁(197) → 198

Ab₁(42) → 43

Ab₁(57) → 58

Ab₁(288) → 289

Ab₁(121) → 122

Ab₁(133) → 134

Right5₂(225) → 226

Right5₂(255) → 256

Right5₂(185) → 186

Right5₂(263) → 264

Right5₂(282) → 283

Right5₂(277) → 278

Wait₁(165) → 166

Right5₀(21) → 23

Right5₀(3) → 4

Right5₀(15) → 19

Begin₀(2) → 25

Ab₂(194) → 195

Ab₂(247) → 248

Ab₂(254) → 255

Ab₂(215) → 216

Ab₂(235) → 236

Ab₂(290) → 291

Ab₂(276) → 277

Ab₂(274) → 275

Ab₂(224) → 225

Right2₁(71) → 72

a₀(30) → 31

a₀(12) → 13

a₀(7) → 8

a₀(2) → 27

a₀(32) → 26

a₀(6) → 7

a₀(10) → 11

a₀(27) → 28

End₀(13) → 5

b₁(150) → 151

b₁(148) → 149

b₁(161) → 162

b₁(147) → 148

Right3₀(15) → 17

Aa₂(281) → 282

Aa₂(227) → 228

Aa₂(208) → 209

Aa₂(286) → 287

Aa₂(268) → 269

Aa₂(204) → 205

Aa₂(262) → 263

Aa₂(184) → 185

Aa₂(213) → 214

Aa₂(175) → 176

Aa₂(259) → 260

Aa₂(233) → 234

f13₀ → 2

Right3₁(75) → 76

Right4₀(15) → 18

Right4₀(3) → 1

Right4₀(21) → 22

Wait₀(2) → 3

Right2₀(15) → 16

Left₀(2) → 6

Right4₁(82) → 83

Right4₁(103) → 104

Right4₁(106) → 107

Right4₁(79) → 80

Right4₁(166) → 167

Right4₁(94) → 95

Right4₁(91) → 92

Right1₁(34) → 35

Right1₁(67) → 68

Right1₁(58) → 59

Right1₁(46) → 47

Right1₁(55) → 56

Right1₁(43) → 44

b₀(6) → 24

b₀(9) → 10

b₀(28) → 29

b₀(8) → 9

b₀(29) → 30

b₀(11) → 12

b₀(31) → 32

Ab₀(2) → 21

Aa₁(33) → 34

Aa₁(105) → 106

Aa₁(130) → 131

Aa₁(142) → 143

Aa₁(93) → 94

Aa₁(54) → 55

Aa₁(66) → 67

111	→	118
176	→	204
176	→	215
25	→	6
205	→	176
263	→	276
271	→	166
80	→	28
103	→	105
152	→	24
152	→	9
152	→	148
152	→	162
214	→	185
289	→	173
15	→	33
167	→	148
167	→	145
167	→	6
167	→	24
167	→	162
167	→	10
119	→	121
122	→	130
260	→	268
260	→	270
260	→	274
18	→	27
226	→	148
226	→	24
226	→	162
226	→	9
226	→	12
120	→	29
225	→	233
225	→	252
225	→	254
146	→	161
134	→	142
209	→	235
95	→	31
59	→	32
34	→	42
34	→	71
34	→	75
34	→	79
34	→	111
275	→	195
185	→	213
185	→	224
241	→	166
55	→	57
255	→	262
293	→	46
107	→	26
123	→	30
287	→	185
44	→	29
135	→	32
26	→	29
261	→	152
76	→	28
297	→	122
253	→	173
269	→	176
79	→	81
91	→	93
58	→	66
177	→	161
177	→	7
177	→	146
177	→	147
177	→	8
177	→	11
177	→	13
248	→	195
186	→	161
186	→	7
186	→	146
186	→	8
186	→	147
186	→	11
186	→	13
72	→	28
173	→	184
173	→	197
277	→	281
6	→	145
237	→	151
174	→	145
174	→	6
174	→	24
174	→	10
283	→	152
67	→	292
264	→	150
82	→	90
143	→	296
2	→	165
188	→	166
106	→	294
16	→	27
14	→	27
112	→	28
104	→	32
236	→	259
282	→	286
282	→	288
282	→	290
7	→	6
295	→	91
217	→	148
217	→	145
217	→	6
217	→	24
217	→	162
217	→	9
217	→	12
234	→	185
216	→	227
216	→	240
216	→	247
46	→	54
162	→	148
35	→	28
278	→	151
256	→	149
83	→	29
198	→	173
47	→	30
17	→	27
68	→	26
132	→	31
131	→	133
92	→	30
195	→	208
24	→	6
19	→	27
144	→	26
43	→	45
210	→	150
166	→	173
166	→	175
166	→	187
166	→	194
56	→	31
94	→	102
228	→	176
291	→	255
196	→	149
Right4₂(176)	→	177
Right4₂(209)	→	210
Right4₂(216)	→	217
Right4₂(260)	→	261
Right4₂(236)	→	237
Right4₂(195)	→	196
Right5₁(111)	→	112
Right5₁(173)	→	174
Right5₁(122)	→	123
Right5₁(119)	→	120
Right5₁(143)	→	144
Right5₁(131)	→	132
Right5₁(134)	→	135
Aa₀(2)	→	15
a₁(146)	→	147
a₁(145)	→	146
a₁(151)	→	152
a₁(149)	→	150
Right1₀(21)	→	20
Right1₀(15)	→	14
Ab₁(118)	→	119
Ab₁(187)	→	188
Ab₁(102)	→	103
Ab₁(296)	→	297
Ab₁(294)	→	295
Ab₁(90)	→	91
Ab₁(292)	→	293
Ab₁(45)	→	46
Ab₁(81)	→	82
Ab₁(252)	→	253
Ab₁(240)	→	241
Ab₁(270)	→	271
Ab₁(197)	→	198
Ab₁(42)	→	43
Ab₁(57)	→	58
Ab₁(288)	→	289
Ab₁(121)	→	122
Ab₁(133)	→	134
Right5₂(225)	→	226
Right5₂(255)	→	256
Right5₂(185)	→	186
Right5₂(263)	→	264
Right5₂(282)	→	283
Right5₂(277)	→	278
Wait₁(165)	→	166
Right5₀(21)	→	23
Right5₀(3)	→	4
Right5₀(15)	→	19
Begin₀(2)	→	25
Ab₂(194)	→	195
Ab₂(247)	→	248
Ab₂(254)	→	255
Ab₂(215)	→	216
Ab₂(235)	→	236
Ab₂(290)	→	291
Ab₂(276)	→	277
Ab₂(274)	→	275
Ab₂(224)	→	225
Right2₁(71)	→	72
a₀(30)	→	31
a₀(12)	→	13
a₀(7)	→	8
a₀(2)	→	27
a₀(32)	→	26
a₀(6)	→	7
a₀(10)	→	11
a₀(27)	→	28
End₀(13)	→	5
b₁(150)	→	151
b₁(148)	→	149
b₁(161)	→	162
b₁(147)	→	148
Right3₀(15)	→	17
Aa₂(281)	→	282
Aa₂(227)	→	228
Aa₂(208)	→	209
Aa₂(286)	→	287
Aa₂(268)	→	269
Aa₂(204)	→	205
Aa₂(262)	→	263
Aa₂(184)	→	185
Aa₂(213)	→	214
Aa₂(175)	→	176
Aa₂(259)	→	260
Aa₂(233)	→	234
f13₀	→	2
Right3₁(75)	→	76
Right4₀(15)	→	18
Right4₀(3)	→	1
Right4₀(21)	→	22
Wait₀(2)	→	3
Right2₀(15)	→	16
Left₀(2)	→	6
Right4₁(82)	→	83
Right4₁(103)	→	104
Right4₁(106)	→	107
Right4₁(79)	→	80
Right4₁(166)	→	167
Right4₁(94)	→	95
Right4₁(91)	→	92
Right1₁(34)	→	35
Right1₁(67)	→	68
Right1₁(58)	→	59
Right1₁(46)	→	47
Right1₁(55)	→	56
Right1₁(43)	→	44
b₀(6)	→	24
b₀(9)	→	10
b₀(28)	→	29
b₀(8)	→	9
b₀(29)	→	30
b₀(11)	→	12
b₀(31)	→	32
Ab₀(2)	→	21
Aa₁(33)	→	34
Aa₁(105)	→	106
Aa₁(130)	→	131
Aa₁(142)	→	143
Aa₁(93)	→	94
Aa₁(54)	→	55
Aa₁(66)	→	67