fact: Fixpoint check_all_schedules' (nids: list SysPredefs.NId) (N: nat) s (check: Label -> State -> bool) {struct N} : bool := match N with | O => true | S N' => List.forallb (fun n1 => match step_fun (SchedProc n1) s with | Some (l', s') => check l' s' && check_all_schedules' nids N' s' check | None => true end && List.forallb (fun n2 => match step_fun (SchedUpdate n1 n2) s with | Some (l', s') => check l' s' && check_all_schedules' nids N' s' check | None => true end) nids) nids end%bool%list.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)