contract UnboundedNaturalAdd enhances UnboundedNaturalFacility

    procedure Add (updates n: Natural, restores m: Natural)
        ensures
            n = #n + m

end UnboundedNaturalAdd