[
  "Ñ›Ü2Ö7E­7‰\u001cPÈJnˆ",
  [
    [
      "Vale.Arch.HeapLemmas.lemma_heap_impl",
      1,
      1,
      0,
      [ "@query", "equation_Vale.Arch.Heap.heap_impl" ],
      0,
      "71809d2764d206c935547e0b0db8c89d"
    ],
    [
      "Vale.Arch.HeapLemmas.coerce",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_754b00004f4a881ff74d076ab276dfe1"
      ],
      0,
      "56e24ccb4f620c8fe693be6f19f5d305"
    ],
    [
      "Vale.Arch.HeapLemmas.heap_ignore_ghost_machine",
      1,
      1,
      0,
      [ "@query", "equation_Vale.Arch.Heap.heap_impl" ],
      0,
      "5ac12be88823bb7fe03e7542b3a4a236"
    ],
    [
      "Vale.Arch.HeapLemmas.lemma_heap_ignore_ghost_machine",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5a0d46f466b67133f0e6700e582e1ba9"
    ],
    [
      "Vale.Arch.HeapLemmas.lemma_heap_ignore_ghost_machine",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.Heap.heap_get",
        "equation_Vale.Arch.Heap.heap_impl",
        "equation_Vale.Arch.Heap.heap_taint",
        "equation_Vale.Arch.Heap.heap_upd",
        "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost",
        "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost_machine",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint"
      ],
      0,
      "e7d2d772988c1eb9142b455b7566aaeb"
    ]
  ]
]