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 = { __(__(X,Y),Z) -> __(X,__(Y,Z)),
             __(X,nil) -> X,
             __(nil,X) -> X,
             U11(tt) -> U12(tt),
             U12(tt) -> tt,
             isNePal(__(I,__(P,I))) -> U11(tt) } (6 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:
{ U12(tt) -> tt } (1 rules)

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

Checking module:
{ U11(tt) -> U12(tt) } (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:
{ __(__(V_4,V_3),V_2) -> __(V_4,__(V_3,V_2)),
  __(V_4,nil) -> V_4,
  __(nil,V_4) -> V_4 } (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:
(5 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  

Checking module:
{ isNePal(__(V_0,__(V_1,V_0))) -> U11(tt) } (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
  { U12(tt) -> tt } (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
  { U11(tt) -> U12(tt) } (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
  { __(__(V_4,V_3),V_2) -> __(V_4,__(V_3,V_2)),
    __(V_4,nil) -> V_4,
    __(nil,V_4) -> V_4 } (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: '__`(__(V_4,V_3),V_2) ; '__`(V_3,V_2)
    1: '__`(__(V_4,V_3),V_2) ; '__`(V_4,__(V_3,V_2)) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  
    strictly decreases on every cycle

The module
  { isNePal(__(V_0,__(V_1,V_0))) -> U11(tt) } (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: