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