proposition: Theorem CausallyConsistent: forall (p: Syntax.PProg)(h: list N.CExec.Label), N.CExec.history (N.CExec.init p) h -> exists (h': list AExec.Label), AExec.history (AExec.init p) h' /\ N.CExec.ext_hist h = AExec.ext_hist h'.
proof: Proof. intros. assert (A1 := ExecToInstExec.Refinement). specex_deprem A1. eassumption. destruct A1 as [h' [A11 A12]]. assert (A2 := InstExecToAbsExec.Refinement). specex_deprem A2. eassumption. destruct A2 as [h'' [A21 A22]]. exists h''. split. assumption. eapply eq_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)