Termination w.r.t. Q proof of EEG_IJCAR_12_rybalchenko-nonloop-popl08.ari

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

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 NonLoopProof (⇒, 2838 ms)

        ↳17 NO

(0) Obligation:

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

notZero(pos(s(x))) → true
notZero(neg(s(x))) → true
notZero(neg(0)) → false
notZero(pos(0)) → false
greaterZero(pos(s(x))) → true
greaterZero(pos(0)) → false
greaterZero(neg(x)) → false
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
minusT(0, y) → neg(y)
minusT(x, 0) → pos(x)
minusT(s(x), s(y)) → minusT(x, y)
plusNat(0, y) → y
plusNat(s(x), y) → plusNat(x, s(y))
negate(pos(x)) → neg(x)
negate(neg(x)) → pos(x)
minus(pos(x), pos(y)) → minusT(x, y)
minus(neg(x), neg(y)) → negate(minusT(x, y))
minus(pos(x), neg(y)) → pos(plusNat(x, y))
minus(neg(x), pos(y)) → neg(plusNat(x, y))
while(true, i, y) → while(and(notZero(y), greaterZero(i)), minus(i, y), y)

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:

MINUST(s(x), s(y)) → MINUST(x, y)
PLUSNAT(s(x), y) → PLUSNAT(x, s(y))
MINUS(pos(x), pos(y)) → MINUST(x, y)
MINUS(neg(x), neg(y)) → NEGATE(minusT(x, y))
MINUS(neg(x), neg(y)) → MINUST(x, y)
MINUS(pos(x), neg(y)) → PLUSNAT(x, y)
MINUS(neg(x), pos(y)) → PLUSNAT(x, y)
WHILE(true, i, y) → WHILE(and(notZero(y), greaterZero(i)), minus(i, y), y)
WHILE(true, i, y) → AND(notZero(y), greaterZero(i))
WHILE(true, i, y) → NOTZERO(y)
WHILE(true, i, y) → GREATERZERO(i)
WHILE(true, i, y) → MINUS(i, y)

The TRS R consists of the following rules:

notZero(pos(s(x))) → true
notZero(neg(s(x))) → true
notZero(neg(0)) → false
notZero(pos(0)) → false
greaterZero(pos(s(x))) → true
greaterZero(pos(0)) → false
greaterZero(neg(x)) → false
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
minusT(0, y) → neg(y)
minusT(x, 0) → pos(x)
minusT(s(x), s(y)) → minusT(x, y)
plusNat(0, y) → y
plusNat(s(x), y) → plusNat(x, s(y))
negate(pos(x)) → neg(x)
negate(neg(x)) → pos(x)
minus(pos(x), pos(y)) → minusT(x, y)
minus(neg(x), neg(y)) → negate(minusT(x, y))
minus(pos(x), neg(y)) → pos(plusNat(x, y))
minus(neg(x), pos(y)) → neg(plusNat(x, y))
while(true, i, y) → while(and(notZero(y), greaterZero(i)), minus(i, y), y)

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 3 SCCs with 9 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

PLUSNAT(s(x), y) → PLUSNAT(x, s(y))

The TRS R consists of the following rules:

notZero(pos(s(x))) → true
notZero(neg(s(x))) → true
notZero(neg(0)) → false
notZero(pos(0)) → false
greaterZero(pos(s(x))) → true
greaterZero(pos(0)) → false
greaterZero(neg(x)) → false
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
minusT(0, y) → neg(y)
minusT(x, 0) → pos(x)
minusT(s(x), s(y)) → minusT(x, y)
plusNat(0, y) → y
plusNat(s(x), y) → plusNat(x, s(y))
negate(pos(x)) → neg(x)
negate(neg(x)) → pos(x)
minus(pos(x), pos(y)) → minusT(x, y)
minus(neg(x), neg(y)) → negate(minusT(x, y))
minus(pos(x), neg(y)) → pos(plusNat(x, y))
minus(neg(x), pos(y)) → neg(plusNat(x, y))
while(true, i, y) → while(and(notZero(y), greaterZero(i)), minus(i, y), y)

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:

PLUSNAT(s(x), y) → PLUSNAT(x, s(y))

