types

    PPD :: comps:  CompDb    
           equips: EquipDb
        inv mk_PPD(c,e) == okRefIntegrity(c,e);

    CompDb     = map CompId to Comp;
    Comp      :: stock: StockInfo
                 cost:  real;
    CompId    = token;
    StockInfo :: alarm: nat
                 instock: nat
                 description: seq of char;

    EquipDb    = map EquipId to Equip;
    EquipId    = token;
    Equip     :: stock: StockInfo
                 ptree: Unitbag;
    Unitbag    = map Unit to nat;
    Unit    = EquipIdx | CompIdx;
    EquipIdx :: key: EquipId;
    CompIdx  :: key: CompId;