proposition: Lemma update_dep: forall s s' l, (step s l s' /\ label_is_update l) -> let n' := label_orig_node l in let c' := label_clock l in let k := label_key l in let n := label_node l in let ls := label_pre_state l in let r := received ls in let ms := messages s in exists m, let mn' := msg_sender m in let mc' := msg_clock m in let mn := msg_receiver m in let u := msg_update m in let sd := sender_dep u in In m ms /\ n' = mn' /\ c' = mc' /\ n = mn /\ forall p, In p sd -> let n'' := fst p in let c'' := snd p in c'' <= r n''.
proof: Proof. intros. open_conjs. inversion H. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. exists (message n'0 c'0 k0 v u n0 lp). simpl. split_all. subst ms. subst s. simpl. apply in_app_iff. right. apply in_eq. subst n'. rewrite <- H4. simpl. reflexivity. subst c'. rewrite <- H4. simpl. reflexivity. subst n. rewrite <- H4. simpl. reflexivity. intros. unfold guard_method in H2. assert (A:= fold_left_and (NId*Clock) (sender_dep u) p0 (fun p => snd p <=? received s0 (fst p))). depremise A. split; assumption. simpl in A. bool_to_prop_in A. subst r. subst ls. subst l. simpl. assumption. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)