R is empty.
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:

PLUSNAT(s(x), y) → PLUSNAT(x, s(y))
The graph contains the following edges 1 > 1

(9) YES

(10) Obligation:

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

MINUST(s(x), s(y)) → MINUST(x, y)

The TRS R consists of the following rules:

notZero(pos(s(x))) → true
notZero(neg(s(x))) → true
notZero(neg(0)) → false
notZero(pos(0)) → false
greaterZero(pos(s(x))) → true
greaterZero(pos(0)) → false
greaterZero(neg(x)) → false
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
minusT(0, y) → neg(y)
minusT(x, 0) → pos(x)
minusT(s(x), s(y)) → minusT(x, y)
plusNat(0, y) → y
plusNat(s(x), y) → plusNat(x, s(y))
negate(pos(x)) → neg(x)
negate(neg(x)) → pos(x)
minus(pos(x), pos(y)) → minusT(x, y)
minus(neg(x), neg(y)) → negate(minusT(x, y))
minus(pos(x), neg(y)) → pos(plusNat(x, y))
minus(neg(x), pos(y)) → neg(plusNat(x, y))
while(true, i, y) → while(and(notZero(y), greaterZero(i)), minus(i, y), y)

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

(11) UsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

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

MINUST(s(x), s(y)) → MINUST(x, y)

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:

MINUST(s(x), s(y)) → MINUST(x, y)
The graph contains the following edges 1 > 1, 2 > 2

(14) YES

(15) Obligation:

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

WHILE(true, i, y) → WHILE(and(notZero(y), greaterZero(i)), minus(i, y), y)

The TRS R consists of the following rules:

notZero(pos(s(x))) → true
notZero(neg(s(x))) → true
notZero(neg(0)) → false
notZero(pos(0)) → false
greaterZero(pos(s(x))) → true
greaterZero(pos(0)) → false
greaterZero(neg(x)) → false
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
minusT(0, y) → neg(y)
minusT(x, 0) → pos(x)
minusT(s(x), s(y)) → minusT(x, y)
plusNat(0, y) → y
plusNat(s(x), y) → plusNat(x, s(y))
negate(pos(x)) → neg(x)
negate(neg(x)) → pos(x)
minus(pos(x), pos(y)) → minusT(x, y)
minus(neg(x), neg(y)) → negate(minusT(x, y))
minus(pos(x), neg(y)) → pos(plusNat(x, y))
minus(neg(x), pos(y)) → neg(plusNat(x, y))
while(true, i, y) → while(and(notZero(y), greaterZero(i)), minus(i, y), y)

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

