fmod LASTS is 
	sorts MyItem MyList MyLList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	op # : -> MyLList [ctor] .
	op consl : MyList MyLList -> MyLList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op lasts : MyLList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyLList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq lasts(#) = [] .
	eq lasts(consl(cons(Y,[]),#)) = cons(Y,[]) .
	eq lasts(consl(cons(Y,cons(X,[])),#)) = cons(X,[]) .
	eq lasts(consl(cons(Y,cons(X,cons(Z,[]))),#)) = cons(Z,[]) .
	eq lasts(consl(cons(Y,[]),consl(cons(X,[]),#))) = cons(Y,cons(X,[])) .
	eq lasts(consl(cons(X,[]),consl(cons(Y,cons(Z,[])),#))) = cons(X,cons(Z,[])) .
	eq lasts(consl(cons(X,cons(V,[])),consl(cons(Y,cons(Z,[])),#))) = cons(V,cons(Z,[])) .
	eq lasts(consl(cons(X,cons(V,[])),consl(cons(Z,[]),#))) = cons(V,cons(Z,[])) .
	eq lasts(consl(cons(Z,[]),consl(cons(Y,cons(X,[])),consl(cons(V,[]),#)))) = cons(Z,cons(X,cons(V,[]))) .
	eq lasts(consl(cons(Z,cons(X,[])),consl(cons(Y,cons(V,[])),consl(cons(W,[]),#)))) = cons(X,cons(V,cons(W,[]))) .
	***eq lasts(consl(cons(Z,cons(X,[])),consl(cons(V,cons(Y,[])),consl(cons(W,cons(U,[])),#)))) = cons(X,cons(Y,cons(U,[]))) .
endfm