proposition: Lemma prove_no_fault': forall program h s n run_steps, StepStar.step_star (init program) h s -> (forall sched_length, check_all_schedules' nids (run_steps + sched_length) (init program) check_no_fault' = true) -> (forall l, List.In l h -> l <> fault_label n).
proof: Proof. Proof using max_nid_eq. intros program h s n run_steps Hss Hcheck_scheds. generalize (step_star_not_in_nids _ _ _ n Hss); intro Hnot_nids_eq. apply step_star_fun_complete in Hss. destruct Hss as [sched Hss]. intros l Hin. apply List.in_split in Hin. destruct Hin as [h1[h2 Heq]]; subst h. apply step_star_fun_app_inv in Hss. destruct Hss as [sched1[s'[sched2'[Heq[Hss1 Hss2]]]]]; subst sched. apply step_star_fun_cons_inv in Hss2. destruct Hss2 as [task[s''[sched2[Heq[Hs Hss2]]]]]; subst sched2'. eapply check_all_schedules'_correct with (check:=check_no_fault') (max_steps:= run_steps + (S (List.length sched1))) in Hss1; eauto. * unfold check_no_fault' in Hss1. destruct l; try discriminate. * eapply valid_schedule_step_star_fun with (ls1:=nil) (sched:=(sched1++[task])%list) (prog0:=program); eauto. rewrite step_star_fun_app, Hss1. simpl; rewrite Hs; reflexivity. * lia. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)