[
  "œ­s³vöPfæÓaŸëM¨3",
  [
    [
      "Vale.AES.AES_helpers.expand_key_128_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Types_s.quad32",
        "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,
      "b309577f406a19e1cb21dd8e30fc8208"
    ],
    [
      "Vale.AES.AES_helpers.expand_key_128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "6e5e233fba707595c3917f5ee21e6fd9"
    ],
    [
      "Vale.AES.AES_helpers.lemma_expand_key_128_0",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.AES.AES_s.nb",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "a316528e673b7ae8d67fdec9ab897c88"
    ],
    [
      "Vale.AES.AES_helpers.lemma_expand_key_128_i",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.nb", "int_inversion", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96884e177dd23a2209d073a3fa11b201",
        "refinement_interpretation_Tm_refine_c1b1024e28776cd81d3423da5c72fdff"
      ],
      0,
      "4f9f6999fc9af2071afd2a5908139808"
    ],
    [
      "Vale.AES.AES_helpers.lemma_expand_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.nb", "int_inversion", "l_and-interp",
        "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_86c893bd73295cad27c95bea9e692abe"
      ],
      0,
      "1ce3ed7b7927b2bb176181de40a19a2d"
    ],
    [
      "Vale.AES.AES_helpers.lemma_expand_key_128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.nb", "int_inversion", "l_and-interp",
        "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_6b9131a31b8a74e7093141d7985f063a",
        "refinement_interpretation_Tm_refine_9c2d74ae21ebe21dc37eb1ac96ddb62a"
      ],
      0,
      "f51a110f64a0d52d650ceb2c562b95ea"
    ],
    [
      "Vale.AES.AES_helpers.init_rounds_opaque",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ebd6ac12fe48b8c11f95f5b3b7eabe84"
    ],
    [
      "Vale.AES.AES_helpers.finish_cipher",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "b3f9436dfe2bfa46a9662dc651e65c14"
    ],
    [
      "Vale.AES.AES_helpers.finish_cipher_opt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "l_and-interp", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "f6787e4b6632474659e4ad34a1e16be4"
    ],
    [
      "Vale.AES.AES_helpers.lemma_incr_msb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "a3f6e27daa1eed360240e6dc35855c2e"
    ]
  ]
]