proposition: Lemma resourceRecordOK_3 : forall rr : resourceRecord, resourceRecord_OK rr -> ith (icons (B := fun T => T -> Prop) (fun a : DomainName => ValidDomainName a) (icons (B := fun T => T -> Prop) (fun _ : Memory.W => True) (icons (B := fun T => T -> Prop) (fun a : DomainName => ValidDomainName a) (icons (B := fun T => T -> Prop) (fun a : SOA_RDATA => (True /\ (ValidDomainName a!"contact_email")) /\ ValidDomainName a!"sourcehost") inil)))) (SumType_index ResourceRecordTypeTypes rr!sRDATA) (SumType_proj ResourceRecordTypeTypes rr!sRDATA).
proof: Proof. Admitted. Hint Resolve resourceRecordOK_3 : data_inv_hints. Hint Resolve length_app_3 : data_inv_hints . Definition DNS_Packet_OK (data : packet) := lt (|data!"answers" |) (pow2 16) /\ lt (|data!"authority" |) (pow2 16) /\ lt (|data!"additional" |) (pow2 16) /\ ValidDomainName (data!"question")!"qname" /\ forall (rr : resourceRecord), In rr (data!"answers" ++ data!"additional" ++ data!"authority") -> resourceRecord_OK rr. Ltac decompose_parsed_data := repeat match goal with | H : (?x ++ ?y ++ ?z)%list = _ |- _ => eapply firstn_skipn_self in H; try eassumption; destruct H as [? [? ?] ] | H : WS _ WO = _ |- _ => apply (f_equal (@whd 0)) in H; simpl in H; rewrite H in *; clear H | H : length _ = _ |- _ => clear H end; subst. Lemma decides_resourceRecord_OK : forall l n m o, length l = n + m + o -> (forall x : resourceRecord, In x l -> resourceRecord_OK x) -> decides true (forall rr : resourceRecord, In rr (firstn n l ++ firstn m (skipn n l) ++ firstn o (skipn (n + m) l)) -> resourceRecord_OK rr). Proof. simpl; intros. rewrite firstn_skipn_self' in H1; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.Common.StringFacts Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedSumType Fiat.Narcissus.BinLib.AlignedDomainName Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.HintDbExtra Fiat.Common.Tactics.TransparentAbstract Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.Automation.CacheEncoders Bedrock.Word