proposition: Lemma CorrectRefinedDecoder_decode_impl {S T : Type} {store : Cache} (monoid' : Monoid T) (Source_Predicate : S -> Prop) (format : FormatM S T) (decode : T -> CacheDecode -> option (S * T * CacheDecode)) (decode_inv : CacheDecode -> Prop) : CorrectRefinedDecoder monoid' Source_Predicate Source_Predicate eq format format decode decode_inv format -> CorrectDecoder monoid' Source_Predicate Source_Predicate eq format decode decode_inv format.
proof: Proof. intros. eapply weaken_view_pred. intros; subst; eauto. 2: apply H. intros. simpl in H1; intuition eauto. Qed.
imports: Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.Base.SequenceFormat Fiat.Narcissus.Formats.Base.FMapFormat Fiat.Narcissus.Formats.Base.StrictTerminalFormat Fiat.Narcissus.Formats.Base.LaxTerminalFormat Fiat.Narcissus.Formats.Base.FixFormat Fiat.Narcissus.Formats.Base.EnqueueFormat Fiat.Narcissus.Formats.Base.UnionFormat