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) -> tt,
             U21(tt) -> tt,
             U31(tt) -> tt,
             U41(tt,V2) -> U42(isNatIList(V2)),
             U42(tt) -> tt,
             U51(tt,V2) -> U52(isNatList(V2)),
             U52(tt) -> tt,
             U61(tt,L,N) -> U62(isNat(N),L),
             U62(tt,L) -> s(length(L)),
             isNat(0) -> tt,
             isNat(length(V1)) -> U11(isNatList(V1)),
             isNat(s(V1)) -> U21(isNat(V1)),
             isNatIList(V) -> U31(isNatList(V)),
             isNatIList(zeros) -> tt,
             isNatIList(cons(V1,V2)) -> U41(isNat(V1),V2),
             isNatList(nil) -> tt,
             isNatList(cons(V1,V2)) -> U51(isNat(V1),V2),
             length(nil) -> 0,
             length(cons(N,L)) -> U61(isNatList(L),L,N) } (20 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:
{ U52(tt) -> 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:
{ U21(tt) -> tt } (1 rules)

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

Checking module:
{ U11(tt) -> 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:
{ length(nil) -> 0,
  length(cons(V_1,V_0)) -> U61(isNatList(V_0),V_0,V_1),
  isNat(s(V_2)) -> U21(isNat(V_2)),
  isNat(length(V_2)) -> U11(isNatList(V_2)),
  isNat(0) -> tt,
  isNatList(nil) -> tt,
  isNatList(cons(V_2,V_3)) -> U51(isNat(V_2),V_3),
  U51(tt,V_3) -> U52(isNatList(V_3)),
  U62(tt,V_0) -> s(length(V_0)),
  U61(tt,V_0,V_1) -> U62(isNat(V_1),V_0) } (10 rules)

The dependency graph is
(1 nodes)
Checking each of the 2 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(16 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; 
[U11](X0) = 0; 
[U21](X0) = 0; 
[s](X0) = 0; 
[U52](X0) = 0; 
[U61](X0,X1,X2) = 0; 
[U62](X0,X1) = 0; 
[U51](X0,X1) = 0; 
[isNatList](X0) = 0; 
[isNat](X0) = 0; 
[length](X0) = 0; 
['U61`](X0,X1,X2) = 2*X1 + 2; 
['U62`](X0,X1) = 2*X1 + 1; 
['length`](X0) = 2*X0; 

Checking component 2
Trying simple graph criterion.
Trying to solve the following constraints:
(18 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[0] = 0; 
[cons](X0,X1) = X1 + X0 + 2; 
[tt] = 0; 
[nil] = 0; 
[U11](X0) = 0; 
[U21](X0) = 0; 
[s](X0) = X0 + 1; 
[U52](X0) = 0; 
[U61](X0,X1,X2) = X1 + 1; 
[U62](X0,X1) = X1 + 1; 
[U51](X0,X1) = 0; 
[isNatList](X0) = 0; 
[isNat](X0) = 0; 
[length](X0) = X0; 
['U51`](X0,X1) = X1 + 1; 
['isNatList`](X0) = X0; 
['isNat`](X0) = X0 + 1; 


Checking module:
{ U42(tt) -> tt } (1 rules)

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

Checking module:
{ U31(tt) -> tt } (1 rules)

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

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: