Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema

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

0 QTRS

↳1 QTRS Reverse (⇔, 0 ms)

↳2 QTRS

↳3 QTRSRRRProof (⇔, 86 ms)

↳4 QTRS

↳5 DependencyPairsProof (⇔, 89 ms)

↳6 QDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 MRRProof (⇔, 34 ms)

        ↳13 QDP

        ↳14 MRRProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 MRRProof (⇔, 20 ms)

        ↳17 QDP

    ↳18 QDP

        ↳19 UsableRulesProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 QDP

        ↳24 UsableRulesProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 2177 ms)

        ↳27 QDP

        ↳28 MRRProof (⇔, 69 ms)

        ↳29 QDP

        ↳30 QDPOrderProof (⇔, 2422 ms)

        ↳31 QDP

        ↳32 MRRProof (⇔, 157 ms)

        ↳33 QDP

        ↳34 NonTerminationLoopProof (⇒, 1572 ms)

        ↳35 NO

(0) Obligation:

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

Begin(a(a(b(b(x))))) → Wait(Right1(x))
Begin(a(b(b(x)))) → Wait(Right2(x))
Begin(b(b(x))) → Wait(Right3(x))
Begin(b(x)) → Wait(Right4(x))
Begin(a(a(a(b(x))))) → Wait(Right5(x))
Begin(a(a(b(x)))) → Wait(Right6(x))
Begin(a(b(x))) → Wait(Right7(x))
Begin(b(x)) → Wait(Right8(x))
Begin(a(a(x))) → Wait(Right9(x))
Begin(a(x)) → Wait(Right10(x))
Begin(b(x)) → Wait(Right11(x))
Right1(a(End(x))) → Left(b(b(b(End(x)))))
Right2(a(a(End(x)))) → Left(b(b(b(End(x)))))
Right3(a(a(a(End(x))))) → Left(b(b(b(End(x)))))
Right4(a(a(a(b(End(x)))))) → Left(b(b(b(End(x)))))
Right5(b(End(x))) → Left(a(a(a(b(a(a(a(End(x)))))))))
Right6(b(a(End(x)))) → Left(a(a(a(b(a(a(a(End(x)))))))))
Right7(b(a(a(End(x))))) → Left(a(a(a(b(a(a(a(End(x)))))))))
Right8(b(a(a(a(End(x)))))) → Left(a(a(a(b(a(a(a(End(x)))))))))
Right9(a(End(x))) → Left(a(a(End(x))))
Right10(a(a(End(x)))) → Left(a(a(End(x))))
Right11(b(End(x))) → Left(a(b(a(End(x)))))
Right1(a(x)) → Aa(Right1(x))
Right2(a(x)) → Aa(Right2(x))
Right3(a(x)) → Aa(Right3(x))
Right4(a(x)) → Aa(Right4(x))
Right5(a(x)) → Aa(Right5(x))
Right6(a(x)) → Aa(Right6(x))
Right7(a(x)) → Aa(Right7(x))
Right8(a(x)) → Aa(Right8(x))
Right9(a(x)) → Aa(Right9(x))
Right10(a(x)) → Aa(Right10(x))
Right11(a(x)) → Aa(Right11(x))
Right1(b(x)) → Ab(Right1(x))
Right2(b(x)) → Ab(Right2(x))
Right3(b(x)) → Ab(Right3(x))
Right4(b(x)) → Ab(Right4(x))
Right5(b(x)) → Ab(Right5(x))
Right6(b(x)) → Ab(Right6(x))
Right7(b(x)) → Ab(Right7(x))
Right8(b(x)) → Ab(Right8(x))
Right9(b(x)) → Ab(Right9(x))
Right10(b(x)) → Ab(Right10(x))
Right11(b(x)) → Ab(Right11(x))
Aa(Left(x)) → Left(a(x))
Ab(Left(x)) → Left(b(x))
Wait(Left(x)) → Begin(x)
a(a(a(b(b(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))
a(a(a(x))) → a(a(x))
b(b(x)) → a(b(a(x)))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
a(a(Begin(x))) → Right9(Wait(x))
a(Begin(x)) → Right10(Wait(x))
b(Begin(x)) → Right11(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(Right9(x))) → End(a(a(Left(x))))
End(a(a(Right10(x)))) → End(a(a(Left(x))))
End(b(Right11(x))) → End(a(b(a(Left(x)))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))
a(a(a(x))) → a(a(x))
b(b(x)) → a(b(a(x)))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(Aa(x₁)) = 2 + x₁
POL(Ab(x₁)) = 6 + x₁
POL(Begin(x₁)) = x₁
POL(End(x₁)) = x₁
POL(Left(x₁)) = x₁
POL(Right1(x₁)) = 16 + x₁
POL(Right10(x₁)) = 1 + x₁
POL(Right11(x₁)) = 5 + x₁
POL(Right2(x₁)) = 14 + x₁
POL(Right3(x₁)) = 12 + x₁
POL(Right4(x₁)) = 6 + x₁
POL(Right5(x₁)) = 12 + x₁
POL(Right6(x₁)) = 10 + x₁
POL(Right7(x₁)) = 8 + x₁
POL(Right8(x₁)) = 6 + x₁
POL(Right9(x₁)) = 3 + x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 6 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a(a(Begin(x))) → Right9(Wait(x))
a(Begin(x)) → Right10(Wait(x))
b(Begin(x)) → Right11(Wait(x))
End(a(Right9(x))) → End(a(a(Left(x))))
End(a(a(Right10(x)))) → End(a(a(Left(x))))
End(b(Right11(x))) → End(a(b(a(Left(x)))))
a(a(a(x))) → a(a(x))
b(b(x)) → a(b(a(x)))

(4) Obligation:

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

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → B(b(b(Left(x))))
END(a(Right1(x))) → B(b(Left(x)))
END(a(Right1(x))) → B(Left(x))
END(a(Right1(x))) → LEFT(x)
END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(a(Right2(x)))) → B(b(b(Left(x))))
END(a(a(Right2(x)))) → B(b(Left(x)))
END(a(a(Right2(x)))) → B(Left(x))
END(a(a(Right2(x)))) → LEFT(x)
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → B(b(b(Left(x))))
END(a(a(a(Right3(x))))) → B(b(Left(x)))
END(a(a(a(Right3(x))))) → B(Left(x))
END(a(a(a(Right3(x))))) → LEFT(x)
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → B(b(b(Left(x))))
END(b(a(a(a(Right4(x)))))) → B(b(Left(x)))
END(b(a(a(a(Right4(x)))))) → B(Left(x))
END(b(a(a(a(Right4(x)))))) → LEFT(x)
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(b(Right5(x))) → A(a(a(b(a(a(a(Left(x))))))))
END(b(Right5(x))) → A(a(b(a(a(a(Left(x)))))))
END(b(Right5(x))) → A(b(a(a(a(Left(x))))))
END(b(Right5(x))) → B(a(a(a(Left(x)))))
END(b(Right5(x))) → A(a(a(Left(x))))
END(b(Right5(x))) → A(a(Left(x)))
END(b(Right5(x))) → A(Left(x))
END(b(Right5(x))) → LEFT(x)
END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(b(Right6(x)))) → A(a(a(b(a(a(a(Left(x))))))))
END(a(b(Right6(x)))) → A(a(b(a(a(a(Left(x)))))))
END(a(b(Right6(x)))) → A(b(a(a(a(Left(x))))))
END(a(b(Right6(x)))) → B(a(a(a(Left(x)))))
END(a(b(Right6(x)))) → A(a(a(Left(x))))
END(a(b(Right6(x)))) → A(a(Left(x)))
END(a(b(Right6(x)))) → A(Left(x))
END(a(b(Right6(x)))) → LEFT(x)
END(a(a(b(Right7(x))))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(b(Right7(x))))) → A(a(a(b(a(a(a(Left(x))))))))
END(a(a(b(Right7(x))))) → A(a(b(a(a(a(Left(x)))))))
END(a(a(b(Right7(x))))) → A(b(a(a(a(Left(x))))))
END(a(a(b(Right7(x))))) → B(a(a(a(Left(x)))))
END(a(a(b(Right7(x))))) → A(a(a(Left(x))))
END(a(a(b(Right7(x))))) → A(a(Left(x)))
END(a(a(b(Right7(x))))) → A(Left(x))
END(a(a(b(Right7(x))))) → LEFT(x)
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → A(a(a(b(a(a(a(Left(x))))))))
END(a(a(a(b(Right8(x)))))) → A(a(b(a(a(a(Left(x)))))))
END(a(a(a(b(Right8(x)))))) → A(b(a(a(a(Left(x))))))
END(a(a(a(b(Right8(x)))))) → B(a(a(a(Left(x)))))
END(a(a(a(b(Right8(x)))))) → A(a(a(Left(x))))
END(a(a(a(b(Right8(x)))))) → A(a(Left(x)))
END(a(a(a(b(Right8(x)))))) → A(Left(x))
END(a(a(a(b(Right8(x)))))) → LEFT(x)
LEFT(Aa(x)) → A(Left(x))
LEFT(Aa(x)) → LEFT(x)
LEFT(Ab(x)) → B(Left(x))
LEFT(Ab(x)) → LEFT(x)
B(b(a(a(a(x))))) → B(b(b(x)))
B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → A(a(a(b(a(a(a(x)))))))
B(a(a(a(b(x))))) → A(a(b(a(a(a(x))))))
B(a(a(a(b(x))))) → A(b(a(a(a(x)))))
B(a(a(a(b(x))))) → B(a(a(a(x))))
B(a(a(a(b(x))))) → A(a(a(x)))
B(a(a(a(b(x))))) → A(a(x))
B(a(a(a(b(x))))) → A(x)

