fmod MULTADD is sorts MyNat InVec . *** DT definitions (constructors) op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op Mult : MyNat MyNat -> MyNat [metadata "induce"] . op Add : MyNat MyNat -> MyNat [metadata "induce"] . *** input encapsulation op in : MyNat MyNat -> InVec [ctor] . vars X Y : MyNat . ***eq Add(0,X) = X . ***eq Add(s(0),X) = s(X) . ***eq Add(s(s(0)),X) = s(s(X)) . ***eq Add(0,0) = 0 . ***eq Add(s(0),0) = s(0) . ***eq Add(s(s(0)),0) = s(s(0)) . eq Add(0,s(0)) = s(0) . eq Add(s(0),s(0)) = s(s(0)) . eq Add(s(s(0)),s(0)) = s(s(s(0))) . eq Add(0,s(s(0))) = s(s(0)) . eq Add(s(0),s(s(0))) = s(s(s(0))) . eq Add(s(s(0)),s(s(0))) = s(s(s(s(0)))) . eq Mult(0,s(0)) = 0 . eq Mult(0,0) = 0 . eq Mult(s(0),s(0)) = s(0) . eq Mult(s(s(0)),s(0)) = s(s(0)) . ***eq Mult(X,0) = 0 . ***eq Mult(0,s(s(0))) = 0 . ***eq Mult(0,s(X)) = 0 . eq Mult(s(0),s(s(0))) = s(s(0)) . eq Mult(s(s(0)),s(s(0))) = s(s(s(s(0)))) . ***eq Mult(s(s(0)),s(0)) = s(s(0)) . ***eq Mult(0,s(s(0))) = 0 . ***eq Mult(s(0),s(s(0))) = s(s(0)) . endfm