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

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

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

(0) Obligation:

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

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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:

.1(.(x, y), z) → .1(x, .(y, z))
.1(.(x, y), z) → .1(y, z)
A(f(x)) → F(a(x))
A(f(x)) → A(x)
A(.(x, y)) → .1(a(x), y)
A(.(x, y)) → A(x)
A(b1(x)) → B1(a(x))
A(b1(x)) → A(x)
F(b(x)) → F(x)
.1(b(x), y) → .1(x, y)
A(f(.(0, x))) → B1(.(f(.(0, x)), .(0, f(x))))
A(f(.(0, x))) → .1(f(.(0, x)), .(0, f(x)))
A(f(.(0, x))) → .1(0, f(x))
A(f(.(0, x))) → F(x)
A(f(0)) → B1(.(f(0), 0))
A(f(0)) → .1(f(0), 0)
F(.(0, x)) → .1(0, f(x))
F(.(0, x)) → F(x)
C(b(x)) → C(a(x))
C(b(x)) → A(x)
A(b(x)) → A(x)

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

.1(.(x, y), z) → .1(y, z)
.1(.(x, y), z) → .1(x, .(y, z))
.1(b(x), y) → .1(x, y)

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

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

(7) Obligation:

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

.1(.(x, y), z) → .1(y, z)
.1(.(x, y), z) → .1(x, .(y, z))
.1(b(x), y) → .1(x, y)

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
.(b(x), y) → b(.(x, y))

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:

  • .1(.(x, y), z) → .1(y, z)
    The graph contains the following edges 1 > 1, 2 >= 2

  • .1(.(x, y), z) → .1(x, .(y, z))
    The graph contains the following edges 1 > 1

  • .1(b(x), y) → .1(x, y)
    The graph contains the following edges 1 > 1, 2 >= 2

(9) YES

(10) Obligation:

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

F(.(0, x)) → F(x)
F(b(x)) → F(x)

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

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

(12) Obligation:

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

F(.(0, x)) → F(x)
F(b(x)) → F(x)

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

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

  • F(.(0, x)) → F(x)
    The graph contains the following edges 1 > 1

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

(14) YES

(15) Obligation:

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

A(.(x, y)) → A(x)
A(f(x)) → A(x)
A(b1(x)) → A(x)
A(b(x)) → A(x)

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

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

(17) Obligation:

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

A(.(x, y)) → A(x)
A(f(x)) → A(x)
A(b1(x)) → A(x)
A(b(x)) → A(x)

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

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

  • A(.(x, y)) → A(x)
    The graph contains the following edges 1 > 1

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

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

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

(19) YES

(20) Obligation:

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

C(b(x)) → C(a(x))

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

(21) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule C(b(x)) → C(a(x)) at position [0] we obtained the following new rules [LPAR04]:

C(b(f(x0))) → C(f(a(x0))) → C(b(f(x0))) → C(f(a(x0)))
C(b(.(x0, x1))) → C(.(a(x0), x1)) → C(b(.(x0, x1))) → C(.(a(x0), x1))
C(b(b1(x0))) → C(b1(a(x0))) → C(b(b1(x0))) → C(b1(a(x0)))
C(b(f(.(0, x0)))) → C(b1(.(f(.(0, x0)), .(0, f(x0))))) → C(b(f(.(0, x0)))) → C(b1(.(f(.(0, x0)), .(0, f(x0)))))
C(b(f(0))) → C(b1(.(f(0), 0))) → C(b(f(0))) → C(b1(.(f(0), 0)))
C(b(b(x0))) → C(b(a(x0))) → C(b(b(x0))) → C(b(a(x0)))

(22) Obligation:

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

C(b(f(x0))) → C(f(a(x0)))
C(b(.(x0, x1))) → C(.(a(x0), x1))
C(b(b1(x0))) → C(b1(a(x0)))
C(b(f(.(0, x0)))) → C(b1(.(f(.(0, x0)), .(0, f(x0)))))
C(b(f(0))) → C(b1(.(f(0), 0)))
C(b(b(x0))) → C(b(a(x0)))

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

(23) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


C(b(f(.(0, x0)))) → C(b1(.(f(.(0, x0)), .(0, f(x0)))))
C(b(f(0))) → C(b1(.(f(0), 0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
C(x1)  =  x1
b(x1)  =  x1
f(x1)  =  f
.(x1, x2)  =  .
b1(x1)  =  x1
a(x1)  =  x1
0  =  0

Knuth-Bendix order [KBO] with precedence:
f > 0
f > .

and weight map:

0=1
.=1
f=1

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

a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
a(b(x)) → b(a(x))
f(b(x)) → b(f(x))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
.(.(x, y), z) → .(x, .(y, z))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))

(24) Obligation:

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

C(b(f(x0))) → C(f(a(x0)))
C(b(.(x0, x1))) → C(.(a(x0), x1))
C(b(b1(x0))) → C(b1(a(x0)))
C(b(b(x0))) → C(b(a(x0)))

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(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(b(b1(x0))) → C(b1(a(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(C(x1)) = 1 +
[1,1]
·x1

POL(b(x1)) =
/0\
\0/
 +
/10\
\10/
·x1

POL(f(x1)) =
/1\
\1/
 +
/10\
\10/
·x1

POL(a(x1)) =
/0\
\0/
 +
/10\
\11/
·x1

POL(.(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(b1(x1)) =
/1\
\0/
 +
/10\
\10/
·x1

POL(0) =
/1\
\1/

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

a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
a(b(x)) → b(a(x))
f(b(x)) → b(f(x))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
.(.(x, y), z) → .(x, .(y, z))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))

(26) Obligation:

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

C(b(f(x0))) → C(f(a(x0)))
C(b(.(x0, x1))) → C(.(a(x0), x1))
C(b(b(x0))) → C(b(a(x0)))

The TRS R consists of the following rules:

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(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.


C(b(f(x0))) → C(f(a(x0)))
C(b(.(x0, x1))) → C(.(a(x0), x1))
C(b(b(x0))) → C(b(a(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(C(x1)) = 0 +
[2,2]
·x1

POL(b(x1)) =
/2\
\1/
 +
/11\
\22/
·x1

POL(f(x1)) =
/2\
\2/
 +
/21\
\23/
·x1

POL(a(x1)) =
/0\
\2/
 +
/30\
\03/
·x1

POL(.(x1, x2)) =
/0\
\0/
 +
/10\
\01/
·x1 +
/00\
\00/
·x2

POL(b1(x1)) =
/0\
\1/
 +
/30\
\22/
·x1

POL(0) =
/0\
\2/

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

a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
a(b(x)) → b(a(x))
f(b(x)) → b(f(x))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
.(.(x, y), z) → .(x, .(y, z))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))

(28) Obligation:

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

.(.(x, y), z) → .(x, .(y, z))
a(f(x)) → f(a(x))
a(.(x, y)) → .(a(x), y)
a(b1(x)) → b1(a(x))
f(b(x)) → b(f(x))
.(b(x), y) → b(.(x, y))
b1(b(x)) → b(b(x))
a(f(.(0, x))) → b1(.(f(.(0, x)), .(0, f(x))))
a(f(0)) → b1(.(f(0), 0))
f(.(0, x)) → b(.(0, f(x)))
f(0) → b(0)
c(b(x)) → c(a(x))
a(b(x)) → b(a(x))

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

(29) PisEmptyProof (EQUIVALENT transformation)

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

(30) YES