Termination w.r.t. Q proof of /tmp/tmpbeWlp1/wiehe07.trs

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 UsableRulesProof (⇔)

    ↳7 QDP

    ↳8 QDPSizeChangeProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 QDPOrderProof (⇔)

    ↳14 QDP

    ↳15 QDPSizeChangeProof (⇔)

    ↳16 TRUE

  ↳17 QDP

    ↳18 QDPOrderProof (⇔)

    ↳19 QDP

    ↳20 Narrowing (⇔)

    ↳21 QDP

    ↳22 Narrowing (⇔)

    ↳23 QDP

    ↳24 DependencyGraphProof (⇔)

    ↳25 QDP

    ↳26 Narrowing (⇔)

    ↳27 QDP

    ↳28 DependencyGraphProof (⇔)

    ↳29 QDP

    ↳30 QDPOrderProof (⇔)

    ↳31 QDP

    ↳32 UsableRulesProof (⇔)

    ↳33 QDP

    ↳34 QDPSizeChangeProof (⇔)

    ↳35 TRUE

(0) Obligation:

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

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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:

TIMES(x, plus(y, s(z))) → PLUS(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0)))
TIMES(x, plus(y, s(z))) → PLUS(y, times(s(z), 0))
TIMES(x, plus(y, s(z))) → TIMES(s(z), 0)
TIMES(x, plus(y, s(z))) → TIMES(x, s(z))
TIMES(x, s(y)) → PLUS(times(x, y), x)
TIMES(x, s(y)) → TIMES(x, y)
PLUS(s(x), s(y)) → PLUS(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
PLUS(s(x), s(y)) → IF(gt(x, y), x, y)
PLUS(s(x), s(y)) → GT(x, y)
PLUS(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
PLUS(s(x), s(y)) → NOT(gt(x, y))
PLUS(s(x), s(y)) → ID(x)
PLUS(s(x), s(y)) → ID(y)
PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))
PLUS(s(x), x) → IF(gt(x, x), id(x), id(x))
PLUS(s(x), x) → GT(x, x)
PLUS(s(x), x) → ID(x)
PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))
PLUS(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
PLUS(id(x), s(y)) → GT(s(y), y)
NOT(x) → IF(x, false, true)
GT(s(x), s(y)) → GT(x, y)

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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 16 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

GT(s(x), s(y)) → GT(x, y)

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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:

GT(s(x), s(y)) → GT(x, 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:

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

(9) TRUE

(10) Obligation:

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

PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))
PLUS(s(x), s(y)) → PLUS(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PLUS(s(x), s(y)) → PLUS(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(PLUS(x₁, x₂)) = 0A + 1A · x₁ + 0A · x₂

POL(s(x₁)) = 5A + 2A · x₁

POL(if(x₁, x₂, x₃)) = -I + 0A · x₁ + 1A · x₂ + 0A · x₃

POL(gt(x₁, x₂)) = 0A + 0A · x₁ + 0A · x₂

POL(id(x₁)) = 4A + 0A · x₁

POL(not(x₁)) = 5A + 0A · x₁

POL(true) = 5A

POL(false) = 0A

POL(zero) = 0A

The following usable rules [FROCOS05] were oriented:

id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

(12) Obligation:

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

PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))
PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(PLUS(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(s(x₁)) =
/ 1 \

\ 1 /

+
/ 1 1 \

\ 1 1 /

· x₁

POL(if(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 1 /

· x₂ +
/ 1 0 \

\ 0 1 /

· x₃

POL(gt(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(id(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(true) =
/ 1 \

\ 0 /

POL(false) =
/ 0 \

\ 1 /

POL(zero) =
/ 0 \

\ 0 /

The following usable rules [FROCOS05] were oriented:

id(x) → x
if(true, x, y) → x
if(false, x, y) → y

(14) Obligation:

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

PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(15) 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(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))
The graph contains the following edges 1 > 1

(16) TRUE

(17) Obligation:

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

TIMES(x, plus(y, s(z))) → TIMES(x, s(z))
TIMES(x, s(y)) → TIMES(x, y)
TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0)))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

TIMES(x, plus(y, s(z))) → TIMES(x, s(z))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(TIMES(x₁, x₂)) = 0A + -I · x₁ + 0A · x₂

POL(plus(x₁, x₂)) = 1A + 1A · x₁ + 1A · x₂

POL(s(x₁)) = -I + 0A · x₁

POL(times(x₁, x₂)) = 0A + -I · x₁ + 0A · x₂

POL(0) = 0A

POL(if(x₁, x₂, x₃)) = 0A + -I · x₁ + 0A · x₂ + 0A · x₃

POL(gt(x₁, x₂)) = -I + 0A · x₁ + -I · x₂

POL(not(x₁)) = 2A + 0A · x₁

POL(id(x₁)) = -I + 0A · x₁

POL(zero) = 0A

POL(true) = 0A

POL(false) = 0A

The following usable rules [FROCOS05] were oriented:

times(x, 0) → 0
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y

(19) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0)))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(20) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0))) at position [1] we obtained the following new rules [LPAR04]:

TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))
TIMES(y0, plus(zero, s(y2))) → TIMES(y0, times(s(y2), 0))
TIMES(y0, plus(y1, s(y2))) → TIMES(y0, plus(y1, 0))

(21) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))
TIMES(y0, plus(zero, s(y2))) → TIMES(y0, times(s(y2), 0))
TIMES(y0, plus(y1, s(y2))) → TIMES(y0, plus(y1, 0))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(22) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMES(y0, plus(zero, s(y2))) → TIMES(y0, times(s(y2), 0)) at position [1] we obtained the following new rules [LPAR04]:

TIMES(y0, plus(zero, s(y1))) → TIMES(y0, 0)

(23) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))
TIMES(y0, plus(y1, s(y2))) → TIMES(y0, plus(y1, 0))
TIMES(y0, plus(zero, s(y1))) → TIMES(y0, 0)

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(24) DependencyGraphProof (EQUIVALENT transformation)

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

(25) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))
TIMES(y0, plus(y1, s(y2))) → TIMES(y0, plus(y1, 0))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(26) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMES(y0, plus(y1, s(y2))) → TIMES(y0, plus(y1, 0)) at position [1] we obtained the following new rules [LPAR04]:

TIMES(y0, plus(s(0), s(y2))) → TIMES(y0, plus(if(gt(0, 0), id(0), id(0)), s(0)))
TIMES(y0, plus(zero, s(y2))) → TIMES(y0, 0)

(27) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))
TIMES(y0, plus(s(0), s(y2))) → TIMES(y0, plus(if(gt(0, 0), id(0), id(0)), s(0)))
TIMES(y0, plus(zero, s(y2))) → TIMES(y0, 0)

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)
TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

TIMES(y0, plus(s(times(s(y2), 0)), s(y2))) → TIMES(y0, plus(if(gt(times(s(y2), 0), times(s(y2), 0)), id(times(s(y2), 0)), id(times(s(y2), 0))), s(times(s(y2), 0))))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(TIMES(x₁, x₂)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₁ +
/ -I -I 0A \

| -I -I -I |

\ -I -I 0A /

· x₂

POL(s(x₁)) =
/ 0A \

| 1A |

\ -I /

+
/ 0A 0A -I \

| -I -I 0A |

\ -I -I 0A /

· x₁

POL(plus(x₁, x₂)) =
/ -I \

| 0A |

\ -I /

+
/ 0A 0A 1A \

| 0A 0A 0A |

\ 0A 0A -I /

· x₁ +
/ 0A -I 1A \

| 0A 0A 0A |

\ 0A -I 0A /

· x₂

POL(times(x₁, x₂)) =
/ 0A \

| 0A |

\ -I /

+
/ -I -I -I \

| -I -I -I |

\ -I -I -I /

· x₁ +
/ 0A -I -I \

| 0A -I 0A |

\ -I -I -I /

· x₂

POL(0) =
/ 0A \

| -I |

\ -I /

POL(if(x₁, x₂, x₃)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A 0A |

\ -I -I -I /

· x₁ +
/ 0A -I -I \

| 0A 0A 0A |

\ -I -I 0A /

· x₂ +
/ 0A -I 0A \

| 0A 0A -I |

\ -I -I 0A /

· x₃

POL(gt(x₁, x₂)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I 0A \

| 0A -I 0A |

\ 0A 0A 0A /

· x₁ +
/ 0A 0A -I \

| 0A -I -I |

\ 0A 0A -I /

· x₂

POL(id(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(not(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(zero) =
/ 0A \

| 0A |

\ -I /

POL(true) =
/ 0A \

| -I |

\ -I /

POL(false) =
/ 0A \

| 0A |

\ -I /

The following usable rules [FROCOS05] were oriented:

times(x, 0) → 0
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

(31) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)

The TRS R consists of the following rules:

times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)

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

(32) UsableRulesProof (EQUIVALENT transformation)

(33) Obligation:

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

TIMES(x, s(y)) → TIMES(x, y)

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

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

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

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

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) QDPOrderProof (EQUIVALENT transformation)

(14) Obligation:

(15) QDPSizeChangeProof (EQUIVALENT transformation)

(16) TRUE

(17) Obligation:

(18) QDPOrderProof (EQUIVALENT transformation)

(19) Obligation:

(20) Narrowing (EQUIVALENT transformation)

(21) Obligation:

(22) Narrowing (EQUIVALENT transformation)

(23) Obligation:

(24) DependencyGraphProof (EQUIVALENT transformation)

(25) Obligation:

(26) Narrowing (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) Obligation:

(30) QDPOrderProof (EQUIVALENT transformation)

(31) Obligation:

(32) UsableRulesProof (EQUIVALENT transformation)

(33) Obligation:

(34) QDPSizeChangeProof (EQUIVALENT transformation)

(35) TRUE