proposition: Corollary CorrectDecoderNone_dec_Source_Predicates (monoid : Monoid T) {V} : forall (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (Source_Predicate_dec : forall a, Source_Predicate a \/ ~ Source_Predicate a) (format : FormatM) (decode : _) (decode_inv : CacheDecode -> Prop) view_format, CorrectDecoder _ Source_Predicate View_Predicate view format decode decode_inv view_format -> forall b b' s_d, decode_inv s_d -> decode (mappend b b') s_d = None -> forall a , (~ Source_Predicate a) \/ forall s_e s_e', Equiv s_e s_d -> format a s_e ∌ (b, s_e').
proof: Proof. intros. destruct (Source_Predicate_dec a); intuition. right; intros; eapply CorrectDecoderNone; eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache