proposition: Lemma addD_addD_plus : forall (cd : CacheDecode) (n m : nat), addD (addD cd n) m = addD cd (n + m).
proof: Proof. simpl; intros. destruct (fst cd); simpl; eauto. repeat (find_if_inside; simpl); eauto. f_equal; f_equal. rewrite !natToWord_plus. rewrite !natToWord_wordToNat. rewrite wplus_assoc; reflexivity. rewrite !natToWord_plus in l0. rewrite !natToWord_wordToNat in l0. exfalso. apply n0. rewrite <- (natToWord_wordToNat w) in l0. rewrite <- natToWord_plus in l0. rewrite wordToNat_natToWord_idempotent in l0. omega. apply Nomega.Nlt_in; rewrite Nnat.Nat2N.id, Npow2_nat; assumption. exfalso. apply n0. rewrite <- (natToWord_wordToNat w). rewrite !natToWord_plus. rewrite !wordToNat_natToWord_idempotent. rewrite <- natToWord_plus. rewrite !wordToNat_natToWord_idempotent. omega. apply Nomega.Nlt_in; rewrite Nnat.Nat2N.id, Npow2_nat; assumption. apply Nomega.Nlt_in; rewrite Nnat.Nat2N.id, Npow2_nat; omega. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Strings.String Coq.Arith.Mult Fiat.Common Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Formats.DomainNameOpt Bedrock.Word