proposition: Lemma cacheIndependent_add_13 : forall (env : CacheDecode) (p : pointerT) (domain : string) (H : GoodCache env) (H0 : ValidDomainName domain /\ (String.length domain > 0)%nat) (H1 : getD env p = None) (H2 : forall p' : pointerT, peekD env = Some p' -> lt (pointerT2Nat p) (pointerT2Nat p')) (domain0 : string) (p0 : pointerT) (H3 : getD (addD_G env (domain, p)) p0 = Some domain0) (p' : pointerT), peekD (addD_G env (domain, p)) = Some p' -> lt (pointerT2Nat p0) (pointerT2Nat p').
proof: Proof. simpl; intros. destruct (fst env) eqn: ?; simpl in *; try discriminate. find_if_inside; subst. - injections. apply (H2 _ (eq_refl _)). - injections. pose proof (H2 _ (eq_refl _)). unfold GoodCache in *; intuition. eapply H; simpl. eassumption. eassumption. rewrite Heqo; simpl; reflexivity. 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.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core 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.DNSPacket Bedrock.Word