fact: Definition guard_method (n: NId)(this: @State Val)(k: Key)(v: Val)(u: @Update Val): bool := let s := store this in let c := clock this in let n' := sender_node u in let c' := sender_clock u in ((c' n') =? ((c n') + 1)) && (fold_left (fun b n => b && ((n =? n') || ((c' n) <=? (c n)))) nids true).
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)