val parse_ifthenelse_eq (p: parse_ifthenelse_param) (input: bytes)
    : Lemma
    (parse (parse_ifthenelse p) input ==
      (match parse p.parse_ifthenelse_tag_parser input with
        | None -> None
        | Some (t, consumed_t) ->
          let b = p.parse_ifthenelse_tag_cond t in
          let input' = Seq.slice input consumed_t (Seq.length input) in
          match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
          | None -> None
          | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x)))
let parse_ifthenelse_eq
  (p: parse_ifthenelse_param)
  (input: bytes)
: Lemma
  (parse (parse_ifthenelse p) input == (
    match parse p.parse_ifthenelse_tag_parser input with
    | None -> None
    | Some (t, consumed_t) ->
      let b = p.parse_ifthenelse_tag_cond t in
      let input' = Seq.slice input consumed_t (Seq.length input) in
      match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
      | None -> None
      | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x)
  ))
= and_then_eq p.parse_ifthenelse_tag_parser (parse_ifthenelse_payload p) input;
  match parse p.parse_ifthenelse_tag_parser input with
  | None -> ()
  | Some (t, consumed_t) ->
      let b = p.parse_ifthenelse_tag_cond t in
      let input' = Seq.slice input consumed_t (Seq.length input) in
      let f : (p.parse_ifthenelse_payload_t (p.parse_ifthenelse_tag_cond t) -> GTot p.parse_ifthenelse_t) = (p.parse_ifthenelse_synth) t in
      let f' = coerce (p.parse_ifthenelse_payload_t b -> GTot p.parse_ifthenelse_t) f in
      parse_synth_eq
        #(dfst (p.parse_ifthenelse_payload_parser b))
        #(p.parse_ifthenelse_payload_t b)
        #(p.parse_ifthenelse_t)
        (dsnd (p.parse_ifthenelse_payload_parser b)) f' input'
val parse_ifthenelse_eq (p: parse_ifthenelse_param) (input: bytes)
    : Lemma
    (parse (parse_ifthenelse p) input ==
      (match parse p.parse_ifthenelse_tag_parser input with
        | None -> None
        | Some (t, consumed_t) ->
          let b = p.parse_ifthenelse_tag_cond t in
          let input' = Seq.slice input consumed_t (Seq.length input) in
          match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
          | None -> None
          | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x)))
let parse_ifthenelse_eq (p: parse_ifthenelse_param) (input: bytes)
    : Lemma
    (parse (parse_ifthenelse p) input ==
      (match parse p.parse_ifthenelse_tag_parser input with
        | None -> None
        | Some (t, consumed_t) ->
          let b = p.parse_ifthenelse_tag_cond t in
          let input' = Seq.slice input consumed_t (Seq.length input) in
          match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
          | None -> None
          | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x))) =
and_then_eq p.parse_ifthenelse_tag_parser (parse_ifthenelse_payload p) input;
match parse p.parse_ifthenelse_tag_parser input with
| None -> ()
| Some (t, consumed_t) ->
  let b = p.parse_ifthenelse_tag_cond t in
  let input' = Seq.slice input consumed_t (Seq.length input) in
  let f:(p.parse_ifthenelse_payload_t (p.parse_ifthenelse_tag_cond t) -> GTot p.parse_ifthenelse_t)
  =
    (p.parse_ifthenelse_synth) t
  in
  let f' = coerce (p.parse_ifthenelse_payload_t b -> GTot p.parse_ifthenelse_t) f in
  parse_synth_eq #(dfst (p.parse_ifthenelse_payload_parser b))
    #(p.parse_ifthenelse_payload_t b)
    #(p.parse_ifthenelse_t)
    (dsnd (p.parse_ifthenelse_payload_parser b))
    f'
    input'
LowParse.Spec.IfThenElse.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.IfThenElse.fst
LowParse.Spec.IfThenElse.parse_ifthenelse_param LowParse.Bytes.bytes LowParse.Spec.Base.parse LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_parser LowParse.Spec.Base.consumed_length LowParse.Spec.Combinators.parse_synth_eq FStar.Pervasives.dfst LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_parser LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_t FStar.Pervasives.dsnd LowParse.Spec.Base.coerce LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_cond LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_synth FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice FStar.Seq.Base.length Prims.bool Prims.unit LowParse.Spec.Combinators.and_then_eq LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_kind LowParse.Spec.IfThenElse.parse_ifthenelse_payload_kind LowParse.Spec.IfThenElse.parse_ifthenelse_payload Prims.l_True Prims.squash Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.IfThenElse.parse_ifthenelse FStar.Pervasives.Native.None FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.op_Addition Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.IfThenElse
include LowParse.Spec.Combinators

module Seq = FStar.Seq

[@@(noextract_to "krml")]
inline_for_extraction
noeq
type parse_ifthenelse_param = {
  parse_ifthenelse_tag_kind: parser_kind;
  parse_ifthenelse_tag_t: Type;
  parse_ifthenelse_tag_parser: parser parse_ifthenelse_tag_kind parse_ifthenelse_tag_t;
  parse_ifthenelse_tag_cond: (parse_ifthenelse_tag_t -> Tot bool);
  parse_ifthenelse_payload_t: (bool -> Tot Type);
  parse_ifthenelse_payload_parser: ((b: bool) -> Tot (k: parser_kind & parser k (parse_ifthenelse_payload_t b)));
  parse_ifthenelse_t: Type;
  parse_ifthenelse_synth: ((t: parse_ifthenelse_tag_t) -> (parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t)) -> GTot parse_ifthenelse_t);
  parse_ifthenelse_synth_injective: (
    (t1: parse_ifthenelse_tag_t) ->
    (x1: parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t1)) ->
    (t2: parse_ifthenelse_tag_t) ->
    (x2: parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t2)) ->
    Lemma
    (requires (parse_ifthenelse_synth t1 x1 == parse_ifthenelse_synth t2 x2))
              (ensures (t1 == t2 /\ coerce (parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t2)) x1 == x2))
  );
}

inline_for_extraction
let parse_ifthenelse_payload_kind
  (p: parse_ifthenelse_param)
: Tot parser_kind
= glb (dfst (p.parse_ifthenelse_payload_parser true)) (dfst (p.parse_ifthenelse_payload_parser false))

inline_for_extraction
let parse_ifthenelse_kind
  (p: parse_ifthenelse_param)
: Tot parser_kind
= and_then_kind p.parse_ifthenelse_tag_kind (parse_ifthenelse_payload_kind p)

let parse_ifthenelse_synth_injective (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t) : Lemma (synth_injective (p.parse_ifthenelse_synth t)) [SMTPat (synth_injective (p.parse_ifthenelse_synth t))] =
  Classical.forall_intro_2 (fun x1 x2 -> Classical.move_requires (p.parse_ifthenelse_synth_injective t x1 t) x2)

let parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t) : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t) =
  weaken (parse_ifthenelse_payload_kind p) (parse_synth (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t))) (p.parse_ifthenelse_synth t))

let parse_ifthenelse_payload_and_then_cases_injective  (p: parse_ifthenelse_param) : Lemma
  (and_then_cases_injective (parse_ifthenelse_payload p))
  [SMTPat (and_then_cases_injective (parse_ifthenelse_payload p))]
= and_then_cases_injective_intro
    (parse_ifthenelse_payload p)
    (fun t1 t2 b1 b2 ->
      parse_synth_eq (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t1))) (p.parse_ifthenelse_synth t1) b1;
      parse_synth_eq (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t2))) (p.parse_ifthenelse_synth t2) b2;
      let Some (x1, _) = parse (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t1))) b1 in
      let Some (x2, _) = parse (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t2))) b2 in
      p.parse_ifthenelse_synth_injective t1 x1 t2 x2
    )

let parse_ifthenelse (p: parse_ifthenelse_param) : Tot (parser (parse_ifthenelse_kind p) p.parse_ifthenelse_t) =
  and_then p.parse_ifthenelse_tag_parser (parse_ifthenelse_payload p)

let parse_ifthenelse_eq
  (p: parse_ifthenelse_param)
  (input: bytes)
: Lemma
  (parse (parse_ifthenelse p) input == (
    match parse p.parse_ifthenelse_tag_parser input with
    | None -> None
    | Some (t, consumed_t) ->
      let b = p.parse_ifthenelse_tag_cond t in
      let input' = Seq.slice input consumed_t (Seq.length input) in
      match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
      | None -> None
      | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x)
val parse_ifthenelse_eq (p: parse_ifthenelse_param) (input: bytes)
    : Lemma
    (parse (parse_ifthenelse p) input ==
      (match parse p.parse_ifthenelse_tag_parser input with
        | None -> None
        | Some (t, consumed_t) ->
          let b = p.parse_ifthenelse_tag_cond t in
          let input' = Seq.slice input consumed_t (Seq.length input) in
          match parse (dsnd (p.parse_ifthenelse_payload_parser b)) input' with
          | None -> None
          | Some (x, consumed_x) -> Some (p.parse_ifthenelse_synth t x, consumed_t + consumed_x)))
p: LowParse.Spec.IfThenElse.parse_ifthenelse_param -> input: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.parse (LowParse.Spec.IfThenElse.parse_ifthenelse p) input ==
      (match
          LowParse.Spec.Base.parse (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p) input
        with
        | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
        | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ t consumed_t) ->
          let b = Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t in
          let input' = FStar.Seq.Base.slice input consumed_t (FStar.Seq.Base.length input) in
          (match
              LowParse.Spec.Base.parse (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        b))
                input'
            with
            | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
            | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed_x) ->
              FStar.Pervasives.Native.Some
              (Mkparse_ifthenelse_param?.parse_ifthenelse_synth p t x, consumed_t + consumed_x))
          <:
          FStar.Pervasives.Native.option (Mkparse_ifthenelse_param?.parse_ifthenelse_t p *
              LowParse.Spec.Base.consumed_length input)))