YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/examples/collection/bincountremove-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 (⇔, 51 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 31 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 MRRProof (⇔, 33 ms)
        ↳18 QDP
        ↳19 PisEmptyProof (⇔, 0 ms)
        ↳20 YES
    ↳21 QDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QDPSizeChangeProof (⇔, 0 ms)
        ↳25 YES
    ↳26 QDP
        ↳27 UsableRulesProof (⇔, 0 ms)
        ↳28 QDP
        ↳29 QDPOrderProof (⇔, 56 ms)
        ↳30 QDP
        ↳31 QDPOrderProof (⇔, 29 ms)
        ↳32 QDP
        ↳33 MRRProof (⇔, 39 ms)
        ↳34 QDP
        ↳35 MRRProof (⇔, 38 ms)
        ↳36 QDP
        ↳37 MRRProof (⇔, 17 ms)
        ↳38 QDP
        ↳39 MRRProof (⇔, 47 ms)
        ↳40 QDP
        ↳41 MRRProof (⇔, 13 ms)
        ↳42 QDP
        ↳43 MRRProof (⇔, 12 ms)
        ↳44 QDP
        ↳45 MRRProof (⇔, 25 ms)
        ↳46 QDP
        ↳47 MRRProof (⇔, 14 ms)
        ↳48 QDP
        ↳49 UsableRulesProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QDPOrderProof (⇔, 5 ms)
        ↳52 QDP
        ↳53 PisEmptyProof (⇔, 0 ms)
        ↳54 YES

(0) Obligation:

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

Begin(P(x)) → Wait(Right1(x))
Begin(P(x)) → Wait(Right2(x))
Begin(c(x)) → Wait(Right3(x))
Begin(c(x)) → Wait(Right4(x))
Begin(c(x)) → Wait(Right5(x))
Right1(0(End(x))) → Left(1(P(End(x))))
Right2(1(End(x))) → Left(c(P(End(x))))
Right3(0(End(x))) → Left(1(0(End(x))))
Right4(1(End(x))) → Left(c(0(End(x))))
Right5(P(End(x))) → Left(P(End(x)))
Right1(0(x)) → A0(Right1(x))
Right2(0(x)) → A0(Right2(x))
Right3(0(x)) → A0(Right3(x))
Right4(0(x)) → A0(Right4(x))
Right5(0(x)) → A0(Right5(x))
Right1(P(x)) → AP(Right1(x))
Right2(P(x)) → AP(Right2(x))
Right3(P(x)) → AP(Right3(x))
Right4(P(x)) → AP(Right4(x))
Right5(P(x)) → AP(Right5(x))
Right1(1(x)) → A1(Right1(x))
Right2(1(x)) → A1(Right2(x))
Right3(1(x)) → A1(Right3(x))
Right4(1(x)) → A1(Right4(x))
Right5(1(x)) → A1(Right5(x))
Right1(c(x)) → Ac(Right1(x))
Right2(c(x)) → Ac(Right2(x))
Right3(c(x)) → Ac(Right3(x))
Right4(c(x)) → Ac(Right4(x))
Right5(c(x)) → Ac(Right5(x))
A0(Left(x)) → Left(0(x))
AP(Left(x)) → Left(P(x))
A1(Left(x)) → Left(1(x))
Ac(Left(x)) → Left(c(x))
Wait(Left(x)) → Begin(x)
0(P(x)) → 1(P(x))
1(P(x)) → c(P(x))
0(c(x)) → 1(0(x))
1(c(x)) → c(0(x))
P(c(x)) → P(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:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Begin(x)) → Right5(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
End(P(Right5(x))) → End(P(Left(x)))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
c(P(x)) → P(x)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0(x1)) = 2 + x1   
POL(1(x1)) = 2 + x1   
POL(A0(x1)) = 2 + x1   
POL(A1(x1)) = 2 + x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = 2 + x1   
POL(Begin(x1)) = x1   
POL(End(x1)) = x1   
POL(Left(x1)) = x1   
POL(P(x1)) = x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = 2 + x1   
POL(Right4(x1)) = 2 + x1   
POL(Right5(x1)) = 1 + x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 2 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

c(Begin(x)) → Right5(Wait(x))
End(P(Right5(x))) → End(P(Left(x)))
c(P(x)) → P(x)


(4) Obligation:

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

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(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(0(Right1(x))) → END(P(1(Left(x))))
END(0(Right1(x))) → P1(1(Left(x)))
END(0(Right1(x))) → 11(Left(x))
END(0(Right1(x))) → LEFT(x)
END(1(Right2(x))) → END(P(c(Left(x))))
END(1(Right2(x))) → P1(c(Left(x)))
END(1(Right2(x))) → C(Left(x))
END(1(Right2(x))) → LEFT(x)
END(0(Right3(x))) → END(0(1(Left(x))))
END(0(Right3(x))) → 01(1(Left(x)))
END(0(Right3(x))) → 11(Left(x))
END(0(Right3(x))) → LEFT(x)
END(1(Right4(x))) → END(0(c(Left(x))))
END(1(Right4(x))) → 01(c(Left(x)))
END(1(Right4(x))) → C(Left(x))
END(1(Right4(x))) → LEFT(x)
LEFT(A0(x)) → 01(Left(x))
LEFT(A0(x)) → LEFT(x)
LEFT(AP(x)) → P1(Left(x))
LEFT(AP(x)) → LEFT(x)
LEFT(A1(x)) → 11(Left(x))
LEFT(A1(x)) → LEFT(x)
LEFT(Ac(x)) → C(Left(x))
LEFT(Ac(x)) → LEFT(x)
P1(0(x)) → P1(1(x))
P1(0(x)) → 11(x)
P1(1(x)) → P1(c(x))
P1(1(x)) → C(x)
C(0(x)) → 01(1(x))
C(0(x)) → 11(x)
C(1(x)) → 01(c(x))
C(1(x)) → C(x)

The TRS R consists of the following rules:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(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 4 SCCs with 21 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

C(1(x)) → C(x)

The TRS R consists of the following rules:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(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:

C(1(x)) → C(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:

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

(13) YES

(14) Obligation:

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

P1(1(x)) → P1(c(x))
P1(0(x)) → P1(1(x))

The TRS R consists of the following rules:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(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:

P1(1(x)) → P1(c(x))
P1(0(x)) → P1(1(x))

The TRS R consists of the following rules:

1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))

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

(17) 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 dependency pairs:

P1(1(x)) → P1(c(x))
P1(0(x)) → P1(1(x))

Strictly oriented rules of the TRS R:

1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 3 + 2·x1   
POL(1(x1)) = 2 + 2·x1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 3 + 3·x1   
POL(P1(x1)) = 3·x1   
POL(Right1(x1)) = 2 + 2·x1   
POL(Right2(x1)) = 2·x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = x1   
POL(Right5(x1)) = 2 + 2·x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 1 + 2·x1   

(18) Obligation:

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

c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

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

(19) PisEmptyProof (EQUIVALENT transformation)

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

(20) YES

(21) Obligation:

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

LEFT(AP(x)) → LEFT(x)
LEFT(A0(x)) → LEFT(x)
LEFT(A1(x)) → LEFT(x)
LEFT(Ac(x)) → LEFT(x)

The TRS R consists of the following rules:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

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

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

(23) Obligation:

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

LEFT(AP(x)) → LEFT(x)
LEFT(A0(x)) → LEFT(x)
LEFT(A1(x)) → LEFT(x)
LEFT(Ac(x)) → LEFT(x)

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

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

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

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

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

(25) YES

(26) Obligation:

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

END(1(Right2(x))) → END(P(c(Left(x))))
END(0(Right1(x))) → END(P(1(Left(x))))
END(0(Right3(x))) → END(0(1(Left(x))))
END(1(Right4(x))) → END(0(c(Left(x))))

The TRS R consists of the following rules:

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
End(0(Right1(x))) → End(P(1(Left(x))))
End(1(Right2(x))) → End(P(c(Left(x))))
End(0(Right3(x))) → End(0(1(Left(x))))
End(1(Right4(x))) → End(0(c(Left(x))))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

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

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

(28) Obligation:

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

END(1(Right2(x))) → END(P(c(Left(x))))
END(0(Right1(x))) → END(P(1(Left(x))))
END(0(Right3(x))) → END(0(1(Left(x))))
END(1(Right4(x))) → END(0(c(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

(29) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


END(1(Right2(x))) → END(P(c(Left(x))))
END(1(Right4(x))) → END(0(c(Left(x))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 0   
POL(1(x1)) = 1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 0   
POL(P(x1)) = 0   
POL(Right1(x1)) = 0   
POL(Right2(x1)) = 0   
POL(Right3(x1)) = 0   
POL(Right4(x1)) = 0   
POL(Right5(x1)) = 0   
POL(Wait(x1)) = x1   
POL(c(x1)) = 0   

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

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))

(30) Obligation:

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

END(0(Right1(x))) → END(P(1(Left(x))))
END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

(31) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


END(0(Right1(x))) → END(P(1(Left(x))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 1   
POL(1(x1)) = 0   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 0   
POL(P(x1)) = 0   
POL(Right1(x1)) = 0   
POL(Right2(x1)) = 0   
POL(Right3(x1)) = 0   
POL(Right4(x1)) = 0   
POL(Right5(x1)) = 0   
POL(Wait(x1)) = x1   
POL(c(x1)) = 0   

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

P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(0(x)) → P(1(x))
P(1(x)) → P(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))

(32) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
0(Right5(x)) → Right5(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
1(Right5(x)) → Right5(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

c(Right5(x)) → Right5(Ac(x))
0(Right5(x)) → Right5(A0(x))
1(Right5(x)) → Right5(A1(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 2·x1   
POL(1(x1)) = 2·x1   
POL(A0(x1)) = 2·x1   
POL(A1(x1)) = 2·x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = 2·x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = x1   
POL(P(x1)) = x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = 2·x1   
POL(Right5(x1)) = 2 + 2·x1   
POL(Wait(x1)) = 2·x1   
POL(c(x1)) = 2·x1   

(34) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right4(x)) → Right4(AP(x))
P(Right5(x)) → Right5(AP(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = x1   
POL(1(x1)) = x1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(AP(x1)) = 1 + x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 2 + x1   
POL(Right1(x1)) = 2 + x1   
POL(Right2(x1)) = 2 + x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = x1   
POL(Right5(x1)) = 2 + x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = x1   

(36) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Begin(x)) → Right4(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

c(Begin(x)) → Right4(Wait(x))
c(Right4(x)) → Right4(Ac(x))
0(Right4(x)) → Right4(A0(x))
1(Right4(x)) → Right4(A1(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 2·x1   
POL(1(x1)) = 2·x1   
POL(A0(x1)) = 2·x1   
POL(A1(x1)) = 2·x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = 2·x1   
POL(Begin(x1)) = 2 + x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = x1   
POL(P(x1)) = x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = 1 + x1   
POL(Wait(x1)) = 2 + x1   
POL(c(x1)) = 2·x1   

(38) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

c(Right2(x)) → Right2(Ac(x))
0(Right2(x)) → Right2(A0(x))
1(Right2(x)) → Right2(A1(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 2·x1   
POL(1(x1)) = 2·x1   
POL(A0(x1)) = 2·x1   
POL(A1(x1)) = 2·x1   
POL(AP(x1)) = 2·x1   
POL(Ac(x1)) = 2·x1   
POL(Begin(x1)) = 2 + x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = x1   
POL(P(x1)) = 2·x1   
POL(Right1(x1)) = 2·x1   
POL(Right2(x1)) = 2 + x1   
POL(Right3(x1)) = 2·x1   
POL(Wait(x1)) = 2 + x1   
POL(c(x1)) = 2·x1   

(40) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right3(x)) → Right3(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right3(x)) → Right3(A1(x))
P(Begin(x)) → Right1(Wait(x))
P(Begin(x)) → Right2(Wait(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

P(Begin(x)) → Right1(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = x1   
POL(1(x1)) = x1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(AP(x1)) = 1 + x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 2 + x1   
POL(Right1(x1)) = 2·x1   
POL(Right2(x1)) = 2 + x1   
POL(Right3(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = x1   

(42) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right3(x)) → Right3(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right3(x)) → Right3(A1(x))
P(Begin(x)) → Right2(Wait(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

P(Begin(x)) → Right2(Wait(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = x1   
POL(1(x1)) = x1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(AP(x1)) = 1 + x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 2 + x1   
POL(Right1(x1)) = 2·x1   
POL(Right2(x1)) = 1 + 2·x1   
POL(Right3(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = x1   

(44) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right1(x)) → Right1(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right1(x)) → Right1(A0(x))
0(Right3(x)) → Right3(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right3(x)) → Right3(A1(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

c(Right1(x)) → Right1(Ac(x))
0(Right1(x)) → Right1(A0(x))
1(Right1(x)) → Right1(A1(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 2·x1   
POL(1(x1)) = 2·x1   
POL(A0(x1)) = 2·x1   
POL(A1(x1)) = 2·x1   
POL(AP(x1)) = x1   
POL(Ac(x1)) = 2·x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = x1   
POL(P(x1)) = x1   
POL(Right1(x1)) = 3 + x1   
POL(Right3(x1)) = 2·x1   
POL(Wait(x1)) = 2·x1   
POL(c(x1)) = 2·x1   

(46) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(AP(x)) → P(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right3(x)) → Right3(A0(x))
1(Right3(x)) → Right3(A1(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

Left(AP(x)) → P(Left(x))

Used ordering: Polynomial interpretation [POLO]:

POL(0(x1)) = 2 + x1   
POL(1(x1)) = 2 + x1   
POL(A0(x1)) = 1 + x1   
POL(A1(x1)) = 1 + x1   
POL(AP(x1)) = 1 + 2·x1   
POL(Ac(x1)) = 1 + x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 2·x1   
POL(Right3(x1)) = 2 + 2·x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 2 + x1   

(48) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
c(Begin(x)) → Right3(Wait(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right3(x)) → Right3(A0(x))
1(Right3(x)) → Right3(A1(x))
P(Right3(x)) → Right3(AP(x))
P(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

(50) Obligation:

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

END(0(Right3(x))) → END(0(1(Left(x))))

The TRS R consists of the following rules:

Left(A0(x)) → 0(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
1(Right3(x)) → Right3(A1(x))
0(Right3(x)) → Right3(A0(x))
c(Begin(x)) → Right3(Wait(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

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

(51) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


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

POL(0(x1)) = x1   
POL(1(x1)) = x1   
POL(A0(x1)) = x1   
POL(A1(x1)) = x1   
POL(Ac(x1)) = 1 + x1   
POL(Begin(x1)) = 1 + x1   
POL(END(x1)) = x1   
POL(Left(x1)) = x1   
POL(Right3(x1)) = 1 + x1   
POL(Wait(x1)) = 1 + x1   
POL(c(x1)) = 1 + x1   

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

Left(A0(x)) → 0(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
1(Right3(x)) → Right3(A1(x))
0(Right3(x)) → Right3(A0(x))
c(Begin(x)) → Right3(Wait(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

(52) Obligation:

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

Left(A0(x)) → 0(Left(x))
Left(A1(x)) → 1(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Wait(x)) → Begin(x)
1(Right3(x)) → Right3(A1(x))
0(Right3(x)) → Right3(A0(x))
c(Begin(x)) → Right3(Wait(x))
c(Right3(x)) → Right3(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))

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

(53) PisEmptyProof (EQUIVALENT transformation)

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

(54) YES