DONT KNOW
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 = { zeros -> cons(0,zeros),
             U11(tt,L) -> U12(tt,L),
             U12(tt,L) -> s(length(L)),
             U21(tt,IL,M,N) -> U22(tt,IL,M,N),
             U22(tt,IL,M,N) -> U23(tt,IL,M,N),
             U23(tt,IL,M,N) -> cons(N,take(M,IL)),
             length(nil) -> 0,
             length(cons(N,L)) -> U11(tt,L),
             take(0,IL) -> nil,
             take(s(M),cons(N,IL)) -> U21(tt,IL,M,N) } (10 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:
{}

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

Checking module:
{ take(s(V_2),cons(V_3,V_0)) -> U21(tt,V_0,V_2,V_3),
  take(0,V_0) -> nil,
  U23(tt,V_0,V_2,V_3) -> cons(V_3,take(V_2,V_0)),
  U22(tt,V_0,V_2,V_3) -> U23(tt,V_0,V_2,V_3),
  U21(tt,V_0,V_2,V_3) -> U22(tt,V_0,V_2,V_3) } (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:
(9 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[0] = 0; 
[cons](X0,X1) = 0; 
[tt] = 2; 
[nil] = 0; 
[s](X0) = X0 + 2; 
[U21](X0,X1,X2,X3) = 0; 
[U22](X0,X1,X2,X3) = 0; 
[U23](X0,X1,X2,X3) = 0; 
[take](X0,X1) = 0; 
['U21`](X0,X1,X2,X3) = 2*X2 + 2*X0; 
['U22`](X0,X1,X2,X3) = 2*X2 + X0 + 1; 
['U23`](X0,X1,X2,X3) = 2*X2 + X0; 
['take`](X0,X1) = 2*X0 + 1; 


Checking module:
{ length(cons(V_3,V_1)) -> U11(tt,V_1),
  length(nil) -> 0,
  U12(tt,V_1) -> s(length(V_1)),
  U11(tt,V_1) -> U12(tt,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:
[0] = 0; 
[cons](X0,X1) = X1 + 2; 
[tt] = 0; 
[nil] = 0; 
[s](X0) = 0; 
[U11](X0,X1) = 0; 
[U12](X0,X1) = 0; 
[length](X0) = 0; 
['U11`](X0,X1) = 2*X1 + 2; 
['U12`](X0,X1) = 2*X1 + 1; 
['length`](X0) = 2*X0; 


Checking module:
{ zeros -> cons(0,zeros) } (1 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:
(2 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
No solution found for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(2 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
No solution found for these parameters.
No solution found for these constraints.
No modular termination proof found.
- : unit = ()
The last proof attempt failed.
- : unit = ()

Quitting.
Standard error: