proposition: Lemma update_no_self_message: forall p h s m, step_star (init p) h s /\ In m (messages s) -> not (sender_node (msg_update m) = msg_receiver m).
proof: Proof. intros. destruct H as [H1 H2]. assert (A1 := message_update_node_clock_eq p h s m). simpl in A1. depremise A1. split; assumption. destruct A1 as [A1 _]. assert (A2 := no_self_message p h s m). depremise A2. split; assumption. rewrite A1 in A2. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)