# Z Notation: sequence of sequences - find sum

Let me just say that this is for a university project. I do not expect an answer but more of a "hint".

I have a schema of a Supermarket that holds a sequence of queues:

+-- Supermarket-------
|queues: seq Queue
----------------------


And here is how I've defined a queue:

+-- Queue ----------
|length: ℕ
--------------------


I wish to define a schema that returns the total number of customers, waiting in line. Thus far I have:

+--TotalQueueCustomers----
|Ξsupermarket: Supermarket
|totalCustomers!: ℕ
|-------------------------
|totalCustomers = total θ supermarket
--------------------------


I'm struggling with defining the total function. It needs to "loop" every customer in every queue and sum their lengths. Here is what I have so far: total = q: Queue ⦁ q.length ↦ q.length

Any idea?

• I am unfamiliar with Z notation, but looking here I believe you can do something in the spirit of $\text{total } s = \text{if } s = \langle\rangle \text{ then } 0 \text{ else } (\text{head } s).\text{length} + (\text{total tail } s)$.
– orlp
Jan 4, 2021 at 3:59