proposition: Corollary refine_no_usurp_authority_check'_dns : forall (rr : resourceRecord) r_o r_n, @DropQSConstraints_AbsR DnsSchema r_o r_n -> refine {b | decides b (forall tup' : IndexedElement, (GetUnConstrRelation r_n Fin.F1) tup' -> RDataTypeToRRecordType (indexedElement tup')!sRDATA = NS -> RDataTypeToRRecordType rr!sRDATA <> NS -> prefix (indexedElement tup')!sNAME rr!sNAME -> (indexedElement tup')!sNAME = rr!sNAME)} (If (beq_RRecordType (RDataTypeToRRecordType rr!sRDATA) NS) Then (ret true) Else (count <- Count For (UnConstrQuery_In r_n Fin.F1 (fun tup => Where (RDataTypeToRRecordType tup!sRDATA = NS /\ prefix (tup!sNAME) (rr!sNAME) /\ tup!sNAME <> rr!sNAME) Return () )%QueryImpl); ret (beq_nat count 0))).
proof: Proof. intros; rewrite refine_no_usurp_authority_check'. setoid_rewrite (@refine_Count_map DnsSchema Fin.F1 r_n). reflexivity. apply DecideableEnsemble_And. intros; eapply (DropQSConstraints_AbsR_SatisfiesTupleConstraints H Fin.F1); eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema