proposition: Lemma rec_inc: forall p h s1 h' s2 n n', (step_star (init p) h s1 /\ step_star s1 h' s2) -> received (alg_state (node_states s1 n)) n' <= received (alg_state (node_states s2 n)) n'.
proof: Proof. intros. destruct H as [H1 H2]. induction H2. apply Nat.le_refl. depremise IHstep_star. assumption. assert (A1: received (alg_state (node_states s2 n)) n' <= received (alg_state (node_states s3 n)) n'). clear IHstep_star. inversion H. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec n0 n'). subst n'. simpl_override. assert (A := rec_eq_clock p (h++ls) s2 n0). simpl in A. depremise A. apply step_star_app. exists s1. split; assumption. rewrite <- H3 in A. simpl in A. simpl_override_in A. simpl in A. rewrite A. rewrite Nat.add_comm. simpl. apply le_S. apply Nat.le_refl. simpl_override. apply Nat.le_refl. simpl. simpl_override. simpl_override. reflexivity. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. simpl_override. simpl. apply Nat.le_refl. simpl_override. simpl. simpl_override. apply Nat.le_refl. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec (sender_node u) n'). subst n'. simpl_override. assert (A1 := message_update_node_clock_eq p (h++ls) s2 (message n'0 c' k v u n0 lp)). simpl in A1. depremise A1. split_all. apply step_star_app. exists s1. split; assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. destruct A1 as [A11 A12]. rewrite <- A11. rewrite <- A12. assert (A2 := received_lt_message_clock p (h++ls) s2 (message n'0 c' k v u n0 lp) n0). simpl in A2. depremise A2. split_all. apply step_star_app. exists s1. split; assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. reflexivity. rewrite <- H4 in A2. simpl in A2. simpl_override_in A2. simpl in A2. apply Nat.lt_le_incl. assumption. simpl_override. apply Nat.le_refl. simpl_override. simpl. simpl_override. apply Nat.le_refl. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl_override. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)