[
  "�^���@.��\t�?�m�\f",
  [
    [
      "Test.Lowstarize.int_of_hex",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Test.Lowstarize.hex_digit",
        "equation_Test.Lowstarize.is_hex_digit",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_a5a95a381bd6ec23d6f192daa87c8658"
      ],
      0,
      "cca0197a073eb95884926b8deb7a84fb"
    ],
    [
      "Test.Lowstarize.as_uint8s",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "FStar.Char_pretyping_dc6ef56115bc91878da75a1e0625bb73",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_FStar.Tactics.Result.Failed",
        "constructor_distinct_FStar.Tactics.Result.Success",
        "constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Test.Lowstarize.is_hex_digit",
        "equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Test.Lowstarize.is_hex_digit",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Tactics.Result.Failed_a",
        "projection_inverse_FStar.Tactics.Result.Failed_exn",
        "projection_inverse_FStar.Tactics.Result.Failed_ps",
        "projection_inverse_FStar.Tactics.Result.Success_a",
        "projection_inverse_FStar.Tactics.Result.Success_ps",
        "projection_inverse_FStar.Tactics.Result.Success_v",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_6803d8bff25f2a1dabffd441303ed842",
        "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "token_correspondence_Test.Lowstarize.is_hex_digit",
        "typing_FStar.Char.char", "typing_FStar.List.Tot.Base.length",
        "typing_Prims.__proj__Cons__item__tl",
        "typing_Test.Lowstarize.is_hex_digit"
      ],
      0,
      "52bda653b0621f2cfc976314f61a5d6b"
    ],
    [
      "Test.Lowstarize.is_some",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "d937879f35be856b39d62eb14af462b9"
    ],
    [
      "Test.Lowstarize.must",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "978b142142ed11149d76492bb01d84ee"
    ],
    [
      "Test.Lowstarize.destruct_list",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
        "function_token_typing_Prims.string",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "469885e8bcc0ad0e3938911f81be045a"
    ],
    [
      "Test.Lowstarize.is_list",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
        "function_token_typing_Prims.string",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "3b95c3eda1b46c34447a1b32817867aa"
    ],
    [
      "Test.Lowstarize.destruct_tuple",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
        "function_token_typing_Prims.string",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "faf342508b85669559186d8d37eeb6a3"
    ],
    [
      "Test.Lowstarize.is_tuple",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Prims.list__uu___haseq", "equation_Prims.eqtype",
        "function_token_typing_Prims.string",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "55e3497ce575c185566ab7421ded95ff"
    ],
    [
      "Test.Lowstarize.destruct_hex",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
        "equation_FStar.Reflection.Data.argv", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_FStar.Reflection.Data.argv",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "44e85c427a760cc31f59b2189722380e"
    ],
    [
      "Test.Lowstarize.fresh",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_FStar.Tactics.Result.Success",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Test.Lowstarize.gensym",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.nat",
        "function_token_typing_Prims.string", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Tactics.Result.Success_a",
        "projection_inverse_FStar.Tactics.Result.Success_ps",
        "projection_inverse_FStar.Tactics.Result.Success_v",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Pervasives.Native.snd"
      ],
      0,
      "38090b1dea305aaa00910a8a1b73e83a"
    ],
    [
      "Test.Lowstarize.__proj__LB__item__b",
      1,
      2,
      1,
      [
        "@query", "proj_equation_Test.Lowstarize.LB_len",
        "projection_inverse_Test.Lowstarize.LB_len"
      ],
      0,
      "9f6ab04d27564901716a196eaf0be3f2"
    ],
    [
      "Test.Lowstarize.mk_gcmalloc_of_list",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Reflection.Data_pretyping_ee655bc751cef679bca813f86c407d6b",
        "bool_inversion", "constructor_distinct_FStar.Tactics.Result.Failed",
        "constructor_distinct_FStar.Tactics.Result.Success",
        "data_typing_intro_FStar.Reflection.Data.Tv_Unknown@tok",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "function_token_typing_FStar.Reflection.Types.term",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Tactics.Result.Failed_a",
        "projection_inverse_FStar.Tactics.Result.Failed_exn",
        "projection_inverse_FStar.Tactics.Result.Failed_ps",
        "projection_inverse_FStar.Tactics.Result.Success_a",
        "projection_inverse_FStar.Tactics.Result.Success_ps",
        "projection_inverse_FStar.Tactics.Result.Success_v",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "26642f25a46e30a5978d864cbfeed440"
    ],
    [
      "Test.Lowstarize.lowstarize_hex",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "equation_FStar.String.char", "equation_FStar.String.strlen",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Test.Lowstarize.is_hex_digit",
        "int_inversion", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_Test.Lowstarize.is_hex_digit",
        "typing_FStar.Char.char", "typing_FStar.List.Tot.Base.for_all",
        "typing_FStar.String.list_of_string", "typing_FStar.String.strlen"
      ],
      0,
      "9f1082114ec205adb08f818a4df4316e"
    ],
    [
      "Test.Lowstarize.lowstarize_expr",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_FStar.Tactics.Result.Failed",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "function_token_typing_FStar.Reflection.Types.sigelt",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_FStar.Tactics.Result.Failed_a",
        "projection_inverse_FStar.Tactics.Result.Failed_exn",
        "projection_inverse_FStar.Tactics.Result.Failed_ps",
        "typing_FStar.Pervasives.Native.uu___is_None",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "4e3bee3cf91f9a87aa85c376153ab509"
    ]
  ]
]