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