fmod ODD is sorts MyNat MyBool InVec . op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op t : -> MyBool [ctor] . op f : -> MyBool [ctor] . op Odd : MyNat -> MyBool [metadata "induce"] . op in : MyNat -> InVec [ctor] . eq Odd(0) = f . eq Odd(s(0)) = t . eq Odd(s(s(0))) = f . ***eq Odd(s(s(s(0)))) = t . endfm