[
  " NG<4½¬Ib\u0002\u0010é%ödœ",
  [
    [
      "Vale.AES.GHash.fun_seq_quad32_LE_poly128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "int_inversion", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303"
      ],
      0,
      "c9b8f16b3933ea1397c886f722130ab6"
    ],
    [
      "Vale.AES.GHash.ghash_poly",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
        "int_typing", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
      ],
      0,
      "ce8e399243d6dd27f85e0a7ccc1f8bb3"
    ],
    [
      "Vale.AES.GHash.lemma_g_power_n",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "cc36d6e34587d5c6bdd37db25ff66613"
    ],
    [
      "Vale.AES.GHash.hkeys_reqs_priv",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "f6f2e8231c37ec3e18394ad53fc16e6a"
    ],
    [
      "Vale.AES.GHash.ghash_unroll",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "ee7ca42919174527b91f8a2f4741a3df"
    ],
    [
      "Vale.AES.GHash.ghash_unroll_back",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3310e3e1980be82b030d7723ed022cf9"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_back_forward",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "6d81d0679fa880cf1637845130697141"
    ],
    [
      "Vale.AES.GHash.lemma_add_manip",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e7b45d20bd30ec1c886000fbbd179d16"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
      ],
      0,
      "658647d510b292df85998a735cec3771"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5268820afc0120b9bfa0ea44ea57c047"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_to_ghash",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "d1f9aa7280fe7672fad073020a0fb106"
    ],
    [
      "Vale.AES.GHash.lemma_hash_append3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "c534e9a40e7040d3f948a244a33a9fee"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "33f96c2b9e3c50580f11114e88eae622"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes"
      ],
      0,
      "d767b029a80338c90909b7e1030ca811"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes"
      ],
      0,
      "9c4e6883b5531fc613c6cd9b1f472b45"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_registers",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "int_inversion", "l_and-interp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "6f1897f5d39cd5bd8e3ca61b278ebed2"
    ]
  ]
]