proposition: Lemma received_plus_one_eq_message_clock: forall p h s l s', (step_star (init p) h s /\ step s l s' /\ label_is_update l) -> (let n := label_node l in let n' := label_orig_node l in (received (alg_state (node_states s n)) n') + 1) = msg_clock (label_message l).
proof: Proof. intros. simpl. destruct H as [N1 [N2 N3]]. destruct l; simpl in *; try contradiction; clear N3. assert (A0 := message_update_node_clock_eq). specex A0. simpl in A0. depremise A0. split_all. eassumption. inversion N2. simpl. apply in_app_iff. right. apply in_eq. destruct A0 as [A01 A02]. assert (A1 := update_sender_clock). specex_deprem A1. split_all. eassumption. eassumption. simpl. apply I. simpl in A1. assert (A2 := received_lt_message_clock). specex A2. simpl in A2. depremise A2. split_all. eassumption. inversion N2. simpl. apply in_app_iff. right. apply in_eq. inversion N2. simpl. reflexivity. rewrite <- A02 in A1. assert (A3: msg_sender m = n0). inversion N2. simpl. reflexivity. rewrite A3 in A2. clear A01 A02 A3. apply le_lt_eq_dec in A1. destruct A1. exfalso. rewrite Nat.add_comm in l. simpl in l. apply (proj1 (Nat.lt_succ_r _ _)) in l. apply Nat.lt_nge in A2. apply A2. assumption. symmetry. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)