proposition: Lemma AlignedDecode_ifb_dep {A : Type} (decode_T decode_E : DecodeM (A * ByteString) ByteString) (cond : ByteString -> bool) (cond' : forall sz, ByteBuffer.t sz -> nat -> bool) (aligned_decoder_T aligned_decoder_E : forall numBytes : nat, AlignedDecodeM A numBytes) (cond'OK : forall sz (v : Vector.t _ sz), cond (build_aligned_ByteString v) = cond' _ v 0) (cond'OK2 : forall sz v idx, cond' (S sz) v (S idx) = cond' _ (Vector.tl v) idx ) : DecodeMEquivAlignedDecodeM decode_T aligned_decoder_T -> DecodeMEquivAlignedDecodeM decode_E aligned_decoder_E -> DecodeMEquivAlignedDecodeM (fun bs cd => if cond bs then decode_T bs cd else decode_E bs cd) (fun sz v idx => if cond' sz v idx then aligned_decoder_T sz v idx else aligned_decoder_E sz v idx).
proof: Proof. split. intros. rewrite cond'OK2. destruct (cond' numBytes_hd (Vector.tl v)) eqn: ? ; try eapply H; try eapply H0; try reflexivity. split; intros. destruct (cond b). eapply H; eauto. eapply H0; eauto. rewrite cond'OK. simpl; destruct (cond' n v); simpl; split; intros. eapply H; eauto. eapply H; eauto. eapply H0; eauto. eapply H0; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word