proposition: Lemma cacheIndependent_add : forall (b : nat) (cd : CacheDecode), GoodCache cd -> GoodCache (addD cd b).
proof: Proof. unfold GoodCache; intros. rewrite IndependentCaches in *; eapply H in H0; intuition eauto. simpl in *. destruct (fst cd); simpl in *; try discriminate. find_if_inside; simpl in *; try discriminate. injections. pose proof (H4 _ (eq_refl _)). eapply lt_le_trans; eauto. rewrite !pointerT2Nat_Nat2pointerT in *; rewrite !wtl_div in *. rewrite wordToNat_natToWord_idempotent. apply NPeano.Nat.div_le_mono; omega. apply Nomega.Nlt_in. rewrite Nnat.Nat2N.id, Npow2_nat; auto. eapply (mult_lt_compat_l' _ _ 8); try omega. + eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. rewrite wordToNat_natToWord_idempotent. rewrite mult_pow2_8; simpl; omega. apply Nomega.Nlt_in. rewrite Nnat.Nat2N.id, Npow2_nat; auto. + eapply (mult_lt_compat_l' _ _ 8); try omega. eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. rewrite mult_pow2_8; simpl; omega. + eapply (mult_lt_compat_l' _ _ 8); try omega. eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. rewrite mult_pow2_8; simpl; omega. + eapply (mult_lt_compat_l' _ _ 8); try omega. eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. rewrite mult_pow2_8; simpl; omega. 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