[
  "�\u0007���T���3ͳ��P",
  [
    [
      "Vale.Arch.HeapImpl.buffer",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "05dce806c82cbc7e5bc26d9cdf77f43e"
    ],
    [
      "Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_buffer",
      1,
      1,
      0,
      [
        "@query", "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ"
      ],
      0,
      "50f16d33e9363b3b201de6cac2ac21f2"
    ],
    [
      "Vale.Arch.HeapImpl.__proj__ValeHeap__item__ih",
      1,
      1,
      0,
      [
        "@query", "proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
        "projection_inverse_Vale.Arch.HeapImpl.ValeHeap_mh"
      ],
      0,
      "d6d9b1eb03cef1b42511ec243c993ca2"
    ],
    [
      "Vale.Arch.HeapImpl.mi_heap_upd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0",
        "Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53",
        "equation_Vale.Arch.HeapImpl._ih",
        "equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
        "equation_Vale.Arch.MachineHeap_s.machine_heap",
        "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Interop.Heap_s.correct_down",
        "equation_Vale.Interop.Heap_s.down_mem_t",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Interop.Heap_s.interop_heap@tok",
        "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Set.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
        "proj_equation_Vale.Arch.HeapImpl.ValeHeap_mh",
        "projection_inverse_Vale.Arch.HeapImpl.ValeHeap_mh",
        "refinement_interpretation_Tm_refine_1d91a1ccb8ed3b9c6990d1f08f8c1332",
        "refinement_interpretation_Tm_refine_2688fdb7e84bdee1cf9ca4c017aaa352",
        "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
        "typing_FStar.Map.domain",
        "typing_Vale.Arch.HeapImpl.__proj__ValeHeap__item__ih",
        "typing_Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh",
        "typing_Vale.Interop.down_mem"
      ],
      0,
      "a1bcd950cb9da0826644c25d8c865207"
    ]
  ]
]