(16) NonLoopProof (COMPLETE transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 1,
σ' = [ ], and μ' = [ ] on the rule
WHILE(true, pos(s(s(zr1))), neg(s(0)))[zr1 / s(zr1)]ⁿ[zr1 / 0] → WHILE(true, pos(s(s(s(zr1)))), neg(s(0)))[zr1 / s(zr1)]ⁿ[zr1 / 0]
This rule is correct for the QDP as the following derivation shows:

WHILE(true, pos(s(s(zr1))), neg(s(0)))[zr1 / s(zr1)]ⁿ[zr1 / 0] → WHILE(true, pos(s(s(s(zr1)))), neg(s(0)))[zr1 / s(zr1)]ⁿ[zr1 / 0]
    by Equivalency by Simplifying Mu with µ1: [zl1 / 0] µ2: [zr1 / 0]
    intermediate steps: Equiv Sµ (lhs) - Equiv DR (rhs) - Equiv DR (lhs) - Equiv DR (rhs) - Equiv DR (lhs) - Instantiate mu - Instantiate mu - Equiv DR (lhs) - Equiv DR (rhs) - Equiv DR (lhs) - Equiv IPS (rhs) - Equiv IPS (lhs)
    WHILE(true, pos(s(s(zl1))), neg(s(x0)))[zr1 / s(zr1), zl1 / s(zl1)]ⁿ[zr1 / x0, zl1 / 0] → WHILE(true, pos(s(s(s(zr1)))), neg(s(x0)))[zr1 / s(zr1), zl1 / s(zl1)]ⁿ[zr1 / x0, zl1 / 0]
        by Narrowing at position: [1,0]
        intermediate steps: Equiv IPS (rhs) - Equiv IPS (lhs) - Equiv IPS (rhs) - Equiv IPS (lhs) - Instantiation - Equiv DR (rhs) - Equiv DR (lhs) - Instantiation - Equiv DR (rhs) - Equiv DR (lhs) - Equiv IPS (rhs) - Equiv IPS (lhs)
        WHILE(true, pos(s(s(zs1))), neg(s(x0)))[zt1 / s(zt1), zs1 / s(zs1)]ⁿ[zt1 / x0, zs1 / y1] → WHILE(true, pos(plusNat(y1, s(s(s(zt1))))), neg(s(x0)))[zt1 / s(zt1), zs1 / s(zs1)]ⁿ[zt1 / x0, zs1 / y1]
            by Narrowing at position: [1,0]
            intermediate steps: Equiv IPS (rhs) - Equiv IPS (lhs) - Instantiate mu - Equiv IPS (rhs) - Equiv IPS (lhs) - Instantiate Sigma - Instantiation - Instantiation
            WHILE(true, pos(s(y0)), neg(s(x1)))[ ]ⁿ[ ] → WHILE(true, pos(plusNat(y0, s(s(x1)))), neg(s(x1)))[ ]ⁿ[ ]
                by Rewrite t with the rewrite sequence : [([0],and(true, true) -> true), ([1],minus(pos(x), neg(y)) -> pos(plusNat(x, y))), ([1,0],plusNat(s(x), y) -> plusNat(x, s(y)))]
                WHILE(true, pos(s(y0)), neg(s(x1)))[ ]ⁿ[ ] → WHILE(and(true, true), minus(pos(s(y0)), neg(s(x1))), neg(s(x1)))[ ]ⁿ[ ]
                    by Narrowing at position: [0,1]
                    intermediate steps: Instantiation - Instantiation
                    WHILE(true, x0, neg(s(y0)))[ ]ⁿ[ ] → WHILE(and(true, greaterZero(x0)), minus(x0, neg(s(y0))), neg(s(y0)))[ ]ⁿ[ ]
                        by Narrowing at position: [0,0]
                        intermediate steps: Instantiation - Instantiation
                        WHILE(true, i, y)[ ]ⁿ[ ] → WHILE(and(notZero(y), greaterZero(i)), minus(i, y), y)[ ]ⁿ[ ]
                            by Rule from TRS P

                        intermediate steps: Instantiation
                        notZero(neg(s(x)))[ ]ⁿ[ ] → true[ ]ⁿ[ ]
                            by Rule from TRS R

                    intermediate steps: Instantiation
                    greaterZero(pos(s(x)))[ ]ⁿ[ ] → true[ ]ⁿ[ ]
                        by Rule from TRS R

            intermediate steps: Equiv IPS (rhs) - Equiv IPS (lhs) - Equiv IPS (rhs) - Equiv IPS (lhs) - Equiv Sµ (rhs) - Instantiation - Instantiation - Equiv DR (rhs) - Equiv DR (lhs) - Instantiation - Equiv DR (rhs) - Equiv DR (lhs)
            plusNat(s(x), y)[x / s(x)]ⁿ[ ] → plusNat(x, s(y))[y / s(y)]ⁿ[ ]
                by PatternCreation I with delta: [ ], theta: [y / s(y)], sigma: [x / s(x)]
                plusNat(s(x), y)[ ]ⁿ[ ] → plusNat(x, s(y))[ ]ⁿ[ ]
                    by Rule from TRS R

        intermediate steps: Equiv IPS (rhs) - Equiv IPS (lhs) - Instantiate mu - Equiv IPS (rhs) - Equiv IPS (lhs) - Instantiate Sigma - Instantiation - Instantiation
        plusNat(0, y)[ ]ⁿ[ ] → y[ ]ⁿ[ ]
            by Rule from TRS R

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) UsableRulesProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPSizeChangeProof (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) UsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

(13) QDPSizeChangeProof (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) NonLoopProof (COMPLETE transformation)

(17) NO