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

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

0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 36 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 QDP
        ↳13 UsableRulesProof (⇔, 0 ms)
        ↳14 QDP
        ↳15 MRRProof (⇔, 28 ms)
        ↳16 QDP
        ↳17 PisEmptyProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 QDPSizeChangeProof (⇔, 0 ms)
        ↳23 YES
    ↳24 QDP
        ↳25 UsableRulesProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 QDPOrderProof (⇔, 38 ms)
        ↳28 QDP
        ↳29 QDPOrderProof (⇔, 35 ms)
        ↳30 QDP
        ↳31 MRRProof (⇔, 43 ms)
        ↳32 QDP
        ↳33 MRRProof (⇔, 26 ms)
        ↳34 QDP
        ↳35 MRRProof (⇔, 32 ms)
        ↳36 QDP
        ↳37 MRRProof (⇔, 17 ms)
        ↳38 QDP
        ↳39 MRRProof (⇔, 4 ms)
        ↳40 QDP
        ↳41 MRRProof (⇔, 13 ms)
        ↳42 QDP
        ↳43 MRRProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 UsableRulesProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 QDPOrderProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 PisEmptyProof (⇔, 0 ms)
        ↳50 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))
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))))
Right1(0(x)) → A0(Right1(x))
Right2(0(x)) → A0(Right2(x))
Right3(0(x)) → A0(Right3(x))
Right4(0(x)) → A0(Right4(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))
Right1(1(x)) → A1(Right1(x))
Right2(1(x)) → A1(Right2(x))
Right3(1(x)) → A1(Right3(x))
Right4(1(x)) → A1(Right4(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))
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))

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))
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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) 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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) 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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

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

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

(10) 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

(11) YES

(12) 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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

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

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

1(Right1(x)) → Right1(A1(x))
1(Right2(x)) → Right2(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(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(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))

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

(15) 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))
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))
0(Right1(x)) → Right1(A0(x))
0(Right2(x)) → Right2(A0(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(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)) = 2·x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 3 + 3·x1   
POL(P1(x1)) = 3·x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = 2 + 2·x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = 2·x1   
POL(Wait(x1)) = 2·x1   
POL(c(x1)) = 1 + 2·x1   

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

(17) PisEmptyProof (EQUIVALENT transformation)

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

(18) YES

(19) 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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

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

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.

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

(23) YES

(24) 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))
P(Right1(x)) → Right1(AP(x))
P(Right2(x)) → Right2(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(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.

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

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

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(1(x)) → P(c(x))
P(0(x)) → P(1(x))

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

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

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

(30) 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(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) 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))
P(Begin(x)) → Right2(Wait(x))
P(Right2(x)) → Right2(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)) = 2·x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2 + x1   
POL(END(x1)) = x1   
POL(Left(x1)) = x1   
POL(P(x1)) = 2·x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = 1 + x1   
POL(Right3(x1)) = x1   
POL(Right4(x1)) = x1   
POL(Wait(x1)) = 2 + x1   
POL(c(x1)) = x1   

(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(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(Right1(x)) → Right1(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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(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)) = x1   
POL(Ac(x1)) = 2·x1   
POL(Begin(x1)) = x1   
POL(END(x1)) = 2·x1   
POL(Left(x1)) = x1   
POL(P(x1)) = x1   
POL(Right1(x1)) = x1   
POL(Right2(x1)) = 1 + 2·x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = 2·x1   
POL(Wait(x1)) = 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(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(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right1(x)) → Right1(A1(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
P(Right1(x)) → Right1(AP(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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:

c(Right1(x)) → Right1(Ac(x))
0(Right1(x)) → Right1(A0(x))
1(Right1(x)) → Right1(A1(x))
P(Right1(x)) → Right1(AP(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)) = x1   
POL(END(x1)) = x1   
POL(Left(x1)) = x1   
POL(P(x1)) = 2·x1   
POL(Right1(x1)) = 1 + x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = 2·x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 2·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(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(A1(x))
P(Right3(x)) → Right3(AP(x))
P(Right4(x)) → Right4(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:

P(Right4(x)) → Right4(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(Right3(x1)) = 2·x1   
POL(Right4(x1)) = x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 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(Begin(x)) → Right4(Wait(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(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(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.

(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(Begin(x)) → Right4(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)) = x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2 + 2·x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = x1   
POL(Right3(x1)) = 2·x1   
POL(Right4(x1)) = x1   
POL(Wait(x1)) = 1 + x1   
POL(c(x1)) = 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(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(0(x)) → 0(1(x))
c(1(x)) → 0(c(x))
0(Right3(x)) → Right3(A0(x))
0(Right4(x)) → Right4(A0(x))
1(Right3(x)) → Right3(A1(x))
1(Right4(x)) → Right4(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.

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

c(Right4(x)) → Right4(Ac(x))
0(Right4(x)) → Right4(A0(x))
1(Right4(x)) → Right4(A1(x))
P(Right3(x)) → Right3(AP(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)) = 2·x1   
POL(Ac(x1)) = 1 + x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 2·x1   
POL(Right3(x1)) = 2 + 2·x1   
POL(Right4(x1)) = 2 + x1   
POL(Wait(x1)) = x1   
POL(c(x1)) = 2 + 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(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(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:

Left(AP(x)) → P(Left(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 + 2·x1   
POL(Ac(x1)) = x1   
POL(Begin(x1)) = 2·x1   
POL(END(x1)) = x1   
POL(Left(x1)) = 2·x1   
POL(P(x1)) = 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(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(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) 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.

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

(47) 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)) = 2·x1   
POL(1(x1)) = 2·x1   
POL(A0(x1)) = 2·x1   
POL(A1(x1)) = 2·x1   
POL(Ac(x1)) = 4·x1   
POL(Begin(x1)) = 4   
POL(END(x1)) = x1   
POL(Left(x1)) = x1   
POL(Right3(x1)) = 1 + 2·x1   
POL(Wait(x1)) = 4   
POL(c(x1)) = 4·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))

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

(49) PisEmptyProof (EQUIVALENT transformation)

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

(50) YES