scheme explicit =
	class
	type
		ProdName=Text,			/*Наименование товара*/
		CompName=Text,			/*Наименование производителя*/
		Product=ProdName >< CompName,	/*Конкретный товар*/
		Place=Nat,			/*Местоположение товара*/
		QTY=Nat,			/*Количество товара*/
		ProdInfo=Product >< QTY >< Place,/*Информация о конкретном товаре*/
		Stock=ProdInfo-set		/*Склад товаров*/
	value

		allNaturalNumbers: Nat-inflist	/*Бесконечный список натуральных чисел*/
	axiom
		allNaturalNumbers(1)=0,
		all idx: Nat :- idx>=2 => allNaturalNumbers(idx)=allNaturalNumbers(idx-1)+1
	value

	/*Инициализация продукта*/

		construct: Product >< Stock -~-> Stock
		construct(Prod,St) is
			St union {(Prod,0,0)}
			pre ~ IsInit(Prod,St),

	/*Деинициализация продукта*/

		destruct: Product >< Stock -~-> Stock
		destruct(Prod,St) is
			{(p,c,d) | (p,c,d): ProdInfo :- (p,c,d) isin St /\ p~=Prod}
			pre IsInit(Prod,St),

	/*Проверка наличия информации о конкретном товаре на складе*/

		IsInit: Product >< Stock -> Bool
		IsInit(P,St) is
			(exists (Prod,k,l): ProdInfo :- (Prod,k,l) isin St /\ P=Prod),

	/*Проверка наличия данного наименования товара на складе*/

		IsInStockPN: ProdName >< Stock -> Bool
		IsInStockPN(PN,St) is
			(exists ((i,j),k,l): ProdInfo :- ((i,j),k,l) isin St /\ i=PN /\ k>0),

	/*Проверка наличия данного производителя на складе*/

		IsInStockCN: CompName >< Stock -> Bool
		IsInStockCN(CN,St) is
			(exists ((i,j),k,l): ProdInfo :- ((i,j),k,l) isin St /\ j=CN /\ k>0),

	/*Выдача информации по конкретному товару*/

		forProduct: Product >< Stock -> Stock
		forProduct(P,St) is
			{(prod,k,l) | (prod,k,l):ProdInfo :- (prod,k,l) isin St /\ prod=P},

	/*Выдача информации по наименованию товара*/

		forProdName: ProdName >< Stock -> Stock
		forProdName(PN,St) is
			{((i,j),k,l) | ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ i=PN},

	/*Выдача информации по производителю*/

		forCompName: CompName >< Stock -> Stock
		forCompName(CN,St) is
			{((i,j),k,l) | ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ j=CN},

	/*Выдача информации по конкретной полке*/

		forPlace: Place >< Stock -> Stock
		forPlace(Pl,St) is
			{((i,j),k,l) | ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ l=Pl},

	/*Выдача конкретных товаров, нуждающихся в дозакупке*/

		needofProduct: QTY >< Stock -> Product-set
		needofProduct(A,St) is
			{Prod | Prod:Product :- qtyofProduct(Prod,St)<=A},

	/*Выдача конкретных товаров, не пользующихся спросом*/

		manyofProduct: QTY >< Stock -> Product-set
		manyofProduct(B,St) is
			{Prod | Prod:Product :- qtyofProduct(Prod,St)>=B},

	/*Вспомогательная функция, формирующая из множества товаров список их количеств*/

		Stock_to_list: Stock -~-> QTY-list
		Stock_to_list(St) is
			<.n | n in allNaturalNumbers :- all (Prod,k,l):ProdInfo :- (Prod,k,l) isin St /\ n=k.>
			pre St~={},

	/*Вспомогательная функция, выдающая сумму всех элементов списка*/

		summ_elems_of_list: QTY-list -> QTY
		summ_elems_of_list(list) is
			if (list=<..>) then 0
				else hd list + summ_elems_of_list(tl list)
			end,

	/*Подсчёт количества конкретного товара*/

		qtyofProduct: Product >< Stock -~-> QTY
		qtyofProduct(Prod,St) is
			summ_elems_of_list(Stock_to_list(forProduct(Prod,St)))
			pre IsInit(Prod,St),

	/*Подсчёт количества данного наименования товара, присутстующего на складе*/

		qtyofProdName: ProdName >< Stock -~-> QTY
		qtyofProdName(PN,St) is
			summ_elems_of_list(Stock_to_list(forProdName(PN,St)))
			pre IsInStockPN(PN,St),

	/*Общее количество товаров на складе*/

		qtyAllProduct: Stock -~-> QTY
		qtyAllProduct(St) is
			summ_elems_of_list(Stock_to_list(St))
			pre St~={},

	/*Множество всех наименований товаров, присутствующих на на складе*/

		setAllProdName: Stock -~-> ProdName-set
		setAllProdName(St) is
			{i | i:ProdName :- all ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ k>0}
			pre St~={},

	/*Количество всех наименований товаров, присутствующих на на складе*/

		qtyAllProdName: Stock -~-> Nat
		qtyAllProdName(St) is
			card setAllProdName(St)
			pre St~={},

	/*Множество всех производителей, присутствующих на складе*/

		setAllCompName: Stock -~-> CompName-set
		setAllCompName(St) is
			{j | j: CompName :- all ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ k>0}
			pre St~={},

	/*Количество всех производителей, присутствующих на складе*/

		qtyAllCompName: Stock -~-> Nat
		qtyAllCompName(St) is
			card setAllCompName(St)
			pre St~={},

	/*Вспомогательная функция, проверяющая наличие не меньшего количества конкретного товара на данной полке, возвращает это не меньшее количество, а иначе 0*/

		IsGreat: ProdInfo >< Stock -~-> QTY
		IsGreat((P,k,l),St) is
			if (exists (P,c,l):ProdInfo :- (P,c,l) isin St /\ c>=k) then qtyhelp((P,k,l),St)(1)
				else 0
			end
			pre IsInit(P,forPlace(l,St)),

	/*Вспомогательная функция возвращает список неменьших количеств конкретных товаров на данной полке*/

		qtyhelp: ProdInfo >< Stock -> QTY-list
		qtyhelp((P,k,l),St) is
			<.q | q in Stock_to_list(forPlace(l,forProduct(P,St))) :- q>=k.>,

	/*Добавление данного количества конкретного продукта на склад*/
		
		addToStock: ProdInfo >< Stock -~-> Stock
		addToStock((P,k,l),St) is
			if (IsInit(P,forPlace(l,St))) then St\{(P,qk,l) | (P,qk,l): ProdInfo :- qk=IsGreat((P,0,l),St)} union {(P,newqty,l) | (P,newqty,l):ProdInfo :- newqty=k+IsGreat((P,0,l),St)}
				else St union {(P,k,l)}
			end
			pre IsInit(P,St) /\ k>0 /\ l>0,

	/*Изъятие данного количества конкретного продукта со склада*/

		deleteFromPlace: ProdInfo >< Stock -~-> Stock
		deleteFromPlace((Prod,k,l),St) is
			if (k<IsGreat((Prod,k,l),St)) then St\{(Prod,c,l) | (Prod,c,l): ProdInfo :- c=IsGreat((Prod,0,l),St)} union {(Prod,newqty,l) | (Prod,newqty,l):ProdInfo :- newqty=IsGreat((Prod,k,l),St)-k}
				else St\{(Prod,k,l)} union {(Prod,0,0)}
			end
			pre k<=IsGreat((Prod,k,l),St) /\ k>0 /\ l>0,

	/*Изменение местоположения данного количества конкретного товара на складе*/

		changePlaceofProduct: ProdInfo >< Place >< Stock -~-> Stock
		changePlaceofProduct((Prod,k,l),PL,St) is
			if (IsGreat((Prod,0,PL),St)>=0) then deleteFromPlace((Prod,k,l),St) union addToStock((Prod,k,PL),St)
				else deleteFromPlace((Prod,k,l),St) union {(Prod,k,PL)}
			end
			pre IsGreat((Prod,0,l),St)>=k /\ k>0 /\ PL>0,

	/*Вспомогательная функция, формирующая список полок, на которых лежит данный конкретный товар*/

		listOFPlaces: Product >< Stock -> Place-list
		listOFPlaces(P,St) is
			<.n | n in allNaturalNumbers :- all (P,y,z): ProdInfo :- (P,y,z) isin St /\ n=z.>,

	/*Вспомогательная фунция, список из одного элемента, равного количеству данного продукта, лежащего на существующей полке*/

		placeQTY: Product >< Stock -> QTY-list
		placeQTY(P,St) is
			<.n | n in allNaturalNumbers :- all (P,y,z): ProdInfo :- (P,y,z) isin St /\ z= hd listOFPlaces(P,St) /\ n=y.>,

	/*Продажа конкретного продукта*/

		deleteFromStock: Product >< QTY >< Stock -~-> Stock
		deleteFromStock(P,QT,St) is
			if (exists (P,y,z): ProdInfo :- (P,y,z) isin St /\ z=hd listOFPlaces(P,St) /\ y>QT) then St\{(P,n,m) | (P,n,m): ProdInfo :- (P,n,m) isin St /\ m=hd listOFPlaces(P,St)} union {(P,hd placeQTY(P,St)-QT,hd listOFPlaces(P,St))}
				elsif (exists (P,QT,z):ProdInfo :- (P,QT,z) isin St /\ z=hd listOFPlaces(P,St)) then if (exists (P,y,z): ProdInfo :- (P,y,z) isin St /\ z~=hd listOFPlaces(P,St)) then St\{(P,QT,z) | (P,QT,z): ProdInfo :- z=hd listOFPlaces(P,St)}
					else St\{(P,QT,z) | (P,QT,z): ProdInfo :- z=hd listOFPlaces(P,St)} union {(P,0,0)}
				end
			else deleteFromStock(P,QT-hd placeQTY(P,St),St\{(P,x,y) | (P,x,y): ProdInfo :- (P,x,y) isin St /\ x=hd placeQTY(P,St) /\ y=hd listOFPlaces(P,St)})
			end
			pre qtyofProduct(P,St)>=QT

	end