proposition: Lemma filter_negb_Prefix : forall (b : BagType) m st l search_term', TrieOK (Node b m) l -> Prefix l st -> Permutation (List.filter (fun a => negb (bfind_matcher search_term' a)) (benumerate b)) (List.filter (fun a => negb (TrieBag_bfind_matcher (Some st, search_term') a)) (benumerate b)).
proof: Proof. intros; inversion H; subst. revert H0 H5; clear. induction (benumerate b); simpl; eauto. unfold TrieBag_bfind_matcher; simpl. intros; case_eq (Prefix_dec F.eq_dec (projection a) st); simpl; intros. find_if_inside; simpl; rewrite IHl0; eauto. assert (Prefix (projection a) l) by (eexists nil; rewrite app_nil_r; eauto). destruct n. rewrite H1; apply H0. Qed.
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