proposition: Lemma check_all_schedules'_correct: forall max_steps check s, check_all_schedules' nids max_steps s check = true -> forall task sched ls l' s' s'', valid_schedule nids (sched++[task]) -> List.length sched < max_steps -> step_star_fun nil sched s = Some (ls, s') -> step_fun task s' = Some (l', s'') -> check l' s'' = true.
proof: Proof. Proof using max_nid_eq. intros. eapply check_all_schedules'_correct_fun_equiv; eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)