proposition: Lemma decode_word_lt : forall (b' : T) (cd : CacheDecode) (a : word (S sz)) (b1 : T) (cd' : CacheDecode), Ifopt decode_word' _ b' as decoded Then Some (decoded, addD cd (S sz)) Else None = Some (a, b1, cd') -> lt_B b1 b'.
proof: Proof. intros; destruct (decode_word' (S sz) b') as [ [? ?] | ] eqn: ? ; try eapply decode_word'_lt in Heqo; simpl in *; try (subst; discriminate). injections. unfold lt_B in *. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats