law replay_tick_due

bend-kit-scheduler@0.4.1.0 · recurrence_laws.bend:71

import Base

71# For any one-based index in the exact replay prefix, its anchored tick is due.
72law replay_tick_due:
73  for +previous: Nat
74  for +completion: Nat
75  for +p: Nat
76  for +bound: Nat
77  for +i: Nat
78  for h: {Nat.is_le(previous, completion) == True{} : Bool}
79  for hi: {Nat.is_le(i, Nat.min(bound,
80    Nat.div(Nat.sub(completion, previous), 1n+p))) == True{} : Bool}
81  {Nat.is_le(Nat.add(previous, Nat.mul(i, 1n+p)), completion) == True{} : Bool}