proposition: Lemma Start_CorrectDecoderFor {S T} {cache : Cache} {monoid : Monoid T} Invariant FormatSpec (decoder decoder_opt : T -> CacheDecode -> option (S * T * CacheDecode)) (cache_inv : CacheDecode -> Prop) (P_inv : (CacheDecode -> Prop) -> Prop) (decoder_OK : cache_inv_Property cache_inv P_inv -> CorrectDecoder monoid Invariant Invariant eq FormatSpec decoder cache_inv FormatSpec) (cache_inv_OK : cache_inv_Property cache_inv P_inv) (decoder_opt_OK : forall b cd, decoder b cd = decoder_opt b cd) : @CorrectDecoderFor S T cache monoid Invariant FormatSpec.
proof: Proof. exists (decoder_opt, cache_inv); exists P_inv; split; simpl; eauto. unfold CorrectDecoder in *; intuition; intros. - destruct (H1 _ _ _ _ _ ext env_OK H0 H3 H4). rewrite decoder_opt_OK in H5; eauto. - rewrite <- decoder_opt_OK in H4; destruct (H2 _ _ _ _ _ _ H0 H3 H4); eauto. - rewrite <- decoder_opt_OK in H4; destruct (H2 _ _ _ _ _ _ H0 H3 H4); eauto. Defined.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache