by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| Begin(q0(0(x0))) | → | Wait(Right1(x0)) |
| Begin(0(x0)) | → | Wait(Right2(x0)) |
| Begin(q0(h(x0))) | → | Wait(Right3(x0)) |
| Begin(h(x0)) | → | Wait(Right4(x0)) |
| Begin(q0(1(x0))) | → | Wait(Right5(x0)) |
| Begin(1(x0)) | → | Wait(Right6(x0)) |
| Begin(q1(0(x0))) | → | Wait(Right7(x0)) |
| Begin(0(x0)) | → | Wait(Right8(x0)) |
| Begin(q1(h(x0))) | → | Wait(Right9(x0)) |
| Begin(h(x0)) | → | Wait(Right10(x0)) |
| Begin(q1(1(x0))) | → | Wait(Right11(x0)) |
| Begin(1(x0)) | → | Wait(Right12(x0)) |
| Begin(q1(0(x0))) | → | Wait(Right13(x0)) |
| Begin(0(x0)) | → | Wait(Right14(x0)) |
| Begin(q1(h(x0))) | → | Wait(Right15(x0)) |
| Begin(h(x0)) | → | Wait(Right16(x0)) |
| Begin(q1(1(x0))) | → | Wait(Right17(x0)) |
| Begin(1(x0)) | → | Wait(Right18(x0)) |
| Begin(q2(0(x0))) | → | Wait(Right19(x0)) |
| Begin(0(x0)) | → | Wait(Right20(x0)) |
| Begin(q2(h(x0))) | → | Wait(Right21(x0)) |
| Begin(h(x0)) | → | Wait(Right22(x0)) |
| Begin(q2(1(x0))) | → | Wait(Right23(x0)) |
| Begin(1(x0)) | → | Wait(Right24(x0)) |
| Begin(q2(x0)) | → | Wait(Right25(x0)) |
| Begin(q3(x0)) | → | Wait(Right26(x0)) |
| Begin(q3(x0)) | → | Wait(Right27(x0)) |
| Begin(q4(x0)) | → | Wait(Right28(x0)) |
| Begin(q4(0(x0))) | → | Wait(Right29(x0)) |
| Begin(0(x0)) | → | Wait(Right30(x0)) |
| Begin(q4(h(x0))) | → | Wait(Right31(x0)) |
| Begin(h(x0)) | → | Wait(Right32(x0)) |
| Begin(q4(1(x0))) | → | Wait(Right33(x0)) |
| Begin(1(x0)) | → | Wait(Right34(x0)) |
| Begin(q5(0(x0))) | → | Wait(Right35(x0)) |
| Begin(0(x0)) | → | Wait(Right36(x0)) |
| Begin(q5(h(x0))) | → | Wait(Right37(x0)) |
| Begin(h(x0)) | → | Wait(Right38(x0)) |
| Begin(q5(1(x0))) | → | Wait(Right39(x0)) |
| Begin(1(x0)) | → | Wait(Right40(x0)) |
| Begin(q0(x0)) | → | Wait(Right41(x0)) |
| Begin(q1(x0)) | → | Wait(Right42(x0)) |
| Begin(q2(x0)) | → | Wait(Right43(x0)) |
| Begin(q3(x0)) | → | Wait(Right44(x0)) |
| Begin(q4(x0)) | → | Wait(Right45(x0)) |
| Begin(q5(x0)) | → | Wait(Right46(x0)) |
| Right1(0(End(x0))) | → | Left(0(0(q0(End(x0))))) |
| Right2(0(q0(End(x0)))) | → | Left(0(0(q0(End(x0))))) |
| Right3(0(End(x0))) | → | Left(0(0(q0(h(End(x0)))))) |
| Right4(0(q0(End(x0)))) | → | Left(0(0(q0(h(End(x0)))))) |
| Right5(0(End(x0))) | → | Left(0(1(q0(End(x0))))) |
| Right6(0(q0(End(x0)))) | → | Left(0(1(q0(End(x0))))) |
| Right7(1(End(x0))) | → | Left(1(0(q1(End(x0))))) |
| Right8(1(q1(End(x0)))) | → | Left(1(0(q1(End(x0))))) |
| Right9(1(End(x0))) | → | Left(1(0(q1(h(End(x0)))))) |
| Right10(1(q1(End(x0)))) | → | Left(1(0(q1(h(End(x0)))))) |
| Right11(1(End(x0))) | → | Left(1(1(q1(End(x0))))) |
| Right12(1(q1(End(x0)))) | → | Left(1(1(q1(End(x0))))) |
| Right13(0(End(x0))) | → | Left(0(0(q2(End(x0))))) |
| Right14(0(q1(End(x0)))) | → | Left(0(0(q2(End(x0))))) |
| Right15(0(End(x0))) | → | Left(0(0(q2(h(End(x0)))))) |
| Right16(0(q1(End(x0)))) | → | Left(0(0(q2(h(End(x0)))))) |
| Right17(0(End(x0))) | → | Left(0(1(q2(End(x0))))) |
| Right18(0(q1(End(x0)))) | → | Left(0(1(q2(End(x0))))) |
| Right19(1(End(x0))) | → | Left(1(0(q2(End(x0))))) |
| Right20(1(q2(End(x0)))) | → | Left(1(0(q2(End(x0))))) |
| Right21(1(End(x0))) | → | Left(1(0(q2(h(End(x0)))))) |
| Right22(1(q2(End(x0)))) | → | Left(1(0(q2(h(End(x0)))))) |
| Right23(1(End(x0))) | → | Left(1(1(q2(End(x0))))) |
| Right24(1(q2(End(x0)))) | → | Left(1(1(q2(End(x0))))) |
| Right25(0(End(x0))) | → | Left(q3(1(End(x0)))) |
| Right26(1(End(x0))) | → | Left(q3(1(End(x0)))) |
| Right27(0(End(x0))) | → | Left(q4(0(End(x0)))) |
| Right28(1(End(x0))) | → | Left(q4(1(End(x0)))) |
| Right29(0(End(x0))) | → | Left(1(0(q5(End(x0))))) |
| Right30(0(q4(End(x0)))) | → | Left(1(0(q5(End(x0))))) |
| Right31(0(End(x0))) | → | Left(1(0(q5(h(End(x0)))))) |
| Right32(0(q4(End(x0)))) | → | Left(1(0(q5(h(End(x0)))))) |
| Right33(0(End(x0))) | → | Left(1(1(q5(End(x0))))) |
| Right34(0(q4(End(x0)))) | → | Left(1(1(q5(End(x0))))) |
| Right35(1(End(x0))) | → | Left(0(0(q1(End(x0))))) |
| Right36(1(q5(End(x0)))) | → | Left(0(0(q1(End(x0))))) |
| Right37(1(End(x0))) | → | Left(0(0(q1(h(End(x0)))))) |
| Right38(1(q5(End(x0)))) | → | Left(0(0(q1(h(End(x0)))))) |
| Right39(1(End(x0))) | → | Left(0(1(q1(End(x0))))) |
| Right40(1(q5(End(x0)))) | → | Left(0(1(q1(End(x0))))) |
| Right41(h(End(x0))) | → | Left(h(0(q0(End(x0))))) |
| Right42(h(End(x0))) | → | Left(h(0(q1(End(x0))))) |
| Right43(h(End(x0))) | → | Left(h(0(q2(End(x0))))) |
| Right44(h(End(x0))) | → | Left(h(0(q3(End(x0))))) |
| Right45(h(End(x0))) | → | Left(h(0(q4(End(x0))))) |
| Right46(h(End(x0))) | → | Left(h(0(q5(End(x0))))) |
| Right1(0(x0)) | → | A0(Right1(x0)) |
| Right2(0(x0)) | → | A0(Right2(x0)) |
| Right3(0(x0)) | → | A0(Right3(x0)) |
| Right4(0(x0)) | → | A0(Right4(x0)) |
| Right5(0(x0)) | → | A0(Right5(x0)) |
| Right6(0(x0)) | → | A0(Right6(x0)) |
| Right7(0(x0)) | → | A0(Right7(x0)) |
| Right8(0(x0)) | → | A0(Right8(x0)) |
| Right9(0(x0)) | → | A0(Right9(x0)) |
| Right10(0(x0)) | → | A0(Right10(x0)) |
| Right11(0(x0)) | → | A0(Right11(x0)) |
| Right12(0(x0)) | → | A0(Right12(x0)) |
| Right13(0(x0)) | → | A0(Right13(x0)) |
| Right14(0(x0)) | → | A0(Right14(x0)) |
| Right15(0(x0)) | → | A0(Right15(x0)) |
| Right16(0(x0)) | → | A0(Right16(x0)) |
| Right17(0(x0)) | → | A0(Right17(x0)) |
| Right18(0(x0)) | → | A0(Right18(x0)) |
| Right19(0(x0)) | → | A0(Right19(x0)) |
| Right20(0(x0)) | → | A0(Right20(x0)) |
| Right21(0(x0)) | → | A0(Right21(x0)) |
| Right22(0(x0)) | → | A0(Right22(x0)) |
| Right23(0(x0)) | → | A0(Right23(x0)) |
| Right24(0(x0)) | → | A0(Right24(x0)) |
| Right25(0(x0)) | → | A0(Right25(x0)) |
| Right26(0(x0)) | → | A0(Right26(x0)) |
| Right27(0(x0)) | → | A0(Right27(x0)) |
| Right28(0(x0)) | → | A0(Right28(x0)) |
| Right29(0(x0)) | → | A0(Right29(x0)) |
| Right30(0(x0)) | → | A0(Right30(x0)) |
| Right31(0(x0)) | → | A0(Right31(x0)) |
| Right32(0(x0)) | → | A0(Right32(x0)) |
| Right33(0(x0)) | → | A0(Right33(x0)) |
| Right34(0(x0)) | → | A0(Right34(x0)) |
| Right35(0(x0)) | → | A0(Right35(x0)) |
| Right36(0(x0)) | → | A0(Right36(x0)) |
| Right37(0(x0)) | → | A0(Right37(x0)) |
| Right38(0(x0)) | → | A0(Right38(x0)) |
| Right39(0(x0)) | → | A0(Right39(x0)) |
| Right40(0(x0)) | → | A0(Right40(x0)) |
| Right41(0(x0)) | → | A0(Right41(x0)) |
| Right42(0(x0)) | → | A0(Right42(x0)) |
| Right43(0(x0)) | → | A0(Right43(x0)) |
| Right44(0(x0)) | → | A0(Right44(x0)) |
| Right45(0(x0)) | → | A0(Right45(x0)) |
| Right46(0(x0)) | → | A0(Right46(x0)) |
| Right1(q0(x0)) | → | Aq0(Right1(x0)) |
| Right2(q0(x0)) | → | Aq0(Right2(x0)) |
| Right3(q0(x0)) | → | Aq0(Right3(x0)) |
| Right4(q0(x0)) | → | Aq0(Right4(x0)) |
| Right5(q0(x0)) | → | Aq0(Right5(x0)) |
| Right6(q0(x0)) | → | Aq0(Right6(x0)) |
| Right7(q0(x0)) | → | Aq0(Right7(x0)) |
| Right8(q0(x0)) | → | Aq0(Right8(x0)) |
| Right9(q0(x0)) | → | Aq0(Right9(x0)) |
| Right10(q0(x0)) | → | Aq0(Right10(x0)) |
| Right11(q0(x0)) | → | Aq0(Right11(x0)) |
| Right12(q0(x0)) | → | Aq0(Right12(x0)) |
| Right13(q0(x0)) | → | Aq0(Right13(x0)) |
| Right14(q0(x0)) | → | Aq0(Right14(x0)) |
| Right15(q0(x0)) | → | Aq0(Right15(x0)) |
| Right16(q0(x0)) | → | Aq0(Right16(x0)) |
| Right17(q0(x0)) | → | Aq0(Right17(x0)) |
| Right18(q0(x0)) | → | Aq0(Right18(x0)) |
| Right19(q0(x0)) | → | Aq0(Right19(x0)) |
| Right20(q0(x0)) | → | Aq0(Right20(x0)) |
| Right21(q0(x0)) | → | Aq0(Right21(x0)) |
| Right22(q0(x0)) | → | Aq0(Right22(x0)) |
| Right23(q0(x0)) | → | Aq0(Right23(x0)) |
| Right24(q0(x0)) | → | Aq0(Right24(x0)) |
| Right25(q0(x0)) | → | Aq0(Right25(x0)) |
| Right26(q0(x0)) | → | Aq0(Right26(x0)) |
| Right27(q0(x0)) | → | Aq0(Right27(x0)) |
| Right28(q0(x0)) | → | Aq0(Right28(x0)) |
| Right29(q0(x0)) | → | Aq0(Right29(x0)) |
| Right30(q0(x0)) | → | Aq0(Right30(x0)) |
| Right31(q0(x0)) | → | Aq0(Right31(x0)) |
| Right32(q0(x0)) | → | Aq0(Right32(x0)) |
| Right33(q0(x0)) | → | Aq0(Right33(x0)) |
| Right34(q0(x0)) | → | Aq0(Right34(x0)) |
| Right35(q0(x0)) | → | Aq0(Right35(x0)) |
| Right36(q0(x0)) | → | Aq0(Right36(x0)) |
| Right37(q0(x0)) | → | Aq0(Right37(x0)) |
| Right38(q0(x0)) | → | Aq0(Right38(x0)) |
| Right39(q0(x0)) | → | Aq0(Right39(x0)) |
| Right40(q0(x0)) | → | Aq0(Right40(x0)) |
| Right41(q0(x0)) | → | Aq0(Right41(x0)) |
| Right42(q0(x0)) | → | Aq0(Right42(x0)) |
| Right43(q0(x0)) | → | Aq0(Right43(x0)) |
| Right44(q0(x0)) | → | Aq0(Right44(x0)) |
| Right45(q0(x0)) | → | Aq0(Right45(x0)) |
| Right46(q0(x0)) | → | Aq0(Right46(x0)) |
| Right1(h(x0)) | → | Ah(Right1(x0)) |
| Right2(h(x0)) | → | Ah(Right2(x0)) |
| Right3(h(x0)) | → | Ah(Right3(x0)) |
| Right4(h(x0)) | → | Ah(Right4(x0)) |
| Right5(h(x0)) | → | Ah(Right5(x0)) |
| Right6(h(x0)) | → | Ah(Right6(x0)) |
| Right7(h(x0)) | → | Ah(Right7(x0)) |
| Right8(h(x0)) | → | Ah(Right8(x0)) |
| Right9(h(x0)) | → | Ah(Right9(x0)) |
| Right10(h(x0)) | → | Ah(Right10(x0)) |
| Right11(h(x0)) | → | Ah(Right11(x0)) |
| Right12(h(x0)) | → | Ah(Right12(x0)) |
| Right13(h(x0)) | → | Ah(Right13(x0)) |
| Right14(h(x0)) | → | Ah(Right14(x0)) |
| Right15(h(x0)) | → | Ah(Right15(x0)) |
| Right16(h(x0)) | → | Ah(Right16(x0)) |
| Right17(h(x0)) | → | Ah(Right17(x0)) |
| Right18(h(x0)) | → | Ah(Right18(x0)) |
| Right19(h(x0)) | → | Ah(Right19(x0)) |
| Right20(h(x0)) | → | Ah(Right20(x0)) |
| Right21(h(x0)) | → | Ah(Right21(x0)) |
| Right22(h(x0)) | → | Ah(Right22(x0)) |
| Right23(h(x0)) | → | Ah(Right23(x0)) |
| Right24(h(x0)) | → | Ah(Right24(x0)) |
| Right25(h(x0)) | → | Ah(Right25(x0)) |
| Right26(h(x0)) | → | Ah(Right26(x0)) |
| Right27(h(x0)) | → | Ah(Right27(x0)) |
| Right28(h(x0)) | → | Ah(Right28(x0)) |
| Right29(h(x0)) | → | Ah(Right29(x0)) |
| Right30(h(x0)) | → | Ah(Right30(x0)) |
| Right31(h(x0)) | → | Ah(Right31(x0)) |
| Right32(h(x0)) | → | Ah(Right32(x0)) |
| Right33(h(x0)) | → | Ah(Right33(x0)) |
| Right34(h(x0)) | → | Ah(Right34(x0)) |
| Right35(h(x0)) | → | Ah(Right35(x0)) |
| Right36(h(x0)) | → | Ah(Right36(x0)) |
| Right37(h(x0)) | → | Ah(Right37(x0)) |
| Right38(h(x0)) | → | Ah(Right38(x0)) |
| Right39(h(x0)) | → | Ah(Right39(x0)) |
| Right40(h(x0)) | → | Ah(Right40(x0)) |
| Right41(h(x0)) | → | Ah(Right41(x0)) |
| Right42(h(x0)) | → | Ah(Right42(x0)) |
| Right43(h(x0)) | → | Ah(Right43(x0)) |
| Right44(h(x0)) | → | Ah(Right44(x0)) |
| Right45(h(x0)) | → | Ah(Right45(x0)) |
| Right46(h(x0)) | → | Ah(Right46(x0)) |
| Right1(1(x0)) | → | A1(Right1(x0)) |
| Right2(1(x0)) | → | A1(Right2(x0)) |
| Right3(1(x0)) | → | A1(Right3(x0)) |
| Right4(1(x0)) | → | A1(Right4(x0)) |
| Right5(1(x0)) | → | A1(Right5(x0)) |
| Right6(1(x0)) | → | A1(Right6(x0)) |
| Right7(1(x0)) | → | A1(Right7(x0)) |
| Right8(1(x0)) | → | A1(Right8(x0)) |
| Right9(1(x0)) | → | A1(Right9(x0)) |
| Right10(1(x0)) | → | A1(Right10(x0)) |
| Right11(1(x0)) | → | A1(Right11(x0)) |
| Right12(1(x0)) | → | A1(Right12(x0)) |
| Right13(1(x0)) | → | A1(Right13(x0)) |
| Right14(1(x0)) | → | A1(Right14(x0)) |
| Right15(1(x0)) | → | A1(Right15(x0)) |
| Right16(1(x0)) | → | A1(Right16(x0)) |
| Right17(1(x0)) | → | A1(Right17(x0)) |
| Right18(1(x0)) | → | A1(Right18(x0)) |
| Right19(1(x0)) | → | A1(Right19(x0)) |
| Right20(1(x0)) | → | A1(Right20(x0)) |
| Right21(1(x0)) | → | A1(Right21(x0)) |
| Right22(1(x0)) | → | A1(Right22(x0)) |
| Right23(1(x0)) | → | A1(Right23(x0)) |
| Right24(1(x0)) | → | A1(Right24(x0)) |
| Right25(1(x0)) | → | A1(Right25(x0)) |
| Right26(1(x0)) | → | A1(Right26(x0)) |
| Right27(1(x0)) | → | A1(Right27(x0)) |
| Right28(1(x0)) | → | A1(Right28(x0)) |
| Right29(1(x0)) | → | A1(Right29(x0)) |
| Right30(1(x0)) | → | A1(Right30(x0)) |
| Right31(1(x0)) | → | A1(Right31(x0)) |
| Right32(1(x0)) | → | A1(Right32(x0)) |
| Right33(1(x0)) | → | A1(Right33(x0)) |
| Right34(1(x0)) | → | A1(Right34(x0)) |
| Right35(1(x0)) | → | A1(Right35(x0)) |
| Right36(1(x0)) | → | A1(Right36(x0)) |
| Right37(1(x0)) | → | A1(Right37(x0)) |
| Right38(1(x0)) | → | A1(Right38(x0)) |
| Right39(1(x0)) | → | A1(Right39(x0)) |
| Right40(1(x0)) | → | A1(Right40(x0)) |
| Right41(1(x0)) | → | A1(Right41(x0)) |
| Right42(1(x0)) | → | A1(Right42(x0)) |
| Right43(1(x0)) | → | A1(Right43(x0)) |
| Right44(1(x0)) | → | A1(Right44(x0)) |
| Right45(1(x0)) | → | A1(Right45(x0)) |
| Right46(1(x0)) | → | A1(Right46(x0)) |
| Right1(q1(x0)) | → | Aq1(Right1(x0)) |
| Right2(q1(x0)) | → | Aq1(Right2(x0)) |
| Right3(q1(x0)) | → | Aq1(Right3(x0)) |
| Right4(q1(x0)) | → | Aq1(Right4(x0)) |
| Right5(q1(x0)) | → | Aq1(Right5(x0)) |
| Right6(q1(x0)) | → | Aq1(Right6(x0)) |
| Right7(q1(x0)) | → | Aq1(Right7(x0)) |
| Right8(q1(x0)) | → | Aq1(Right8(x0)) |
| Right9(q1(x0)) | → | Aq1(Right9(x0)) |
| Right10(q1(x0)) | → | Aq1(Right10(x0)) |
| Right11(q1(x0)) | → | Aq1(Right11(x0)) |
| Right12(q1(x0)) | → | Aq1(Right12(x0)) |
| Right13(q1(x0)) | → | Aq1(Right13(x0)) |
| Right14(q1(x0)) | → | Aq1(Right14(x0)) |
| Right15(q1(x0)) | → | Aq1(Right15(x0)) |
| Right16(q1(x0)) | → | Aq1(Right16(x0)) |
| Right17(q1(x0)) | → | Aq1(Right17(x0)) |
| Right18(q1(x0)) | → | Aq1(Right18(x0)) |
| Right19(q1(x0)) | → | Aq1(Right19(x0)) |
| Right20(q1(x0)) | → | Aq1(Right20(x0)) |
| Right21(q1(x0)) | → | Aq1(Right21(x0)) |
| Right22(q1(x0)) | → | Aq1(Right22(x0)) |
| Right23(q1(x0)) | → | Aq1(Right23(x0)) |
| Right24(q1(x0)) | → | Aq1(Right24(x0)) |
| Right25(q1(x0)) | → | Aq1(Right25(x0)) |
| Right26(q1(x0)) | → | Aq1(Right26(x0)) |
| Right27(q1(x0)) | → | Aq1(Right27(x0)) |
| Right28(q1(x0)) | → | Aq1(Right28(x0)) |
| Right29(q1(x0)) | → | Aq1(Right29(x0)) |
| Right30(q1(x0)) | → | Aq1(Right30(x0)) |
| Right31(q1(x0)) | → | Aq1(Right31(x0)) |
| Right32(q1(x0)) | → | Aq1(Right32(x0)) |
| Right33(q1(x0)) | → | Aq1(Right33(x0)) |
| Right34(q1(x0)) | → | Aq1(Right34(x0)) |
| Right35(q1(x0)) | → | Aq1(Right35(x0)) |
| Right36(q1(x0)) | → | Aq1(Right36(x0)) |
| Right37(q1(x0)) | → | Aq1(Right37(x0)) |
| Right38(q1(x0)) | → | Aq1(Right38(x0)) |
| Right39(q1(x0)) | → | Aq1(Right39(x0)) |
| Right40(q1(x0)) | → | Aq1(Right40(x0)) |
| Right41(q1(x0)) | → | Aq1(Right41(x0)) |
| Right42(q1(x0)) | → | Aq1(Right42(x0)) |
| Right43(q1(x0)) | → | Aq1(Right43(x0)) |
| Right44(q1(x0)) | → | Aq1(Right44(x0)) |
| Right45(q1(x0)) | → | Aq1(Right45(x0)) |
| Right46(q1(x0)) | → | Aq1(Right46(x0)) |
| Right1(q2(x0)) | → | Aq2(Right1(x0)) |
| Right2(q2(x0)) | → | Aq2(Right2(x0)) |
| Right3(q2(x0)) | → | Aq2(Right3(x0)) |
| Right4(q2(x0)) | → | Aq2(Right4(x0)) |
| Right5(q2(x0)) | → | Aq2(Right5(x0)) |
| Right6(q2(x0)) | → | Aq2(Right6(x0)) |
| Right7(q2(x0)) | → | Aq2(Right7(x0)) |
| Right8(q2(x0)) | → | Aq2(Right8(x0)) |
| Right9(q2(x0)) | → | Aq2(Right9(x0)) |
| Right10(q2(x0)) | → | Aq2(Right10(x0)) |
| Right11(q2(x0)) | → | Aq2(Right11(x0)) |
| Right12(q2(x0)) | → | Aq2(Right12(x0)) |
| Right13(q2(x0)) | → | Aq2(Right13(x0)) |
| Right14(q2(x0)) | → | Aq2(Right14(x0)) |
| Right15(q2(x0)) | → | Aq2(Right15(x0)) |
| Right16(q2(x0)) | → | Aq2(Right16(x0)) |
| Right17(q2(x0)) | → | Aq2(Right17(x0)) |
| Right18(q2(x0)) | → | Aq2(Right18(x0)) |
| Right19(q2(x0)) | → | Aq2(Right19(x0)) |
| Right20(q2(x0)) | → | Aq2(Right20(x0)) |
| Right21(q2(x0)) | → | Aq2(Right21(x0)) |
| Right22(q2(x0)) | → | Aq2(Right22(x0)) |
| Right23(q2(x0)) | → | Aq2(Right23(x0)) |
| Right24(q2(x0)) | → | Aq2(Right24(x0)) |
| Right25(q2(x0)) | → | Aq2(Right25(x0)) |
| Right26(q2(x0)) | → | Aq2(Right26(x0)) |
| Right27(q2(x0)) | → | Aq2(Right27(x0)) |
| Right28(q2(x0)) | → | Aq2(Right28(x0)) |
| Right29(q2(x0)) | → | Aq2(Right29(x0)) |
| Right30(q2(x0)) | → | Aq2(Right30(x0)) |
| Right31(q2(x0)) | → | Aq2(Right31(x0)) |
| Right32(q2(x0)) | → | Aq2(Right32(x0)) |
| Right33(q2(x0)) | → | Aq2(Right33(x0)) |
| Right34(q2(x0)) | → | Aq2(Right34(x0)) |
| Right35(q2(x0)) | → | Aq2(Right35(x0)) |
| Right36(q2(x0)) | → | Aq2(Right36(x0)) |
| Right37(q2(x0)) | → | Aq2(Right37(x0)) |
| Right38(q2(x0)) | → | Aq2(Right38(x0)) |
| Right39(q2(x0)) | → | Aq2(Right39(x0)) |
| Right40(q2(x0)) | → | Aq2(Right40(x0)) |
| Right41(q2(x0)) | → | Aq2(Right41(x0)) |
| Right42(q2(x0)) | → | Aq2(Right42(x0)) |
| Right43(q2(x0)) | → | Aq2(Right43(x0)) |
| Right44(q2(x0)) | → | Aq2(Right44(x0)) |
| Right45(q2(x0)) | → | Aq2(Right45(x0)) |
| Right46(q2(x0)) | → | Aq2(Right46(x0)) |
| Right1(q3(x0)) | → | Aq3(Right1(x0)) |
| Right2(q3(x0)) | → | Aq3(Right2(x0)) |
| Right3(q3(x0)) | → | Aq3(Right3(x0)) |
| Right4(q3(x0)) | → | Aq3(Right4(x0)) |
| Right5(q3(x0)) | → | Aq3(Right5(x0)) |
| Right6(q3(x0)) | → | Aq3(Right6(x0)) |
| Right7(q3(x0)) | → | Aq3(Right7(x0)) |
| Right8(q3(x0)) | → | Aq3(Right8(x0)) |
| Right9(q3(x0)) | → | Aq3(Right9(x0)) |
| Right10(q3(x0)) | → | Aq3(Right10(x0)) |
| Right11(q3(x0)) | → | Aq3(Right11(x0)) |
| Right12(q3(x0)) | → | Aq3(Right12(x0)) |
| Right13(q3(x0)) | → | Aq3(Right13(x0)) |
| Right14(q3(x0)) | → | Aq3(Right14(x0)) |
| Right15(q3(x0)) | → | Aq3(Right15(x0)) |
| Right16(q3(x0)) | → | Aq3(Right16(x0)) |
| Right17(q3(x0)) | → | Aq3(Right17(x0)) |
| Right18(q3(x0)) | → | Aq3(Right18(x0)) |
| Right19(q3(x0)) | → | Aq3(Right19(x0)) |
| Right20(q3(x0)) | → | Aq3(Right20(x0)) |
| Right21(q3(x0)) | → | Aq3(Right21(x0)) |
| Right22(q3(x0)) | → | Aq3(Right22(x0)) |
| Right23(q3(x0)) | → | Aq3(Right23(x0)) |
| Right24(q3(x0)) | → | Aq3(Right24(x0)) |
| Right25(q3(x0)) | → | Aq3(Right25(x0)) |
| Right26(q3(x0)) | → | Aq3(Right26(x0)) |
| Right27(q3(x0)) | → | Aq3(Right27(x0)) |
| Right28(q3(x0)) | → | Aq3(Right28(x0)) |
| Right29(q3(x0)) | → | Aq3(Right29(x0)) |
| Right30(q3(x0)) | → | Aq3(Right30(x0)) |
| Right31(q3(x0)) | → | Aq3(Right31(x0)) |
| Right32(q3(x0)) | → | Aq3(Right32(x0)) |
| Right33(q3(x0)) | → | Aq3(Right33(x0)) |
| Right34(q3(x0)) | → | Aq3(Right34(x0)) |
| Right35(q3(x0)) | → | Aq3(Right35(x0)) |
| Right36(q3(x0)) | → | Aq3(Right36(x0)) |
| Right37(q3(x0)) | → | Aq3(Right37(x0)) |
| Right38(q3(x0)) | → | Aq3(Right38(x0)) |
| Right39(q3(x0)) | → | Aq3(Right39(x0)) |
| Right40(q3(x0)) | → | Aq3(Right40(x0)) |
| Right41(q3(x0)) | → | Aq3(Right41(x0)) |
| Right42(q3(x0)) | → | Aq3(Right42(x0)) |
| Right43(q3(x0)) | → | Aq3(Right43(x0)) |
| Right44(q3(x0)) | → | Aq3(Right44(x0)) |
| Right45(q3(x0)) | → | Aq3(Right45(x0)) |
| Right46(q3(x0)) | → | Aq3(Right46(x0)) |
| Right1(q4(x0)) | → | Aq4(Right1(x0)) |
| Right2(q4(x0)) | → | Aq4(Right2(x0)) |
| Right3(q4(x0)) | → | Aq4(Right3(x0)) |
| Right4(q4(x0)) | → | Aq4(Right4(x0)) |
| Right5(q4(x0)) | → | Aq4(Right5(x0)) |
| Right6(q4(x0)) | → | Aq4(Right6(x0)) |
| Right7(q4(x0)) | → | Aq4(Right7(x0)) |
| Right8(q4(x0)) | → | Aq4(Right8(x0)) |
| Right9(q4(x0)) | → | Aq4(Right9(x0)) |
| Right10(q4(x0)) | → | Aq4(Right10(x0)) |
| Right11(q4(x0)) | → | Aq4(Right11(x0)) |
| Right12(q4(x0)) | → | Aq4(Right12(x0)) |
| Right13(q4(x0)) | → | Aq4(Right13(x0)) |
| Right14(q4(x0)) | → | Aq4(Right14(x0)) |
| Right15(q4(x0)) | → | Aq4(Right15(x0)) |
| Right16(q4(x0)) | → | Aq4(Right16(x0)) |
| Right17(q4(x0)) | → | Aq4(Right17(x0)) |
| Right18(q4(x0)) | → | Aq4(Right18(x0)) |
| Right19(q4(x0)) | → | Aq4(Right19(x0)) |
| Right20(q4(x0)) | → | Aq4(Right20(x0)) |
| Right21(q4(x0)) | → | Aq4(Right21(x0)) |
| Right22(q4(x0)) | → | Aq4(Right22(x0)) |
| Right23(q4(x0)) | → | Aq4(Right23(x0)) |
| Right24(q4(x0)) | → | Aq4(Right24(x0)) |
| Right25(q4(x0)) | → | Aq4(Right25(x0)) |
| Right26(q4(x0)) | → | Aq4(Right26(x0)) |
| Right27(q4(x0)) | → | Aq4(Right27(x0)) |
| Right28(q4(x0)) | → | Aq4(Right28(x0)) |
| Right29(q4(x0)) | → | Aq4(Right29(x0)) |
| Right30(q4(x0)) | → | Aq4(Right30(x0)) |
| Right31(q4(x0)) | → | Aq4(Right31(x0)) |
| Right32(q4(x0)) | → | Aq4(Right32(x0)) |
| Right33(q4(x0)) | → | Aq4(Right33(x0)) |
| Right34(q4(x0)) | → | Aq4(Right34(x0)) |
| Right35(q4(x0)) | → | Aq4(Right35(x0)) |
| Right36(q4(x0)) | → | Aq4(Right36(x0)) |
| Right37(q4(x0)) | → | Aq4(Right37(x0)) |
| Right38(q4(x0)) | → | Aq4(Right38(x0)) |
| Right39(q4(x0)) | → | Aq4(Right39(x0)) |
| Right40(q4(x0)) | → | Aq4(Right40(x0)) |
| Right41(q4(x0)) | → | Aq4(Right41(x0)) |
| Right42(q4(x0)) | → | Aq4(Right42(x0)) |
| Right43(q4(x0)) | → | Aq4(Right43(x0)) |
| Right44(q4(x0)) | → | Aq4(Right44(x0)) |
| Right45(q4(x0)) | → | Aq4(Right45(x0)) |
| Right46(q4(x0)) | → | Aq4(Right46(x0)) |
| Right1(q5(x0)) | → | Aq5(Right1(x0)) |
| Right2(q5(x0)) | → | Aq5(Right2(x0)) |
| Right3(q5(x0)) | → | Aq5(Right3(x0)) |
| Right4(q5(x0)) | → | Aq5(Right4(x0)) |
| Right5(q5(x0)) | → | Aq5(Right5(x0)) |
| Right6(q5(x0)) | → | Aq5(Right6(x0)) |
| Right7(q5(x0)) | → | Aq5(Right7(x0)) |
| Right8(q5(x0)) | → | Aq5(Right8(x0)) |
| Right9(q5(x0)) | → | Aq5(Right9(x0)) |
| Right10(q5(x0)) | → | Aq5(Right10(x0)) |
| Right11(q5(x0)) | → | Aq5(Right11(x0)) |
| Right12(q5(x0)) | → | Aq5(Right12(x0)) |
| Right13(q5(x0)) | → | Aq5(Right13(x0)) |
| Right14(q5(x0)) | → | Aq5(Right14(x0)) |
| Right15(q5(x0)) | → | Aq5(Right15(x0)) |
| Right16(q5(x0)) | → | Aq5(Right16(x0)) |
| Right17(q5(x0)) | → | Aq5(Right17(x0)) |
| Right18(q5(x0)) | → | Aq5(Right18(x0)) |
| Right19(q5(x0)) | → | Aq5(Right19(x0)) |
| Right20(q5(x0)) | → | Aq5(Right20(x0)) |
| Right21(q5(x0)) | → | Aq5(Right21(x0)) |
| Right22(q5(x0)) | → | Aq5(Right22(x0)) |
| Right23(q5(x0)) | → | Aq5(Right23(x0)) |
| Right24(q5(x0)) | → | Aq5(Right24(x0)) |
| Right25(q5(x0)) | → | Aq5(Right25(x0)) |
| Right26(q5(x0)) | → | Aq5(Right26(x0)) |
| Right27(q5(x0)) | → | Aq5(Right27(x0)) |
| Right28(q5(x0)) | → | Aq5(Right28(x0)) |
| Right29(q5(x0)) | → | Aq5(Right29(x0)) |
| Right30(q5(x0)) | → | Aq5(Right30(x0)) |
| Right31(q5(x0)) | → | Aq5(Right31(x0)) |
| Right32(q5(x0)) | → | Aq5(Right32(x0)) |
| Right33(q5(x0)) | → | Aq5(Right33(x0)) |
| Right34(q5(x0)) | → | Aq5(Right34(x0)) |
| Right35(q5(x0)) | → | Aq5(Right35(x0)) |
| Right36(q5(x0)) | → | Aq5(Right36(x0)) |
| Right37(q5(x0)) | → | Aq5(Right37(x0)) |
| Right38(q5(x0)) | → | Aq5(Right38(x0)) |
| Right39(q5(x0)) | → | Aq5(Right39(x0)) |
| Right40(q5(x0)) | → | Aq5(Right40(x0)) |
| Right41(q5(x0)) | → | Aq5(Right41(x0)) |
| Right42(q5(x0)) | → | Aq5(Right42(x0)) |
| Right43(q5(x0)) | → | Aq5(Right43(x0)) |
| Right44(q5(x0)) | → | Aq5(Right44(x0)) |
| Right45(q5(x0)) | → | Aq5(Right45(x0)) |
| Right46(q5(x0)) | → | Aq5(Right46(x0)) |
| A0(Left(x0)) | → | Left(0(x0)) |
| Aq0(Left(x0)) | → | Left(q0(x0)) |
| Ah(Left(x0)) | → | Left(h(x0)) |
| A1(Left(x0)) | → | Left(1(x0)) |
| Aq1(Left(x0)) | → | Left(q1(x0)) |
| Aq2(Left(x0)) | → | Left(q2(x0)) |
| Aq3(Left(x0)) | → | Left(q3(x0)) |
| Aq4(Left(x0)) | → | Left(q4(x0)) |
| Aq5(Left(x0)) | → | Left(q5(x0)) |
| Wait(Left(x0)) | → | Begin(x0) |
| 0(q0(0(x0))) | → | 0(0(q0(x0))) |
| 0(q0(h(x0))) | → | 0(0(q0(h(x0)))) |
| 0(q0(1(x0))) | → | 0(1(q0(x0))) |
| 1(q1(0(x0))) | → | 1(0(q1(x0))) |
| 1(q1(h(x0))) | → | 1(0(q1(h(x0)))) |
| 1(q1(1(x0))) | → | 1(1(q1(x0))) |
| 0(q1(0(x0))) | → | 0(0(q2(x0))) |
| 0(q1(h(x0))) | → | 0(0(q2(h(x0)))) |
| 0(q1(1(x0))) | → | 0(1(q2(x0))) |
| 1(q2(0(x0))) | → | 1(0(q2(x0))) |
| 1(q2(h(x0))) | → | 1(0(q2(h(x0)))) |
| 1(q2(1(x0))) | → | 1(1(q2(x0))) |
| 0(q2(x0)) | → | q3(1(x0)) |
| 1(q3(x0)) | → | q3(1(x0)) |
| 0(q3(x0)) | → | q4(0(x0)) |
| 1(q4(x0)) | → | q4(1(x0)) |
| 0(q4(0(x0))) | → | 1(0(q5(x0))) |
| 0(q4(h(x0))) | → | 1(0(q5(h(x0)))) |
| 0(q4(1(x0))) | → | 1(1(q5(x0))) |
| 1(q5(0(x0))) | → | 0(0(q1(x0))) |
| 1(q5(h(x0))) | → | 0(0(q1(h(x0)))) |
| 1(q5(1(x0))) | → | 0(1(q1(x0))) |
| h(q0(x0)) | → | h(0(q0(x0))) |
| h(q1(x0)) | → | h(0(q1(x0))) |
| h(q2(x0)) | → | h(0(q2(x0))) |
| h(q3(x0)) | → | h(0(q3(x0))) |
| h(q4(x0)) | → | h(0(q4(x0))) |
| h(q5(x0)) | → | h(0(q5(x0))) |
| t0 | = | 0(q0(h(x0))) |
| →ε | 0(0(q0(h(x0)))) | |
| = | t1 |