mod EVEN 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 in : MyNat -> InVec [ctor] . eq Even(0) = t . eq Even(s(0)) = f . eq Even(s(s(0))) = t . endfm