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

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

0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 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 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES
    ↳17 QDP
        ↳18 UsableRulesProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 QDPSizeChangeProof (⇔, 0 ms)
        ↳21 YES
    ↳22 QDP
        ↳23 UsableRulesProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 QDPOrderProof (⇔, 18 ms)
        ↳26 QDP
        ↳27 DependencyGraphProof (⇔, 0 ms)
        ↳28 AND
            ↳29 QDP
                ↳30 MRRProof (⇔, 0 ms)
                ↳31 QDP
                ↳32 PisEmptyProof (⇔, 0 ms)
                ↳33 YES
            ↳34 QDP
                ↳35 MRRProof (⇔, 0 ms)
                ↳36 QDP
                ↳37 PisEmptyProof (⇔, 0 ms)
                ↳38 YES

(0) Obligation:

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

active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
proper(g(X)) → g(proper(X))
proper(h(X)) → h(proper(X))
proper(c) → ok(c)
proper(d) → ok(d)
g(ok(X)) → ok(g(X))
h(ok(X)) → ok(h(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(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:

G(active(X)) → H(mark(X))
G(active(X)) → MARK(X)
C'(active(x)) → D'(mark(x))
C'(active(x)) → MARK(x)
D'(h(active(x))) → C'(g(mark(x)))
D'(h(active(x))) → G(mark(x))
D'(h(active(x))) → MARK(x)
G(proper(X)) → G(X)
H(proper(X)) → H(X)
C'(proper(x)) → C'(ok(x))
C'(proper(x)) → OK(x)
D'(proper(x)) → D'(ok(x))
D'(proper(x)) → OK(x)
OK(g(X)) → G(ok(X))
OK(g(X)) → OK(X)
OK(h(X)) → H(ok(X))
OK(h(X)) → OK(X)

The TRS R consists of the following rules:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(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 9 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

H(proper(X)) → H(X)

The TRS R consists of the following rules:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(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:

H(proper(X)) → H(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:

  • H(proper(X)) → H(X)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

G(proper(X)) → G(X)

The TRS R consists of the following rules:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(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:

G(proper(X)) → G(X)

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

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

  • G(proper(X)) → G(X)
    The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

OK(h(X)) → OK(X)
OK(g(X)) → OK(X)

The TRS R consists of the following rules:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(X))

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

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

(19) Obligation:

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

OK(h(X)) → OK(X)
OK(g(X)) → OK(X)

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

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

  • OK(h(X)) → OK(X)
    The graph contains the following edges 1 > 1

  • OK(g(X)) → OK(X)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

D'(h(active(x))) → C'(g(mark(x)))
C'(active(x)) → D'(mark(x))
D'(proper(x)) → D'(ok(x))
C'(proper(x)) → C'(ok(x))

The TRS R consists of the following rules:

g(active(X)) → h(mark(X))
c'(active(x)) → d'(mark(x))
d'(h(active(x))) → c'(g(mark(x)))
g(proper(X)) → proper(g(X))
h(proper(X)) → proper(h(X))
c'(proper(x)) → c'(ok(x))
d'(proper(x)) → d'(ok(x))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
mark(top(X)) → proper(top(X))
ok(top(X)) → active(top(X))

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

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

(24) Obligation:

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

D'(h(active(x))) → C'(g(mark(x)))
C'(active(x)) → D'(mark(x))
D'(proper(x)) → D'(ok(x))
C'(proper(x)) → C'(ok(x))

The TRS R consists of the following rules:

ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(X))

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

(25) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


C'(active(x)) → D'(mark(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(C'(x1)) = x1   
POL(D'(x1)) = 0   
POL(active(x1)) = 1   
POL(g(x1)) = 0   
POL(h(x1)) = 0   
POL(mark(x1)) = 0   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   
POL(top(x1)) = 1   

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

g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))

(26) Obligation:

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

D'(h(active(x))) → C'(g(mark(x)))
D'(proper(x)) → D'(ok(x))
C'(proper(x)) → C'(ok(x))

The TRS R consists of the following rules:

ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(X))

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

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.

(28) Complex Obligation (AND)

(29) Obligation:

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

C'(proper(x)) → C'(ok(x))

The TRS R consists of the following rules:

ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(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 dependency pairs:

C'(proper(x)) → C'(ok(x))

Strictly oriented rules of the TRS R:

ok(g(X)) → g(ok(X))

Used ordering: Polynomial interpretation [POLO]:

POL(C'(x1)) = x1   
POL(active(x1)) = x1   
POL(g(x1)) = 3 + 3·x1   
POL(h(x1)) = x1   
POL(mark(x1)) = 3 + 3·x1   
POL(ok(x1)) = 2·x1   
POL(proper(x1)) = 3 + 3·x1   
POL(top(x1)) = 2·x1   

(31) Obligation:

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

ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(X))

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

(32) PisEmptyProof (EQUIVALENT transformation)

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

(33) YES

(34) Obligation:

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

D'(proper(x)) → D'(ok(x))

The TRS R consists of the following rules:

ok(g(X)) → g(ok(X))
ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(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 dependency pairs:

D'(proper(x)) → D'(ok(x))

Strictly oriented rules of the TRS R:

ok(g(X)) → g(ok(X))

Used ordering: Polynomial interpretation [POLO]:

POL(D'(x1)) = x1   
POL(active(x1)) = x1   
POL(g(x1)) = 3 + 3·x1   
POL(h(x1)) = x1   
POL(mark(x1)) = 3 + 3·x1   
POL(ok(x1)) = 2·x1   
POL(proper(x1)) = 3 + 3·x1   
POL(top(x1)) = 2·x1   

(36) Obligation:

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

ok(h(X)) → h(ok(X))
ok(top(X)) → active(top(X))
h(proper(X)) → proper(h(X))
g(active(X)) → h(mark(X))
g(proper(X)) → proper(g(X))
mark(top(X)) → proper(top(X))

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

(37) PisEmptyProof (EQUIVALENT transformation)

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

(38) YES