@[reducible, inline]

abbrev ShiftTransition (p : MidgardParameters) (schin schout : Scheduler.State.SchedulerDatum) : Bool

Equations

• ShiftTransition p schin schout = decide (schout.shift_start = schin.shift_start + p.shift_duration)

def OperatorsConcent (schDat : Scheduler.State.SchedulerDatum) (p : MidgardParameters) (i : InputInfo) : Bool

Equations

• One or more equations did not get rendered due to their size.