[
  "�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,
      "d7eeae07c16cbc38f93b5a859edbcf3a"
    ],
    [
      "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,
      "ff0b30f326359ffef6bf3676fc4792a4"
    ],
    [
      "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,
      "8cd1522f0e52ec29704e7fe169fb77b8"
    ],
    [
      "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,
      "448da40ead3866179f05ddc56b03193f"
    ],
    [
      "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,
      "831c6b1fbb52a7831e9484657b789dc0"
    ],
    [
      "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,
      "81979350dbe485d5e790abc6ab731262"
    ],
    [
      "Vale.X64.Stack_Sems.equiv_init_rsp",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "c1d2c81d88249a2a8ceb56dac5d00e5c"
    ],
    [
      "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,
      "98592c7f0d9b648b72e8ecc50b6dfcf5"
    ],
    [
      "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,
      "660cba84df2a4e23a7b4f4b69284a7df"
    ],
    [
      "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,
      "8bb3b41405b693dd28e0b8a44a20302b"
    ],
    [
      "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,
      "a7008f8a72f7e0ed42e14f95339c4db8"
    ],
    [
      "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,
      "9e0051e545e0300d70d2949b5c79ae8f"
    ],
    [
      "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,
      "ad9af00f2839e97bb3d0ba490e228e14"
    ]
  ]
]