[
  ";��\u0015��V\u000f�} ����\u000f",
  [
    [
      "Vale.Arch.Types.lemma_nat_to_two32",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "int_typing",
        "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6047cea221b106e5c2867c7976231d3f"
    ],
    [
      "Vale.Arch.Types.lo64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "6f7102c799cb7ac452d970a9f770838f"
    ],
    [
      "Vale.Arch.Types.hi64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "3a5bf994e2a7994814cdd66f63583499"
    ],
    [
      "Vale.Arch.Types.lemma_equality_check_helper_2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "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",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "primitive_Prims.op_Equality",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "aa1be585804629813a9fd5ecab923ee6"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "14e7c06e5df6cf05003a530c105e7fce"
    ],
    [
      "Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
      ],
      0,
      "ed9ccf4e2fc04b500c56c16236e8df73"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "f77c9f7e3ebcc9d672c9c0a3a5ef29ea"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "f9e7e3e95b3687e45b2fb24d2f731111"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "32d43ff2597f0885fc7e9804c4635442"
    ],
    [
      "Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
      ],
      0,
      "50b86162ff10bbda4c169b36ee22d652"
    ],
    [
      "Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
      ],
      0,
      "2261aa1f57a90fc08ce5fdfa235af2ef"
    ],
    [
      "Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "a92851ab2eb4175fad5a93d1edb42593"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
      ],
      0,
      "4cb5592fe07d545cf70554297ee37dde"
    ],
    [
      "Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "9d19c67678de2171c0e2655b704dba77"
    ],
    [
      "Vale.Arch.Types.be_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_029dc40463b676c106e396144db4f6f0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE"
      ],
      0,
      "2558768d1cc5b1c5e925a75819425f2f"
    ],
    [
      "Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat8",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_Vale.Arch.Types.be_quad32_to_bytes"
      ],
      0,
      "a6da345ad414729db1fa0c918ffbe43c"
    ],
    [
      "Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "kinding_Vale.Def.Words_s.four@tok",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "bba29f2825cdb35f2b8baccf6fa27f2f"
    ],
    [
      "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion",
        "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_3234ac1d1198c8b724cbaa98bc293002",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee"
      ],
      0,
      "195e3b85bd55048530ddc88a14b3f414"
    ],
    [
      "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion",
        "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_c064a9ee86fe2a45597a2563ec269cee"
      ],
      0,
      "453feb653df93c87a8953dcba2f77de7"
    ],
    [
      "Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
      ],
      0,
      "189ffd17420a12a3ed608bfa84701cff"
    ]
  ]
]