[
  "ÆÓBcw¤fé}L½‘úÈÍZ",
  [
    [
      "Vale.X64.Regs.sel",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Lib.Map16.sel16", "typing_Vale.X64.Machine_s.n_regs"
      ],
      0,
      "eb1d9d1888b9cd82d5b4240822e84309"
    ],
    [
      "Vale.X64.Regs.upd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file", "int_inversion",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.X64.Machine_s.n_regs"
      ],
      0,
      "585b9e00cee012e239d547017735e612"
    ],
    [
      "Vale.X64.Regs.eta",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_0233a8fa9dab68752b72fc7b92282347",
        "refinement_interpretation_Tm_refine_09c71f8bf0211aae98d104f1b7a5ec29",
        "refinement_interpretation_Tm_refine_133499ff74fb42166c14fa71c9de0eea",
        "refinement_interpretation_Tm_refine_26eb76be4be69db887a85d42b1f2b300",
        "refinement_interpretation_Tm_refine_38f357697d1871728b6efa5b2c6cde08",
        "refinement_interpretation_Tm_refine_43c5913b2b7ffe79bfc84b338aebf2db",
        "refinement_interpretation_Tm_refine_44029dc661215e748b7d118126bebb66",
        "refinement_interpretation_Tm_refine_5547be08e4bf37ada42c4f9514d38ed6",
        "refinement_interpretation_Tm_refine_561dadd74cf2df492c815a73732ca860",
        "refinement_interpretation_Tm_refine_5f681121df65376329bcc4a806c6c40d",
        "refinement_interpretation_Tm_refine_81c1990eca1445fdc599682f9293121b",
        "refinement_interpretation_Tm_refine_8867d2dd49d971c543d8bd3f041f24b5",
        "refinement_interpretation_Tm_refine_8c5ee1b914ba03e7354f7cc43de1b254",
        "refinement_interpretation_Tm_refine_9ccaa6f5896e99675865f9c84a36e019",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_fd01003f793c223ce122405177249431",
        "refinement_interpretation_Tm_refine_fe479871b3967d0c9b8d8614ccf88035"
      ],
      0,
      "615fc9a17502cfc1e7e695aa5c78b873"
    ]
  ]
]