Specify a car rental software system in the z notation. There are two categories of cars $$ small and large. Cars can be rented by members of the Car Rental Club $($KNA$)$ at preferential prices. After the third car rental, the user automatically becomes a member of KPA. For each category, cars are returned and rented on a first$-$in$,$ last$-$out basis. If a customer wants to rent a car from a category in which no cars are available, he rents a car from another category or does not rent a car.

A$)$ Specify the basic and initial state of the system.

Make a short robust version of the operations:

B$)$ renting a car from a customer with the desired car category by specifying the system response for the rented car and the rental value.

C$)$ filling in the members Club of rental cars.

D$)$ Current reference of the available cars available for rent, as well as their order.

E$)$ reference for a list of customers who have rented a car of a given category.