Termination w.r.t. Q proof of /tmp/tmp5ZEeH7/aprove02.trs

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

0 QTRS

↳1 AAECC Innermost (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 AND

  ↳7 QDP

  ↳8 QDP

    ↳9 QDPOrderProof (⇔)

    ↳10 QDP

    ↳11 PisEmptyProof (⇔)

    ↳12 TRUE

  ↳13 QDP

    ↳14 QDPOrderProof (⇔)

    ↳15 QDP

    ↳16 PisEmptyProof (⇔)

    ↳17 TRUE

  ↳18 QDP

    ↳19 QDPOrderProof (⇔)

    ↳20 QDP

    ↳21 PisEmptyProof (⇔)

    ↳22 TRUE

  ↳23 QDP

    ↳24 QDPOrderProof (⇔)

    ↳25 QDP

    ↳26 PisEmptyProof (⇔)

    ↳27 TRUE

  ↳28 QDP

  ↳29 QDP

(0) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)

The TRS R 2 is

f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The signature Sigma is {c, f2, d, f0, f1}

(2) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))
PLUS(x, y) → ISZERO(x)
PLUS(x, y) → INC(y)
IFPLUS(true, x, y) → P(y)
IFPLUS(false, x, y) → PLUS(p(x), y)
IFPLUS(false, x, y) → P(x)
TIMES(x, y) → TIMESITER(0, x, y, 0)
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z)
TIMESITER(i, x, y, z) → GE(i, x)
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
IFTIMES(false, i, x, y, z) → INC(i)
IFTIMES(false, i, x, y, z) → PLUS(z, y)
ISZERO(s(s(x))) → ISZERO(s(x))
INC(s(x)) → INC(x)
P(s(s(x))) → P(s(x))
GE(s(x), s(y)) → GE(x, y)
F0(0, y, x) → F1(x, y, x)
F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(8) Obligation:

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

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(s(x), s(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
GE(x1, x2) = GE(x2)
s(x1) = s(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

s₁: [1]
GE₁: [1]

The following usable rules [FROCOS05] were oriented: none

(10) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(11) PisEmptyProof (EQUIVALENT transformation)

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

(12) TRUE

(13) Obligation:

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

P(s(s(x))) → P(s(x))

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P(s(s(x))) → P(s(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:

P₁ > s₁

Status:

P₁: [1]
s₁: [1]

The following usable rules [FROCOS05] were oriented: none

(15) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(16) PisEmptyProof (EQUIVALENT transformation)

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

(17) TRUE

(18) Obligation:

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

INC(s(x)) → INC(x)

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INC(s(x)) → INC(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
INC(x1) = x1
s(x1) = s(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

s₁: [1]

The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(21) PisEmptyProof (EQUIVALENT transformation)

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

(22) TRUE

(23) Obligation:

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

ISZERO(s(s(x))) → ISZERO(s(x))

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISZERO(s(s(x))) → ISZERO(s(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic path order with status [LPO].
Quasi-Precedence:

ISZERO₁ > s₁

Status:

ISZERO₁: [1]
s₁: [1]

The following usable rules [FROCOS05] were oriented: none

(25) Obligation:

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

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(26) PisEmptyProof (EQUIVALENT transformation)

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

(27) TRUE

(28) Obligation:

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

IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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

(29) Obligation:

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

IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z)

The TRS R consists of the following rules:

plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c

The set Q consists of the following terms:

plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)

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