[
  "��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_Prims.LexTop@tok",
        "equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
        "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,
      "bb7ae8ed36943a68f37f202fcc13fb08"
    ],
    [
      "Vale.AES.AES_helpers.expand_key_128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "1183c842eadd6a3d02a02a1bdba01ee1"
    ],
    [
      "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,
      "a21b3a3ffd9da9e94c5681544552dd3e"
    ],
    [
      "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,
      "7e59b225c2c834bb773705c1e7c320bd"
    ],
    [
      "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,
      "509aed9665b87c36b3d0ea649c9fb09c"
    ],
    [
      "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,
      "5ec59afb792b7af566e6da84dc109116"
    ],
    [
      "Vale.AES.AES_helpers.init_rounds_opaque",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4c87271871558368981bac45b5a568ee"
    ],
    [
      "Vale.AES.AES_helpers.finish_cipher",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "2641b74c742b038024c7cebac1ddccac"
    ],
    [
      "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,
      "61114a327ecfc4c74dba8f91c234e244"
    ],
    [
      "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,
      "9070bd609f6c6b8ef972b3bd8a7dce98"
    ]
  ]
]