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

	eq oddpos([]) = [] .
	eq oddpos(cons(X,[])) = cons(X,[]) .
	eq oddpos(cons(X,cons(Z,[]))) = cons(X,[]) .
	eq oddpos(cons(X,cons(V,cons(Z,[])))) = cons(X, cons(Z,[]) ) .
	eq oddpos(cons(X,cons(Z,cons(Y,cons(U,[]))))) = cons(X, cons(Y,[])) .
	eq oddpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,[])))))) = cons(X, cons(Z, cons(Y, []))) .
	eq oddpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,cons(V,[]))))))) = cons(X, cons(Z, cons(Y, []))) .

endfm