scheme 
  algebr = 
    class 
      type 
        ProdName = Text,  
        CompName = Text,  
        Place = Nat,  
        QTY = Nat,  
        Stock = ProdInfo-set,  
        Product,  
        ProdInfo
         
      value 
        allNaturalNumbers : Nat-inflist,  
        emptyStock : Stock,  
        makeProduct : ProdName >< CompName -> Product,  
        makeProdInfo : Product >< QTY >< Place -> ProdInfo,  
        makeStock : Stock -> Stock,  
        construct : Product >< Stock -~-> Stock,  
        destruct : Product >< Stock -~-> Stock,  
        isInit : Product >< Stock -> Bool,  
        forProduct : Product >< Stock -> Stock,  
        forPlace : Place >< Stock -> Stock,  
        needOfProduct : QTY >< Stock -> Product-set,    
        qtyOfProduct : Product >< Stock -> QTY,  
        setAllProdName : Stock -> ProdName-set,  
        addToStock : ProdInfo >< Stock -~-> Stock,  
        deleteFromStock : Product >< QTY >< Stock -~-> Stock,  
        changePlaceOfProduct : ProdInfo >< Place >< Stock -~-> Stock
     
         
      axiom 
        [allNaturalNumbers] allNaturalNumbers(1) = 0,  

        all idx : Nat :- 
          idx >= 2 => allNaturalNumbers(idx) = allNaturalNumbers(idx - 1) + 1,  

        [emptyStock] emptyStock is {},  

        [construct] 
          all St : Stock, PN : ProdName, CN : CompName :- 
            construct(makeProduct(PN, CN), makeStock(St)) is 
              St union {makeProdInfo(makeProduct(PN, CN), 0, 0)} 
              pre ~ isInit(makeProduct(PN, CN), St),  

        [destruct] 
          all St : Stock, PN : ProdName, CN : CompName :- 
            destruct(makeProduct(PN, CN), makeStock(St)) is 
              St \ forProduct(makeProduct(PN, CN), St) 
              pre isInit(makeProduct(PN, CN), St),  

        [isInit] all P : Product :- isInit(P, emptyStock) is false,  

        all St : Stock, PN, PNx : ProdName, CN, CNx : CompName :- 
          isInit(makeProduct(PN, CN), construct(makeProduct(PNx, CNx), St)) is 
            if (makeProduct(PNx, CNx) = makeProduct(PN, CN)) then 
              true 
            else 
              isInit(makeProduct(PN, CN), St) 
            end,  

        all St : Stock, PN, PNx : ProdName, CN, CNx : CompName, k : QTY, l : Place :- 
          isInit
            (
              makeProduct(PN, CN), 
              addToStock(makeProdInfo(makeProduct(PNx, CNx), k, l), St)
            ) is 
            if (makeProduct(PNx, CNx) = makeProduct(PN, CN)) then 
              true 
            else 
              isInit(makeProduct(PN, CN), St) 
            end,  

        [forProduct] all P : Product :- forProduct(P, emptyStock) is {},  

        all P : Product, St : Stock :- 
          forProduct(P, construct(P, St)) is {makeProdInfo(P, 0, 0)},  

        all St : Stock, PN, PNx : ProdName, CN, CNx : CompName, k : QTY, l : Place :- 
          forProduct
            (
              makeProduct(PN, CN), 
              addToStock(makeProdInfo(makeProduct(PNx, CNx), k, l), St)
            ) is 
            if (makeProduct(PN, CN) = makeProduct(PNx, CNx)) then 
              {
                makeProdInfo
                  (
                    makeProduct(PN, CN), 
                    qtyOfProduct(makeProduct(PN, CN), forPlace(l, St)) + k, 
                    l
                  )
              } union 
              forProduct(makeProduct(PN, CN), St) 
            else 
              forProduct(makeProduct(PN, CN), St) 
            end,  

        [forPlace] all P : Place :- forPlace(P, emptyStock) is {},  

        all St : Stock, PN : ProdName, CN : CompName, k : QTY, Pl, l : Place :- 
          forPlace(Pl, addToStock(makeProdInfo(makeProduct(PN, CN), k, l), St)) is 
            if (Pl = l) then 
              {
                makeProdInfo
                  (
                    makeProduct(PN, CN), 
                    qtyOfProduct(makeProduct(PN, CN), forPlace(Pl, St)) + k, 
                    Pl
                  )
              } union 
              forPlace(Pl, St) 
            else 
              forPlace(Pl, St) 
            end,  

        [needOfProduct] all QT : QTY :- needOfProduct(QT, emptyStock) is {},  

        all P : Product, QT : QTY, St : Stock :- 
          needOfProduct(QT, construct(P, St)) is {P},  

        all St : Stock, QT, k : QTY, PN : ProdName, CN : CompName, l : Place :- 
          needOfProduct
            (QT, addToStock(makeProdInfo(makeProduct(PN, CN), k, l), St)) is 
            if (qtyOfProduct(makeProduct(PN, CN), St) + k <= QT) then 
              {makeProduct(PN, CN)} union needOfProduct(QT, St) 
            else 
              needOfProduct(QT, St) 
            end,  

          

        [qtyOfProduct] all P : Product :- qtyOfProduct(P, emptyStock) is 0,  

        all P : Product, St : Stock :- qtyOfProduct(P, construct(P, St)) is 0,  

        all St : Stock, P, Px : Product, k : QTY, l : Place :- 
          qtyOfProduct(P, addToStock(makeProdInfo(Px, k, l), St)) is 
            if (P = Px) then 
              k + qtyOfProduct(P,St) 
            else 
              qtyOfProduct(P, St) 
            end,  

        [setAllProdName] setAllProdName(emptyStock) is {},  

        all PN : ProdName, CN : CompName, St : Stock :- 
          setAllProdName(construct(makeProduct(PN, CN), St)) is 
            {PN} union setAllProdName(St),  

        all St : Stock, PN : ProdName, CN : CompName, k : QTY, l : Place :- 
          setAllProdName
            (addToStock(makeProdInfo(makeProduct(PN, CN), k, l), St)) is 
            {PN} union setAllProdName(St), 

        [addToStock] 
          all St : Stock, P : Product, k : QTY, l : Place :- 
            addToStock(makeProdInfo(P, k, l), construct(P, St)) as bbc 
              post qtyOfProduct(P, forPlace(l, bbc)) = k 
              pre k > 0 /\ l > 0,  

        all St : Stock, P, Px : Product, k, kx : QTY, l, lx : Place :- 
          addToStock
            (makeProdInfo(P, k, l), addToStock(makeProdInfo(Px, kx, lx), St)) as cnn 
            post 
              if (P = Px /\ l = lx) then 
                qtyOfProduct(P, forPlace(l, cnn)) = qtyOfProduct(P, forPlace(l, St)) + k + kx 
              else 
                qtyOfProduct(P, forPlace(l, cnn)) = qtyOfProduct(P, forPlace(l, St)) + k 
              end 
            pre k > 0 /\ l > 0 /\ (isInit(P, St) \/ qtyOfProduct(P, St) > 0),  

        [deleteFromStock] 
          all St : Stock, P, Px : Product, k, kx : QTY, lx : Place :- 
            deleteFromStock(P, k, addToStock(makeProdInfo(Px, kx, lx), St)) as abc 
              post 
                if (P = Px) then 
                  qtyOfProduct(P, abc) = qtyOfProduct(P, St) + kx - k 
                else 
                  qtyOfProduct(P, abc) = qtyOfProduct(P, St) - k 
                end 
              pre 
                if (P = Px) then 
                  k <= qtyOfProduct(P, St)/* + kx */
                else 
                  k <= qtyOfProduct(P, St) 
                end,  

        [changePlaceOfProduct] 
          all St : Stock, P : Product, k : QTY, l, Pl : Place :- 
            changePlaceOfProduct
              (makeProdInfo(P, k, l), Pl, makeStock(St)) as mtv              post 
              qtyOfProduct(P, forPlace(Pl,mtv)) = qtyOfProduct(P,forPlace(Pl, St)) + k /\ qtyOfProduct(P, forPlace(l,mtv)) = qtyOfProduct(P, forPlace(l, St)) -k
pre qtyOfProduct (P, forPlace(l,St)) >= k /\ k>0 /\ Pl>0
    end