fact: Definition ValidDomainName s := (forall pre label post, s = pre ++ label ++ post -> ValidLabel label -> String.length label <= 63)%string%nat /\ (forall pre post, s = pre ++ "." ++ post -> post <> EmptyString /\ pre <> EmptyString /\ (~ exists s', post = String "." s') /\ (~ exists s', pre = s' ++ ".")).
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt