fmod DROP is sorts MyItem MyNat MyList InVec . *** DT definitions (constructors) op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op [] : -> MyList [ctor] . op cons : MyItem MyList -> MyList [ctor] . *** defined function names (to be induced, preds, bk) op drop : MyNat MyList -> MyList [metadata "induce"] . *** input encapsulation op in : MyNat MyList -> InVec [ctor] . vars W X Y Z : MyItem . eq drop(0,[]) = [] . eq drop(s(0),[]) = [] . eq drop(s(s(0)),[]) = [] . eq drop(s(s(s(0))),[]) = [] . %eq drop(s(s(s(s(0)))),[]) = [] . eq drop(0,cons(X,[])) = cons(X,[]) . eq drop(s(0),cons(X,[])) = [] . eq drop(s(s(0)),cons(X,[])) = [] . eq drop(s(s(s(0))),cons(X,[])) = [] . %eq drop(s(s(s(s(0)))),cons(X,[])) = [] . eq drop(0,cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) . eq drop(s(0),cons(X,cons(Y,[]))) = cons(Y,[]) . eq drop(s(s(0)),cons(X,cons(Y,[]))) = [] . eq drop(s(s(s(0))),cons(X,cons(Y,[]))) = [] . %eq drop(s(s(s(s(0)))),cons(X,cons(Y,[]))) = [] . eq drop(0,cons(X,cons(Y,cons(Z,[])))) = cons(X,cons(Y,cons(Z,[]))) . eq drop(s(0),cons(X,cons(Y,cons(Z,[])))) = cons(Y,cons(Z,[])) . eq drop(s(s(0)),cons(X,cons(Y,cons(Z,[])))) = cons(Z,[]) . eq drop(s(s(s(0))),cons(X,cons(Y,cons(Z,[])))) = [] . %eq drop(s(s(s(s(0)))),cons(X,cons(Y,cons(Z,[])))) = [] . eq drop(0,cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,cons(X,cons(Z,cons(Y,[])))) . eq drop(s(0),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(X,cons(Z,cons(Y,[]))) . eq drop(s(s(0)),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Z,cons(Y,[])) . eq drop(s(s(s(0))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,[]) . %eq drop(s(s(s(s(0)))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = [] . endfm