[
  "{�W@��Ɣ�`���\u0018�",
  [
    [
      "AES_helpers.expand_key_128_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_1",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok", "equality_tok_Prims.LexTop@tok",
        "equation_AES_s.is_aes_key_LE", "equation_Prims.nat",
        "equation_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_ba523126f67e00e7cd55f0b92f16681d",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3fcaebfd7633e8538bfdfa8aa2dd0501"
    ],
    [
      "AES_helpers.lemma_expand_key_128_0",
      1,
      1,
      0,
      [ "@query", "equation_AES_s.nb", "projection_inverse_BoxInt_proj_0" ],
      0,
      "789029c13445d68e009509dd98dfca3b"
    ],
    [
      "AES_helpers.lemma_expand_key_128_i",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_AES_s.nb",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Words_s.nat32", "int_inversion",
        "l_and-interp", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0b4a13f44563398bd21134c879b4f4b7",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_974ea6f3ebb2d8e5fd635575758d08ab",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "ae5dfffe06d20e355bd5cf2ac015a229"
    ],
    [
      "AES_helpers.lemma_expand_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_AES_s.nb",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "de3515719b6abba19edfc4e7c4be3be9"
    ],
    [
      "AES_helpers.lemma_expand_key_128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_AES_s.nb",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "int_inversion", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_9cb82c4ebe6abcb785bea99f8b687bdd",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "da23c0f1b13b59fccdc0147ff5564d9f"
    ],
    [
      "AES_helpers.cipher_opaque",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm"
      ],
      0,
      "19f6ec84848b74edbe01ae45d0e67403"
    ],
    [
      "AES_helpers.init_rounds_opaque",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8418ec35ce5cb89242531d7cd137991b"
    ],
    [
      "AES_helpers.finish_cipher",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "a8bbdc2db568485585887737cd327504"
    ]
  ]
]