proposition: Lemma received_lt_sent: forall p h s n n', let sn := alg_state (node_states s n) in let sn' := alg_state (node_states s n') in step_star (init p) h s -> received sn n' <= clock sn'.
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst sn. subst sn'. subst s. simpl. apply Nat.le_refl. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H0. subst sn. subst sn'. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl_override. simpl. reflexivity. simpl_override. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. eapply Nat.le_trans, Nat.le_add_r. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl_override_in IHstep_star. assumption. subst sn. subst sn'. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst sn. subst sn'. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. destruct (eq_nat_dec (sender_node u) n'). simpl_override. assert (A1 := message_clock_le_state_clock p ls s2 (message n'0 c' k v u n0 lp)). simpl in A1. depremise A1. split. subst s1. assumption. rewrite <- H3. apply in_app_iff. right. apply in_eq. rewrite <- H3 in A1. simpl in A1. assert (A2 := message_update_node_clock_eq p ls s2 (message n'0 c' k v u n0 lp)). simpl in A2. depremise A2. split. subst s1. assumption. rewrite <- H3. apply in_app_iff. right. apply in_eq. destruct A2 as [A21 A22]. rewrite A21 in A1. rewrite e0 in A1. rewrite A22 in A1. destruct (eq_nat_dec n0 n'). rewrite e1 in A1. simpl_override. simpl. simpl_override_in A1. simpl in A1. assumption. simpl_override. simpl. simpl_override_in A1. simpl in A1. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 n'). rewrite e0 in IHstep_star. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. destruct (eq_nat_dec n0 n'). rewrite e0 in IHstep_star. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. subst sn. subst sn'. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)