proposition: Lemma put_nochange: forall (s s': State)(l: Label), let n := label_node l in let k := label_key l in let m := store (alg_state (node_states s n)) in let m' := store (alg_state (node_states s' n)) in (step s l s' /\ label_is_put l) -> (forall k', (not (k = k')) -> m k' = m' k').
proof: Proof. intros. open_conjs. inversion H. subst m. subst m'. subst s. subst s'. simpl. destruct (eq_nat_dec n n0). simpl_override. simpl_override. simpl. subst k. rewrite <- H4 in H0. simpl in H0. simpl_override. reflexivity. simpl_override. simpl_override. reflexivity. rewrite <- H4 in H1; unfold label_is_put in H1; inversion H1. rewrite <- H5 in H1; unfold label_is_put in H1; inversion H1. rewrite <- H4 in H1; unfold label_is_put in H1; inversion H1. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)