The TRS R consists of the following rules:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 56 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(b(b(x)))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → B(a(a(a(x))))

The TRS R consists of the following rules:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(b(b(x)))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → B(a(a(a(x))))

The TRS R consists of the following rules:

a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(B(x₁)) = 2·x₁
POL(Begin(x₁)) = 2 + 2·x₁
POL(Right1(x₁)) = x₁
POL(Right10(x₁)) = 2·x₁
POL(Right11(x₁)) = 2·x₁
POL(Right2(x₁)) = x₁
POL(Right3(x₁)) = x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = 2·x₁
POL(Right7(x₁)) = 2·x₁
POL(Right8(x₁)) = 2·x₁
POL(Right9(x₁)) = x₁
POL(Wait(x₁)) = 1 + x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(b(b(x)))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → B(a(a(a(x))))

The TRS R consists of the following rules:

a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) MRRProof (EQUIVALENT transformation)

b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(B(x₁)) = 2·x₁
POL(Begin(x₁)) = 3 + 2·x₁
POL(Right1(x₁)) = x₁
POL(Right10(x₁)) = x₁
POL(Right11(x₁)) = 2·x₁
POL(Right2(x₁)) = x₁
POL(Right3(x₁)) = 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = x₁
POL(Right6(x₁)) = 2·x₁
POL(Right7(x₁)) = x₁
POL(Right8(x₁)) = x₁
POL(Right9(x₁)) = 2·x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(b(b(x)))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → B(a(a(a(x))))

