fact: Definition FieldUpdateCheck (p : Program) (loc : Location) (st : State.t): Prop := forall n, (n < length st@fr@assignables)%nat -> (exists m, (m <= n /\ m < length st@fr@fresh)%nat /\ LocSet.In loc (ObjSet2LocSet (nth m st@fr@fresh ObjSet.empty))) \/ Assignable p st@bl loc (nth n st@fr@assignables (LocSet.empty,LocSet.empty)) = true.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)