proposition: Lemma clock_self_lte_received: forall p h s l, let n := label_node l in (step_star (init p) h s /\ label_is_put l /\ In l h) -> label_clock l <= received (alg_state (node_states s n)) n.
proof: Proof. intros. destruct H as [H1 [H2 H3]]. assert (A1 := in_exec h (init p) s l). depremise A1. split; assumption. destruct A1 as [h1 [s1 [s2 [h2 [A11 [A12 [A13 A14]]]]]]]. assert (A2: label_clock l = clock_state (node_states s2 n)). destruct l; simpl in *; try contradiction; clear H2. inversion A13. simpl. subst n. simpl_override. simpl. reflexivity. assert (A3 := sem_clock_alg_state_clock p (h1++[l]) s2 n). simpl in A3. depremise A3. apply step_star_app_one. exists s1. split; assumption. assert (A4 := rec_eq_clock p (h1++[l]) s2 n). simpl in A4. depremise A4. apply step_star_app_one. exists s1. split; assumption. assert (A5 := rec_inc p (h1++[l]) s2 h2 s n n). depremise A5. split. apply step_star_app_one. exists s1. split; assumption. assumption. rewrite A2. rewrite A3. rewrite <- A4. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)