YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/examples/collection/a-bPhi-split.srs

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

0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 90 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 19 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 UsableRulesProof (⇔, 1 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 QDPOrderProof (⇔, 91 ms)
        ↳23 QDP
        ↳24 QDPOrderProof (⇔, 49 ms)
        ↳25 QDP
        ↳26 MRRProof (⇔, 89 ms)
        ↳27 QDP
        ↳28 MRRProof (⇔, 89 ms)
        ↳29 QDP
        ↳30 MRRProof (⇔, 42 ms)
        ↳31 QDP
        ↳32 MRRProof (⇔, 50 ms)
        ↳33 QDP
        ↳34 MRRProof (⇔, 48 ms)
        ↳35 QDP
        ↳36 MRRProof (⇔, 44 ms)
        ↳37 QDP
        ↳38 QDPOrderProof (⇔, 56 ms)
        ↳39 QDP
        ↳40 PisEmptyProof (⇔, 0 ms)
        ↳41 YES

(0) Obligation:

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

Begin(E(x)) → Wait(Right1(x))
Begin(L(x)) → Wait(Right2(x))
Begin(L(x)) → Wait(Right3(x))
Begin(Aa(x)) → Wait(Right4(x))
Begin(Ab(x)) → Wait(Right5(x))
Begin(L(x)) → Wait(Right6(x))
Right1(R(End(x))) → Left(L(E(End(x))))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right4(R(End(x))) → Left(a(R(End(x))))
Right5(R(End(x))) → Left(b(R(End(x))))
Right6(a(End(x))) → Left(b(R(End(x))))
Right1(R(x)) → AR(Right1(x))
Right2(R(x)) → AR(Right2(x))
Right3(R(x)) → AR(Right3(x))
Right4(R(x)) → AR(Right4(x))
Right5(R(x)) → AR(Right5(x))
Right6(R(x)) → AR(Right6(x))
Right1(E(x)) → AE(Right1(x))
Right2(E(x)) → AE(Right2(x))
Right3(E(x)) → AE(Right3(x))
Right4(E(x)) → AE(Right4(x))
Right5(E(x)) → AE(Right5(x))
Right6(E(x)) → AE(Right6(x))
Right1(L(x)) → AL(Right1(x))
Right2(L(x)) → AL(Right2(x))
Right3(L(x)) → AL(Right3(x))
Right4(L(x)) → AL(Right4(x))
Right5(L(x)) → AL(Right5(x))
Right6(L(x)) → AL(Right6(x))
Right1(a(x)) → AAa(Right1(x))
Right2(a(x)) → AAa(Right2(x))
Right3(a(x)) → AAa(Right3(x))
Right4(a(x)) → AAa(Right4(x))
Right5(a(x)) → AAa(Right5(x))
Right6(a(x)) → AAa(Right6(x))
Right1(Aa(x)) → AAAa(Right1(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right1(b(x)) → AAb(Right1(x))
Right2(b(x)) → AAb(Right2(x))
Right3(b(x)) → AAb(Right3(x))
Right4(b(x)) → AAb(Right4(x))
Right5(b(x)) → AAb(Right5(x))
Right6(b(x)) → AAb(Right6(x))
Right1(Ab(x)) → AAAb(Right1(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right6(Ab(x)) → AAAb(Right6(x))
AR(Left(x)) → Left(R(x))
AE(Left(x)) → Left(E(x))
AL(Left(x)) → Left(L(x))
AAa(Left(x)) → Left(a(x))
AAAa(Left(x)) → Left(Aa(x))
AAb(Left(x)) → Left(b(x))
AAAb(Left(x)) → Left(Ab(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
a(L(x)) → b(R(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:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(Begin(x)) → Right6(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(a(x)) → R(b(x))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(AAAa(x1)) = 4 + x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = 4 + x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = 1 + x1   
POL(AL(x1)) = 1 + x1   
POL(AR(x1)) = 3 + x1   
POL(Aa(x1)) = 4 + x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = x1   
POL(E(x1)) = 1 + x1   
POL(End(x1)) = x1   
POL(L(x1)) = 1 + x1   
POL(Left(x1)) = x1   
POL(R(x1)) = 3 + x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = 1 + x1   
POL(Right3(x1)) = 1 + x1   
POL(Right4(x1)) = 4 + x1   
POL(Right5(x1)) = x1   
POL(Right6(x1)) = x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = 4 + x1   
POL(b(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right6(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right6(x))) → End(R(b(Left(x))))
E(R(x)) → E(L(x))
L(a(x)) → R(b(x))


(4) Obligation:

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

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(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(Right2(x))) → END(Aa(L(Left(x))))
END(a(Right2(x))) → AA(L(Left(x)))
END(a(Right2(x))) → L1(Left(x))
END(a(Right2(x))) → LEFT(x)
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(b(Right3(x))) → AB(L(Left(x)))
END(b(Right3(x))) → L1(Left(x))
END(b(Right3(x))) → LEFT(x)
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right4(x))) → R1(a(Left(x)))
END(R(Right4(x))) → A(Left(x))
END(R(Right4(x))) → LEFT(x)
END(R(Right5(x))) → END(R(b(Left(x))))
END(R(Right5(x))) → R1(b(Left(x)))
END(R(Right5(x))) → B(Left(x))
END(R(Right5(x))) → LEFT(x)
LEFT(AR(x)) → R1(Left(x))
LEFT(AR(x)) → LEFT(x)
LEFT(AE(x)) → E1(Left(x))
LEFT(AE(x)) → LEFT(x)
LEFT(AL(x)) → L1(Left(x))
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → A(Left(x))
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → AA(Left(x))
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → B(Left(x))
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → AB(Left(x))
LEFT(AAAb(x)) → LEFT(x)
L1(a(x)) → AA(L(x))
L1(a(x)) → L1(x)
L1(b(x)) → AB(L(x))
L1(b(x)) → L1(x)
AA(R(x)) → R1(a(x))
AA(R(x)) → A(x)
AB(R(x)) → R1(b(x))
AB(R(x)) → B(x)

The TRS R consists of the following rules:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(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 25 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

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

The TRS R consists of the following rules:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(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:

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

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

(12) 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:

  • L1(b(x)) → L1(x)
    The graph contains the following edges 1 > 1

  • L1(a(x)) → L1(x)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LEFT(AE(x)) → LEFT(x)
LEFT(AR(x)) → LEFT(x)
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → LEFT(x)

The TRS R consists of the following rules:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))

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

(15) 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.

(16) Obligation:

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

LEFT(AE(x)) → LEFT(x)
LEFT(AR(x)) → LEFT(x)
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → LEFT(x)

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

(17) 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(AE(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AR(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AL(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AAa(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AAAa(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AAb(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

  • LEFT(AAAb(x)) → LEFT(x)
    The graph contains the following edges 1 > 1

(18) YES

(19) Obligation:

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

END(b(Right3(x))) → END(Ab(L(Left(x))))
END(a(Right2(x))) → END(Aa(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))

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

(20) 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.

(21) Obligation:

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

END(b(Right3(x))) → END(Ab(L(Left(x))))
END(a(Right2(x))) → END(Aa(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))

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

(22) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


END(a(Right2(x))) → END(Aa(L(Left(x))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = x1   
POL(AL(x1)) = x1   
POL(AR(x1)) = x1   
POL(Aa(x1)) = 0   
POL(Ab(x1)) = 0   
POL(Begin(x1)) = x1   
POL(E(x1)) = 0   
POL(END(x1)) = x1   
POL(L(x1)) = 0   
POL(Left(x1)) = 0   
POL(R(x1)) = 0   
POL(Right1(x1)) = 0   
POL(Right2(x1)) = 0   
POL(Right3(x1)) = 0   
POL(Right4(x1)) = 0   
POL(Right5(x1)) = 0   
POL(Right6(x1)) = 0   
POL(Wait(x1)) = x1   
POL(a(x1)) = 1   
POL(b(x1)) = 0   

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

Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))

(23) Obligation:

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

END(b(Right3(x))) → END(Ab(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))

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

(24) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


END(b(Right3(x))) → END(Ab(L(Left(x))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = x1   
POL(AL(x1)) = x1   
POL(AR(x1)) = x1   
POL(Aa(x1)) = 0   
POL(Ab(x1)) = 0   
POL(Begin(x1)) = x1   
POL(E(x1)) = 0   
POL(END(x1)) = x1   
POL(L(x1)) = 0   
POL(Left(x1)) = 0   
POL(R(x1)) = 0   
POL(Right1(x1)) = 0   
POL(Right2(x1)) = 0   
POL(Right3(x1)) = 0   
POL(Right4(x1)) = 0   
POL(Right5(x1)) = 0   
POL(Right6(x1)) = 0   
POL(Wait(x1)) = x1   
POL(a(x1)) = 0   
POL(b(x1)) = 1   

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

Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))

(25) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))

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

(26) 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:

R(Right6(x)) → Right6(AR(x))
E(Right6(x)) → Right6(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = 2·x1   
POL(AL(x1)) = x1   
POL(AR(x1)) = 2·x1   
POL(Aa(x1)) = x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(E(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(L(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(R(x1)) = 2·x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = 2·x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2 + 2·x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   

(27) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(28) 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:

R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
L(Right6(x)) → Right6(AL(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = x1   
POL(AL(x1)) = 2·x1   
POL(AR(x1)) = 1 + 2·x1   
POL(Aa(x1)) = x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(E(x1)) = x1   
POL(END(x1)) = x1   
POL(L(x1)) = 2·x1   
POL(Left(x1)) = 2·x1   
POL(R(x1)) = 2 + 2·x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2 + x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   

(29) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(30) 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:

E(Right1(x)) → Right1(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = 2·x1   
POL(AL(x1)) = x1   
POL(AR(x1)) = 2·x1   
POL(Aa(x1)) = x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(E(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(L(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(R(x1)) = 2·x1   
POL(Right1(x1)) = 2 + 2·x1   
POL(Right2(x1)) = 2·x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   

(31) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(32) 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:

L(Right1(x)) → Right1(AL(x))
E(Right3(x)) → Right3(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = 1 + 2·x1   
POL(AL(x1)) = 2·x1   
POL(AR(x1)) = 2·x1   
POL(Aa(x1)) = x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(E(x1)) = 2 + 2·x1   
POL(END(x1)) = 2·x1   
POL(L(x1)) = 2·x1   
POL(Left(x1)) = 2·x1   
POL(R(x1)) = 2·x1   
POL(Right1(x1)) = 2 + 2·x1   
POL(Right2(x1)) = 2·x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   

(33) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(34) 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(Right1(x)) → Right1(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Aa(Right1(x)) → Right1(AAAa(x))
a(Right1(x)) → Right1(AAa(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = 2·x1   
POL(AAAb(x1)) = 2·x1   
POL(AAa(x1)) = 2·x1   
POL(AAb(x1)) = 2·x1   
POL(AE(x1)) = 2·x1   
POL(AL(x1)) = x1   
POL(AR(x1)) = 2·x1   
POL(Aa(x1)) = 2·x1   
POL(Ab(x1)) = 2·x1   
POL(Begin(x1)) = x1   
POL(E(x1)) = 2·x1   
POL(END(x1)) = x1   
POL(L(x1)) = x1   
POL(Left(x1)) = x1   
POL(R(x1)) = 2·x1   
POL(Right1(x1)) = 3 + 2·x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = 2·x1   
POL(b(x1)) = 2·x1   

(35) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(36) 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:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x1)) = x1   
POL(AAAb(x1)) = x1   
POL(AAa(x1)) = x1   
POL(AAb(x1)) = x1   
POL(AE(x1)) = 2·x1   
POL(AL(x1)) = 1 + 3·x1   
POL(AR(x1)) = 2·x1   
POL(Aa(x1)) = x1   
POL(Ab(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(E(x1)) = 2·x1   
POL(END(x1)) = x1   
POL(L(x1)) = 2 + 3·x1   
POL(Left(x1)) = 2·x1   
POL(R(x1)) = 2·x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = 1 + x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2·x1   
POL(Right6(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   

(37) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(38) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( END(x1) ) = max{0, 2x1 - 1}

POL( R(x1) ) = max{0, 2x1 - 2}

POL( a(x1) ) = x1 + 1

POL( b(x1) ) = x1 + 1

POL( Left(x1) ) = x1

POL( AR(x1) ) = 2x1

POL( AE(x1) ) = 2x1

POL( E(x1) ) = max{0, 2x1 - 2}

POL( AL(x1) ) = 2x1 + 2

POL( L(x1) ) = 2x1 + 2

POL( AAa(x1) ) = x1 + 1

POL( AAAa(x1) ) = x1 + 2

POL( Aa(x1) ) = x1 + 2

POL( AAb(x1) ) = x1 + 1

POL( AAAb(x1) ) = x1 + 2

POL( Ab(x1) ) = x1 + 2

POL( Wait(x1) ) = 0

POL( Begin(x1) ) = 0

POL( Right2(x1) ) = 2

POL( Right3(x1) ) = 2

POL( Right4(x1) ) = x1 + 2

POL( Right5(x1) ) = x1 + 2

POL( Right6(x1) ) = max{0, x1 - 1}


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

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))

(39) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(R(x)) → R(a(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))

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

(40) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(41) YES