(***************************************************************************)
(* Given a sequence s = <<S1, ..., Sn>> of sets, Cartesian(s) computes the *)
(* n-ary Cartesian product of these sets, i.e. the set of all sequences *)
(* whose i-th element belongs to the set Si. For example, *)
(* Cartesian(<<{1,2}, {"a", "b"}, {{}}>>) = *)
(* {<<1, "a", {}>>, <<1, "b", {}>>, <<2, "a", {}>>, <<2, "b", {}>>} *)
(***************************************************************************)
RECURSIVE Cartesian(_)
Cartesian(s) ==
IF s = << >> THEN { << >> }
ELSE LET C == Cartesian(Tail(s))
AllCons(seq) == { <<x>> \o seq : x \in Head(s) }
IN UNION { AllCons(seq) : seq \in C }