[
  "B'\t\u0011Q���%(�6a>Z�",
  [
    [
      "X64.Vale.Regs.reg_to_int",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_X64.Machine_s.R10",
        "disc_equation_X64.Machine_s.R11", "disc_equation_X64.Machine_s.R12",
        "disc_equation_X64.Machine_s.R13", "disc_equation_X64.Machine_s.R14",
        "disc_equation_X64.Machine_s.R15", "disc_equation_X64.Machine_s.R8",
        "disc_equation_X64.Machine_s.R9", "disc_equation_X64.Machine_s.Rax",
        "disc_equation_X64.Machine_s.Rbp", "disc_equation_X64.Machine_s.Rbx",
        "disc_equation_X64.Machine_s.Rcx", "disc_equation_X64.Machine_s.Rdi",
        "disc_equation_X64.Machine_s.Rdx", "disc_equation_X64.Machine_s.Rsi",
        "disc_equation_X64.Machine_s.Rsp",
        "fuel_guarded_inversion_X64.Machine_s.reg"
      ],
      0,
      "837af8ce91abfbf985f1c6d79f67820c"
    ],
    [
      "X64.Vale.Regs.of_fun",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "fuel_guarded_inversion_X64.Machine_s.reg"
      ],
      0,
      "943cb4d92fb5079c1874322bc73993f7"
    ],
    [
      "X64.Vale.Regs.lemma_upd_eq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Map16.map2", "equation_Map16.map4", "equation_Map16.sel2",
        "equation_Map16.sel4", "equation_Map16.sel8", "equation_Map16.upd2",
        "equation_Map16.upd4", "equation_Map16.upd8", "equation_Prims.nat",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_Words_s.pow2_1", "equation_X64.Vale.Regs.reg_int",
        "equation_X64.Vale.Regs.reg_to_int",
        "function_token_typing_Words_s.pow2_1", "int_inversion",
        "int_typing", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Regs.reg_to_int"
      ],
      0,
      "11559c80ded2bb0d8de077cf4f1dde44"
    ],
    [
      "X64.Vale.Regs.lemma_upd_ne",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "equation_Map16.map2",
        "equation_Map16.map4", "equation_Map16.sel2", "equation_Map16.sel4",
        "equation_Map16.sel8", "equation_Map16.upd2", "equation_Map16.upd4",
        "equation_Map16.upd8", "equation_Prims.nat",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Vale.Regs.reg_int",
        "equation_X64.Vale.Regs.reg_to_int",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Regs.reg_to_int"
      ],
      0,
      "6401f02b176be30b3882f7746c0a25a3"
    ],
    [
      "X64.Vale.Regs.lemma_equal_intro",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_X64.Machine_s.R10",
        "constructor_distinct_X64.Machine_s.R11",
        "constructor_distinct_X64.Machine_s.R12",
        "constructor_distinct_X64.Machine_s.R13",
        "constructor_distinct_X64.Machine_s.R14",
        "constructor_distinct_X64.Machine_s.R15",
        "constructor_distinct_X64.Machine_s.R8",
        "constructor_distinct_X64.Machine_s.R9",
        "constructor_distinct_X64.Machine_s.Rax",
        "constructor_distinct_X64.Machine_s.Rbp",
        "constructor_distinct_X64.Machine_s.Rbx",
        "constructor_distinct_X64.Machine_s.Rcx",
        "constructor_distinct_X64.Machine_s.Rdi",
        "constructor_distinct_X64.Machine_s.Rdx",
        "constructor_distinct_X64.Machine_s.Rsi",
        "constructor_distinct_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok", "equation_X64.Vale.Regs.equal",
        "equation_X64.Vale.Regs.reg_to_int", "int_inversion",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok"
      ],
      0,
      "0c18a83fe2caf46d68c182fcb0f10822"
    ],
    [
      "X64.Vale.Regs.lemma_equal_elim",
      1,
      1,
      0,
      [ "@query", "eq2-interp", "equation_X64.Vale.Regs.equal" ],
      0,
      "a72b16f61720ea7ab477799b444a99db"
    ],
    [
      "X64.Vale.Regs.lemma_eta",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "fuel_guarded_inversion_X64.Machine_s.reg",
        "lemma_X64.Vale.Regs.lemma_equal_elim", "typing_X64.Vale.Regs.eta"
      ],
      0,
      "2284017e1cc7b4aac57aea20b5169e4a"
    ]
  ]
]