RecurrenceLaws.no_wrapping: law of bend-kit-scheduler@0.4.1.0 Import: import bend-kit-scheduler@0.4.1.0/recurrence_laws.bend as RecurrenceLaws Lines 65-69 of bend-kit-scheduler@0.4.1.0/recurrence_laws.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-scheduler@0.4.1.0/recurrence_laws.bend&start_line=65&end_line=69 import Base # Addition is monotone on arbitrary Nat: deadlines never wrap below their origin. law no_wrapping: for +origin: Nat for period: Nat {Nat.is_le(origin, Nat.add(origin, period)) == True{} : Bool} Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_add_right