Folgerung aus Spezifikation für Zählnetze

Satz: für jedes n > 0, S≥ 0 gibt es genau eine Schrittfolge [z₁,…, z_n] mit S = $\sum$z_i.

Satz: für jeden Zustand jedes Zählnetzes gilt:

• wenn $\sum$x_i - $\sum$y_i = D > 0

  (es befinden sich noch D Token im Netz),

• dann gilt ∀i : z_i - $\fbox{\phantom{D}} \le y_i \le z_i$

  wobei [z₁,…] die (eindeutige) Schrittfolge mit $\sum$z_i = $\sum$x_i

Folgerung: auch wenn der Ruhezustand nie eintritt, sind die Ausgänge gut verteilt

(hoher Durchsatz $\implies$ kleines D $\implies$ gute Verteilung)