fact: Fixpoint Trie_delete' (trie : Trie) (search_term : SearchTermType) {struct trie} : (list TItem) * Trie := match trie with | Node bag tries => let (deletedItems, bag') := bdelete (TrieNode trie) search_term in let tries' := XMapfold (fun k tries (deleted : (list TItem) * _) => let (deletedItems', bag') := Trie_delete' tries search_term in let (deletedItems'', bags') := deleted in (deletedItems' ++ deletedItems'', XMap.add k bag' bags')) tries ([ ], XMap.empty _) in (deletedItems ++ fst tries', Node bag' (XMap.this (snd tries'))) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix