types

BAMS = map AccId to Account
inv x == forall mk_Account(h,a) in set rng x &
         card h > 0 and a >= 0;

Account :: H: set of AccHolder
           B: Amount;

AccId = seq of char;
AccHolder = seq of char;
Amount = nat