proposition: Lemma format_const_sequence_correct {cache : Cache} {S V1 T : Type} {P : CacheDecode -> Prop} {P_inv1 P_inv2 : (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_inv1 P /\ P_inv2 P)) (monoid : Monoid T) (v1 : V1) (Source_Predicate : S -> Prop) (View_Predicate1 : V1 -> Prop) (format1 : FormatM V1 T) (format2 : FormatM S T ) (decode1 : DecodeM (V1 * T) T) (decode_1_OK : cache_inv_Property P P_inv1 -> CorrectDecoder monoid View_Predicate1 View_Predicate1 eq format1 decode1 P format1) (v1_OK : View_Predicate1 v1) (decode2 : DecodeM (S * T) T) (decode2_pf : forall v0, cache_inv_Property P P_inv2 -> View_Predicate1 v0 -> CorrectDecoder monoid (fun s : S => Source_Predicate s /\ v1 = v0) (fun s : S => Source_Predicate s /\ v1 = v0) eq format2 decode2 P format2) : CorrectDecoder monoid Source_Predicate Source_Predicate eq (format1 ◦ (fun _ => v1) ++ format2) (sequence_Decode decode1 (fun _ => decode2)) P (format1 ◦ (fun _ => v1) ++ format2).
proof: Proof. unfold IsProj in *. eapply format_sequence_correct; eauto. Qed.
imports: Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Computation.Refinements.General Fiat.Narcissus.BaseFormats