A condensed specification of a multi-level marketing enterprise in the Z specification language is presented and a number of proof obligations that result from operations on the state is stated. The feasibility of using ...