[
  "�w%\u007f�a>�\u0016��o���_",
  [
    [
      "DoublyLinkedListIface.g_node_vals",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_5529d1ec063451477f1e5ac4ca5ccdc8_2",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
      ],
      0,
      "9a120de61581c80b8543e6778c17d0e7"
    ],
    [
      "DoublyLinkedListIface.dll_head",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_3aac47f90ec5f312f230a639872610fd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_DoublyLinkedListIface.node",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "ea454165c8b2099208a3e96108fbf296"
    ],
    [
      "DoublyLinkedListIface.dll_tail",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3aac47f90ec5f312f230a639872610fd"
      ],
      0,
      "8c4e030c4a5b5f0234205ab4074b6bac"
    ],
    [
      "DoublyLinkedListIface.has_next",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_6bceef2fe1a51f9aee1e75c41c68a03e"
      ],
      0,
      "e03ace1ef8459f09fbc07851e767e671"
    ],
    [
      "DoublyLinkedListIface.has_prev",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_6bceef2fe1a51f9aee1e75c41c68a03e"
      ],
      0,
      "b8b75316fa07832558c323c61c8c3f69"
    ],
    [
      "DoublyLinkedListIface.next_node",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4b7f486949c030b94228e6106566a490",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ce52b7121c636592230bd67a03c02599"
      ],
      0,
      "18d5e41640220ef7ff7e8fb68f081970"
    ],
    [
      "DoublyLinkedListIface.prev_node",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_98e6e2f79e76c56949096085c8061d51",
        "refinement_interpretation_Tm_refine_ce52b7121c636592230bd67a03c02599"
      ],
      0,
      "d7b78c321fb0fe5281839ab366f2eb1c"
    ],
    [
      "DoublyLinkedListIface.l_insert_before",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_18b4556aabc6626d8d5bc2bb83aa5d71"
      ],
      0,
      "47b6deaebebe3783a11c47e60dd778c9"
    ],
    [
      "DoublyLinkedListIface.l_insert_after",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit",
        "disc_equation_Prims.Cons", "equation_FStar.List.Tot.Base.hd",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "kinding_Prims.list@tok",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_18b4556aabc6626d8d5bc2bb83aa5d71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.List.Tot.Base.length",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
      ],
      0,
      "c89c30261aa6fdf650aca215725de446"
    ],
    [
      "DoublyLinkedListIface.l_insert_after'",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "disc_equation_Prims.Cons",
        "equation_FStar.Pervasives.Native.snd",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list", "kinding_Prims.list@tok",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_513bd087ae2f2716a3ebb59386c2db50",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
      ],
      0,
      "4c047ce118f95d153850faad6049832b"
    ],
    [
      "DoublyLinkedListIface.l_remove_head",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion",
        "refinement_interpretation_Tm_refine_3f6b38b2852708f36615f9b4db0f9ff1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "88d554438db93113c51870993396c980"
    ],
    [
      "DoublyLinkedListIface.l_remove_mid",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons",
        "equation_FStar.List.Tot.Base.hd", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "kinding_Prims.list@tok",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.List.Tot.Base.length",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
      ],
      0,
      "d6ff4fb483dda045893ec3873f1ae1b6"
    ],
    [
      "DoublyLinkedListIface.l_remove_mid'",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "disc_equation_Prims.Cons",
        "equation_FStar.Pervasives.Native.snd",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list", "kinding_Prims.list@tok",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
      ],
      0,
      "c9e58c694cddaea77b93943fa766e697"
    ],
    [
      "DoublyLinkedListIface.dll_insert_before",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_4d912e105966ac35136c583fe866a795"
      ],
      0,
      "521599c591f4e7a9170f829379df9a43"
    ],
    [
      "DoublyLinkedListIface.dll_insert_after",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4d912e105966ac35136c583fe866a795",
        "refinement_interpretation_Tm_refine_ce52b7121c636592230bd67a03c02599"
      ],
      0,
      "79e392942c9c3da07fb0f96d31643c74"
    ],
    [
      "DoublyLinkedListIface.dll_remove_head",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons",
        "disc_equation_Prims.Cons",
        "equation_DoublyLinkedListIface.as_payload_list",
        "equation_FStar.List.Tot.Base.hd", "equation_Prims.nat",
        "equation_with_fuel_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_Addition",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_3aac47f90ec5f312f230a639872610fd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_DoublyLinkedListIface.as_list",
        "typing_DoublyLinkedListIface.node"
      ],
      0,
      "789a87a6c8e35bdbc2846ff1afaeeb62"
    ],
    [
      "DoublyLinkedListIface.dll_remove_tail",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons",
        "disc_equation_Prims.Cons",
        "equation_DoublyLinkedListIface.as_payload_list",
        "equation_Prims.nat",
        "equation_with_fuel_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_Addition",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_3aac47f90ec5f312f230a639872610fd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_DoublyLinkedListIface.g_node_vals.fuel_instrumented",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_DoublyLinkedListIface.as_list",
        "typing_DoublyLinkedListIface.node"
      ],
      0,
      "1dd1ee95d54cbe8f1cd0fe4789bbfc3b"
    ],
    [
      "DoublyLinkedListIface.dll_remove_mid",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
        "@query", "data_elim_Prims.Cons", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
        "false_interp", "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7a3b887478da9d11fd253c0bb94bb7ba",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_DoublyLinkedListIface.as_list",
        "typing_DoublyLinkedListIface.node"
      ],
      0,
      "cd67edddc487f5a00c79552b83d337f9"
    ],
    [
      "DoublyLinkedListIface.dll_split_using",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_75b973181c1e06bed5da9965f6c8c60c"
      ],
      0,
      "38384e03b4930a7ee5c08aad126c0145"
    ]
  ]
]