context Zug
  inv Kette_zuWeich:
  self.waggon->select(w: Waggon | w.vorgaenger->isEmpty)->size = 1

context Waggon
  inv VorgaengerImGleichenZug:
  (not self.vorgaenger->isEmpty) implies
    self.vorgaenger.zug = self.zug