YES Termination w.r.t. Q proof of Secret_05_TRS_cime2.ari

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

0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 QDPOrderProof (⇔, 2610 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 QDPSizeChangeProof (⇔, 0 ms)
        ↳9 YES
    ↳10 QDP
        ↳11 QDPSizeChangeProof (⇔, 0 ms)
        ↳12 YES

(0) Obligation:

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

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

CIRC(cons(a, s), t) → MSUBST(a, t)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
MSUBST(msubst(a, s), t) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

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

(3) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


CIRC(cons(a, s), t) → MSUBST(a, t)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation with max and min functions [POLO,MAXPOLO]:

POL(CIRC(x1, x2)) = x1 + x2   
POL(MSUBST(x1, x2)) = x1 + x2   
POL(circ(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + max(x1, x2)   
POL(id) = 1   
POL(lift) = 1   
POL(msubst(x1, x2)) = x1 + x2   

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

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
msubst(msubst(a, s), t) → msubst(a, circ(s, t))
msubst(a, id) → a

(4) Obligation:

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

CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(circ(s, t), u) → CIRC(t, u)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
MSUBST(msubst(a, s), t) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

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 2 SCCs with 1 less node.

(6) Complex Obligation (AND)

(7) Obligation:

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

CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(circ(s, t), u) → CIRC(s, circ(t, u))

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

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

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

  • CIRC(circ(s, t), u) → CIRC(t, u)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
    The graph contains the following edges 1 > 1

(9) YES

(10) Obligation:

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

MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

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

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

  • MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
    The graph contains the following edges 1 > 1

(12) YES