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