DONT KNOW Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { U101(tt,N,XS) -> fst(splitAt(N,XS)), U11(tt,N,XS) -> snd(splitAt(N,XS)), U21(tt,X) -> X, U31(tt,N) -> N, U41(tt,N) -> cons(N,natsFrom(s(N))), U51(tt,N,XS) -> head(afterNth(N,XS)), U61(tt,Y) -> Y, U71(tt,XS) -> pair(nil,XS), U81(tt,N,X,XS) -> U82(splitAt(N,XS),X), U82(pair(YS,ZS),X) -> pair(cons(X,YS),ZS), U91(tt,XS) -> XS, afterNth(N,XS) -> U11(and(isNatural(N),isLNat(XS)),N,XS), and(tt,X) -> X, fst(pair(X,Y)) -> U21(and(isLNat(X),isLNat(Y)),X), head(cons(N,XS)) -> U31(and(isNatural(N),isLNat(XS)),N), isLNat(nil) -> tt, isLNat(afterNth(V1,V2)) -> and(isNatural(V1),isLNat(V2)), isLNat(cons(V1,V2)) -> and(isNatural(V1),isLNat(V2)), isLNat(fst(V1)) -> isPLNat(V1), isLNat(natsFrom(V1)) -> isNatural(V1), isLNat(snd(V1)) -> isPLNat(V1), isLNat(tail(V1)) -> isLNat(V1), isLNat(take(V1,V2)) -> and(isNatural(V1),isLNat(V2)), isNatural(0) -> tt, isNatural(head(V1)) -> isLNat(V1), isNatural(s(V1)) -> isNatural(V1), isNatural(sel(V1,V2)) -> and(isNatural(V1),isLNat(V2)), isPLNat(pair(V1,V2)) -> and(isLNat(V1),isLNat(V2)), isPLNat(splitAt(V1,V2)) -> and(isNatural(V1),isLNat(V2)), natsFrom(N) -> U41(isNatural(N),N), sel(N,XS) -> U51(and(isNatural(N),isLNat(XS)),N,XS), snd(pair(X,Y)) -> U61(and(isLNat(X),isLNat(Y)),Y), splitAt(0,XS) -> U71(isLNat(XS),XS), splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS), tail(cons(N,XS)) -> U91(and(isNatural(N),isLNat(XS)),XS), take(N,XS) -> U101(and(isNatural(N),isLNat(XS)),N,XS) } (36 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: { and(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: { U31(tt,V_0) -> V_0 } (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: { U21(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U82(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: { U71(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: { U91(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U61(tt,V_5) -> V_5 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { sel(V_0,V_4) -> U51(and(isNatural(V_0),isLNat(V_4)),V_0,V_4), isNatural(0) -> tt, isNatural(head(V_1)) -> isLNat(V_1), isNatural(s(V_1)) -> isNatural(V_1), isNatural(sel(V_1,V_2)) -> and(isNatural(V_1),isLNat(V_2)), natsFrom(V_0) -> U41(isNatural(V_0),V_0), U41(tt,V_0) -> cons(V_0,natsFrom(s(V_0))), take(V_0,V_4) -> U101(and(isNatural(V_0),isLNat(V_4)),V_0,V_4), isLNat(nil) -> tt, isLNat(afterNth(V_1,V_2)) -> and(isNatural(V_1),isLNat(V_2)), isLNat(cons(V_1,V_2)) -> and(isNatural(V_1),isLNat(V_2)), isLNat(fst(V_1)) -> isPLNat(V_1), isLNat(natsFrom(V_1)) -> isNatural(V_1), isLNat(snd(V_1)) -> isPLNat(V_1), isLNat(tail(V_1)) -> isLNat(V_1), isLNat(take(V_1,V_2)) -> and(isNatural(V_1),isLNat(V_2)), splitAt(s(V_0),cons(V_3,V_4)) -> U81(and(isNatural(V_0),and(isNatural(V_3),isLNat(V_4))),V_0,V_3,V_4), splitAt(0,V_4) -> U71(isLNat(V_4),V_4), U81(tt,V_0,V_3,V_4) -> U82(splitAt(V_0,V_4),V_3), fst(pair(V_3,V_5)) -> U21(and(isLNat(V_3),isLNat(V_5)),V_3), U101(tt,V_0,V_4) -> fst(splitAt(V_0,V_4)), snd(pair(V_3,V_5)) -> U61(and(isLNat(V_3),isLNat(V_5)),V_5), U11(tt,V_0,V_4) -> snd(splitAt(V_0,V_4)), afterNth(V_0,V_4) -> U11(and(isNatural(V_0),isLNat(V_4)),V_0,V_4), head(cons(V_0,V_4)) -> U31(and(isNatural(V_0),isLNat(V_4)),V_0), U51(tt,V_0,V_4) -> head(afterNth(V_0,V_4)), isPLNat(pair(V_1,V_2)) -> and(isLNat(V_1),isLNat(V_2)), isPLNat(splitAt(V_1,V_2)) -> and(isNatural(V_1),isLNat(V_2)), tail(cons(V_0,V_4)) -> U91(and(isNatural(V_0),isLNat(V_4)),V_4) } (29 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: (38 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: (38 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: (38 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: