NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Mixed_SRS/turing_copy.srs-torpacyc2out-split.srs

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 NonTerminationProof (⇒, 0 ms)
↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Begin(q0(0(x))) → Wait(Right1(x))
Begin(0(x)) → Wait(Right2(x))
Begin(q0(h(x))) → Wait(Right3(x))
Begin(h(x)) → Wait(Right4(x))
Begin(q0(1(x))) → Wait(Right5(x))
Begin(1(x)) → Wait(Right6(x))
Begin(q1(0(x))) → Wait(Right7(x))
Begin(0(x)) → Wait(Right8(x))
Begin(q1(h(x))) → Wait(Right9(x))
Begin(h(x)) → Wait(Right10(x))
Begin(q1(1(x))) → Wait(Right11(x))
Begin(1(x)) → Wait(Right12(x))
Begin(q1(0(x))) → Wait(Right13(x))
Begin(0(x)) → Wait(Right14(x))
Begin(q1(h(x))) → Wait(Right15(x))
Begin(h(x)) → Wait(Right16(x))
Begin(q1(1(x))) → Wait(Right17(x))
Begin(1(x)) → Wait(Right18(x))
Begin(q2(0(x))) → Wait(Right19(x))
Begin(0(x)) → Wait(Right20(x))
Begin(q2(h(x))) → Wait(Right21(x))
Begin(h(x)) → Wait(Right22(x))
Begin(q2(1(x))) → Wait(Right23(x))
Begin(1(x)) → Wait(Right24(x))
Begin(q2(x)) → Wait(Right25(x))
Begin(q3(x)) → Wait(Right26(x))
Begin(q3(x)) → Wait(Right27(x))
Begin(q4(x)) → Wait(Right28(x))
Begin(q4(0(x))) → Wait(Right29(x))
Begin(0(x)) → Wait(Right30(x))
Begin(q4(h(x))) → Wait(Right31(x))
Begin(h(x)) → Wait(Right32(x))
Begin(q4(1(x))) → Wait(Right33(x))
Begin(1(x)) → Wait(Right34(x))
Begin(q5(0(x))) → Wait(Right35(x))
Begin(0(x)) → Wait(Right36(x))
Begin(q5(h(x))) → Wait(Right37(x))
Begin(h(x)) → Wait(Right38(x))
Begin(q5(1(x))) → Wait(Right39(x))
Begin(1(x)) → Wait(Right40(x))
Begin(q0(x)) → Wait(Right41(x))
Begin(q1(x)) → Wait(Right42(x))
Begin(q2(x)) → Wait(Right43(x))
Begin(q3(x)) → Wait(Right44(x))
Begin(q4(x)) → Wait(Right45(x))
Begin(q5(x)) → Wait(Right46(x))
Right1(0(End(x))) → Left(0(0(q0(End(x)))))
Right2(0(q0(End(x)))) → Left(0(0(q0(End(x)))))
Right3(0(End(x))) → Left(0(0(q0(h(End(x))))))
Right4(0(q0(End(x)))) → Left(0(0(q0(h(End(x))))))
Right5(0(End(x))) → Left(0(1(q0(End(x)))))
Right6(0(q0(End(x)))) → Left(0(1(q0(End(x)))))
Right7(1(End(x))) → Left(1(0(q1(End(x)))))
Right8(1(q1(End(x)))) → Left(1(0(q1(End(x)))))
Right9(1(End(x))) → Left(1(0(q1(h(End(x))))))
Right10(1(q1(End(x)))) → Left(1(0(q1(h(End(x))))))
Right11(1(End(x))) → Left(1(1(q1(End(x)))))
Right12(1(q1(End(x)))) → Left(1(1(q1(End(x)))))
Right13(0(End(x))) → Left(0(0(q2(End(x)))))
Right14(0(q1(End(x)))) → Left(0(0(q2(End(x)))))
Right15(0(End(x))) → Left(0(0(q2(h(End(x))))))
Right16(0(q1(End(x)))) → Left(0(0(q2(h(End(x))))))
Right17(0(End(x))) → Left(0(1(q2(End(x)))))
Right18(0(q1(End(x)))) → Left(0(1(q2(End(x)))))
Right19(1(End(x))) → Left(1(0(q2(End(x)))))
Right20(1(q2(End(x)))) → Left(1(0(q2(End(x)))))
Right21(1(End(x))) → Left(1(0(q2(h(End(x))))))
Right22(1(q2(End(x)))) → Left(1(0(q2(h(End(x))))))
Right23(1(End(x))) → Left(1(1(q2(End(x)))))
Right24(1(q2(End(x)))) → Left(1(1(q2(End(x)))))
Right25(0(End(x))) → Left(q3(1(End(x))))
Right26(1(End(x))) → Left(q3(1(End(x))))
Right27(0(End(x))) → Left(q4(0(End(x))))
Right28(1(End(x))) → Left(q4(1(End(x))))
Right29(0(End(x))) → Left(1(0(q5(End(x)))))
Right30(0(q4(End(x)))) → Left(1(0(q5(End(x)))))
Right31(0(End(x))) → Left(1(0(q5(h(End(x))))))
Right32(0(q4(End(x)))) → Left(1(0(q5(h(End(x))))))
Right33(0(End(x))) → Left(1(1(q5(End(x)))))
Right34(0(q4(End(x)))) → Left(1(1(q5(End(x)))))
Right35(1(End(x))) → Left(0(0(q1(End(x)))))
Right36(1(q5(End(x)))) → Left(0(0(q1(End(x)))))
Right37(1(End(x))) → Left(0(0(q1(h(End(x))))))
Right38(1(q5(End(x)))) → Left(0(0(q1(h(End(x))))))
Right39(1(End(x))) → Left(0(1(q1(End(x)))))
Right40(1(q5(End(x)))) → Left(0(1(q1(End(x)))))
Right41(h(End(x))) → Left(h(0(q0(End(x)))))
Right42(h(End(x))) → Left(h(0(q1(End(x)))))
Right43(h(End(x))) → Left(h(0(q2(End(x)))))
Right44(h(End(x))) → Left(h(0(q3(End(x)))))
Right45(h(End(x))) → Left(h(0(q4(End(x)))))
Right46(h(End(x))) → Left(h(0(q5(End(x)))))
Right1(0(x)) → A0(Right1(x))
Right2(0(x)) → A0(Right2(x))
Right3(0(x)) → A0(Right3(x))
Right4(0(x)) → A0(Right4(x))
Right5(0(x)) → A0(Right5(x))
Right6(0(x)) → A0(Right6(x))
Right7(0(x)) → A0(Right7(x))
Right8(0(x)) → A0(Right8(x))
Right9(0(x)) → A0(Right9(x))
Right10(0(x)) → A0(Right10(x))
Right11(0(x)) → A0(Right11(x))
Right12(0(x)) → A0(Right12(x))
Right13(0(x)) → A0(Right13(x))
Right14(0(x)) → A0(Right14(x))
Right15(0(x)) → A0(Right15(x))
Right16(0(x)) → A0(Right16(x))
Right17(0(x)) → A0(Right17(x))
Right18(0(x)) → A0(Right18(x))
Right19(0(x)) → A0(Right19(x))
Right20(0(x)) → A0(Right20(x))
Right21(0(x)) → A0(Right21(x))
Right22(0(x)) → A0(Right22(x))
Right23(0(x)) → A0(Right23(x))
Right24(0(x)) → A0(Right24(x))
Right25(0(x)) → A0(Right25(x))
Right26(0(x)) → A0(Right26(x))
Right27(0(x)) → A0(Right27(x))
Right28(0(x)) → A0(Right28(x))
Right29(0(x)) → A0(Right29(x))
Right30(0(x)) → A0(Right30(x))
Right31(0(x)) → A0(Right31(x))
Right32(0(x)) → A0(Right32(x))
Right33(0(x)) → A0(Right33(x))
Right34(0(x)) → A0(Right34(x))
Right35(0(x)) → A0(Right35(x))
Right36(0(x)) → A0(Right36(x))
Right37(0(x)) → A0(Right37(x))
Right38(0(x)) → A0(Right38(x))
Right39(0(x)) → A0(Right39(x))
Right40(0(x)) → A0(Right40(x))
Right41(0(x)) → A0(Right41(x))
Right42(0(x)) → A0(Right42(x))
Right43(0(x)) → A0(Right43(x))
Right44(0(x)) → A0(Right44(x))
Right45(0(x)) → A0(Right45(x))
Right46(0(x)) → A0(Right46(x))
Right1(q0(x)) → Aq0(Right1(x))
Right2(q0(x)) → Aq0(Right2(x))
Right3(q0(x)) → Aq0(Right3(x))
Right4(q0(x)) → Aq0(Right4(x))
Right5(q0(x)) → Aq0(Right5(x))
Right6(q0(x)) → Aq0(Right6(x))
Right7(q0(x)) → Aq0(Right7(x))
Right8(q0(x)) → Aq0(Right8(x))
Right9(q0(x)) → Aq0(Right9(x))
Right10(q0(x)) → Aq0(Right10(x))
Right11(q0(x)) → Aq0(Right11(x))
Right12(q0(x)) → Aq0(Right12(x))
Right13(q0(x)) → Aq0(Right13(x))
Right14(q0(x)) → Aq0(Right14(x))
Right15(q0(x)) → Aq0(Right15(x))
Right16(q0(x)) → Aq0(Right16(x))
Right17(q0(x)) → Aq0(Right17(x))
Right18(q0(x)) → Aq0(Right18(x))
Right19(q0(x)) → Aq0(Right19(x))
Right20(q0(x)) → Aq0(Right20(x))
Right21(q0(x)) → Aq0(Right21(x))
Right22(q0(x)) → Aq0(Right22(x))
Right23(q0(x)) → Aq0(Right23(x))
Right24(q0(x)) → Aq0(Right24(x))
Right25(q0(x)) → Aq0(Right25(x))
Right26(q0(x)) → Aq0(Right26(x))
Right27(q0(x)) → Aq0(Right27(x))
Right28(q0(x)) → Aq0(Right28(x))
Right29(q0(x)) → Aq0(Right29(x))
Right30(q0(x)) → Aq0(Right30(x))
Right31(q0(x)) → Aq0(Right31(x))
Right32(q0(x)) → Aq0(Right32(x))
Right33(q0(x)) → Aq0(Right33(x))
Right34(q0(x)) → Aq0(Right34(x))
Right35(q0(x)) → Aq0(Right35(x))
Right36(q0(x)) → Aq0(Right36(x))
Right37(q0(x)) → Aq0(Right37(x))
Right38(q0(x)) → Aq0(Right38(x))
Right39(q0(x)) → Aq0(Right39(x))
Right40(q0(x)) → Aq0(Right40(x))
Right41(q0(x)) → Aq0(Right41(x))
Right42(q0(x)) → Aq0(Right42(x))
Right43(q0(x)) → Aq0(Right43(x))
Right44(q0(x)) → Aq0(Right44(x))
Right45(q0(x)) → Aq0(Right45(x))
Right46(q0(x)) → Aq0(Right46(x))
Right1(h(x)) → Ah(Right1(x))
Right2(h(x)) → Ah(Right2(x))
Right3(h(x)) → Ah(Right3(x))
Right4(h(x)) → Ah(Right4(x))
Right5(h(x)) → Ah(Right5(x))
Right6(h(x)) → Ah(Right6(x))
Right7(h(x)) → Ah(Right7(x))
Right8(h(x)) → Ah(Right8(x))
Right9(h(x)) → Ah(Right9(x))
Right10(h(x)) → Ah(Right10(x))
Right11(h(x)) → Ah(Right11(x))
Right12(h(x)) → Ah(Right12(x))
Right13(h(x)) → Ah(Right13(x))
Right14(h(x)) → Ah(Right14(x))
Right15(h(x)) → Ah(Right15(x))
Right16(h(x)) → Ah(Right16(x))
Right17(h(x)) → Ah(Right17(x))
Right18(h(x)) → Ah(Right18(x))
Right19(h(x)) → Ah(Right19(x))
Right20(h(x)) → Ah(Right20(x))
Right21(h(x)) → Ah(Right21(x))
Right22(h(x)) → Ah(Right22(x))
Right23(h(x)) → Ah(Right23(x))
Right24(h(x)) → Ah(Right24(x))
Right25(h(x)) → Ah(Right25(x))
Right26(h(x)) → Ah(Right26(x))
Right27(h(x)) → Ah(Right27(x))
Right28(h(x)) → Ah(Right28(x))
Right29(h(x)) → Ah(Right29(x))
Right30(h(x)) → Ah(Right30(x))
Right31(h(x)) → Ah(Right31(x))
Right32(h(x)) → Ah(Right32(x))
Right33(h(x)) → Ah(Right33(x))
Right34(h(x)) → Ah(Right34(x))
Right35(h(x)) → Ah(Right35(x))
Right36(h(x)) → Ah(Right36(x))
Right37(h(x)) → Ah(Right37(x))
Right38(h(x)) → Ah(Right38(x))
Right39(h(x)) → Ah(Right39(x))
Right40(h(x)) → Ah(Right40(x))
Right41(h(x)) → Ah(Right41(x))
Right42(h(x)) → Ah(Right42(x))
Right43(h(x)) → Ah(Right43(x))
Right44(h(x)) → Ah(Right44(x))
Right45(h(x)) → Ah(Right45(x))
Right46(h(x)) → Ah(Right46(x))
Right1(1(x)) → A1(Right1(x))
Right2(1(x)) → A1(Right2(x))
Right3(1(x)) → A1(Right3(x))
Right4(1(x)) → A1(Right4(x))
Right5(1(x)) → A1(Right5(x))
Right6(1(x)) → A1(Right6(x))
Right7(1(x)) → A1(Right7(x))
Right8(1(x)) → A1(Right8(x))
Right9(1(x)) → A1(Right9(x))
Right10(1(x)) → A1(Right10(x))
Right11(1(x)) → A1(Right11(x))
Right12(1(x)) → A1(Right12(x))
Right13(1(x)) → A1(Right13(x))
Right14(1(x)) → A1(Right14(x))
Right15(1(x)) → A1(Right15(x))
Right16(1(x)) → A1(Right16(x))
Right17(1(x)) → A1(Right17(x))
Right18(1(x)) → A1(Right18(x))
Right19(1(x)) → A1(Right19(x))
Right20(1(x)) → A1(Right20(x))
Right21(1(x)) → A1(Right21(x))
Right22(1(x)) → A1(Right22(x))
Right23(1(x)) → A1(Right23(x))
Right24(1(x)) → A1(Right24(x))
Right25(1(x)) → A1(Right25(x))
Right26(1(x)) → A1(Right26(x))
Right27(1(x)) → A1(Right27(x))
Right28(1(x)) → A1(Right28(x))
Right29(1(x)) → A1(Right29(x))
Right30(1(x)) → A1(Right30(x))
Right31(1(x)) → A1(Right31(x))
Right32(1(x)) → A1(Right32(x))
Right33(1(x)) → A1(Right33(x))
Right34(1(x)) → A1(Right34(x))
Right35(1(x)) → A1(Right35(x))
Right36(1(x)) → A1(Right36(x))
Right37(1(x)) → A1(Right37(x))
Right38(1(x)) → A1(Right38(x))
Right39(1(x)) → A1(Right39(x))
Right40(1(x)) → A1(Right40(x))
Right41(1(x)) → A1(Right41(x))
Right42(1(x)) → A1(Right42(x))
Right43(1(x)) → A1(Right43(x))
Right44(1(x)) → A1(Right44(x))
Right45(1(x)) → A1(Right45(x))
Right46(1(x)) → A1(Right46(x))
Right1(q1(x)) → Aq1(Right1(x))
Right2(q1(x)) → Aq1(Right2(x))
Right3(q1(x)) → Aq1(Right3(x))
Right4(q1(x)) → Aq1(Right4(x))
Right5(q1(x)) → Aq1(Right5(x))
Right6(q1(x)) → Aq1(Right6(x))
Right7(q1(x)) → Aq1(Right7(x))
Right8(q1(x)) → Aq1(Right8(x))
Right9(q1(x)) → Aq1(Right9(x))
Right10(q1(x)) → Aq1(Right10(x))
Right11(q1(x)) → Aq1(Right11(x))
Right12(q1(x)) → Aq1(Right12(x))
Right13(q1(x)) → Aq1(Right13(x))
Right14(q1(x)) → Aq1(Right14(x))
Right15(q1(x)) → Aq1(Right15(x))
Right16(q1(x)) → Aq1(Right16(x))
Right17(q1(x)) → Aq1(Right17(x))
Right18(q1(x)) → Aq1(Right18(x))
Right19(q1(x)) → Aq1(Right19(x))
Right20(q1(x)) → Aq1(Right20(x))
Right21(q1(x)) → Aq1(Right21(x))
Right22(q1(x)) → Aq1(Right22(x))
Right23(q1(x)) → Aq1(Right23(x))
Right24(q1(x)) → Aq1(Right24(x))
Right25(q1(x)) → Aq1(Right25(x))
Right26(q1(x)) → Aq1(Right26(x))
Right27(q1(x)) → Aq1(Right27(x))
Right28(q1(x)) → Aq1(Right28(x))
Right29(q1(x)) → Aq1(Right29(x))
Right30(q1(x)) → Aq1(Right30(x))
Right31(q1(x)) → Aq1(Right31(x))
Right32(q1(x)) → Aq1(Right32(x))
Right33(q1(x)) → Aq1(Right33(x))
Right34(q1(x)) → Aq1(Right34(x))
Right35(q1(x)) → Aq1(Right35(x))
Right36(q1(x)) → Aq1(Right36(x))
Right37(q1(x)) → Aq1(Right37(x))
Right38(q1(x)) → Aq1(Right38(x))
Right39(q1(x)) → Aq1(Right39(x))
Right40(q1(x)) → Aq1(Right40(x))
Right41(q1(x)) → Aq1(Right41(x))
Right42(q1(x)) → Aq1(Right42(x))
Right43(q1(x)) → Aq1(Right43(x))
Right44(q1(x)) → Aq1(Right44(x))
Right45(q1(x)) → Aq1(Right45(x))
Right46(q1(x)) → Aq1(Right46(x))
Right1(q2(x)) → Aq2(Right1(x))
Right2(q2(x)) → Aq2(Right2(x))
Right3(q2(x)) → Aq2(Right3(x))
Right4(q2(x)) → Aq2(Right4(x))
Right5(q2(x)) → Aq2(Right5(x))
Right6(q2(x)) → Aq2(Right6(x))
Right7(q2(x)) → Aq2(Right7(x))
Right8(q2(x)) → Aq2(Right8(x))
Right9(q2(x)) → Aq2(Right9(x))
Right10(q2(x)) → Aq2(Right10(x))
Right11(q2(x)) → Aq2(Right11(x))
Right12(q2(x)) → Aq2(Right12(x))
Right13(q2(x)) → Aq2(Right13(x))
Right14(q2(x)) → Aq2(Right14(x))
Right15(q2(x)) → Aq2(Right15(x))
Right16(q2(x)) → Aq2(Right16(x))
Right17(q2(x)) → Aq2(Right17(x))
Right18(q2(x)) → Aq2(Right18(x))
Right19(q2(x)) → Aq2(Right19(x))
Right20(q2(x)) → Aq2(Right20(x))
Right21(q2(x)) → Aq2(Right21(x))
Right22(q2(x)) → Aq2(Right22(x))
Right23(q2(x)) → Aq2(Right23(x))
Right24(q2(x)) → Aq2(Right24(x))
Right25(q2(x)) → Aq2(Right25(x))
Right26(q2(x)) → Aq2(Right26(x))
Right27(q2(x)) → Aq2(Right27(x))
Right28(q2(x)) → Aq2(Right28(x))
Right29(q2(x)) → Aq2(Right29(x))
Right30(q2(x)) → Aq2(Right30(x))
Right31(q2(x)) → Aq2(Right31(x))
Right32(q2(x)) → Aq2(Right32(x))
Right33(q2(x)) → Aq2(Right33(x))
Right34(q2(x)) → Aq2(Right34(x))
Right35(q2(x)) → Aq2(Right35(x))
Right36(q2(x)) → Aq2(Right36(x))
Right37(q2(x)) → Aq2(Right37(x))
Right38(q2(x)) → Aq2(Right38(x))
Right39(q2(x)) → Aq2(Right39(x))
Right40(q2(x)) → Aq2(Right40(x))
Right41(q2(x)) → Aq2(Right41(x))
Right42(q2(x)) → Aq2(Right42(x))
Right43(q2(x)) → Aq2(Right43(x))
Right44(q2(x)) → Aq2(Right44(x))
Right45(q2(x)) → Aq2(Right45(x))
Right46(q2(x)) → Aq2(Right46(x))
Right1(q3(x)) → Aq3(Right1(x))
Right2(q3(x)) → Aq3(Right2(x))
Right3(q3(x)) → Aq3(Right3(x))
Right4(q3(x)) → Aq3(Right4(x))
Right5(q3(x)) → Aq3(Right5(x))
Right6(q3(x)) → Aq3(Right6(x))
Right7(q3(x)) → Aq3(Right7(x))
Right8(q3(x)) → Aq3(Right8(x))
Right9(q3(x)) → Aq3(Right9(x))
Right10(q3(x)) → Aq3(Right10(x))
Right11(q3(x)) → Aq3(Right11(x))
Right12(q3(x)) → Aq3(Right12(x))
Right13(q3(x)) → Aq3(Right13(x))
Right14(q3(x)) → Aq3(Right14(x))
Right15(q3(x)) → Aq3(Right15(x))
Right16(q3(x)) → Aq3(Right16(x))
Right17(q3(x)) → Aq3(Right17(x))
Right18(q3(x)) → Aq3(Right18(x))
Right19(q3(x)) → Aq3(Right19(x))
Right20(q3(x)) → Aq3(Right20(x))
Right21(q3(x)) → Aq3(Right21(x))
Right22(q3(x)) → Aq3(Right22(x))
Right23(q3(x)) → Aq3(Right23(x))
Right24(q3(x)) → Aq3(Right24(x))
Right25(q3(x)) → Aq3(Right25(x))
Right26(q3(x)) → Aq3(Right26(x))
Right27(q3(x)) → Aq3(Right27(x))
Right28(q3(x)) → Aq3(Right28(x))
Right29(q3(x)) → Aq3(Right29(x))
Right30(q3(x)) → Aq3(Right30(x))
Right31(q3(x)) → Aq3(Right31(x))
Right32(q3(x)) → Aq3(Right32(x))
Right33(q3(x)) → Aq3(Right33(x))
Right34(q3(x)) → Aq3(Right34(x))
Right35(q3(x)) → Aq3(Right35(x))
Right36(q3(x)) → Aq3(Right36(x))
Right37(q3(x)) → Aq3(Right37(x))
Right38(q3(x)) → Aq3(Right38(x))
Right39(q3(x)) → Aq3(Right39(x))
Right40(q3(x)) → Aq3(Right40(x))
Right41(q3(x)) → Aq3(Right41(x))
Right42(q3(x)) → Aq3(Right42(x))
Right43(q3(x)) → Aq3(Right43(x))
Right44(q3(x)) → Aq3(Right44(x))
Right45(q3(x)) → Aq3(Right45(x))
Right46(q3(x)) → Aq3(Right46(x))
Right1(q4(x)) → Aq4(Right1(x))
Right2(q4(x)) → Aq4(Right2(x))
Right3(q4(x)) → Aq4(Right3(x))
Right4(q4(x)) → Aq4(Right4(x))
Right5(q4(x)) → Aq4(Right5(x))
Right6(q4(x)) → Aq4(Right6(x))
Right7(q4(x)) → Aq4(Right7(x))
Right8(q4(x)) → Aq4(Right8(x))
Right9(q4(x)) → Aq4(Right9(x))
Right10(q4(x)) → Aq4(Right10(x))
Right11(q4(x)) → Aq4(Right11(x))
Right12(q4(x)) → Aq4(Right12(x))
Right13(q4(x)) → Aq4(Right13(x))
Right14(q4(x)) → Aq4(Right14(x))
Right15(q4(x)) → Aq4(Right15(x))
Right16(q4(x)) → Aq4(Right16(x))
Right17(q4(x)) → Aq4(Right17(x))
Right18(q4(x)) → Aq4(Right18(x))
Right19(q4(x)) → Aq4(Right19(x))
Right20(q4(x)) → Aq4(Right20(x))
Right21(q4(x)) → Aq4(Right21(x))
Right22(q4(x)) → Aq4(Right22(x))
Right23(q4(x)) → Aq4(Right23(x))
Right24(q4(x)) → Aq4(Right24(x))
Right25(q4(x)) → Aq4(Right25(x))
Right26(q4(x)) → Aq4(Right26(x))
Right27(q4(x)) → Aq4(Right27(x))
Right28(q4(x)) → Aq4(Right28(x))
Right29(q4(x)) → Aq4(Right29(x))
Right30(q4(x)) → Aq4(Right30(x))
Right31(q4(x)) → Aq4(Right31(x))
Right32(q4(x)) → Aq4(Right32(x))
Right33(q4(x)) → Aq4(Right33(x))
Right34(q4(x)) → Aq4(Right34(x))
Right35(q4(x)) → Aq4(Right35(x))
Right36(q4(x)) → Aq4(Right36(x))
Right37(q4(x)) → Aq4(Right37(x))
Right38(q4(x)) → Aq4(Right38(x))
Right39(q4(x)) → Aq4(Right39(x))
Right40(q4(x)) → Aq4(Right40(x))
Right41(q4(x)) → Aq4(Right41(x))
Right42(q4(x)) → Aq4(Right42(x))
Right43(q4(x)) → Aq4(Right43(x))
Right44(q4(x)) → Aq4(Right44(x))
Right45(q4(x)) → Aq4(Right45(x))
Right46(q4(x)) → Aq4(Right46(x))
Right1(q5(x)) → Aq5(Right1(x))
Right2(q5(x)) → Aq5(Right2(x))
Right3(q5(x)) → Aq5(Right3(x))
Right4(q5(x)) → Aq5(Right4(x))
Right5(q5(x)) → Aq5(Right5(x))
Right6(q5(x)) → Aq5(Right6(x))
Right7(q5(x)) → Aq5(Right7(x))
Right8(q5(x)) → Aq5(Right8(x))
Right9(q5(x)) → Aq5(Right9(x))
Right10(q5(x)) → Aq5(Right10(x))
Right11(q5(x)) → Aq5(Right11(x))
Right12(q5(x)) → Aq5(Right12(x))
Right13(q5(x)) → Aq5(Right13(x))
Right14(q5(x)) → Aq5(Right14(x))
Right15(q5(x)) → Aq5(Right15(x))
Right16(q5(x)) → Aq5(Right16(x))
Right17(q5(x)) → Aq5(Right17(x))
Right18(q5(x)) → Aq5(Right18(x))
Right19(q5(x)) → Aq5(Right19(x))
Right20(q5(x)) → Aq5(Right20(x))
Right21(q5(x)) → Aq5(Right21(x))
Right22(q5(x)) → Aq5(Right22(x))
Right23(q5(x)) → Aq5(Right23(x))
Right24(q5(x)) → Aq5(Right24(x))
Right25(q5(x)) → Aq5(Right25(x))
Right26(q5(x)) → Aq5(Right26(x))
Right27(q5(x)) → Aq5(Right27(x))
Right28(q5(x)) → Aq5(Right28(x))
Right29(q5(x)) → Aq5(Right29(x))
Right30(q5(x)) → Aq5(Right30(x))
Right31(q5(x)) → Aq5(Right31(x))
Right32(q5(x)) → Aq5(Right32(x))
Right33(q5(x)) → Aq5(Right33(x))
Right34(q5(x)) → Aq5(Right34(x))
Right35(q5(x)) → Aq5(Right35(x))
Right36(q5(x)) → Aq5(Right36(x))
Right37(q5(x)) → Aq5(Right37(x))
Right38(q5(x)) → Aq5(Right38(x))
Right39(q5(x)) → Aq5(Right39(x))
Right40(q5(x)) → Aq5(Right40(x))
Right41(q5(x)) → Aq5(Right41(x))
Right42(q5(x)) → Aq5(Right42(x))
Right43(q5(x)) → Aq5(Right43(x))
Right44(q5(x)) → Aq5(Right44(x))
Right45(q5(x)) → Aq5(Right45(x))
Right46(q5(x)) → Aq5(Right46(x))
A0(Left(x)) → Left(0(x))
Aq0(Left(x)) → Left(q0(x))
Ah(Left(x)) → Left(h(x))
A1(Left(x)) → Left(1(x))
Aq1(Left(x)) → Left(q1(x))
Aq2(Left(x)) → Left(q2(x))
Aq3(Left(x)) → Left(q3(x))
Aq4(Left(x)) → Left(q4(x))
Aq5(Left(x)) → Left(q5(x))
Wait(Left(x)) → Begin(x)
0(q0(0(x))) → 0(0(q0(x)))
0(q0(h(x))) → 0(0(q0(h(x))))
0(q0(1(x))) → 0(1(q0(x)))
1(q1(0(x))) → 1(0(q1(x)))
1(q1(h(x))) → 1(0(q1(h(x))))
1(q1(1(x))) → 1(1(q1(x)))
0(q1(0(x))) → 0(0(q2(x)))
0(q1(h(x))) → 0(0(q2(h(x))))
0(q1(1(x))) → 0(1(q2(x)))
1(q2(0(x))) → 1(0(q2(x)))
1(q2(h(x))) → 1(0(q2(h(x))))
1(q2(1(x))) → 1(1(q2(x)))
0(q2(x)) → q3(1(x))
1(q3(x)) → q3(1(x))
0(q3(x)) → q4(0(x))
1(q4(x)) → q4(1(x))
0(q4(0(x))) → 1(0(q5(x)))
0(q4(h(x))) → 1(0(q5(h(x))))
0(q4(1(x))) → 1(1(q5(x)))
1(q5(0(x))) → 0(0(q1(x)))
1(q5(h(x))) → 0(0(q1(h(x))))
1(q5(1(x))) → 0(1(q1(x)))
h(q0(x)) → h(0(q0(x)))
h(q1(x)) → h(0(q1(x)))
h(q2(x)) → h(0(q2(x)))
h(q3(x)) → h(0(q3(x)))
h(q4(x)) → h(0(q4(x)))
h(q5(x)) → h(0(q5(x)))

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:
0 q0 h → 0 0 q0 h

0 q0 h → 0 0 q0 h
by original rule (OC 1)

(2) NO