fmod SHIFTL 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 shiftl : MyList -> MyList [metadata "induce"] . *** input encapsulation op in : MyList -> InVec [ctor] . vars U V W X Y Z : MyItem . eq shiftl([]) = [] . eq shiftl(cons(W,[])) = cons(W,[]) . eq shiftl(cons(Y,cons(Z,[]))) = cons(Z,cons(Y,[])) . eq shiftl(cons(X,cons(Z,cons(W,[])))) = cons(Z,cons(W,cons(X,[]))) . eq shiftl(cons(X,cons(Z,cons(W,cons(Y,[]))))) = cons(Z,cons(W,cons(Y,cons(X,[])))) . endfm