/* * Characterization of partial functions. */ MACHINE ParFun ASSERTIONS !(ss, tt, ff) . (ss <: INTEGER & tt <: INTEGER & ff : ss <-> tt & (!xx . (xx : ss => (ff[{xx}] : FIN(INTEGER) & card(ff[{xx}]) <= 1))) => (ff : ss +-> tt)) END