proposition: Lemma AlignedDecode_assoc {A B C : Type} (decode_A : DecodeM (A * ByteString) ByteString) (decode_B : A -> DecodeM (B * ByteString) ByteString) (decode_C : A -> B -> DecodeM (C * ByteString) ByteString) (aligned_decoder : forall numBytes : nat, AlignedDecodeM C numBytes) : DecodeMEquivAlignedDecodeM (fun bs cd => `(ab, bs', cd') <- (`(a, bs', cd') <- decode_A bs cd; `(b, bs', cd') <- decode_B a bs' cd'; Some (a, b, bs', cd')); decode_C (fst ab) (snd ab) bs' cd') aligned_decoder -> DecodeMEquivAlignedDecodeM (fun bs cd => `(a, bs', cd') <- decode_A bs cd; `(b, bs', cd') <- decode_B a bs' cd'; decode_C a b bs' cd') aligned_decoder.
proof: Proof. intros; eapply DecodeMEquivAlignedDecodeM_trans; eauto; intros; simpl; try reflexivity. simpl; destruct (decode_A b cd) as [ [ [? ?] ?] | ]; simpl; eauto. destruct (decode_B a b0 c) as [ [ [? ?] ?] | ]; simpl; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString