YES Termination w.r.t. Q proof of CiME_04_list-sum-prod-bin-assoc-distr-app.ari

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

0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 QDP
        ↳6 UsableRulesProof (⇔, 0 ms)
        ↳7 QDP
        ↳8 QDPSizeChangeProof (⇔, 0 ms)
        ↳9 YES
    ↳10 QDP
        ↳11 UsableRulesProof (⇔, 0 ms)
        ↳12 QDP
        ↳13 MRRProof (⇔, 0 ms)
        ↳14 QDP
        ↳15 PisEmptyProof (⇔, 0 ms)
        ↳16 YES
    ↳17 QDP
        ↳18 UsableRulesProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 QDPSizeChangeProof (⇔, 0 ms)
        ↳21 YES
    ↳22 QDP
        ↳23 QDPSizeChangeProof (⇔, 0 ms)
        ↳24 YES
    ↳25 QDP
        ↳26 UsableRulesProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 QDPSizeChangeProof (⇔, 0 ms)
        ↳29 YES

(0) Obligation:

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

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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:

+1(0(x), 0(y)) → 01(+(x, y))
+1(0(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → 01(+(+(x, y), 1(#)))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
*1(0(x), y) → 01(*(x, y))
*1(0(x), y) → *1(x, y)
*1(1(x), y) → +1(0(*(x, y)), y)
*1(1(x), y) → 01(*(x, y))
*1(1(x), y) → *1(x, y)
*1(*(x, y), z) → *1(x, *(y, z))
*1(*(x, y), z) → *1(y, z)
*1(x, +(y, z)) → +1(*(x, y), *(x, z))
*1(x, +(y, z)) → *1(x, y)
*1(x, +(y, z)) → *1(x, z)
APP(cons(x, l1), l2) → APP(l1, l2)
SUM(nil) → 01(#)
SUM(cons(x, l)) → +1(x, sum(l))
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → +1(sum(l1), sum(l2))
SUM(app(l1, l2)) → SUM(l1)
SUM(app(l1, l2)) → SUM(l2)
PROD(cons(x, l)) → *1(x, prod(l))
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → *1(prod(l1), prod(l2))
PROD(app(l1, l2)) → PROD(l1)
PROD(app(l1, l2)) → PROD(l2)

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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

(4) Complex Obligation (AND)

(5) Obligation:

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

APP(cons(x, l1), l2) → APP(l1, l2)

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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:

APP(cons(x, l1), l2) → APP(l1, l2)

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:

  • APP(cons(x, l1), l2) → APP(l1, l2)
    The graph contains the following edges 1 > 1, 2 >= 2

(9) YES

(10) Obligation:

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

+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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

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

(12) Obligation:

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

+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

The TRS R consists of the following rules:

+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
0(#) → #

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

(13) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)

Strictly oriented rules of the TRS R:

+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
0(#) → #

Used ordering: Knuth-Bendix order [KBO] with precedence:
# > +2 > 11 > 01 > +^12

and weight map:

#=2
0_1=1
1_1=3
+_2=0
+^1_2=0

The variable weight is 1

(14) Obligation:

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

(15) PisEmptyProof (EQUIVALENT transformation)

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

(16) YES

(17) Obligation:

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

SUM(app(l1, l2)) → SUM(l1)
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → SUM(l2)

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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

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

(19) Obligation:

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

SUM(app(l1, l2)) → SUM(l1)
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → SUM(l2)

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

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

  • SUM(app(l1, l2)) → SUM(l1)
    The graph contains the following edges 1 > 1

  • SUM(cons(x, l)) → SUM(l)
    The graph contains the following edges 1 > 1

  • SUM(app(l1, l2)) → SUM(l2)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

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

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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

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

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

  • *1(0(x), y) → *1(x, y)
    The graph contains the following edges 1 > 1, 2 >= 2

  • *1(*(x, y), z) → *1(x, *(y, z))
    The graph contains the following edges 1 > 1

  • *1(*(x, y), z) → *1(y, z)
    The graph contains the following edges 1 > 1, 2 >= 2

  • *1(x, +(y, z)) → *1(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • *1(x, +(y, z)) → *1(x, z)
    The graph contains the following edges 1 >= 1, 2 > 2

(24) YES

(25) Obligation:

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

PROD(app(l1, l2)) → PROD(l1)
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → PROD(l2)

The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))

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

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

(27) Obligation:

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

PROD(app(l1, l2)) → PROD(l1)
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → PROD(l2)

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

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

  • PROD(app(l1, l2)) → PROD(l1)
    The graph contains the following edges 1 > 1

  • PROD(cons(x, l)) → PROD(l)
    The graph contains the following edges 1 > 1

  • PROD(app(l1, l2)) → PROD(l2)
    The graph contains the following edges 1 > 1

(29) YES