The TRS R consists of the following rules:

a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) MRRProof (EQUIVALENT transformation)

B(b(a(a(a(x))))) → B(b(x))
B(b(a(a(a(x))))) → B(x)
B(a(a(a(b(x))))) → B(a(a(a(x))))

Strictly oriented rules of the TRS R:

a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = 1 + x₁
POL(B(x₁)) = x₁
POL(Right1(x₁)) = x₁
POL(Right10(x₁)) = 3 + 2·x₁
POL(Right11(x₁)) = 1 + x₁
POL(Right2(x₁)) = 1 + 2·x₁
POL(Right3(x₁)) = 2·x₁
POL(Right4(x₁)) = 2 + x₁
POL(Right5(x₁)) = x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = 3 + 2·x₁
POL(Right8(x₁)) = 1 + x₁
POL(Right9(x₁)) = x₁
POL(a(x₁)) = 1 + x₁
POL(b(x₁)) = 3 + x₁

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

B(b(a(a(a(x))))) → B(b(b(x)))

The TRS R consists of the following rules:

b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEFT(Ab(x)) → LEFT(x)
LEFT(Aa(x)) → LEFT(x)

The TRS R consists of the following rules:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEFT(Ab(x)) → LEFT(x)
LEFT(Aa(x)) → LEFT(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LEFT(Ab(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(Aa(x)) → LEFT(x)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(b(Right7(x))))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
End(a(Right1(x))) → End(b(b(b(Left(x)))))
End(a(a(Right2(x)))) → End(b(b(b(Left(x)))))
End(a(a(a(Right3(x))))) → End(b(b(b(Left(x)))))
End(b(a(a(a(Right4(x)))))) → End(b(b(b(Left(x)))))
End(b(Right5(x))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(b(Right6(x)))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(b(Right7(x))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
End(a(a(a(b(Right8(x)))))) → End(a(a(a(b(a(a(a(Left(x)))))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(b(Right7(x))))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

END(a(a(b(Right7(x))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(END(x₁)) = 0A +
[ -I, 0A, 0A ]

· x₁

POL(a(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 1A -I \

| -I -I -I |

\ 0A 0A -I /

· x₁

POL(Right2(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(b(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Left(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right1(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right3(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right4(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I 1A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right5(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right6(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I -I 0A /

· x₁

POL(Right7(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right8(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I -I 0A /

· x₁

POL(Aa(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I 0A -I /

· x₁

POL(Ab(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Wait(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Begin(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| -I 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right9(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right10(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(Right11(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ -I 0A 1A \

| -I 0A -I |

\ -I 0A 0A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(a(Begin(x))) → Right7(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) MRRProof (EQUIVALENT transformation)

b(a(Begin(x))) → Right7(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 1 + 2·x₁
POL(END(x₁)) = 2·x₁
POL(Left(x₁)) = 1 + 2·x₁
POL(Right1(x₁)) = 1 + 2·x₁
POL(Right10(x₁)) = 2·x₁
POL(Right11(x₁)) = 2·x₁
POL(Right2(x₁)) = 1 + 2·x₁
POL(Right3(x₁)) = 1 + 2·x₁
POL(Right4(x₁)) = 1 + 2·x₁
POL(Right5(x₁)) = 1 + 2·x₁
POL(Right6(x₁)) = 1 + 2·x₁
POL(Right7(x₁)) = x₁
POL(Right8(x₁)) = 1 + 2·x₁
POL(Right9(x₁)) = 2·x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

END(a(b(Right6(x)))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(END(x₁)) = 0A +
[ -I, 0A, -I ]

· x₁

POL(a(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I -I -I \

| 0A -I -I |

\ 0A 0A 0A /

· x₁

POL(Right2(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A -I \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(b(x₁)) =
/ 1A \

| 0A |

\ 1A /

+
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Left(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right1(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right3(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right4(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I -I -I /

· x₁

POL(Right5(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right6(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ -I 0A -I \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right8(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Aa(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Ab(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Wait(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| -I -I -I |

\ -I -I -I /

· x₁

POL(Begin(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A -I 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right7(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A -I \

| -I 0A 0A |

\ -I 0A -I /

· x₁

POL(Right9(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I -I \

| -I -I -I |

\ -I 0A -I /

· x₁

POL(Right10(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ -I 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right11(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A 0A \

| -I -I 0A |

\ -I 0A 0A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(a(a(Begin(x)))) → Right6(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) MRRProof (EQUIVALENT transformation)

b(a(a(Begin(x)))) → Right6(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 1 + 2·x₁
POL(END(x₁)) = 2·x₁
POL(Left(x₁)) = 1 + 2·x₁
POL(Right1(x₁)) = 1 + 2·x₁
POL(Right10(x₁)) = 2·x₁
POL(Right11(x₁)) = 2·x₁
POL(Right2(x₁)) = 1 + 2·x₁
POL(Right3(x₁)) = 1 + 2·x₁
POL(Right4(x₁)) = 1 + 2·x₁
POL(Right5(x₁)) = 1 + 2·x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = 2·x₁
POL(Right8(x₁)) = 1 + 2·x₁
POL(Right9(x₁)) = 2·x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(33) Obligation:

Q DP problem:
The TRS P consists of the following rules:

END(a(a(Right2(x)))) → END(b(b(b(Left(x)))))
END(a(Right1(x))) → END(b(b(b(Left(x)))))
END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))
END(b(a(a(a(Right4(x)))))) → END(b(b(b(Left(x)))))
END(b(Right5(x))) → END(a(a(a(b(a(a(a(Left(x)))))))))
END(a(a(a(b(Right8(x)))))) → END(a(a(a(b(a(a(a(Left(x)))))))))

The TRS R consists of the following rules:

Left(Aa(x)) → a(Left(x))
Left(Ab(x)) → b(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
a(Right6(x)) → Right6(Aa(x))
a(Right7(x)) → Right7(Aa(x))
a(Right8(x)) → Right8(Aa(x))
a(Right9(x)) → Right9(Aa(x))
a(Right10(x)) → Right10(Aa(x))
a(Right11(x)) → Right11(Aa(x))
b(b(a(a(Begin(x))))) → Right1(Wait(x))
b(b(a(Begin(x)))) → Right2(Wait(x))
b(b(Begin(x))) → Right3(Wait(x))
b(Begin(x)) → Right4(Wait(x))
b(a(a(a(Begin(x))))) → Right5(Wait(x))
b(Begin(x)) → Right8(Wait(x))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
b(Right6(x)) → Right6(Ab(x))
b(Right7(x)) → Right7(Ab(x))
b(Right8(x)) → Right8(Ab(x))
b(Right9(x)) → Right9(Ab(x))
b(Right10(x)) → Right10(Ab(x))
b(Right11(x)) → Right11(Ab(x))
b(b(a(a(a(x))))) → b(b(b(x)))
b(a(a(a(b(x))))) → a(a(a(b(a(a(a(x)))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(34) NonTerminationLoopProof (COMPLETE transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = END(b(b(b(Left(Ab(Aa(Aa(Aa(Wait(x)))))))))) evaluates to t =END(b(b(b(Left(Ab(Aa(Aa(Aa(Wait(x))))))))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

END(b(b(b(Left(Ab(Aa(Aa(Aa(Wait(x)))))))))) → END(b(b(b(b(Left(Aa(Aa(Aa(Wait(x))))))))))
with rule Left(Ab(x')) → b(Left(x')) at position [0,0,0,0] and matcher [x' / Aa(Aa(Aa(Wait(x))))]

END(b(b(b(b(Left(Aa(Aa(Aa(Wait(x)))))))))) → END(b(b(b(b(a(Left(Aa(Aa(Wait(x))))))))))
with rule Left(Aa(x')) → a(Left(x')) at position [0,0,0,0,0] and matcher [x' / Aa(Aa(Wait(x)))]

END(b(b(b(b(a(Left(Aa(Aa(Wait(x)))))))))) → END(b(b(b(b(a(a(Left(Aa(Wait(x))))))))))
with rule Left(Aa(x')) → a(Left(x')) at position [0,0,0,0,0,0] and matcher [x' / Aa(Wait(x))]

END(b(b(b(b(a(a(Left(Aa(Wait(x)))))))))) → END(b(b(b(b(a(a(a(Left(Wait(x))))))))))
with rule Left(Aa(x')) → a(Left(x')) at position [0,0,0,0,0,0,0] and matcher [x' / Wait(x)]

END(b(b(b(b(a(a(a(Left(Wait(x)))))))))) → END(b(b(b(b(a(a(a(Begin(x)))))))))
with rule Left(Wait(x')) → Begin(x') at position [0,0,0,0,0,0,0,0] and matcher [x' / x]

END(b(b(b(b(a(a(a(Begin(x))))))))) → END(b(b(b(Right5(Wait(x))))))
with rule b(a(a(a(Begin(x'))))) → Right5(Wait(x')) at position [0,0,0,0] and matcher [x' / x]

END(b(b(b(Right5(Wait(x)))))) → END(b(b(Right5(Ab(Wait(x))))))
with rule b(Right5(x')) → Right5(Ab(x')) at position [0,0,0] and matcher [x' / Wait(x)]

END(b(b(Right5(Ab(Wait(x)))))) → END(b(Right5(Ab(Ab(Wait(x))))))
with rule b(Right5(x')) → Right5(Ab(x')) at position [0,0] and matcher [x' / Ab(Wait(x))]

END(b(Right5(Ab(Ab(Wait(x)))))) → END(a(a(a(b(a(a(a(Left(Ab(Ab(Wait(x))))))))))))
with rule END(b(Right5(x'))) → END(a(a(a(b(a(a(a(Left(x'))))))))) at position [] and matcher [x' / Ab(Ab(Wait(x)))]

END(a(a(a(b(a(a(a(Left(Ab(Ab(Wait(x)))))))))))) → END(a(a(a(b(a(a(a(b(Left(Ab(Wait(x))))))))))))
with rule Left(Ab(x')) → b(Left(x')) at position [0,0,0,0,0,0,0,0] and matcher [x' / Ab(Wait(x))]

END(a(a(a(b(a(a(a(b(Left(Ab(Wait(x)))))))))))) → END(a(a(a(b(a(a(a(b(b(Left(Wait(x))))))))))))
with rule Left(Ab(x')) → b(Left(x')) at position [0,0,0,0,0,0,0,0,0] and matcher [x' / Wait(x)]

END(a(a(a(b(a(a(a(b(b(Left(Wait(x)))))))))))) → END(a(a(a(b(a(a(a(b(b(Begin(x)))))))))))
with rule Left(Wait(x')) → Begin(x') at position [0,0,0,0,0,0,0,0,0,0] and matcher [x' / x]

END(a(a(a(b(a(a(a(b(b(Begin(x))))))))))) → END(a(a(a(b(a(a(a(Right3(Wait(x))))))))))
with rule b(b(Begin(x'))) → Right3(Wait(x')) at position [0,0,0,0,0,0,0,0] and matcher [x' / x]

END(a(a(a(b(a(a(a(Right3(Wait(x)))))))))) → END(a(a(a(b(a(a(Right3(Aa(Wait(x))))))))))
with rule a(Right3(x')) → Right3(Aa(x')) at position [0,0,0,0,0,0,0] and matcher [x' / Wait(x)]

END(a(a(a(b(a(a(Right3(Aa(Wait(x)))))))))) → END(a(a(a(b(a(Right3(Aa(Aa(Wait(x))))))))))
with rule a(Right3(x')) → Right3(Aa(x')) at position [0,0,0,0,0,0] and matcher [x' / Aa(Wait(x))]

END(a(a(a(b(a(Right3(Aa(Aa(Wait(x)))))))))) → END(a(a(a(b(Right3(Aa(Aa(Aa(Wait(x))))))))))
with rule a(Right3(x')) → Right3(Aa(x')) at position [0,0,0,0,0] and matcher [x' / Aa(Aa(Wait(x)))]

END(a(a(a(b(Right3(Aa(Aa(Aa(Wait(x)))))))))) → END(a(a(a(Right3(Ab(Aa(Aa(Aa(Wait(x))))))))))
with rule b(Right3(x')) → Right3(Ab(x')) at position [0,0,0,0] and matcher [x' / Aa(Aa(Aa(Wait(x))))]

END(a(a(a(Right3(Ab(Aa(Aa(Aa(Wait(x)))))))))) → END(b(b(b(Left(Ab(Aa(Aa(Aa(Wait(x))))))))))
with rule END(a(a(a(Right3(x))))) → END(b(b(b(Left(x)))))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(0) Obligation:

(1) QTRS Reverse (EQUIVALENT transformation)

(2) Obligation:

(3) QTRSRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) MRRProof (EQUIVALENT transformation)

(13) Obligation:

(14) MRRProof (EQUIVALENT transformation)

(15) Obligation:

(16) MRRProof (EQUIVALENT transformation)

(17) Obligation:

(18) Obligation:

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) MRRProof (EQUIVALENT transformation)

(29) Obligation:

(30) QDPOrderProof (EQUIVALENT transformation)

(31) Obligation:

(32) MRRProof (EQUIVALENT transformation)

(33) Obligation:

(34) NonTerminationLoopProof (COMPLETE transformation)

(35) NO