fmod MULT is 
	sorts MyNat InVec .
	 
	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	 
	op mult : MyNat MyNat -> MyNat [metadata "induce"] .
	 
	*** input encapsulation
	op in : MyNat MyNat -> InVec [ctor] .

	eq mult(0,0) = 0 .
	eq mult(s(0),0) = 0 .
	eq mult(s(s(0)),0) = 0 .
	eq mult(s(s(s(0))),0) = 0 .
	eq mult(s(s(s(s(0)))),0) = 0 .
	eq mult(0,s(0)) = 0 .
	eq mult(s(0),s(0)) = s(0) .
	eq mult(s(s(0)),s(0)) = s(s(0)) .
	eq mult(s(s(s(0))),s(0)) = s(s(s(0))) .
	eq mult(s(s(s(s(0)))),s(0)) = s(s(s(s(0)))) .
	eq mult(0,s(s(0))) = 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(s(0))),s(s(0))) = s(s(s(s(s(s(0)))))) .
	eq mult(s(s(s(s(0)))),s(s(0))) = s(s(s(s(s(s(s(s(0)))))))) .
	eq mult(0,s(s(s(0)))) = 0 .
	eq mult(s(0),s(s(s(0)))) = s(s(s(0))) .
	eq mult(s(s(0)),s(s(s(0)))) = s(s(s(s(s(s(0)))))) .
	eq mult(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(0))))))))) .
	eq mult(s(s(s(s(0)))),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) .
	eq mult(0,s(s(s(s(0))))) = 0 .
	eq mult(s(0),s(s(s(s(0))))) = s(s(s(s(0)))) .
	eq mult(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))) .
	eq mult(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) .
	eq mult(s(s(s(s(0)))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))) .

endfm