Termination w.r.t. Q proof of /tmp/tmpjdOVb6/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 QDP

  ↳10 QDP

  ↳11 QDP

  ↳12 QDP

  ↳13 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 {f0, f1, f2, d, c}

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

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

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

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

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