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,
             and(tt,X) -> X,
             mult(z,X) -> z,
             mult(0(X),Y) -> 0(mult(X,Y)),
             mult(1(X),Y) -> plus(0(mult(X,Y)),Y),
             plus(z,X) -> X,
             plus(0(X),0(Y)) -> 0(plus(X,Y)),
             plus(0(X),1(Y)) -> 1(plus(X,Y)),
             plus(1(X),1(Y)) -> 0(plus(1(z),X,Y)),
             prod(empty) -> 1(z),
             prod(singl(X)) -> X,
             prod(union(A,B)) -> mult(prod(A),prod(B)),
             sum(empty) -> 0(z),
             sum(singl(X)) -> X,
             sum(union(A,B)) -> plus(sum(A),sum(B)) } (17 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:
{ 0(z) -> z } (1 rules)

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:
{ plus(1(V_2),1(V_3)) -> 0(plus(1(z),V_2,V_3)),
  plus(0(V_2),1(V_3)) -> 1(plus(V_2,V_3)),
  plus(0(V_2),0(V_3)) -> 0(plus(V_2,V_3)),
  plus(z,V_2) -> V_2 } (4 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:
(14 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[z] = 0;  [0](X0) = X0 + 1;  [1](X0) = X0 + 2;  [plus](X0,X1) = X1 + X0;  

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(union(V_0,V_1)) -> plus(sum(V_0),sum(V_1)),
  sum(singl(V_2)) -> V_2,
  sum(empty) -> 0(z) } (3 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:
(11 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[empty] = 1; 
[union](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; 
[z] = 1; 
[0](X0) = X0; 
[1](X0) = 0; 
[plus](X0,X1) = X1*X0; 
[singl](X0) = X0; 
[sum](X0) = X0; 
['sum`](X0) = X0; 


Checking module:
{ mult(z,V_2) -> z,
  mult(0(V_2),V_3) -> 0(mult(V_2,V_3)),
  mult(1(V_2),V_3) -> plus(0(mult(V_2,V_3)),V_3) } (3 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:
(15 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[z] = 0; 
[0](X0) = X0 + 1; 
[1](X0) = X0 + 1; 
[plus](X0,X1) = X1 + X0; 
[mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; 


Checking module:
{ prod(union(V_0,V_1)) -> mult(prod(V_0),prod(V_1)),
  prod(singl(V_2)) -> V_2,
  prod(empty) -> 1(z) } (3 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:
(14 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[empty] = 0; 
[union](X0,X1) = X1 + X0 + 1; 
[z] = 0; 
[0](X0) = 0; 
[1](X0) = 0; 
[plus](X0,X1) = X1 + X0; 
[mult](X0,X1) = X1 + X0; 
[singl](X0) = X0; 
[prod](X0) = X0; 
['prod`](X0) = X0; 


Checking module:
{}

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

Checking module:
{ and(tt,V_2) -> V_2 } (1 rules)

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

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
  { 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
  {}
  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
  { plus(1(V_2),1(V_3)) -> 0(plus(1(z),V_2,V_3)),
    plus(0(V_2),1(V_3)) -> 1(plus(V_2,V_3)),
    plus(0(V_2),0(V_3)) -> 0(plus(V_2,V_3)),
    plus(z,V_2) -> V_2 } (4 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: plus(0(V_2),0(V_3),V_0) ; plus(V_2,V_3)
    1: plus(0(V_2),0(V_3),V_0) ; plus(0(plus(V_2,V_3)),V_0)
    2: plus(0(V_2),0(V_3)) ; plus(V_2,V_3)
    3: plus(0(V_2),1(V_3),V_0) ; plus(V_2,V_3)
    4: plus(0(V_2),1(V_3),V_0) ; plus(1(plus(V_2,V_3)),V_0)
    5: plus(0(V_2),1(V_3)) ; plus(V_2,V_3)
    6: plus(1(V_2),1(V_3),V_0) ; plus(1(z),V_2,V_3)
    7: plus(1(V_2),1(V_3),V_0) ; plus(0(plus(1(z),V_2,V_3)),V_0)
    8: plus(1(V_2),1(V_3)) ; plus(1(z),V_2,V_3) 
    0 -> 0, 0 -> 1, 0 -> 2, 0 -> 3, 0 -> 4, 0 -> 5, 0 -> 6, 0 -> 7, 0 -> 8,
    1 -> 0, 1 -> 1, 1 -> 2, 1 -> 3, 1 -> 4, 1 -> 5, 1 -> 6, 1 -> 7, 1 -> 8,
    2 -> 0, 2 -> 1, 2 -> 2, 2 -> 3, 2 -> 4, 2 -> 5, 2 -> 6, 2 -> 7, 2 -> 8,
    3 -> 0, 3 -> 1, 3 -> 2, 3 -> 3, 3 -> 4, 3 -> 5, 3 -> 6, 3 -> 7, 3 -> 8,
    4 -> 0, 4 -> 1, 4 -> 2, 4 -> 3, 4 -> 4, 4 -> 5, 4 -> 6, 4 -> 7, 4 -> 8,
    5 -> 0, 5 -> 1, 5 -> 2, 5 -> 3, 5 -> 4, 5 -> 5, 5 -> 6, 5 -> 7, 5 -> 8,
    6 -> 0, 6 -> 1, 6 -> 2, 6 -> 3, 6 -> 4, 6 -> 5, 6 -> 6, 6 -> 7, 6 -> 8,
    7 -> 0, 7 -> 1, 7 -> 2, 7 -> 3, 7 -> 4, 7 -> 5, 7 -> 6, 7 -> 7, 7 -> 8,
    8 -> 0, 8 -> 1, 8 -> 2, 8 -> 3, 8 -> 4, 8 -> 5, 8 -> 6, 8 -> 7, 8 -> 8, 
    On this component, the interpretation
    [z] = 0;  [0](X0) = X0 + 1;  [1](X0) = X0 + 2;  [plus](X0,X1) = X1 + X0;  
    strictly decreases on every cycle

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(union(V_0,V_1)) -> plus(sum(V_0),sum(V_1)),
    sum(singl(V_2)) -> V_2,
    sum(empty) -> 0(z) } (3 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'sum`(union(V_0,V_1)) ; 'sum`(V_1)
    1: 'sum`(union(V_0,V_1)) ; 'sum`(V_0) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [empty] = 1; 
    [union](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; 
    [z] = 1; 
    [0](X0) = X0; 
    [1](X0) = 0; 
    [plus](X0,X1) = X1*X0; 
    [singl](X0) = X0; 
    [sum](X0) = X0; 
    ['sum`](X0) = X0; 
     strictly decreases on every cycle

The module
  { mult(z,V_2) -> z,
    mult(0(V_2),V_3) -> 0(mult(V_2,V_3)),
    mult(1(V_2),V_3) -> plus(0(mult(V_2,V_3)),V_3) } (3 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: mult(1(V_2),V_0,V_3) ; mult(V_2,V_3)
    1: mult(1(V_2),V_0,V_3) ; mult(plus(0(mult(V_2,V_3)),V_3),V_0)
    2: mult(1(V_2),V_3) ; mult(V_2,V_3)
    3: mult(0(V_2),V_0,V_3) ; mult(V_2,V_3)
    4: mult(0(V_2),V_0,V_3) ; mult(0(mult(V_2,V_3)),V_0)
    5: mult(0(V_2),V_3) ; mult(V_2,V_3) 6: mult(z,V_0,V_2) ; mult(z,V_0) 
    0 -> 0, 0 -> 1, 0 -> 2, 0 -> 3, 0 -> 4, 0 -> 5, 0 -> 6, 1 -> 0, 1 -> 1,
    1 -> 2, 1 -> 3, 1 -> 4, 1 -> 5, 1 -> 6, 2 -> 0, 2 -> 1, 2 -> 2, 2 -> 3,
    2 -> 4, 2 -> 5, 2 -> 6, 3 -> 0, 3 -> 1, 3 -> 2, 3 -> 3, 3 -> 4, 3 -> 5,
    3 -> 6, 4 -> 0, 4 -> 1, 4 -> 2, 4 -> 3, 4 -> 4, 4 -> 5, 4 -> 6, 5 -> 0,
    5 -> 1, 5 -> 2, 5 -> 3, 5 -> 4, 5 -> 5, 5 -> 6, 6 -> 0, 6 -> 1, 6 -> 2,
    6 -> 3, 6 -> 4, 6 -> 5, 6 -> 6, 
    On this component, the interpretation
    [z] = 0; 
    [0](X0) = X0 + 1; 
    [1](X0) = X0 + 1; 
    [plus](X0,X1) = X1 + X0; 
    [mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; 
     strictly decreases on every cycle

The module
  { prod(union(V_0,V_1)) -> mult(prod(V_0),prod(V_1)),
    prod(singl(V_2)) -> V_2,
    prod(empty) -> 1(z) } (3 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'prod`(union(V_0,V_1)) ; 'prod`(V_1)
    1: 'prod`(union(V_0,V_1)) ; 'prod`(V_0) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [empty] = 0; 
    [union](X0,X1) = X1 + X0 + 1; 
    [z] = 0; 
    [0](X0) = 0; 
    [1](X0) = 0; 
    [plus](X0,X1) = X1 + X0; 
    [mult](X0,X1) = X1 + X0; 
    [singl](X0) = X0; 
    [prod](X0) = X0; 
    ['prod`](X0) = X0; 
     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
  { and(tt,V_2) -> V_2 } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

- : unit = ()

Quitting.
Standard error: