proposition: Lemma FaultFreedom: forall program h, CausallyContent program -> CExec.history (CExec.init program) h -> forall n l, List.In l h -> l <> CExec.fault_label n.
proof: Proof. unfold CausallyContent. intros program h HcauseContent Hrun. intros. apply CausallyConsistent in Hrun. destruct Hrun as [ls[Hrun Hhist_eq]]. unfold AExec.history in Hrun. destruct Hrun as [s' Hss]. unfold N.CExec.ext_hist, AExec.ext_hist in Hhist_eq. apply List.in_map with (f:=N.CExec.ext) in H. rewrite Hhist_eq in H. apply List.in_map_iff in H. destruct H as [l'[??]]. cut (l' <> AExec.fault_label n); intros. intro; subst l. simpl in H. apply H1. unfold AExec.ext in H. destruct l'; inversion H; clear H; subst; reflexivity. eapply HcauseContent with (ls:=ls); eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)