fmod FIB is sorts MyItem MyList MyNat InVec . *** DT definitions (constructors) op 0 : -> MyNat [ctor] . op [] : -> MyList [ctor] . op succ : MyNat -> MyNat [ctor] . *** defined function names (to be induced, preds, bk) op fib : MyNat -> MyNat [metadata "induce"] . *** input encapsulation op in : MyNat -> InVec [ctor] . eq fib(0) = 0 . eq fib(succ(0)) = succ(0) . eq fib(succ(succ(0)) ) = succ(0) . eq fib(succ(succ(succ(0)))) = succ(succ(0)) . eq fib(succ(succ(succ(succ(0))))) = succ(succ(succ(0))). endfm