fact: Definition CorrespondingFreshAssignables (p: Program) (asem : LocSet.t) (fsem : ObjSet.t) (arac: stack (Heap.t * LocSet.t)) (fresh : stack ObjSet.t) : Prop := forall loc, LocSet.In loc asem \/ (LocInObjSet loc fsem = true) <-> (forall n, (n < length arac)%nat -> (exists m, (m <= n /\ m < length fresh)%nat /\ LocSet.In loc (ObjSet2LocSet (nth m fresh ObjSet.empty))) \/ LocSet.In loc (UnfoldDatagroups p (fst (nth n arac (InitHeap,LocSet.empty))) (snd (nth n arac (InitHeap,LocSet.empty))))).
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)