fact: Definition assignableUnion (fullSpecs : list FULL_SPEC_CASE.t) : option (optional StoreRefList) := let fullSpecsNR := filter (fun fs => negb (FULL_SPEC_CASE.isRedundant fs)) fullSpecs in let assignableLists := flat_map (fun fs => assignableList (FULL_SPEC_CASE.genericSpecCase fs)) fullSpecsNR in mergeAssignable assignableLists.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)