fact: Definition QSEnv_Ax : GLabelMap.t (AxiomaticSpec QsADTs.ADTValue) := (GLabelMap.empty _) ### ("ADT", "WordList_new") ->> (QsADTs.WordListADTSpec.New) ### ("ADT", "WordList_delete") ->> (QsADTs.WordListADTSpec.Delete) ### ("ADT", "WordList_pop") ->> (QsADTs.WordListADTSpec.Pop) ### ("ADT", "WordList_empty") ->> (QsADTs.WordListADTSpec.Empty) ### ("ADT", "WordList_push") ->> (QsADTs.WordListADTSpec.Push) ### ("ADT", "WordList_copy") ->> (QsADTs.WordListADTSpec.Copy) ### ("ADT", "WordList_rev") ->> (QsADTs.WordListADTSpec.Rev) ### ("ADT", "WordList_length") ->> (QsADTs.WordListADTSpec.Length) ### ("ADT", "WTuple_new") ->> (QsADTs.WTupleADTSpec.New) ### ("ADT", "WTuple_delete") ->> (QsADTs.WTupleADTSpec.Delete) ### ("ADT", "WTuple_copy") ->> (QsADTs.WTupleADTSpec.Copy) ### ("ADT", "WTuple_get") ->> (QsADTs.WTupleADTSpec.Get) ### ("ADT", "WTuple_put") ->> (QsADTs.WTupleADTSpec.Put) ### ("ADT", "WTupleList_new") ->> (QsADTs.WTupleListADTSpec.New) ### ("ADT", "WTupleList_delete") ->> (QsADTs.WTupleListADTSpec.Delete) ### ("ADT", "WTupleList_copy") ->> (QsADTs.WTupleListADTSpec.Copy) ### ("ADT", "WTupleList_pop") ->> (QsADTs.WTupleListADTSpec.Pop) ### ("ADT", "WTupleList_empty") ->> (QsADTs.WTupleListADTSpec.Empty) ### ("ADT", "WTupleList_push") ->> (QsADTs.WTupleListADTSpec.Push) ### ("ADT", "WTupleList_rev") ->> (QsADTs.WTupleListADTSpec.Rev) ### ("ADT", "WTupleList_length") ->> (QsADTs.WTupleListADTSpec.Length) ### ("ADT", "WBagOfTuples0_new") ->> (QsADTs.WBagOfTuples0ADTSpec.New) ### ("ADT", "WBagOfTuples0_insert") ->> (QsADTs.WBagOfTuples0ADTSpec.Insert) ### ("ADT", "WBagOfTuples0_enumerate") ->> (QsADTs.WBagOfTuples0ADTSpec.Enumerate) ### ("ADT", "WBagOfTuples1_new") ->> (QsADTs.WBagOfTuples1ADTSpec.New) ### ("ADT", "WBagOfTuples1_insert") ->> (QsADTs.WBagOfTuples1ADTSpec.Insert) ### ("ADT", "WBagOfTuples1_find") ->> (QsADTs.WBagOfTuples1ADTSpec.Find) ### ("ADT", "WBagOfTuples1_enumerate") ->> (QsADTs.WBagOfTuples1ADTSpec.Enumerate) ### ("ADT", "WBagOfTuples2_new") ->> (QsADTs.WBagOfTuples2ADTSpec.New) ### ("ADT", "WBagOfTuples2_insert") ->> (QsADTs.WBagOfTuples2ADTSpec.Insert) ### ("ADT", "WBagOfTuples2_findBoth") ->> (QsADTs.WBagOfTuples2ADTSpec.FindBoth) ### ("ADT", "WBagOfTuples2_findFirst") ->> (QsADTs.WBagOfTuples2ADTSpec.FindFirst) ### ("ADT", "WBagOfTuples2_findSecond") ->> (QsADTs.WBagOfTuples2ADTSpec.FindSecond) ### ("ADT", "WBagOfTuples2_enumerate") ->> (QsADTs.WBagOfTuples2ADTSpec.Enumerate).
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW CertifiedExtraction.Extraction.QueryStructures.CallRules.CallRules CertifiedExtraction.Extraction.QueryStructures.Wrappers Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Bedrock.Platform.Facade.CompileUnit2 CertifiedExtraction.ADT2CompileUnit CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Extraction.QueryStructures.Decompose Bedrock.Memory Bedrock.Platform.Facade.DFModule Bedrock.Platform.Facade.CompileUnit2 Fiat.CertifiedExtraction.PureFacadeLemmas