YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Mixed_SRS/s6.srs

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

0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 29 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 12 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 MNOCProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 UsableRulesProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 QReductionProof (⇔, 0 ms)
        ↳15 QDP
        ↳16 QDPSizeChangeProof (⇔, 0 ms)
        ↳17 YES
    ↳18 QDP
        ↳19 MNOCProof (⇔, 0 ms)
        ↳20 QDP
        ↳21 UsableRulesProof (⇔, 0 ms)
        ↳22 QDP
        ↳23 QReductionProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 QDPSizeChangeProof (⇔, 0 ms)
        ↳26 YES
    ↳27 QDP
        ↳28 UsableRulesProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 QDPSizeChangeProof (⇔, 0 ms)
        ↳31 YES

(0) Obligation:

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

a12(a12(x)) → x
a13(a13(x)) → x
a14(a14(x)) → x
a15(a15(x)) → x
a16(a16(x)) → x
a23(a23(x)) → x
a24(a24(x)) → x
a25(a25(x)) → x
a26(a26(x)) → x
a34(a34(x)) → x
a35(a35(x)) → x
a36(a36(x)) → x
a45(a45(x)) → x
a46(a46(x)) → x
a56(a56(x)) → x
a13(x) → a12(a23(a12(x)))
a14(x) → a12(a23(a34(a23(a12(x)))))
a15(x) → a12(a23(a34(a45(a34(a23(a12(x)))))))
a16(x) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x)))))))))
a24(x) → a23(a34(a23(x)))
a25(x) → a23(a34(a45(a34(a23(x)))))
a26(x) → a23(a34(a45(a56(a45(a34(a23(x)))))))
a35(x) → a34(a45(a34(x)))
a36(x) → a34(a45(a56(a45(a34(x)))))
a46(x) → a45(a56(a45(x)))
a12(a23(a12(a23(a12(a23(x)))))) → x
a23(a34(a23(a34(a23(a34(x)))))) → x
a34(a45(a34(a45(a34(a45(x)))))) → x
a45(a56(a45(a56(a45(a56(x)))))) → x
a12(a34(x)) → a34(a12(x))
a12(a45(x)) → a45(a12(x))
a12(a56(x)) → a56(a12(x))
a23(a45(x)) → a45(a23(x))
a23(a56(x)) → a56(a23(x))
a34(a56(x)) → a56(a34(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:

a12(a12(x)) → x
a13(a13(x)) → x
a14(a14(x)) → x
a15(a15(x)) → x
a16(a16(x)) → x
a23(a23(x)) → x
a24(a24(x)) → x
a25(a25(x)) → x
a26(a26(x)) → x
a34(a34(x)) → x
a35(a35(x)) → x
a36(a36(x)) → x
a45(a45(x)) → x
a46(a46(x)) → x
a56(a56(x)) → x
a13(x) → a12(a23(a12(x)))
a14(x) → a12(a23(a34(a23(a12(x)))))
a15(x) → a12(a23(a34(a45(a34(a23(a12(x)))))))
a16(x) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x)))))))))
a24(x) → a23(a34(a23(x)))
a25(x) → a23(a34(a45(a34(a23(x)))))
a26(x) → a23(a34(a45(a56(a45(a34(a23(x)))))))
a35(x) → a34(a45(a34(x)))
a36(x) → a34(a45(a56(a45(a34(x)))))
a46(x) → a45(a56(a45(x)))
a23(a12(a23(a12(a23(a12(x)))))) → x
a34(a23(a34(a23(a34(a23(x)))))) → x
a45(a34(a45(a34(a45(a34(x)))))) → x
a56(a45(a56(a45(a56(a45(x)))))) → x
a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(a12(x1)) = 1 + x1   
POL(a13(x1)) = 4 + x1   
POL(a14(x1)) = 6 + x1   
POL(a15(x1)) = 8 + x1   
POL(a16(x1)) = 10 + x1   
POL(a23(x1)) = 1 + x1   
POL(a24(x1)) = 4 + x1   
POL(a25(x1)) = 6 + x1   
POL(a26(x1)) = 8 + x1   
POL(a34(x1)) = 1 + x1   
POL(a35(x1)) = 4 + x1   
POL(a36(x1)) = 6 + x1   
POL(a45(x1)) = 1 + x1   
POL(a46(x1)) = 4 + x1   
POL(a56(x1)) = 1 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a12(a12(x)) → x
a13(a13(x)) → x
a14(a14(x)) → x
a15(a15(x)) → x
a16(a16(x)) → x
a23(a23(x)) → x
a24(a24(x)) → x
a25(a25(x)) → x
a26(a26(x)) → x
a34(a34(x)) → x
a35(a35(x)) → x
a36(a36(x)) → x
a45(a45(x)) → x
a46(a46(x)) → x
a56(a56(x)) → x
a13(x) → a12(a23(a12(x)))
a14(x) → a12(a23(a34(a23(a12(x)))))
a15(x) → a12(a23(a34(a45(a34(a23(a12(x)))))))
a16(x) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x)))))))))
a24(x) → a23(a34(a23(x)))
a25(x) → a23(a34(a45(a34(a23(x)))))
a26(x) → a23(a34(a45(a56(a45(a34(a23(x)))))))
a35(x) → a34(a45(a34(x)))
a36(x) → a34(a45(a56(a45(a34(x)))))
a46(x) → a45(a56(a45(x)))
a23(a12(a23(a12(a23(a12(x)))))) → x
a34(a23(a34(a23(a34(a23(x)))))) → x
a45(a34(a45(a34(a45(a34(x)))))) → x
a56(a45(a56(a45(a56(a45(x)))))) → x


