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 = { and(tt,X) -> X,
             plus(N,0) -> N,
             plus(N,s(M)) -> s(plus(N,M)) } (3 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:
{ plus(V_1,0) -> V_1,
  plus(V_1,s(V_0)) -> s(plus(V_1,V_0)) } (2 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:
(3 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[0] = 0;  [s](X0) = X0 + 1;  [plus](X0,X1) = X1 + X0;  ['plus`](X0,X1) = X1;  

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
  { plus(V_1,0) -> V_1,
    plus(V_1,s(V_0)) -> s(plus(V_1,V_0)) } (2 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`(V_1,s(V_0)) ; 'plus`(V_1,V_0)  0 -> 0, 
    On this component, the interpretation
    [0] = 0; 
    [s](X0) = X0 + 1; 
    [plus](X0,X1) = X1 + X0; 
    ['plus`](X0,X1) = X1; 
     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: