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