(4) Obligation:

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

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(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:

A34(a12(x)) → A34(x)
A45(a12(x)) → A45(x)
A56(a12(x)) → A56(x)
A45(a23(x)) → A45(x)
A56(a23(x)) → A56(x)
A56(a34(x)) → A34(a56(x))
A56(a34(x)) → A56(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(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 1 less node.

(8) Complex Obligation (AND)

(9) Obligation:

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

A45(a23(x)) → A45(x)
A45(a12(x)) → A45(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

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

(10) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(11) Obligation:

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

A45(a23(x)) → A45(x)
A45(a12(x)) → A45(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

The set Q consists of the following terms:

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

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

(12) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

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

A45(a23(x)) → A45(x)
A45(a12(x)) → A45(x)

R is empty.
The set Q consists of the following terms:

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

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

(14) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

(15) Obligation:

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

A45(a23(x)) → A45(x)
A45(a12(x)) → A45(x)

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

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

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

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

(17) YES

(18) Obligation:

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

A34(a12(x)) → A34(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

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

(19) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(20) Obligation:

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

A34(a12(x)) → A34(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

The set Q consists of the following terms:

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

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

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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

A34(a12(x)) → A34(x)

R is empty.
The set Q consists of the following terms:

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

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

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a34(a12(x0))
a45(a12(x0))
a56(a12(x0))
a45(a23(x0))
a56(a23(x0))
a56(a34(x0))

(24) Obligation:

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

A34(a12(x)) → A34(x)

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

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

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

(26) YES

(27) Obligation:

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

A56(a23(x)) → A56(x)
A56(a12(x)) → A56(x)
A56(a34(x)) → A56(x)

The TRS R consists of the following rules:

a34(a12(x)) → a12(a34(x))
a45(a12(x)) → a12(a45(x))
a56(a12(x)) → a12(a56(x))
a45(a23(x)) → a23(a45(x))
a56(a23(x)) → a23(a56(x))
a56(a34(x)) → a34(a56(x))

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

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

(29) Obligation:

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

A56(a23(x)) → A56(x)
A56(a12(x)) → A56(x)
A56(a34(x)) → A56(x)

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

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

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

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

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

(31) YES