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.