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),
             U101(tt,V1,V2) -> U102(isNatKind(V1),V1,V2),
             U102(tt,V1,V2) -> U103(isNatIListKind(V2),V1,V2),
             U103(tt,V1,V2) -> U104(isNatIListKind(V2),V1,V2),
             U104(tt,V1,V2) -> U105(isNat(V1),V2),
             U105(tt,V2) -> U106(isNatIList(V2)),
             U106(tt) -> tt,
             U11(tt,V1) -> U12(isNatIListKind(V1),V1),
             U111(tt,L,N) -> U112(isNatIListKind(L),L,N),
             U112(tt,L,N) -> U113(isNat(N),L,N),
             U113(tt,L,N) -> U114(isNatKind(N),L),
             U114(tt,L) -> s(length(L)),
             U12(tt,V1) -> U13(isNatList(V1)),
             U121(tt,IL) -> U122(isNatIListKind(IL)),
             U122(tt) -> nil,
             U13(tt) -> tt,
             U131(tt,IL,M,N) -> U132(isNatIListKind(IL),IL,M,N),
             U132(tt,IL,M,N) -> U133(isNat(M),IL,M,N),
             U133(tt,IL,M,N) -> U134(isNatKind(M),IL,M,N),
             U134(tt,IL,M,N) -> U135(isNat(N),IL,M,N),
             U135(tt,IL,M,N) -> U136(isNatKind(N),IL,M,N),
             U136(tt,IL,M,N) -> cons(N,take(M,IL)),
             U21(tt,V1) -> U22(isNatKind(V1),V1),
             U22(tt,V1) -> U23(isNat(V1)),
             U23(tt) -> tt,
             U31(tt,V) -> U32(isNatIListKind(V),V),
             U32(tt,V) -> U33(isNatList(V)),
             U33(tt) -> tt,
             U41(tt,V1,V2) -> U42(isNatKind(V1),V1,V2),
             U42(tt,V1,V2) -> U43(isNatIListKind(V2),V1,V2),
             U43(tt,V1,V2) -> U44(isNatIListKind(V2),V1,V2),
             U44(tt,V1,V2) -> U45(isNat(V1),V2),
             U45(tt,V2) -> U46(isNatIList(V2)),
             U46(tt) -> tt,
             U51(tt,V2) -> U52(isNatIListKind(V2)),
             U52(tt) -> tt,
             U61(tt,V2) -> U62(isNatIListKind(V2)),
             U62(tt) -> tt,
             U71(tt) -> tt,
             U81(tt) -> tt,
             U91(tt,V1,V2) -> U92(isNatKind(V1),V1,V2),
             U92(tt,V1,V2) -> U93(isNatIListKind(V2),V1,V2),
             U93(tt,V1,V2) -> U94(isNatIListKind(V2),V1,V2),
             U94(tt,V1,V2) -> U95(isNat(V1),V2),
             U95(tt,V2) -> U96(isNatList(V2)),
             U96(tt) -> tt,
             isNat(0) -> tt,
             isNat(length(V1)) -> U11(isNatIListKind(V1),V1),
             isNat(s(V1)) -> U21(isNatKind(V1),V1),
             isNatIList(V) -> U31(isNatIListKind(V),V),
             isNatIList(zeros) -> tt,
             isNatIList(cons(V1,V2)) -> U41(isNatKind(V1),V1,V2),
             isNatIListKind(nil) -> tt,
             isNatIListKind(zeros) -> tt,
             isNatIListKind(cons(V1,V2)) -> U51(isNatKind(V1),V2),
             isNatIListKind(take(V1,V2)) -> U61(isNatKind(V1),V2),
             isNatKind(0) -> tt,
             isNatKind(length(V1)) -> U71(isNatIListKind(V1)),
             isNatKind(s(V1)) -> U81(isNatKind(V1)),
             isNatList(nil) -> tt,
             isNatList(cons(V1,V2)) -> U91(isNatKind(V1),V1,V2),
             isNatList(take(V1,V2)) -> U101(isNatKind(V1),V1,V2),
             length(nil) -> 0,
             length(cons(N,L)) -> U111(isNatList(L),L,N),
             take(0,IL) -> U121(isNatIList(IL),IL),
             take(s(M),cons(N,IL)) -> U131(isNatIList(IL),IL,M,N) }
             (66 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:
{ U96(tt) -> tt } (1 rules)

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

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

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

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

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

Checking module:
{ U71(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:
{}

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

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

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:
{ U122(tt) -> nil } (1 rules)

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

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

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

Checking module:
{ U33(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:
{ 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: