[
  "†D€Ô%ǃýá’]¦*uÎU",
  [
    [
      "Vale.X64.Decls.lemma_mul_in_bounds",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod",
        "equation_FStar.UInt.size", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "c05d72c549f799a3f3cf1a238d6f25c9"
    ],
    [
      "Vale.X64.Decls.lemma_mul_nat",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "22968ec4dcf8257035b13be11022fef2"
    ],
    [
      "Vale.X64.Decls.cf",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.cf", "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.cf"
      ],
      0,
      "95d74dee25f23e412301182de1e3479a"
    ],
    [
      "Vale.X64.Decls.overflow",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.overflow",
        "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.overflow"
      ],
      0,
      "e0325bdb0c512bf28b387924a6f824a3"
    ],
    [
      "Vale.X64.Decls.valid_cf",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.cf", "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.cf"
      ],
      0,
      "2619252e8ebefbd4d58fa377d74fca9a"
    ],
    [
      "Vale.X64.Decls.valid_of",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.overflow",
        "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.overflow"
      ],
      0,
      "b30544a50838caa498b94b90c037a674"
    ],
    [
      "Vale.X64.Decls.updated_cf",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Pervasives.Native.option__uu___haseq",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Tm_unit", "equation_Prims.eqtype",
        "equation_Vale.X64.Decls.cf", "equation_Vale.X64.Decls.valid_cf",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Lemmas.cf",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "function_token_typing_Prims.bool", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Some_a",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.cf"
      ],
      0,
      "c8bfd040eab5fed184e1adcf2de8372f"
    ],
    [
      "Vale.X64.Decls.updated_of",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Pervasives.Native.option__uu___haseq",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Tm_unit", "equation_Prims.eqtype",
        "equation_Vale.X64.Decls.overflow",
        "equation_Vale.X64.Decls.valid_of",
        "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.overflow",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "function_token_typing_Prims.bool", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Some_a",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.overflow"
      ],
      0,
      "39912713ef3bed3cd5825b34ad4b6faf"
    ],
    [
      "Vale.X64.Decls.maintained_cf",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Pervasives.Native.option__uu___haseq",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Decls.cf",
        "equation_Vale.X64.Decls.valid_cf",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Lemmas.cf",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.cf"
      ],
      0,
      "6604193ab813f9b537ed2698f36a4b97"
    ],
    [
      "Vale.X64.Decls.maintained_of",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "assumption_FStar.Pervasives.Native.option__uu___haseq",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_Prims.eqtype", "equation_Vale.X64.Decls.overflow",
        "equation_Vale.X64.Decls.valid_of",
        "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Lemmas.overflow",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "function_token_typing_Prims.bool",
        "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.X64.Lemmas.overflow"
      ],
      0,
      "bd08fe20321632a11cf1aec7d91bc673"
    ],
    [
      "Vale.X64.Decls.va_if",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "147af80e1c711ea92ff42d52bee3fc15"
    ],
    [
      "Vale.X64.Decls.total_thunk_if",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "7d8c4453845fc0cee554d46cf919da44"
    ],
    [
      "Vale.X64.Decls.va_tl",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_1c9655c30deebdd07e36fb0790c48d70"
      ],
      0,
      "a7e6169ebb9843c2f9b607cd5c626612"
    ],
    [
      "Vale.X64.Decls.reg_operand",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "02a6447a85c8a3aa6181cbbb9554501a"
    ],
    [
      "Vale.X64.Decls.va_operand_reg_opr64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8d9a3eb61bd2ab8a9121056bda6ca410"
    ],
    [
      "Vale.X64.Decls.cmp_operand",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "624f915d91cb9a906e3bb63d42d08d48"
    ],
    [
      "Vale.X64.Decls.get_reason",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.Def.PossiblyMonad.Err",
        "disc_equation_Vale.Def.PossiblyMonad.Ok",
        "equation_Vale.X64.Decls.va_pbool",
        "fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly"
      ],
      0,
      "ce5b6081404c96d9fff17c02c591b0e4"
    ],
    [
      "Vale.X64.Decls.get_reg",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "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.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7f25d8577c2dcae065a79f3b087269a8"
    ],
    [
      "Vale.X64.Decls.valid_operand",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "d9dcfbc6aa54444ad5b02d634c86d24f"
    ],
    [
      "Vale.X64.Decls.valid_operand",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f10b100e8f0079d17a4ec34be8bbc483"
    ],
    [
      "Vale.X64.Decls.valid_operand",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b5ac5aa13a6022d076392ff9974f4ea1"
    ],
    [
      "Vale.X64.Decls.valid_operand",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7eb8dbe4ebc39f7d0164e8716888a740"
    ],
    [
      "Vale.X64.Decls.valid_operand128",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8e32aaf0a4d573b26c7e79cb26d4e0bf"
    ],
    [
      "Vale.X64.Decls.valid_operand128",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "07d62a56562ad539446fffc153f695a4"
    ],
    [
      "Vale.X64.Decls.va_op_opr64_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6f502fa50e84d12456c4c42814fdd53e"
    ],
    [
      "Vale.X64.Decls.va_op_reg64_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "521332758dfa162ae2ddbc5d60e6e361"
    ],
    [
      "Vale.X64.Decls.va_op_opr128_xmm",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "dfe5638dc1c254b330180a27cf124004"
    ],
    [
      "Vale.X64.Decls.va_const_opr64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fe1109c8ecdd3225fd1eae7d0788047d"
    ],
    [
      "Vale.X64.Decls.va_const_shift_amt64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b23483d92cf39bf7bd2d5e043f82d55d"
    ],
    [
      "Vale.X64.Decls.va_op_shift_amt64_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "98303c1fe6c531705298c4ca5c9c737b"
    ],
    [
      "Vale.X64.Decls.va_op_cmp_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OMem", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "882083ea140d17936c7c7198c23a49e2"
    ],
    [
      "Vale.X64.Decls.va_const_cmp",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5db91aabeff302ace60ffcd2b13d9268"
    ],
    [
      "Vale.X64.Decls.va_coerce_reg64_opr64_to_cmp",
      1,
      2,
      0,
      [
        "@query", "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Machine_s.reg_64",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "6f41d499e02424473a6512d0b7c33f57"
    ],
    [
      "Vale.X64.Decls.va_coerce_opr64_to_cmp",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8fa7ea1705f83494224ff6b042d580f7"
    ],
    [
      "Vale.X64.Decls.va_op_reg_opr64_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OReg", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6ccde1cf4ded2b42842d8618e0869237"
    ],
    [
      "Vale.X64.Decls.va_op_dst_opr64_reg64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "2d1c38c7a88d3bb5e60960ea31ac5c58"
    ],
    [
      "Vale.X64.Decls.va_coerce_xmm_to_opr128",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "85c11228f2fa1d8bb43a98fcd5f9ffcb"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "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.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
      ],
      0,
      "a72149e4fd17cfb1bbaec55bfc90b805"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem64",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a64d98961e297991d256df0f3ad48ec8"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem64",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "4915520009b3f142311f3bbf3fafd99f"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem64",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "e9ee71e26798a2163aedb69f7b03e120"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem64",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0dd7064e1739c694ca0c6bc380c9c751"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Stack",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "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.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
      ],
      0,
      "fd4b1dc3f0bbc0805e24245da260ffc0"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Stack",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "617c233fa2c3db5c71a8c571fe5cbdb0"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Stack",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7f61f05379d5fea24c184d5df02f0665"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Stack",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "79aa3c7b0920105195d7ca84140a461d"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Stack",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "3e805c77ddf524db035f3463280bcb83"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem128",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
      ],
      0,
      "ae74738a61c65f5ab849c951a7b9aefc"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem128",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "39d9919593e7e66aae6ea89a024b91e6"
    ],
    [
      "Vale.X64.Decls.va_opr_code_Mem128",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "26381a6cc7ce8a22fc1ca4b9843d14d5"
    ],
    [
      "Vale.X64.Decls.lemma_opr_Mem64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.valid_buf_maddr64",
        "equation_Vale.X64.Decls.valid_mem_operand64",
        "equation_Vale.X64.Decls.valid_operand",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.scale_by",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory_Sems.is_full_read",
        "equation_Vale.X64.State.eval_maddr",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.valid_maddr",
        "equation_Vale.X64.State.valid_src_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing", "l_and-interp",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.StateLemmas.lemma_load_buffer_read64",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Vale.X64.Machine_s.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.load_mem64",
        "typing_Vale.X64.Memory.valid_mem64",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
      ],
      0,
      "2099786d36f7b9ca51156329858be11a"
    ],
    [
      "Vale.X64.Decls.lemma_opr_Mem64",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c2409deb8e807ef6a1ecca76b4b4a3ca"
    ],
    [
      "Vale.X64.Decls.lemma_opr_Mem64",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "eadfd469aad2edf918dd133933e8eb3c"
    ],
    [
      "Vale.X64.Decls.lemma_opr_Mem128",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.valid_buf_maddr128",
        "equation_Vale.X64.Decls.valid_mem_operand128",
        "equation_Vale.X64.Decls.valid_operand128",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.scale_by",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory_Sems.is_full_read",
        "equation_Vale.X64.State.eval_maddr",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.valid_maddr128",
        "equation_Vale.X64.State.valid_src_operand128",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.StateLemmas.lemma_load_buffer_read128",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Vale.X64.Machine_s.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.valid_mem128",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.eval_maddr",
        "typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "4df2e7ec9c37dc8723389d057f61e14c"
    ],
    [
      "Vale.X64.Decls.lemma_opr_Mem128",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8504c437872364c5bfe49b1a443a15c3"
    ],
    [
      "Vale.X64.Decls.va_is_dst_opr64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "dab54d454f09511e2328d705594202d3"
    ],
    [
      "Vale.X64.Decls.va_is_dst_opr64",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ba255b01e8d5342db340001b1def4734"
    ],
    [
      "Vale.X64.Decls.va_is_dst_opr64",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9fbeb8665ca219aa3b7c1bfd463343c5"
    ],
    [
      "Vale.X64.Decls.va_is_src_reg_opr64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "061564a8c1b9ce349b449e6c094aae6c"
    ],
    [
      "Vale.X64.Decls.va_is_dst_reg_opr64",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c991255d668ec6ca1f858ad4e079e364"
    ],
    [
      "Vale.X64.Decls.update_operand",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "b64c4b4560cc7b8bf75529141db7a5b8"
    ],
    [
      "Vale.X64.Decls.update_operand",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "940aa297037273766fcc092a2755b0b3"
    ],
    [
      "Vale.X64.Decls.update_operand",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8279be7c7f3730a74b02d362a6e25f36"
    ],
    [
      "Vale.X64.Decls.update_operand",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "89dbec25d7d8bea220465a5ea5c9a2f9"
    ],
    [
      "Vale.X64.Decls.update_operand",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7b3693cfca19648c453e0dda90651dd3"
    ],
    [
      "Vale.X64.Decls.update_operand",
      6,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8cf56dcd8edad4de6318421fa8094722"
    ],
    [
      "Vale.X64.Decls.update_operand",
      7,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f1ad6702468c5c98de0b688c0475ea63"
    ],
    [
      "Vale.X64.Decls.update_operand",
      8,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0e0dc7a3018d1c6d7a1997a5db191f75"
    ],
    [
      "Vale.X64.Decls.update_operand",
      9,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "62f66186d956ebf6552dec7698e4b531"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "1df2b0316597cc12c99eab4283385c27"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "13d16b29814661d000d9612368261043"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5318b9243b2cd5e164c797621d249953"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "dfcd42f4faae4ef6bcdebd5acfc66533"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "e58e2b4ff112e2b79c5f28c1e5d8fcf9"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      6,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a2607fff048f69c1827292ec70b9fc22"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      7,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "1617d631e54d31dc0a15929b51b084a7"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      8,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "42e2c84697e301b9151041a37aa6a245"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_dst_opr64",
      9,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f4e420ca57cb82af88029b13c01fca75"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OConst",
        "disc_equation_Vale.X64.Machine_s.OMem",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand"
      ],
      0,
      "9d7987e9497bd7c513a5dee325a8e2ef"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6c6ab16601855b5b46feca45e356b4ac"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0eba30de73d52aac797a9c47a0400b59"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "351b4df3ee8a1dd0a13c1a6dd2709657"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "55523e59d1a5f7ad93d6e10a27c2b39d"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      6,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "122832f996e060a5ef8a64da8894b49c"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      7,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9d61ca72e6490faaedc0f3552b5bd907"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      8,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0ac774c5614c567ed9c891db627bd062"
    ],
    [
      "Vale.X64.Decls.va_upd_operand_reg_opr64",
      9,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5ebf8a893724d8d6c702000a334a8645"
    ],
    [
      "Vale.X64.Decls.va_lemma_upd_update",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.OReg",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Decls.update_operand",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_operand_reg_opr64",
        "equation_Vale.X64.Decls.va_upd_operand_xmm",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.State.eval_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a7c2c0bc0dc4c9ae3ee8b5295b5ed240"
    ],
    [
      "Vale.X64.Decls.va_cmp_eq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b5da8531098348bbc637b2394ec5604e"
    ],
    [
      "Vale.X64.Decls.va_cmp_eq",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "64253b7a48e10904213cf7e9d2bfb633"
    ],
    [
      "Vale.X64.Decls.va_cmp_ne",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "bc77f5d0d58bc595a07c58aa71f3a966"
    ],
    [
      "Vale.X64.Decls.va_cmp_ne",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "27039565921b6636dfaec5ddbc6e7c55"
    ],
    [
      "Vale.X64.Decls.va_cmp_le",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a930bb8d331804c23dd764e579baeb9d"
    ],
    [
      "Vale.X64.Decls.va_cmp_le",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "86f99adf10c4a87fc88f4ffceea0c870"
    ],
    [
      "Vale.X64.Decls.va_cmp_ge",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "85d84c683c61c17ba996cc0ae7aa645a"
    ],
    [
      "Vale.X64.Decls.va_cmp_ge",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "dc4dfc2161c49e5b9db6d3b82ff5a376"
    ],
    [
      "Vale.X64.Decls.va_cmp_lt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9d9f10a931b4db217cc68400ce1e480c"
    ],
    [
      "Vale.X64.Decls.va_cmp_lt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "bf34f1e95b62967b3c98a626440b4363"
    ],
    [
      "Vale.X64.Decls.va_cmp_gt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fbaff0b667296a7c3b7b30b960a3b75c"
    ],
    [
      "Vale.X64.Decls.va_cmp_gt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c9d04f175b9bdb41158e4e692377f1a0"
    ],
    [
      "Vale.X64.Decls.buffers_readable",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_2ba196b19be26fed8bbff92956a16ea9_1",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok", "equation_Vale.X64.Memory.buffer64",
        "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
      ],
      0,
      "700243c75533a61343d0b8af716bbade"
    ],
    [
      "Vale.X64.Decls.loc_locs_disjoint_rec128",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_b6f06d207926310c35b5daa4508dea69_1",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.X64.Memory.buffer128",
        "fuel_guarded_inversion_Prims.list",
        "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons"
      ],
      0,
      "90f036689567cc80ed22607e7603091c"
    ],
    [
      "Vale.X64.Decls.va_ins_lemma",
      1,
      2,
      0,
      [
        "@query",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins",
        "interpretation_Tm_abs_431565cf08dbebf07925447f42184424"
      ],
      0,
      "85ee4b5e5a0509154943cf950eeae776"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_eq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f7431ff74a4d43fcd20794845c37520f"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_eq",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "df9abf6a239f21487ccd063e401820fd"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_eq",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_eq"
      ],
      0,
      "dfd52219da75fb18c7494ee4067f8794"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ne",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "04e172e4089535d340c5d0d8848c98b1"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ne",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fa271a972da2a15c559b8b469e8fed2c"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ne",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_ne",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_ne"
      ],
      0,
      "d7d6b213b24db151291f1db6dcf89f3e"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_le",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fc53b7c23fbf243321c3ab4c1dcc5ffd"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_le",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ff3d355e41baa4965ed57c1502cee4a8"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_le",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_le",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_le"
      ],
      0,
      "0a14d3403f18058523d6ba237f44035b"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ge",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "d7793c392bb64c73d0262d9e25288eb0"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ge",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fd40058602f820e389ce8ea988e7079b"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_ge",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_ge",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_ge"
      ],
      0,
      "a733e9dbb123065146623c94a84bd50b"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_lt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "57ab5861987e1fda9fea3e5cbf871a07"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_lt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9968f814a475b2a44baf8a31bb8cb565"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_lt",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_lt",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_lt"
      ],
      0,
      "887a87289426c78f7b5e06bab18d3f58"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_gt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f393b4e975171315a9605d417c29c954"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_gt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "555dc97496e92685a8e70546e3801b3e"
    ],
    [
      "Vale.X64.Decls.lemma_cmp_gt",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.va_cmp_gt",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_cmp_gt"
      ],
      0,
      "7efea7d8e670442957495bb70f8c4b16"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_eq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "92d274588691588719e8b9420d1378eb"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_eq",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "424160eaf0e86ddfa31dd85da78f62ab"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_eq",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_eq",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_eq"
      ],
      0,
      "d0251b88b84138e618d948f123760924"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ne",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "950d82f648f45cd5e40a458a3c765979"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ne",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a16fae95002a93ee282d0c41447ed49b"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ne",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_ne",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_ne"
      ],
      0,
      "b37d054d962ed8bf635c80c5270bb5e8"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_le",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0058d4316402ed2c875d63422f66d6ed"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_le",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "99bb5e6cb139987675bffcecec6ae1b5"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_le",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_le",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_le"
      ],
      0,
      "19cc72f68f1b9ee1203ebb9163ccbdf8"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ge",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "825a2b8fa43631e17c2effcfff771ac9"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ge",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "11994fc4d67bdf60c135c1e3299fe2d0"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_ge",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_ge",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_ge"
      ],
      0,
      "d24ddb9d195fbe421513058dac70fdc4"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_lt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "332bb56f22dc71fddd3985e0b49b77c8"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_lt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "4df93819d9b7973f1941727eace07a6f"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_lt",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_lt",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_lt"
      ],
      0,
      "b450849fc3324d47d79a6d9f13fee0e0"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_gt",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c21eca9ec8fb610c64666fb3990d3f69"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_gt",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f672fa8456b93e155ce1edc0ad243165"
    ],
    [
      "Vale.X64.Decls.lemma_valid_cmp_gt",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.va_cmp_gt",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Decls.valid_operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Lemmas.lemma_valid_cmp_gt"
      ],
      0,
      "e5ad66553897dcbe9aed7de10f1f5434"
    ],
    [
      "Vale.X64.Decls.va_lemma_merge_total",
      1,
      2,
      0,
      [ "@query" ],
      0,
      "e0d93eaed34cac2ed9f723f5c7d492cb"
    ],
    [
      "Vale.X64.Decls.va_lemma_merge_total",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_compute_merge_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "06ecb5b8f6280f1a19009a6d807ba554"
    ],
    [
      "Vale.X64.Decls.va_lemma_empty_total",
      1,
      2,
      0,
      [
        "@query", "equation_Vale.X64.Decls.eval_code",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp"
      ],
      0,
      "f01511844cf1b0108dbc4cd762899fcb"
    ],
    [
      "Vale.X64.Decls.va_lemma_ifElse_total",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.havoc_flags",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_Vale.X64.State.vale_state"
      ],
      0,
      "e038ffce41f7da317ec0f6981508fa72"
    ],
    [
      "Vale.X64.Decls.va_lemma_ifElseTrue_total",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.eval_code",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "ff1ec1a3669d14c78f8c9845d7ee578e"
    ],
    [
      "Vale.X64.Decls.va_lemma_ifElseFalse_total",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.eval_code",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "26068f581c00affb8c61548cc126f6d8"
    ],
    [
      "Vale.X64.Decls.va_lemma_while_total",
      1,
      2,
      0,
      [
        "@query", "equation_Vale.X64.Decls.eval_while_inv",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp"
      ],
      0,
      "392e3aa8df998be01c3ae72038e08292"
    ],
    [
      "Vale.X64.Decls.va_lemma_whileTrue_total",
      1,
      2,
      0,
      [
        "@query", "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.havoc_flags",
        "equation_Vale.X64.Decls.va_fuel"
      ],
      0,
      "5ab115cd55de6844573cc5a0161abc3c"
    ],
    [
      "Vale.X64.Decls.va_lemma_whileFalse_total",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Decls.eval_code",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.eval_while_inv",
        "equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "fuel_guarded_inversion_Vale.X64.State.vale_state"
      ],
      0,
      "28fc4ba62b24e807a42cdaaaad7315a1"
    ],
    [
      "Vale.X64.Decls.va_lemma_whileMerge_total",
      1,
      2,
      0,
      [ "@query" ],
      0,
      "b5e1e00ae8cf4cafef55129d5ca58cfd"
    ],
    [
      "Vale.X64.Decls.va_lemma_whileMerge_total",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.X64.Machine_s.While",
        "equation_Vale.X64.Decls.eval_code",
        "equation_Vale.X64.Decls.eval_ocmp",
        "equation_Vale.X64.Decls.eval_while_inv",
        "equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.valid_ocmp",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "83d530677245c9f4e4fee565f0fe530c"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "34389d77779d26da2f8040e699558ecc"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "899cb7ae7211692bbd9c8a9cf4aaf75c"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      3,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "68f6091af3eee953a43c702d96d6385c"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      4,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "567c59129f754d5fab5bf0bda2a2415d"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      5,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "adc8b15a501d5a69dd692d124be62523"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      6,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "14c114fedcb67e9cc30d07a74ced63a4"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      7,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "dc056b993dcaaba39b275a0724a7ad73"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      8,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "585a8f3cfd51ba3f7e4ab0e1fc81b715"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      9,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "d139ac722d06d8cf7d157d7174ba2ed6"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      10,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "e21b1ee8cd89d4245747cbb9100b020c"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      11,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "85f5ba138dc1095221794f96171bd8e4"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      12,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "8fd83aa7fef4a261d66635c513737eb8"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      13,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f0cf234ba552c0a2ff505635feab8dd5"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      14,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "02178f1e1fee29c769d0657f434707ce"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      15,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "77592c067c4b8be8bf47886a3e3d37b9"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      16,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "4c4646a71dda9bc28272aa68763f6094"
    ],
    [
      "Vale.X64.Decls.max_one_mem",
      17,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fa1a2ced8b59befb764bdde24e397fcc"
    ]
  ]
]