use_bag : THEORY
BEGIN
  IMPORTING structures@bags
  % NASA library

% All the conjectures prove with grind
  test1: CONJECTURE
    member(5,insert(5,emptybag)) = 1

%|- test1 : PROOF
%|- (grind)
%|- QED

  test2: CONJECTURE
        count(1, emptybag) = 0 
    AND count(1, insert(1, emptybag)) = 1
    AND count(1, insert(1, insert(1, emptybag))) = 2

%|- test2 : PROOF
%|- (grind)
%|- QED

  PRODUCT: TYPE = posnat
  prd, prd1, prd2: VAR PRODUCT
  
  SET_PRODUCT: TYPE = setof[PRODUCT]
  sp, sp1, sp2: VAR SET_PRODUCT

   % add product p to set of products sp
  add_type(p:PRODUCT,sp): SET_PRODUCT = 
    union(singleton(p), sp)

  %IMPORTING structures@bags[PRODUCT]
  STOCK: TYPE = bag[PRODUCT]
  st, st1, st2: VAR STOCK

  add_product(st1, st): STOCK = % add st1 to stock st if dom(st1)
    plus(st1, st)

  p1,p2,p3: PRODUCT

  test3: CONJECTURE
    st = emptybag WITH [p1 := 1, p2 := 2] implies count(p2, st) = 2

%|- test3 : PROOF
%|- (grind)
%|- QED

  cart1: bag[PRODUCT] = emptybag WITH [p1 := 1, p2 := 2]

  %insert(x,b): bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)
  test4: CONJECTURE
    p3 /= p2 AND p2 /= p1 AND p1 /= p3 => count(p3, cart1) = 0

%|- test4 : PROOF
%|- (grind)
%|- QED
  
END use_bag