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