fact: Definition put_method (n: NId)(this: State)(k: Key)(v: Val): (State * Update) := let s := store this in let c := clock this in let c' := override c n ((c n) + 1) in let s' := override s k v in ((state s' c'), (update Val n c')).
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)