proposition: Lemma put_change: forall (s s': State)(l: Label), let n := label_node l in let c := label_clock l in let k := label_key l in let m' := store (alg_state (node_states s' n)) in let iv := m' k in (step s l s' /\ label_is_put l) -> (inst_val_nid iv = n /\ inst_val_clock iv = c).
proof: Proof. intros. destruct H as [H1 H2]. inversion H1. clear H2. subst iv. subst m'. subst s'. simpl. subst n. subst c. subst k. subst l. simpl. simpl_override. simpl. simpl_override. simpl. split; reflexivity. rewrite <- H3 in H2; unfold label_is_put in H2; inversion H2. rewrite <- H4 in H2; unfold label_is_put in H2; inversion H2. rewrite <- H3 in H2; unfold label_is_put in H2; inversion H2. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)