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

(0) Obligation:

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

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

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

inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
inc(s(x)) → s(inc(x))
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))

The TRS R 2 is

f → g
f → h

The signature Sigma is {f, g, h}

(2) Obligation:

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

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

INC(s(x)) → INC(x)
PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
PLUS(x, y) → EQ(x, 0)
PLUS(x, y) → MINUS(x, s(0))
PLUS(x, y) → INC(x)
IFPLUS(false, x, y, z) → PLUS(x, z)
MINUS(s(x), s(y)) → MINUS(x, y)
EQ(s(x), s(y)) → EQ(x, y)
TIMES(x, y) → TIMESITER(x, y, 0)
TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
TIMESITER(x, y, z) → EQ(x, 0)
TIMESITER(x, y, z) → MINUS(x, s(0))
TIMESITER(x, y, z) → PLUS(y, z)
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

(11) Obligation:

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

EQ(s(x), s(y)) → EQ(x, y)

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

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

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

(13) TRUE

(14) Obligation:

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

MINUS(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

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

MINUS(s(x), s(y)) → MINUS(x, y)

R is empty.
The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

(18) Obligation:

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

MINUS(s(x), s(y)) → MINUS(x, y)

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

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

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

(20) TRUE

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

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

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

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

R is empty.
The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

(25) Obligation:

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

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

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

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

• INC(s(x)) → INC(x)
  The graph contains the following edges 1 > 1

(27) TRUE

(28) Obligation:

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

PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

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

PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

(32) Obligation:

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

PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x)) at position [0] we obtained the following new rules [LPAR04]:

PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
PLUS(0, y1) → IFPLUS(true, minus(0, s(0)), 0, inc(0))

(34) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
PLUS(0, y1) → IFPLUS(true, minus(0, s(0)), 0, inc(0))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(36) Obligation:

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

PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(37) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(38) Obligation:

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

PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

(40) Obligation:

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

PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)

The TRS R consists of the following rules:

minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(41) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0))) at position [3] we obtained the following new rules [LPAR04]:

PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))

(42) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))

The TRS R consists of the following rules:

minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(43) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0))) at position [1] we obtained the following new rules [LPAR04]:

PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))

(44) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))

The TRS R consists of the following rules:

minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(45) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(46) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))

The TRS R consists of the following rules:

inc(0) → s(0)
minus(x, x) → 0
minus(0, x) → 0
minus(x, 0) → x
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(47) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0))) at position [1] we obtained the following new rules [LPAR04]:

PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))

(48) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))

The TRS R consists of the following rules:

inc(0) → s(0)
minus(x, x) → 0
minus(0, x) → 0
minus(x, 0) → x
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(49) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(50) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

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

(51) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)

(52) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(53) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0))) at position [3,0] we obtained the following new rules [LPAR04]:

PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))

(54) Obligation:

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

IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(55) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFPLUS(false, x, y, z) → PLUS(x, z) we obtained the following new rules [LPAR04]:

IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))

(56) Obligation:

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

PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(58) Obligation:

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

IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(59) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0))) we obtained the following new rules [LPAR04]:

PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))

(60) Obligation:

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

IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(61) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0))) we obtained the following new rules [LPAR04]:

PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))

(62) Obligation:

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

IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(63) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0)) we obtained the following new rules [LPAR04]:

IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))

(64) Obligation:

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

PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(65) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(66) Obligation:

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

IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(67) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0))) at position [] we obtained the following new rules [LPAR04]:

PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
PLUS(s(0), s(y1)) → IFPLUS(false, 0, s(0), s(s(0)))

(68) Obligation:

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

IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))
PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
PLUS(s(0), s(y1)) → IFPLUS(false, 0, s(0), s(s(0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(69) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(70) Obligation:

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

PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(71) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1)) we obtained the following new rules [LPAR04]:

IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))

(72) Obligation:

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

PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

(73) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0)))) we obtained the following new rules [LPAR04]:

PLUS(s(s(x0)), s(s(z1))) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))

(74) Obligation:

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

IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)

The set Q consists of the following terms:

inc(s(x0))
inc(0)

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

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

• PLUS(s(s(x0)), s(s(z1))) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
  The graph contains the following edges 1 > 2, 1 >= 3

• IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))
  The graph contains the following edges 2 >= 1, 3 > 1, 4 >= 2

(76) TRUE

(77) Obligation:

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

TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(78) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(79) Obligation:

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

TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

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

(80) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f

(81) Obligation:

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

TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(82) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) at position [0] we obtained the following new rules [LPAR04]:

TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
TIMESITER(0, y1, y2) → IFTIMES(true, minus(0, s(0)), y1, y2, plus(y1, y2))

(83) Obligation:

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

IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
TIMESITER(0, y1, y2) → IFTIMES(true, minus(0, s(0)), y1, y2, plus(y1, y2))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(84) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(85) Obligation:

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

TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(86) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2)) at position [1] we obtained the following new rules [LPAR04]:

TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2))
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))

(87) Obligation:

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

IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2))
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(88) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2)) at position [1] we obtained the following new rules [LPAR04]:

TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))

(89) Obligation:

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

IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))
TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(90) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2)) at position [4] we obtained the following new rules [LPAR04]:

TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))

(91) Obligation:

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

IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(92) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2)) at position [4] we obtained the following new rules [LPAR04]:

TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))

(93) Obligation:

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

IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(94) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u) we obtained the following new rules [LPAR04]:

IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)

(95) Obligation:

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

TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

(96) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(97) Obligation:

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

TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)

The TRS R consists of the following rules:

eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x

The set Q consists of the following terms:

inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)

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

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

• TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
  The graph contains the following edges 1 > 2, 2 >= 3, 3 >= 4

• IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
  The graph contains the following edges 2 >= 1, 3 >= 2, 5 >= 3

• IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)
  The graph contains the following edges 2 >= 1, 3 >= 2, 5 >= 3

(99) TRUE