fact: Definition guard_method (n: NId)(this: @State Val)(k: Key)(v: Val)(u: @Update Val): bool := let r := received this in let d' := sender_dep u in (fold_left (fun b p => let n' := fst p in let c' := snd p in b && (c' <=? r n')) d' true).
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)