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

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

(7) YES

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

(9) 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

(10) YES

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

(12) NonLoopProof (EQUIVALENT 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:

intermediate steps: Equivalent (Simplify mu) - Equivalent (Domain Renaming) - Equivalent (Domain Renaming) - Instantiate mu - Instantiate mu - Equivalent (Domain Renaming) - Instantiation - Equivalent (Domain Renaming) - Equivalent (Remove Unused)
WHILE(true, pos(s(s(zl1))), neg(s(x1)))[zl1 / s(zl1), zr1 / s(zr1)]ⁿ[zl1 / 0, zr1 / x1] → WHILE(true, pos(s(s(s(zr1)))), neg(s(x1)))[zl1 / s(zl1), zr1 / s(zr1)]ⁿ[zl1 / 0, zr1 / x1]
    by Narrowing at position: [1,0]
        intermediate steps: Equivalent (Add Unused) - Equivalent (Add Unused) - Instantiation - Equivalent (Domain Renaming) - Instantiation - Equivalent (Domain Renaming) - Equivalent (Remove Unused)
        WHILE(true, pos(s(s(zs1))), neg(s(x1)))[zs1 / s(zs1), zt1 / s(zt1)]ⁿ[zs1 / y1, zt1 / x1] → WHILE(true, pos(plusNat(y1, s(s(s(zt1))))), neg(s(x1)))[zs1 / s(zs1), zt1 / s(zt1)]ⁿ[zs1 / y1, zt1 / x1]
            by Narrowing at position: [1,0]
                intermediate steps: Equivalent (Add Unused) - Instantiate mu - Equivalent (Add Unused) - Instantiate Sigma - Instantiation - Instantiation
                WHILE(true, pos(s(y0)), neg(s(x0)))[ ]ⁿ[ ] → WHILE(true, pos(plusNat(y0, s(s(x0)))), neg(s(x0)))[ ]ⁿ[ ]
                    by Rewrite t
                        WHILE(true, pos(s(y0)), neg(s(x0)))[ ]ⁿ[ ] → WHILE(and(true, true), minus(pos(s(y0)), neg(s(x0))), neg(s(x0)))[ ]ⁿ[ ]
                            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 OriginalRule from TRS P

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

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

                intermediate steps: Equivalent (Add Unused) - Equivalent (Add Unused) - Equivalent (Simplify mu) - Instantiation - Equivalent (Domain Renaming) - Instantiation - Equivalent (Domain Renaming)
                plusNat(s(x), y)[x / s(x)]ⁿ[ ] → plusNat(x, s(y))[y / s(y)]ⁿ[ ]
                    by PatternCreation I
                        plusNat(s(x), y)[ ]ⁿ[ ] → plusNat(x, s(y))[ ]ⁿ[ ]
                            by OriginalRule from TRS R

        intermediate steps: Equivalent (Add Unused) - Instantiate mu - Equivalent (Add Unused) - Instantiate Sigma - Instantiation - Instantiation
        plusNat(0, y)[ ]ⁿ[ ] → y[ ]ⁿ[ ]
            by OriginalRule from TRS R

(13) NO