scheme algebr=
class
type 	
Author= Text,
Title = Text,
Available = Nat,
QTY= Nat,
Book = Title >< Author,
BookInfo = Book >< Available >< QTY,
Catalog = BookInfo-set,
Name = Text,
Surname = Text,
Reader = Name >< Surname,
BookList = Book-set,
ReaderInfo = Reader >< BookList,
Visitors = ReaderInfo-set,    
Library = Catalog >< Visitors
value
	Nats: Nat-inflist,
	EmptyCatalog: Catalog,
	EmptyVisitors: Visitors,
	EmptyBookList: BookList,
	EmptyLibrary: Library,
	IsBook: Book >< Library -> Bool,
	AddBook: Book >< Library >< Nat-> Library,
	GetAvailable: Book >< Library -> Available,
	GetQTY : Book >< Library -> QTY,
	IsReader : Reader >< Library -> Bool,
	AddReader : Reader >< Library -> Library,
	HaveABook: Book >< Reader >< Library -> Bool,
	BookInfoByBook: Book >< Library -> Catalog,
	ReaderInfoByReader: Reader >< Library -> Visitors,
	DeleteBook : Book >< Library >< Nat -> Library,
	GetReaderBooks : Reader >< Library -~-> BookList,
	DeleteReader : Reader >< Library -> Library,
	GiveBook: Book >< Reader >< Library -~-> Library,
	ReturnBook: Book >< Reader >< Library -~-> Library

axiom
	[Nats]
	Nats(1)=0,
	all i: Nat :- i>=2 => Nats(i)=Nats(i-1)+1,

	[EmptyCatalog] EmptyCatalog is {},

	[EmptyVisitors] EmptyVisitors is {},

	[EmptyBookList] EmptyBookList is {},

	[EmptyLibrary] EmptyLibrary is ({},{}),

	[IsBook]
	all b: Book, V: Visitors :- IsBook(b, (EmptyCatalog,V)) is false,
	all b,bx:Book, q:Nat, L:Library :- IsBook (b, AddBook(bx,L,q)) is
		if b=bx then
			true
		else
	 		IsBook (b,L)
		end,

	[GetAvailable]
	all b: Book, L: Library, V: Visitors :- GetAvailable(b, (EmptyCatalog,V)) is 0,
	all b,bx: Book, q: Nat, L: Library :- GetAvailable(b, AddBook(bx,L,q)) is
		if b=bx then
			GetAvailable(b, L)+q
		else
			GetAvailable(b, L)
		end,

	[GetQTY]
	all b: Book, L: Library, V: Visitors :- GetQTY(b, (EmptyCatalog,V)) is 0,
	all b,bx: Book, q: Nat, L: Library :- GetQTY(b, AddBook(bx,L,q)) is
		if b=bx then
			GetQTY(b, L)+q
		else
			GetQTY(b, L)
		end,

	[IsReader]
	all b: Book, r: Reader, C: Catalog :- IsBook(b, (C,EmptyVisitors)) is false,
	all r,rx: Reader, L: Library :- IsReader (r, AddReader(r,L)) is
		if r=rx then
			true
		else
			IsReader (r,L)
		end,
		
	[HaveABook]
	all b:Book, r:Reader, C:Catalog :- HaveABook(b,r,(C,EmptyVisitors)) is false,
	all b:Book, r,rx: Reader,bl:BookList, C :Catalog, V: Visitors :- 
	HaveABook (b,r,(C, V union {(rx,bl)})) is
	if r=rx then
		if b isin bl then 
			true
		else
			false
		end
	else
		HaveABook (b,r,(C, V))
	end
	pre (rx,bl) ~isin V,

	[BookInfoByBook]
	all b:Book, q:Nat, L:Library :- BookInfoByBook(b, EmptyLibrary) is EmptyCatalog,
	all b,bx:Book, q:Nat, L:Library :- BookInfoByBook(b, AddBook(bx,L,q)) is
		if b=bx then
			{(b, GetAvailable(b, L), GetQTY(b,L))}
		else
			BookInfoByBook(b,L)
		end
	pre IsBook(b,L),

	[ReaderInfoByReader]
	all r:Reader, (C,V):Library :- ReaderInfoByReader(r, (C, EmptyVisitors)) is EmptyVisitors,
	all r,rx: Reader, (C,V): Library :- ReaderInfoByReader(r, AddReader(rx,(C,V))) is
		if r=rx then
			{(r, GetReaderBooks(r,(C,V)))}
		else
			ReaderInfoByReader(r,(C,V))
		end
	pre IsReader(r,(C,V)),

	[AddBook]
	all b:Book, (C,V):Library, q:Nat :- AddBook(b,(C,V),q) is
	(C \ {(b,GetAvailable(b,(C,V)),GetQTY(b,(C,V)))} union {(b,GetAvailable(b,(C,V))+q,GetQTY(b,(C,V))+q)}, V),

	[DeleteBook]
	all b:Book, (C,V):Library, q:Nat :- DeleteBook(b,(C,V),q) is
	if  (q < GetAvailable (b,(C,V))) then
		(C \ {(b,GetAvailable(b,(C,V)),GetQTY(b,(C,V)))} union {(b,GetAvailable(b,(C,V))-q,GetQTY(b,(C,V))-q)}, V)
	else
		(C \ {(b,GetAvailable(b,(C,V)),GetQTY(b,(C,V)))} union {(b,0,GetQTY(b,(C,V))-GetAvailable(b,(C,V)))}, V)
	end
	pre GetQTY(b,(C,V)) >0 /\ q>0,
	
	[GetReaderBooks]
	all r:Reader, C:Catalog :- GetReaderBooks(r,(C,EmptyVisitors)) is EmptyBookList,
	all b:Book, r:Reader, (C,V): Library :- GetReaderBooks(r,(C,V)) is
	{b | b : Book :- HaveABook(b,r,(C,V))}
	pre IsReader(r,(C,V)),

	[AddReader]
	all r:Reader, (C,V):Library :- AddReader(r,(C,V)) is
	(C,V union {(r,{})})
	pre ~IsReader(r,(C,V)),

	[DeleteReader]
	all r:Reader, (C,V):Library :- DeleteReader(r,(C,V)) is
	(C, V \ { (r,GetReaderBooks(r,(C,V))) } )
	pre  IsReader (r,(C,V)) /\ GetReaderBooks(r,(C,V)) = {},

	[GiveBook]
	all r,R:Reader, b,B:Book, (C,V):Library :- GiveBook(b,r,(C,V)) is
	(C \ {(	b,GetAvailable(b,(C,V)), GetQTY(b,(C,V))) : BookInfo} union {(B,GetAvailable (B, (C,V))-1, GetQTY (B, (C,V))) : BookInfo}, V \ {(R,GetReaderBooks(R,(C,V))) : ReaderInfo} union {(r,GetReaderBooks(r, (C,V)) union {B | B : Book :- B=b}) : ReaderInfo})
	pre GetAvailable (b, (C,V)) >0  /\ IsReader(r, (C,V)) /\ b ~isin GetReaderBooks (r, (C,V)),

	[ReturnBook]
	all r,R:Reader, b,B:Book, (C,V):Library :- GiveBook(b,r,(C,V)) is
	(C \ {(	b,GetAvailable(b,(C,V)), GetQTY(b,(C,V))) : BookInfo} union {(B,GetAvailable (B, (C,V))+1, GetQTY (B, (C,V))) : BookInfo}, V \ {(R,GetReaderBooks(R,(C,V))) : ReaderInfo} union {(r,GetReaderBooks(r, (C,V)) union {B | B : Book :- B=b}) : ReaderInfo})
	pre IsReader(r, (C,V)) /\ b isin GetReaderBooks (r, (C,V))

end