[
  "&�\u0018̉�V�\u0014�E\u001c�Cg�",
  [
    [
      "Vale.X64.Memory_Sems.lemma_upd_get_heap",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
        "equation_Vale.Arch.MachineHeap_s.machine_heap",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Set.lemma_equal_refl",
        "refinement_interpretation_Tm_refine_13f55c98202407c42a7edd29f4ef7d8f",
        "typing_FStar.Map.domain"
      ],
      0,
      "aa20df8e4d1562bc47735fdfb346c9b5"
    ],
    [
      "Vale.X64.Memory_Sems.lemma_get_upd_heap",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "a144305366a983f2170bc35ddf0c2472"
    ],
    [
      "Vale.X64.Memory_Sems.coerce",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_754b00004f4a881ff74d076ab276dfe1"
      ],
      0,
      "ede63ec085b01955a89faafa4d2c787c"
    ],
    [
      "Vale.X64.Memory_Sems.lemma_heap_upd_heap",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.X64.Memory.get_vale_heap",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "4d68a090afde3cac611850aad4185d38"
    ],
    [
      "Vale.X64.Memory_Sems.low_lemma_store_mem64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "e727f93923a8b6caa2a2d448f22cae42"
    ],
    [
      "Vale.X64.Memory_Sems.low_lemma_store_mem128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "7f0ac9e38c393d9c3b66caea44ad795c"
    ],
    [
      "Vale.X64.Memory_Sems.low_lemma_store_mem128_lo64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "5b07599b37e731ea940bee1cf3a7e80d"
    ],
    [
      "Vale.X64.Memory_Sems.low_lemma_store_mem128_hi64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "4be7929346f8357e01c15da07b6e830b"
    ]
  ]
]