Termination w.r.t. Q proof of /tmp/tmpexsMuJ/list-sum-prod-assoc.xml

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

        ↳7 QDP

        ↳8 PisEmptyProof (⇔)

        ↳9 TRUE

    ↳10 QDP

        ↳11 QDPOrderProof (⇔)

        ↳12 QDP

        ↳13 PisEmptyProof (⇔)

        ↳14 TRUE

    ↳15 QDP

        ↳16 QDPOrderProof (⇔)

        ↳17 QDP

        ↳18 QDPOrderProof (⇔)

        ↳19 QDP

        ↳20 QDPOrderProof (⇔)

        ↳21 QDP

        ↳22 PisEmptyProof (⇔)

        ↳23 TRUE

    ↳24 QDP

        ↳25 QDPOrderProof (⇔)

        ↳26 QDP

        ↳27 PisEmptyProof (⇔)

        ↳28 TRUE

(0) Obligation:

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

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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:

+¹(s(x), s(y)) → +¹(x, y)
+¹(+(x, y), z) → +¹(x, +(y, z))
+¹(+(x, y), z) → +¹(y, z)
*¹(s(x), s(y)) → +¹(*(x, y), +(x, y))
*¹(s(x), s(y)) → *¹(x, y)
*¹(s(x), s(y)) → +¹(x, y)
*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(y, z)
SUM(cons(x, l)) → +¹(x, sum(l))
SUM(cons(x, l)) → SUM(l)
PROD(cons(x, l)) → *¹(x, prod(l))
PROD(cons(x, l)) → PROD(l)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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 4 SCCs with 4 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

+¹(+(x, y), z) → +¹(x, +(y, z))
+¹(s(x), s(y)) → +¹(x, y)
+¹(+(x, y), z) → +¹(y, z)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(+(x, y), z) → +¹(x, +(y, z))
+¹(s(x), s(y)) → +¹(x, y)
+¹(+(x, y), z) → +¹(y, z)

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

POL(+(x₁, x₂)) = 1 + x₁ + x₂
POL(+¹(x₁, x₂)) = x₁
POL(0) = 0
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(8) PisEmptyProof (EQUIVALENT transformation)

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

(9) TRUE

(10) Obligation:

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

SUM(cons(x, l)) → SUM(l)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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.

SUM(cons(x, l)) → SUM(l)

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

POL(SUM(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

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

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(s(x), s(y)) → *¹(x, y)
*¹(*(x, y), z) → *¹(y, z)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(s(x), s(y)) → *¹(x, y)

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

POL(*(x₁, x₂)) = x₁ + x₂
POL(*¹(x₁, x₂)) = x₁
POL(+(x₁, x₂)) = 0
POL(0) = 0
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(17) Obligation:

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

*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(y, z)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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.

*¹(*(x, y), z) → *¹(y, z)

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

POL(*(x₁, x₂)) = 1 + x₁ + x₂
POL(*¹(x₁, x₂)) = x₁ + x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(0) = 0
POL(s(x₁)) = 0

The following usable rules [FROCOS05] were oriented:

*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))

(19) Obligation:

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

*¹(*(x, y), z) → *¹(x, *(y, z))

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(*(x, y), z) → *¹(x, *(y, z))

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

POL(*(x₁, x₂)) = 1 + x₁
POL(*¹(x₁, x₂)) = x₁
POL(+(x₁, x₂)) = 0
POL(0) = 1
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(21) Obligation:

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

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(22) PisEmptyProof (EQUIVALENT transformation)

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

(23) TRUE

(24) Obligation:

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

PROD(cons(x, l)) → PROD(l)

The TRS R consists of the following rules:

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROD(cons(x, l)) → PROD(l)

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

POL(PROD(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂

The following usable rules [FROCOS05] were oriented: none

(26) Obligation:

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

+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))

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

(27) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) PisEmptyProof (EQUIVALENT transformation)

(9) TRUE

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) PisEmptyProof (EQUIVALENT transformation)

(14) TRUE

(15) Obligation:

(16) QDPOrderProof (EQUIVALENT transformation)

(17) Obligation:

(18) QDPOrderProof (EQUIVALENT transformation)

(19) Obligation:

(20) QDPOrderProof (EQUIVALENT transformation)

(21) Obligation:

(22) PisEmptyProof (EQUIVALENT transformation)

(23) TRUE

(24) Obligation:

(25) QDPOrderProof (EQUIVALENT transformation)

(26) Obligation:

(27) PisEmptyProof (EQUIVALENT transformation)

(28) TRUE