---- typing desugaring: no sorts
---- termination criterion: minimal
---- polynomial interpretation: linear (2), simple-mized (6)
---- CS-TRS transf.: Zantema's

(fmod MYNAT is
   sort Natural .
   op 0 : -> Natural .
   op s : Natural -> Natural .
 endfm)

(fmod LAZYLNAT is
   pr MYNAT .
   sorts LNat PLNat .
   op nil : -> LNat .
   op cons : Natural LNat -> LNat [strat (1 0)] .
   op pair : LNat LNat -> PLNat .
   op natsFrom : Natural -> LNat .
   op fst : PLNat -> LNat .
   op snd : PLNat -> LNat .
   var N : Natural .
   vars X Y : LNat .
   eq natsFrom(N) = cons(N, natsFrom(s(N))) .
   eq fst(pair(X, Y)) = X .
   eq snd(pair(X, Y)) = Y .
 endfm)

(fmod SPLITAT is
   pr LAZYLNAT .
   op splitAt : Natural LNat -> PLNat .
   vars N X : Natural .
   vars XS YS ZS : LNat .
   eq splitAt(0, XS) = pair(nil, XS) .
   ceq splitAt(s(N), cons(X, XS)) 
     = pair(cons(X, YS), ZS)
     if pair(YS, ZS) := splitAt(N, XS) .
 endfm)

(fmod LISTUTILITIES is
   pr SPLITAT .
   op head : LNat -> Natural .
   op tail : LNat -> LNat .
   op sel : Natural LNat -> Natural .
   op take : Natural LNat -> LNat .
   op afterNth : Natural LNat -> LNat .
   vars N : Natural .
   vars XS : LNat .
   eq head(cons(N, XS)) = N .
   eq tail(cons(N, XS)) = XS .
   eq sel(N, XS) = head(afterNth(N, XS)) .
   eq take(N, XS) = fst(splitAt(N, XS)) .
   eq afterNth(N, XS) = snd(splitAt(N, XS)) .
 endfm)