[
  "•O?E\u001a›s\bñ\u001f¢FÕ¨€ò",
  [
    [
      "Vale.X64.Stack_Sems.lemma_stack_from_to",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
        "equation_Vale.X64.Stack_Sems.stack_to_s"
      ],
      0,
      "79f856320f010cfc489bf0b9d4582ca3"
    ],
    [
      "Vale.X64.Stack_Sems.lemma_stack_to_from",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
        "equation_Vale.X64.Stack_Sems.stack_to_s"
      ],
      0,
      "ae7d1f125f15c6344fa2daeb174c3990"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_valid_src_stack64",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.valid_src_stack64"
      ],
      0,
      "a304755b282c3aac88bfcc7aefb17500"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_load_stack64",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.load_stack64"
      ],
      0,
      "455966f5751b7321794f73f9efa98384"
    ],
    [
      "Vale.X64.Stack_Sems.free_stack_same_load",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
        "equation_Vale.Arch.MachineHeap_s.machine_heap",
        "equation_Vale.Arch.MachineHeap_s.valid_addr",
        "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.X64.Machine_Semantics_s.free_stack_",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
        "function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_SelRestrict", "primitive_Prims.op_AmpAmp",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
        "token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
        "typing_FStar.Map.domain",
        "typing_Vale.Arch.MachineHeap_s.valid_addr",
        "typing_Vale.Arch.MachineHeap_s.valid_addr64",
        "typing_Vale.Lib.Set.remove_between"
      ],
      0,
      "7ae016d2f61b0baa9b4f5d803a186e33"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_store_stack64",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
        "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.store_stack64"
      ],
      0,
      "bca9501edcd057fa4fce75761e38e9bd"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_init_rsp",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "59f05f7d97e31b4cfdab61ef6ad7c0c0"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_init_rsp",
      2,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.init_rsp"
      ],
      0,
      "6e832ca1dc6b4d12c6e4a18b4293842b"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_free_stack",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
        "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.free_stack64"
      ],
      0,
      "c1bfffc0a0b524a40c5c690ce6556a93"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_valid_src_stack128",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.valid_src_stack128"
      ],
      0,
      "e4ceff526f51f93437311950f862a9c2"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_load_stack128",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.load_stack128"
      ],
      0,
      "f3af29f6871185f0c352994c71e54a37"
    ],
    [
      "Vale.X64.Stack_Sems.free_stack_same_load128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Vale.Arch.MachineHeap_s.get_heap_val128_def",
        "equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
        "equation_Vale.Arch.MachineHeap_s.machine_heap",
        "equation_Vale.Arch.MachineHeap_s.valid_addr",
        "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.X64.Machine_Semantics_s.free_stack_",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val128",
        "function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val32",
        "function_token_typing_Vale.Arch.MachineHeap_s.valid_addr128",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_14d403333eed8abd9b38f58babfc702d",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_SelRestrict", "primitive_Prims.op_AmpAmp",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
        "token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val128_def",
        "token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
        "typing_FStar.Map.domain",
        "typing_Vale.Arch.MachineHeap_s.valid_addr",
        "typing_Vale.Arch.MachineHeap_s.valid_addr128",
        "typing_Vale.Lib.Set.remove_between"
      ],
      0,
      "cbabb6f7b8a8f9a549ae44e42ef7994d"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_store_stack128",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
        "equation_Vale.X64.Stack_Sems.stack_to_s",
        "equation_Vale.X64.Stack_i.store_stack128"
      ],
      0,
      "15c02fa95df8336e7c1989075faa773d"
    ]
  ]
]