proposition: Lemma check_all_schedules_correct: forall max_steps ls1 sched1 sched2 check s ls' s', valid_schedule nids sched2 -> List.length sched2 <= max_steps -> step_star_fun ls1 (sched1 ++ sched2)%list s = Some (ls', s') -> check_all_schedules nids max_steps ls1 sched1 s check = true -> check ls' 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)