types 

PPD ::  S: Stock
        P: Pricelist
        E: EquipDb;

Stock = map Unit to Quantity;
Unit = Equip | Comp;
Quantity = nat;
Equip :: K: nat;
Comp :: K: nat;
Pricelist = map Comp to Currency;
Currency = real;
EquipDb = map Equip to map Unit to Quantity

values

equip1 = mk_Equip(1);
equip2 = mk_Equip(2);
equip3 = mk_Equip(3);

comp1 = mk_Comp(1);
comp2 = mk_Comp(2);
comp3 = mk_Comp(3);
comp4 = mk_Comp(4);
comp5 = mk_Comp(5);

stock = { equip1 |-> 10, equip2 |-> 20, equip3 |-> 30, 
          comp1 |-> 100, comp2 |-> 200, comp3 |-> 300, 
          comp4 |-> 400, comp5 |-> 500 };

pricelist = { comp1 |-> 10, comp2 |-> 20, comp3 |-> 30, 
              comp4 |-> 40, comp5 |-> 50 };

equipdb = { equip1 |-> { equip2 |-> 2, equip3 |-> 3, comp1 |-> 10},
            equip2 |-> { equip3 |-> 3, comp2 |-> 200, comp3 |-> 300,
                         comp4 |-> 400, comp5 |-> 500}, 
            equip3 |-> { comp1 |-> 1000, comp2 |-> 2000, 
                         comp3 |-> 3000, comp4 |-> 4000,
                         comp5 |-> 5000, equip1 |-> 3 }
          };

bd = mk_PPD(stock, pricelist, equipdb)

functions

mseCup[@A] : (map @A to nat) * (map @A to nat) -> (map @A to nat)
mseCup (m, n) == m ++ n ++
        { a |-> m(a) + n(a) | a in set dom n inter dom m };

mseExMul[@A] : (map @A to nat) * nat -> map @A to nat
mseExMul(m, n) == { a |-> m(a) * n | a in set dom m };

mseCUP[@A] : seq of (map @A to nat) -> map @A to nat
mseCUP (sm) == if sm = [] then { |-> }
               else let res = mseCUP[@A](tl sm)
                    in mseCup[@A](hd sm, res);

Explode : PPD * Equip -> map Comp to nat
Explode (bd, e) == explode_aux(bd, bd.E(e)); 

explode_aux : PPD * (map Unit to Quantity) -> map Comp to nat

explode_aux (bd, u) ==  if u = { |-> } 
                        then { |-> }
                        else let x in set dom u
                             in if is_Comp(x) 
                                then mseCup[Comp]({ x |-> u(x) },
                                                   explode_aux(bd, {x} <-: u)
                                                 )
                                else mseCup[Comp](
                                        mseExMul[Comp](Explode(bd, x),
                                                       u(x)
                                                      ),
                                        explode_aux(bd, {x} <-: u) 
                                                 );

trans_clos : EquipDb -> set of (Equip * Equip)
trans_clos( db ) == let m = flat( db )
                    in trans_clos_aux( m, m );

flat : EquipDb -> set of (Equip * Equip)
flat( db ) == if db = {|->} 
              then {}
              else  let e in set dom db
                    in  { mk_(e,s) | s in set dom db(e) & is_Equip(s) }
                        union flat( {e} <-: db );

trans_clos_aux : set of (Equip * Equip) * set of (Equip * Equip) -> set of (Equip * Equip)
trans_clos_aux( m, mtr ) == 
        let compost = mtr union compT(m,mtr)
        in if mtr = compost
           then mtr
           else trans_clos_aux( m, compost );

compT : set of (Equip * Equip) * set of (Equip * Equip) -> set of (Equip * Equip)
compT (m1, m2) == 
        { mk_(x,y) | mk_(x,w) in set m2, mk_(z,y) in set m1 & w = z };

sub_equip : EquipDb -> bool
sub_equip( edb ) == exists mk_(x,x) in set trans_clos( edb ) & x = x