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 = { U101(tt,V2) -> U102(isLNat(V2)),
             U102(tt) -> tt,
             U11(tt,N,XS) -> U12(isLNat(XS),N,XS),
             U111(tt) -> tt,
             U12(tt,N,XS) -> snd(splitAt(N,XS)),
             U121(tt) -> tt,
             U131(tt,V2) -> U132(isLNat(V2)),
             U132(tt) -> tt,
             U141(tt,V2) -> U142(isLNat(V2)),
             U142(tt) -> tt,
             U151(tt,V2) -> U152(isLNat(V2)),
             U152(tt) -> tt,
             U161(tt,N) -> cons(N,natsFrom(s(N))),
             U171(tt,N,XS) -> U172(isLNat(XS),N,XS),
             U172(tt,N,XS) -> head(afterNth(N,XS)),
             U181(tt,Y) -> U182(isLNat(Y),Y),
             U182(tt,Y) -> Y,
             U191(tt,XS) -> pair(nil,XS),
             U201(tt,N,X,XS) -> U202(isNatural(X),N,X,XS),
             U202(tt,N,X,XS) -> U203(isLNat(XS),N,X,XS),
             U203(tt,N,X,XS) -> U204(splitAt(N,XS),X),
             U204(pair(YS,ZS),X) -> pair(cons(X,YS),ZS),
             U21(tt,X,Y) -> U22(isLNat(Y),X),
             U211(tt,XS) -> U212(isLNat(XS),XS),
             U212(tt,XS) -> XS,
             U22(tt,X) -> X,
             U221(tt,N,XS) -> U222(isLNat(XS),N,XS),
             U222(tt,N,XS) -> fst(splitAt(N,XS)),
             U31(tt,N,XS) -> U32(isLNat(XS),N),
             U32(tt,N) -> N,
             U41(tt,V2) -> U42(isLNat(V2)),
             U42(tt) -> tt,
             U51(tt,V2) -> U52(isLNat(V2)),
             U52(tt) -> tt,
             U61(tt) -> tt,
             U71(tt) -> tt,
             U81(tt) -> tt,
             U91(tt) -> tt,
             afterNth(N,XS) -> U11(isNatural(N),N,XS),
             fst(pair(X,Y)) -> U21(isLNat(X),X,Y),
             head(cons(N,XS)) -> U31(isNatural(N),N,XS),
             isLNat(nil) -> tt,
             isLNat(afterNth(V1,V2)) -> U41(isNatural(V1),V2),
             isLNat(cons(V1,V2)) -> U51(isNatural(V1),V2),
             isLNat(fst(V1)) -> U61(isPLNat(V1)),
             isLNat(natsFrom(V1)) -> U71(isNatural(V1)),
             isLNat(snd(V1)) -> U81(isPLNat(V1)),
             isLNat(tail(V1)) -> U91(isLNat(V1)),
             isLNat(take(V1,V2)) -> U101(isNatural(V1),V2),
             isNatural(0) -> tt,
             isNatural(head(V1)) -> U111(isLNat(V1)),
             isNatural(s(V1)) -> U121(isNatural(V1)),
             isNatural(sel(V1,V2)) -> U131(isNatural(V1),V2),
             isPLNat(pair(V1,V2)) -> U141(isLNat(V1),V2),
             isPLNat(splitAt(V1,V2)) -> U151(isNatural(V1),V2),
             natsFrom(N) -> U161(isNatural(N),N),
             sel(N,XS) -> U171(isNatural(N),N,XS),
             snd(pair(X,Y)) -> U181(isLNat(X),Y),
             splitAt(0,XS) -> U191(isLNat(XS),XS),
             splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,XS),
             tail(cons(N,XS)) -> U211(isNatural(N),XS),
             take(N,XS) -> U221(isNatural(N),N,XS) } (62 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:
{ U32(tt,V_0) -> V_0 } (1 rules)

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

Checking module:
{ U22(tt,V_3) -> V_3 } (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:
{ U204(pair(V_6,V_7),V_3) -> pair(cons(V_3,V_6),V_7) } (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:
{ U191(tt,V_4) -> pair(nil,V_4) } (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:
{ U212(tt,V_4) -> V_4 } (1 rules)

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

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

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

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

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

Checking module:
{ U91(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:
{ U61(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:
{ U42(tt) -> tt } (1 rules)

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

Checking module:
{ U182(tt,V_5) -> V_5 } (1 rules)

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

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

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

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

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

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

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

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

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

Checking module:
{ sel(V_0,V_4) -> U171(isNatural(V_0),V_0,V_4),
  isNatural(sel(V_1,V_2)) -> U131(isNatural(V_1),V_2),
  isNatural(s(V_1)) -> U121(isNatural(V_1)),
  isNatural(head(V_1)) -> U111(isLNat(V_1)),
  isNatural(0) -> tt,
  natsFrom(V_0) -> U161(isNatural(V_0),V_0),
  U161(tt,V_0) -> cons(V_0,natsFrom(s(V_0))),
  take(V_0,V_4) -> U221(isNatural(V_0),V_0,V_4),
  isLNat(take(V_1,V_2)) -> U101(isNatural(V_1),V_2),
  isLNat(tail(V_1)) -> U91(isLNat(V_1)),
  isLNat(snd(V_1)) -> U81(isPLNat(V_1)),
  isLNat(natsFrom(V_1)) -> U71(isNatural(V_1)),
  isLNat(fst(V_1)) -> U61(isPLNat(V_1)),
  isLNat(cons(V_1,V_2)) -> U51(isNatural(V_1),V_2),
  isLNat(afterNth(V_1,V_2)) -> U41(isNatural(V_1),V_2),
  isLNat(nil) -> tt,
  U101(tt,V_2) -> U102(isLNat(V_2)),
  U131(tt,V_2) -> U132(isLNat(V_2)),
  U141(tt,V_2) -> U142(isLNat(V_2)),
  U151(tt,V_2) -> U152(isLNat(V_2)),
  U181(tt,V_5) -> U182(isLNat(V_5),V_5),
  snd(pair(V_3,V_5)) -> U181(isLNat(V_3),V_5),
  U202(tt,V_0,V_3,V_4) -> U203(isLNat(V_4),V_0,V_3,V_4),
  U201(tt,V_0,V_3,V_4) -> U202(isNatural(V_3),V_0,V_3,V_4),
  splitAt(0,V_4) -> U191(isLNat(V_4),V_4),
  splitAt(s(V_0),cons(V_3,V_4)) -> U201(isNatural(V_0),V_0,V_3,V_4),
  U12(tt,V_0,V_4) -> snd(splitAt(V_0,V_4)),
  U11(tt,V_0,V_4) -> U12(isLNat(V_4),V_0,V_4),
  afterNth(V_0,V_4) -> U11(isNatural(V_0),V_0,V_4),
  U203(tt,V_0,V_3,V_4) -> U204(splitAt(V_0,V_4),V_3),
  U21(tt,V_3,V_5) -> U22(isLNat(V_5),V_3),
  U211(tt,V_4) -> U212(isLNat(V_4),V_4),
  tail(cons(V_0,V_4)) -> U211(isNatural(V_0),V_4),
  fst(pair(V_3,V_5)) -> U21(isLNat(V_3),V_3,V_5),
  U222(tt,V_0,V_4) -> fst(splitAt(V_0,V_4)),
  U221(tt,V_0,V_4) -> U222(isLNat(V_4),V_0,V_4),
  U31(tt,V_0,V_4) -> U32(isLNat(V_4),V_0),
  head(cons(V_0,V_4)) -> U31(isNatural(V_0),V_0,V_4),
  U172(tt,V_0,V_4) -> head(afterNth(V_0,V_4)),
  U171(tt,V_0,V_4) -> U172(isLNat(V_4),V_0,V_4),
  U41(tt,V_2) -> U42(isLNat(V_2)),
  U51(tt,V_2) -> U52(isLNat(V_2)),
  isPLNat(splitAt(V_1,V_2)) -> U151(isNatural(V_1),V_2),
  isPLNat(pair(V_1,V_2)) -> U141(isLNat(V_1),V_2) } (44 rules)

The dependency graph is
(1 nodes)
Checking each of the 3 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(64 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(64 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying to solve the following constraints:
(64 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
No modular termination proof found.
- : unit = ()
The last proof attempt failed.
- : unit = ()

Quitting.
Standard error: