# Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes.

1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal quantification such as:

∀x : ran routes • ( #x>20 ∧ x ≠ x')

However i'm really not sure if thats correct that implying 20 different places.

If you say

$$\forall x, x': ran\ routes . x<>x'$$

You're only saying that the sequences are different. For example

$$$$ would be different to $$$$

$$\forall x: ran\ routes . \#x>20$$
$$\forall p,p': Place • p \in ran\ (ran\ routes) \land p' \in ran\ (ran\ routes) \implies p<>p'$$
One for the length as you had and one for the condition that all elements must be unique. Note the double $$ran$$ expression since a sequence is defined as a function between its indexes and its values (the range).