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