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


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
  { plus(V_1,s(V_0)) -> U11(tt,V_0,V_1),
    plus(V_1,0) -> V_1,
    U12(tt,V_0,V_1) -> s(plus(V_1,V_0)),
    U11(tt,V_0,V_1) -> U12(tt,V_0,V_1) } (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: 'U11`(tt,V_0,V_1) ; 'U12`(tt,V_0,V_1)
    1: 'U12`(tt,V_0,V_1) ; 'plus`(V_1,V_0)
    2: 'plus`(V_1,s(V_0)) ; 'U11`(tt,V_0,V_1) 
    0 -> 1, 1 -> 2, 2 -> 0, 
    On this component, the interpretation
    [tt] = 0; 
    [s](X0) = X0 + 2; 
    [0] = 0; 
    [U11](X0,X1,X2) = X2 + X1 + 2; 
    [U12](X0,X1,X2) = X2 + X1 + 2; 
    [plus](X0,X1) = X1 + X0; 
    ['U11`](X0,X1,X2) = 2*X1 + 2; 
    ['U12`](X0,X1,X2) = 2*X1 + 1; 
    ['plus`](X0,X1) = 2*X1; 
     strictly decreases on every cycle

- : unit = ()

Quitting.
Standard error: