YES
Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51

- : unit = ()
- : unit = ()
X : variable_set = <variable set>

F : signature = <signature>
R : HTRS = { union(empty,X) -> X,
             union(empty,X) -> X,
             0(z) -> z,
             U11(tt,X,Y) -> U12(tt,X,Y),
             U12(tt,X,Y) -> 0(mult(X,Y)),
             U21(tt,X,Y) -> U22(tt,X,Y),
             U22(tt,X,Y) -> plus(0(mult(X,Y)),Y),
             U31(tt,X,Y) -> U32(tt,X,Y),
             U32(tt,X,Y) -> 0(plus(X,Y)),
             U41(tt,X,Y) -> U42(tt,X,Y),
             U42(tt,X,Y) -> 1(plus(X,Y)),
             U51(tt,X,Y) -> U52(tt,X,Y),
             U52(tt,X,Y) -> 0(plus(1(z),X,Y)),
             U61(tt,A,B) -> U62(tt,A,B),
             U62(tt,A,B) -> mult(prod(A),prod(B)),
             U71(tt,A,B) -> U72(tt,A,B),
             U72(tt,A,B) -> plus(sum(A),sum(B)),
             mult(z,X) -> z,
             mult(0(X),Y) -> U11(tt,X,Y),
             mult(1(X),Y) -> U21(tt,X,Y),
             plus(z,X) -> X,
             plus(0(X),0(Y)) -> U31(tt,X,Y),
             plus(0(X),1(Y)) -> U41(tt,X,Y),
             plus(1(X),1(Y)) -> U51(tt,X,Y),
             prod(empty) -> 1(z),
             prod(singl(X)) -> X,
             prod(union(A,B)) -> U61(tt,A,B),
             sum(empty) -> 0(z),
             sum(singl(X)) -> X,
             sum(union(A,B)) -> U71(tt,A,B) } (30 rules)
Termination now uses minimal decomposition
- : unit = ()
Entering the termination expert for modules. Verbose level = 0
Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ 0(z) -> z } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ plus(1(V_2),1(V_3)) -> U51(tt,V_2,V_3),
  plus(1(V_3),0(V_2)) -> U41(tt,V_2,V_3),
  plus(0(V_2),0(V_3)) -> U31(tt,V_2,V_3),
  plus(z,V_2) -> V_2,
  U32(tt,V_2,V_3) -> 0(plus(V_2,V_3)),
  U31(tt,V_2,V_3) -> U32(tt,V_2,V_3),
  U42(tt,V_2,V_3) -> 1(plus(V_2,V_3)),
  U41(tt,V_2,V_3) -> U42(tt,V_2,V_3),
  U52(tt,V_2,V_3) -> 0(plus(1(z),V_2,V_3)),
  U51(tt,V_2,V_3) -> U52(tt,V_2,V_3) } (10 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(26 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(26 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[z] = 0; 
[tt] = 0; 
[1](X0) = X0 + 1; 
[0](X0) = X0; 
[U51](X0,X1,X2) = X2 + X1 + 1; 
[U52](X0,X1,X2) = X2 + X1 + 1; 
[U41](X0,X1,X2) = X2 + X1 + 1; 
[U42](X0,X1,X2) = X2 + X1 + 1; 
[U31](X0,X1,X2) = X2 + X1; 
[U32](X0,X1,X2) = X2 + X1; 
[plus](X0,X1) = X1 + X0; 
['U51`](X0,X1,X2) = X2 + X1 + 1; 
['U52`](X0,X1,X2) = X2 + X1 + 1; 
['U41`](X0,X1,X2) = X2 + X1; 
['U42`](X0,X1,X2) = X2 + X1; 
['U31`](X0,X1,X2) = X2 + X1; 
['U32`](X0,X1,X2) = X2 + X1; 

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(17 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[z] = 0; 
[tt] = 2; 
[1](X0) = X0 + 2; 
[0](X0) = X0 + 2; 
[U51](X0,X1,X2) = X2 + X1 + 2*X0; 
[U52](X0,X1,X2) = X2 + X1 + 2*X0; 
[U41](X0,X1,X2) = X2 + X1 + X0; 
[U42](X0,X1,X2) = X2 + X1 + X0; 
[U31](X0,X1,X2) = X2 + X1 + X0; 
[U32](X0,X1,X2) = X2 + X1 + X0; 
[plus](X0,X1) = X1 + X0; 
['U31`](X0,X1,X2) = X2 + X1 + X0; 
['U32`](X0,X1,X2) = X2 + X1 + 1; 


Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ union(empty,V_2) -> V_2,
  union(empty,V_2) -> V_2 } (2 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ sum(empty) -> 0(z),
  sum(singl(V_2)) -> V_2,
  sum(union(V_0,V_1)) -> U71(tt,V_0,V_1),
  U72(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)),
  U71(tt,V_0,V_1) -> U72(tt,V_0,V_1) } (5 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(21 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[empty] = 0; 
[union](X0,X1) = X1 + X0 + 2; 
[z] = 0; 
[tt] = 0; 
[1](X0) = 0; 
[singl](X0) = X0; 
[0](X0) = 0; 
[U51](X0,X1,X2) = 0; 
[U71](X0,X1,X2) = X2 + X1; 
[U52](X0,X1,X2) = 0; 
[U72](X0,X1,X2) = X2 + X1; 
[U41](X0,X1,X2) = 0; 
[sum](X0) = X0; 
[U42](X0,X1,X2) = 0; 
[U31](X0,X1,X2) = 0; 
[U32](X0,X1,X2) = 0; 
[plus](X0,X1) = X1 + X0; 
['U71`](X0,X1,X2) = 2*X2 + 2*X1 + 2; 
['U72`](X0,X1,X2) = 2*X2 + 2*X1 + 1; 
['sum`](X0) = 2*X0; 


Checking module:
{ mult(1(V_2),V_3) -> U21(tt,V_2,V_3),
  mult(0(V_2),V_3) -> U11(tt,V_2,V_3),
  mult(z,V_2) -> z,
  U12(tt,V_2,V_3) -> 0(mult(V_2,V_3)),
  U11(tt,V_2,V_3) -> U12(tt,V_2,V_3),
  U22(tt,V_2,V_3) -> plus(0(mult(V_2,V_3)),V_3),
  U21(tt,V_2,V_3) -> U22(tt,V_2,V_3) } (7 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(29 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(29 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[z] = 0; 
[tt] = 0; 
[1](X0) = X0 + 1; 
[0](X0) = X0; 
[U51](X0,X1,X2) = X2 + X1 + 1; 
[U21](X0,X1,X2) = X2*X1 + 2*X2 + X1; 
[U52](X0,X1,X2) = X2 + X1 + 1; 
[U22](X0,X1,X2) = X2*X1 + 2*X2 + X1; 
[U41](X0,X1,X2) = X2 + X1 + 1; 
[U11](X0,X1,X2) = X2*X1 + X2 + X1; 
[U42](X0,X1,X2) = X2 + X1 + 1; 
[U12](X0,X1,X2) = X2*X1 + X2 + X1; 
[U31](X0,X1,X2) = X2 + X1; 
[mult](X0,X1) = X1*X0 + X1 + X0; 
[U32](X0,X1,X2) = X2 + X1; 
[plus](X0,X1) = X1 + X0; 
['U21`](X0,X1,X2) = X2*X1 + X2 + X1; 
['U22`](X0,X1,X2) = X2*X1 + X2 + X1; 
['U11`](X0,X1,X2) = X2*X1 + X2 + X1; 
['U12`](X0,X1,X2) = X2*X1 + X2 + X1; 

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(24 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(24 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[z] = 0; 
[tt] = 0; 
[1](X0) = X0 + 1; 
[0](X0) = X0 + 1; 
[U51](X0,X1,X2) = X2 + X1 + 2; 
[U21](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; 
[U52](X0,X1,X2) = X2 + X1 + 2; 
[U22](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; 
[U41](X0,X1,X2) = X2 + X1 + 1; 
[U11](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
[U42](X0,X1,X2) = X2 + X1 + 1; 
[U12](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
[U31](X0,X1,X2) = X2 + X1 + 1; 
[mult](X0,X1) = X1*X0 + X1 + X0; 
[U32](X0,X1,X2) = X2 + X1 + 1; 
[plus](X0,X1) = X1 + X0; 
['U11`](X0,X1,X2) = X2*X1 + X2 + X1; 
['U12`](X0,X1,X2) = X2*X1 + X2 + X1; 

The dependency graph is
(3 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(20 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[z] = 1; 
[tt] = 1; 
[1](X0) = 1; 
[0](X0) = 1; 
[U51](X0,X1,X2) = 1; 
[U21](X0,X1,X2) = X2; 
[U52](X0,X1,X2) = 1; 
[U22](X0,X1,X2) = X2; 
[U41](X0,X1,X2) = 1; 
[U11](X0,X1,X2) = X0; 
[U42](X0,X1,X2) = 1; 
[U12](X0,X1,X2) = X0; 
[U31](X0,X1,X2) = X0; 
[mult](X0,X1) = X1 + X0 + 1; 
[U32](X0,X1,X2) = X0; 
[plus](X0,X1) = X1*X0; 


Checking module:
{ prod(empty) -> 1(z),
  prod(singl(V_2)) -> V_2,
  prod(union(V_0,V_1)) -> U61(tt,V_0,V_1),
  U62(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)),
  U61(tt,V_0,V_1) -> U62(tt,V_0,V_1) } (5 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(28 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[empty] = 1; 
[union](X0,X1) = X1 + X0 + 2; 
[z] = 1; 
[tt] = 1; 
[1](X0) = 1; 
[singl](X0) = X0; 
[0](X0) = 1; 
[U51](X0,X1,X2) = 1; 
[U21](X0,X1,X2) = X2; 
[U61](X0,X1,X2) = X2 + X1; 
[U52](X0,X1,X2) = X0; 
[U22](X0,X1,X2) = X2; 
[U62](X0,X1,X2) = X2 + X1; 
[U41](X0,X1,X2) = X0; 
[U11](X0,X1,X2) = X0; 
[prod](X0) = X0; 
[U42](X0,X1,X2) = X0; 
[U12](X0,X1,X2) = X0; 
[U31](X0,X1,X2) = X0; 
[mult](X0,X1) = X1 + X0; 
[U32](X0,X1,X2) = X0; 
[plus](X0,X1) = X1*X0; 
['U61`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; 
['U62`](X0,X1,X2) = 2*X2 + 2*X1 + X0; 
['prod`](X0) = 2*X0; 


Modular termination proof found.
- : unit = ()
The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { 0(z) -> z } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { plus(1(V_2),1(V_3)) -> U51(tt,V_2,V_3),
    plus(1(V_3),0(V_2)) -> U41(tt,V_2,V_3),
    plus(0(V_2),0(V_3)) -> U31(tt,V_2,V_3),
    plus(z,V_2) -> V_2,
    U32(tt,V_2,V_3) -> 0(plus(V_2,V_3)),
    U31(tt,V_2,V_3) -> U32(tt,V_2,V_3),
    U42(tt,V_2,V_3) -> 1(plus(V_2,V_3)),
    U41(tt,V_2,V_3) -> U42(tt,V_2,V_3),
    U52(tt,V_2,V_3) -> 0(plus(1(z),V_2,V_3)),
    U51(tt,V_2,V_3) -> U52(tt,V_2,V_3) } (10 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U51`(tt,V_2,V_3) ; 'U52`(tt,V_2,V_3)
    1: 'U52`(tt,V_2,V_3) ; plus(1(z),V_2,V_3)
    2: 'U41`(tt,V_2,V_3) ; 'U42`(tt,V_2,V_3)
    3: 'U42`(tt,V_2,V_3) ; plus(V_2,V_3)
    4: 'U31`(tt,V_2,V_3) ; 'U32`(tt,V_2,V_3)
    5: 'U32`(tt,V_2,V_3) ; plus(V_2,V_3)
    6: plus(0(V_2),0(V_3),V_0) ; 'U31`(tt,V_2,V_3)
    7: plus(0(V_2),0(V_3),V_0) ; plus(U31(tt,V_2,V_3),V_0)
    8: plus(0(V_2),0(V_3)) ; 'U31`(tt,V_2,V_3)
    9: plus(1(V_3),0(V_2),V_0) ; 'U41`(tt,V_2,V_3)
    10: plus(1(V_3),0(V_2),V_0) ; plus(U41(tt,V_2,V_3),V_0)
    11: plus(1(V_3),0(V_2)) ; 'U41`(tt,V_2,V_3)
    12: plus(1(V_2),1(V_3),V_0) ; 'U51`(tt,V_2,V_3)
    13: plus(1(V_2),1(V_3),V_0) ; plus(U51(tt,V_2,V_3),V_0)
    14: plus(1(V_2),1(V_3)) ; 'U51`(tt,V_2,V_3) 
    0 -> 1, 1 -> 6, 1 -> 7, 1 -> 8, 1 -> 9, 1 -> 10, 1 -> 11, 1 -> 12,
    1 -> 13, 1 -> 14, 2 -> 3, 3 -> 6, 3 -> 7, 3 -> 8, 3 -> 9, 3 -> 10,
    3 -> 11, 3 -> 12, 3 -> 13, 3 -> 14, 4 -> 5, 5 -> 6, 5 -> 7, 5 -> 8,
    5 -> 9, 5 -> 10, 5 -> 11, 5 -> 12, 5 -> 13, 5 -> 14, 6 -> 4, 7 -> 6,
    7 -> 7, 7 -> 8, 7 -> 9, 7 -> 10, 7 -> 11, 7 -> 12, 7 -> 13, 7 -> 14,
    8 -> 4, 9 -> 2, 10 -> 6, 10 -> 7, 10 -> 8, 10 -> 9, 10 -> 10, 10 -> 11,
    10 -> 12, 10 -> 13, 10 -> 14, 11 -> 2, 12 -> 0, 13 -> 6, 13 -> 7,
    13 -> 8, 13 -> 9, 13 -> 10, 13 -> 11, 13 -> 12, 13 -> 13, 13 -> 14,
    14 -> 0, 
    On this component, with the interpretation
      [z] = 0; 
      [tt] = 0; 
      [1](X0) = X0 + 1; 
      [0](X0) = X0; 
      [U51](X0,X1,X2) = X2 + X1 + 1; 
      [U52](X0,X1,X2) = X2 + X1 + 1; 
      [U41](X0,X1,X2) = X2 + X1 + 1; 
      [U42](X0,X1,X2) = X2 + X1 + 1; 
      [U31](X0,X1,X2) = X2 + X1; 
      [U32](X0,X1,X2) = X2 + X1; 
      [plus](X0,X1) = X1 + X0; 
      ['U51`](X0,X1,X2) = X2 + X1 + 1; 
      ['U52`](X0,X1,X2) = X2 + X1 + 1; 
      ['U41`](X0,X1,X2) = X2 + X1; 
      ['U42`](X0,X1,X2) = X2 + X1; 
      ['U31`](X0,X1,X2) = X2 + X1; 
      ['U32`](X0,X1,X2) = X2 + X1; 
      
    the subgraph of pairs that are only weakly decreasing
    has one strongly connected component:
      4: 'U31`(tt,V_2,V_3) ; 'U32`(tt,V_2,V_3)
      5: 'U32`(tt,V_2,V_3) ; plus(V_2,V_3)
      6: plus(0(V_2),0(V_3),V_0) ; 'U31`(tt,V_2,V_3)
      7: plus(0(V_2),0(V_3),V_0) ; plus(U31(tt,V_2,V_3),V_0)
      8: plus(0(V_2),0(V_3)) ; 'U31`(tt,V_2,V_3)
      10: plus(1(V_3),0(V_2),V_0) ; plus(U41(tt,V_2,V_3),V_0) 
      4 -> 5, 5 -> 6, 5 -> 7, 5 -> 8, 5 -> 10, 6 -> 4, 7 -> 6, 7 -> 7,
      7 -> 8, 7 -> 10, 8 -> 4, 10 -> 6, 10 -> 7, 10 -> 8, 10 -> 10, 
      On this component, the interpretation
      [z] = 0; 
      [tt] = 2; 
      [1](X0) = X0 + 2; 
      [0](X0) = X0 + 2; 
      [U51](X0,X1,X2) = X2 + X1 + 2*X0; 
      [U52](X0,X1,X2) = X2 + X1 + 2*X0; 
      [U41](X0,X1,X2) = X2 + X1 + X0; 
      [U42](X0,X1,X2) = X2 + X1 + X0; 
      [U31](X0,X1,X2) = X2 + X1 + X0; 
      [U32](X0,X1,X2) = X2 + X1 + X0; 
      [plus](X0,X1) = X1 + X0; 
      ['U31`](X0,X1,X2) = X2 + X1 + X0; 
      ['U32`](X0,X1,X2) = X2 + X1 + 1; 
       strictly decreases on every cycle

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { union(empty,V_2) -> V_2,
    union(empty,V_2) -> V_2 } (2 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { sum(empty) -> 0(z),
    sum(singl(V_2)) -> V_2,
    sum(union(V_0,V_1)) -> U71(tt,V_0,V_1),
    U72(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)),
    U71(tt,V_0,V_1) -> U72(tt,V_0,V_1) } (5 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U71`(tt,V_0,V_1) ; 'U72`(tt,V_0,V_1)
    1: 'U72`(tt,V_0,V_1) ; 'sum`(V_1) 2: 'U72`(tt,V_0,V_1) ; 'sum`(V_0)
    3: 'sum`(union(V_0,V_1)) ; 'U71`(tt,V_0,V_1) 
    0 -> 1, 0 -> 2, 1 -> 3, 2 -> 3, 3 -> 0, 
    On this component, the interpretation
    [empty] = 0; 
    [union](X0,X1) = X1 + X0 + 2; 
    [z] = 0; 
    [tt] = 0; 
    [1](X0) = 0; 
    [singl](X0) = X0; 
    [0](X0) = 0; 
    [U51](X0,X1,X2) = 0; 
    [U71](X0,X1,X2) = X2 + X1; 
    [U52](X0,X1,X2) = 0; 
    [U72](X0,X1,X2) = X2 + X1; 
    [U41](X0,X1,X2) = 0; 
    [sum](X0) = X0; 
    [U42](X0,X1,X2) = 0; 
    [U31](X0,X1,X2) = 0; 
    [U32](X0,X1,X2) = 0; 
    [plus](X0,X1) = X1 + X0; 
    ['U71`](X0,X1,X2) = 2*X2 + 2*X1 + 2; 
    ['U72`](X0,X1,X2) = 2*X2 + 2*X1 + 1; 
    ['sum`](X0) = 2*X0; 
     strictly decreases on every cycle

The module
  { mult(1(V_2),V_3) -> U21(tt,V_2,V_3),
    mult(0(V_2),V_3) -> U11(tt,V_2,V_3),
    mult(z,V_2) -> z,
    U12(tt,V_2,V_3) -> 0(mult(V_2,V_3)),
    U11(tt,V_2,V_3) -> U12(tt,V_2,V_3),
    U22(tt,V_2,V_3) -> plus(0(mult(V_2,V_3)),V_3),
    U21(tt,V_2,V_3) -> U22(tt,V_2,V_3) } (7 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U21`(tt,V_2,V_3) ; 'U22`(tt,V_2,V_3)
    1: 'U22`(tt,V_2,V_3) ; mult(V_2,V_3)
    2: 'U11`(tt,V_2,V_3) ; 'U12`(tt,V_2,V_3)
    3: 'U12`(tt,V_2,V_3) ; mult(V_2,V_3) 4: mult(z,V_0,V_2) ; mult(z,V_0)
    5: mult(0(V_2),V_0,V_3) ; 'U11`(tt,V_2,V_3)
    6: mult(0(V_2),V_0,V_3) ; mult(U11(tt,V_2,V_3),V_0)
    7: mult(0(V_2),V_3) ; 'U11`(tt,V_2,V_3)
    8: mult(1(V_2),V_0,V_3) ; 'U21`(tt,V_2,V_3)
    9: mult(1(V_2),V_0,V_3) ; mult(U21(tt,V_2,V_3),V_0)
    10: mult(1(V_2),V_3) ; 'U21`(tt,V_2,V_3) 
    0 -> 1, 1 -> 4, 1 -> 5, 1 -> 6, 1 -> 7, 1 -> 8, 1 -> 9, 1 -> 10, 2 -> 3,
    3 -> 4, 3 -> 5, 3 -> 6, 3 -> 7, 3 -> 8, 3 -> 9, 3 -> 10, 4 -> 4, 4 -> 5,
    4 -> 6, 4 -> 7, 4 -> 8, 4 -> 9, 4 -> 10, 5 -> 2, 6 -> 4, 6 -> 5, 6 -> 6,
    6 -> 7, 6 -> 8, 6 -> 9, 6 -> 10, 7 -> 2, 8 -> 0, 9 -> 4, 9 -> 5, 9 -> 6,
    9 -> 7, 9 -> 8, 9 -> 9, 9 -> 10, 10 -> 0, 
    On this component, with the interpretation
      [z] = 0; 
      [tt] = 0; 
      [1](X0) = X0 + 1; 
      [0](X0) = X0; 
      [U51](X0,X1,X2) = X2 + X1 + 1; 
      [U21](X0,X1,X2) = X2*X1 + 2*X2 + X1; 
      [U52](X0,X1,X2) = X2 + X1 + 1; 
      [U22](X0,X1,X2) = X2*X1 + 2*X2 + X1; 
      [U41](X0,X1,X2) = X2 + X1 + 1; 
      [U11](X0,X1,X2) = X2*X1 + X2 + X1; 
      [U42](X0,X1,X2) = X2 + X1 + 1; 
      [U12](X0,X1,X2) = X2*X1 + X2 + X1; 
      [U31](X0,X1,X2) = X2 + X1; 
      [mult](X0,X1) = X1*X0 + X1 + X0; 
      [U32](X0,X1,X2) = X2 + X1; 
      [plus](X0,X1) = X1 + X0; 
      ['U21`](X0,X1,X2) = X2*X1 + X2 + X1; 
      ['U22`](X0,X1,X2) = X2*X1 + X2 + X1; 
      ['U11`](X0,X1,X2) = X2*X1 + X2 + X1; 
      ['U12`](X0,X1,X2) = X2*X1 + X2 + X1; 
      
    the subgraph of pairs that are only weakly decreasing
    has one strongly connected component:
      2: 'U11`(tt,V_2,V_3) ; 'U12`(tt,V_2,V_3)
      3: 'U12`(tt,V_2,V_3) ; mult(V_2,V_3) 4: mult(z,V_0,V_2) ; mult(z,V_0)
      5: mult(0(V_2),V_0,V_3) ; 'U11`(tt,V_2,V_3)
      6: mult(0(V_2),V_0,V_3) ; mult(U11(tt,V_2,V_3),V_0)
      7: mult(0(V_2),V_3) ; 'U11`(tt,V_2,V_3) 
      2 -> 3, 3 -> 4, 3 -> 5, 3 -> 6, 3 -> 7, 4 -> 4, 4 -> 5, 4 -> 6, 4 -> 7,
      5 -> 2, 6 -> 4, 6 -> 5, 6 -> 6, 6 -> 7, 7 -> 2, 
      On this component, with the interpretation
        [z] = 0; 
        [tt] = 0; 
        [1](X0) = X0 + 1; 
        [0](X0) = X0 + 1; 
        [U51](X0,X1,X2) = X2 + X1 + 2; 
        [U21](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; 
        [U52](X0,X1,X2) = X2 + X1 + 2; 
        [U22](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; 
        [U41](X0,X1,X2) = X2 + X1 + 1; 
        [U11](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
        [U42](X0,X1,X2) = X2 + X1 + 1; 
        [U12](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
        [U31](X0,X1,X2) = X2 + X1 + 1; 
        [mult](X0,X1) = X1*X0 + X1 + X0; 
        [U32](X0,X1,X2) = X2 + X1 + 1; 
        [plus](X0,X1) = X1 + X0; 
        ['U11`](X0,X1,X2) = X2*X1 + X2 + X1; 
        ['U12`](X0,X1,X2) = X2*X1 + X2 + X1; 
        
      the subgraph of pairs that are only weakly decreasing
      has one strongly connected component:
        4: mult(z,V_0,V_2) ; mult(z,V_0)
        6: mult(0(V_2),V_0,V_3) ; mult(U11(tt,V_2,V_3),V_0) 
        4 -> 4, 4 -> 6, 6 -> 4, 6 -> 6, 
        On this component, the interpretation
        [z] = 1; 
        [tt] = 1; 
        [1](X0) = 1; 
        [0](X0) = 1; 
        [U51](X0,X1,X2) = 1; 
        [U21](X0,X1,X2) = X2; 
        [U52](X0,X1,X2) = 1; 
        [U22](X0,X1,X2) = X2; 
        [U41](X0,X1,X2) = 1; 
        [U11](X0,X1,X2) = X0; 
        [U42](X0,X1,X2) = 1; 
        [U12](X0,X1,X2) = X0; 
        [U31](X0,X1,X2) = X0; 
        [mult](X0,X1) = X1 + X0 + 1; 
        [U32](X0,X1,X2) = X0; 
        [plus](X0,X1) = X1*X0; 
         strictly decreases on every cycle

The module
  { prod(empty) -> 1(z),
    prod(singl(V_2)) -> V_2,
    prod(union(V_0,V_1)) -> U61(tt,V_0,V_1),
    U62(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)),
    U61(tt,V_0,V_1) -> U62(tt,V_0,V_1) } (5 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U61`(tt,V_0,V_1) ; 'U62`(tt,V_0,V_1)
    1: 'U62`(tt,V_0,V_1) ; 'prod`(V_1) 2: 'U62`(tt,V_0,V_1) ; 'prod`(V_0)
    3: 'prod`(union(V_0,V_1)) ; 'U61`(tt,V_0,V_1) 
    0 -> 1, 0 -> 2, 1 -> 3, 2 -> 3, 3 -> 0, 
    On this component, the interpretation
    [empty] = 1; 
    [union](X0,X1) = X1 + X0 + 2; 
    [z] = 1; 
    [tt] = 1; 
    [1](X0) = 1; 
    [singl](X0) = X0; 
    [0](X0) = 1; 
    [U51](X0,X1,X2) = 1; 
    [U21](X0,X1,X2) = X2; 
    [U61](X0,X1,X2) = X2 + X1; 
    [U52](X0,X1,X2) = X0; 
    [U22](X0,X1,X2) = X2; 
    [U62](X0,X1,X2) = X2 + X1; 
    [U41](X0,X1,X2) = X0; 
    [U11](X0,X1,X2) = X0; 
    [prod](X0) = X0; 
    [U42](X0,X1,X2) = X0; 
    [U12](X0,X1,X2) = X0; 
    [U31](X0,X1,X2) = X0; 
    [mult](X0,X1) = X1 + X0; 
    [U32](X0,X1,X2) = X0; 
    [plus](X0,X1) = X1*X0; 
    ['U61`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; 
    ['U62`](X0,X1,X2) = 2*X2 + 2*X1 + X0; 
    ['prod`](X0) = 2*X0; 
     strictly decreases on every cycle

- : unit = ()

Quitting.
Standard error: