[
  "�ưw�����,�\u0019p\u007f/�",
  [
    [
      "MerkleTree.New.High.Correct.__proj__MTO__item__olds",
      1,
      2,
      1,
      [
        "@query", "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_mt"
      ],
      0,
      "04b1a457e7a12cf81f4a001f484136ca"
    ],
    [
      "MerkleTree.New.High.Correct.mto_base",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5d77d151160281f6a18f1f1cef4379c7"
    ],
    [
      "MerkleTree.New.High.Correct.mto_spec",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_51422cbc1c7c70f67de5bed212fc28bc"
      ],
      0,
      "553261b692f6c3071718d89142bd7dd5"
    ],
    [
      "MerkleTree.New.High.Correct.create_mt_ok",
      1,
      2,
      1,
      [
        "@query", "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.create_empty_mt",
        "equation_MerkleTree.New.High.create_mt",
        "equation_MerkleTree.New.High.hash_init",
        "equation_MerkleTree.New.High.mt_insert",
        "proj_equation_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_i"
      ],
      0,
      "100c37fec236c7940fc87c58d0b6cb87"
    ],
    [
      "MerkleTree.New.High.Correct.create_mt_ok",
      2,
      2,
      1,
      [
        "@query", "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.Correct.mto_inv",
        "equation_MerkleTree.New.High.create_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_olds",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_mt",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_olds"
      ],
      0,
      "f508408ed67f1c6c840527a04ee90ef1"
    ],
    [
      "MerkleTree.New.High.Correct.mt_insert_ok",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_MerkleTree.New.High.mt_insert", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "refinement_interpretation_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt"
      ],
      0,
      "632dfc3559b9b27bf9acacfbe0b533f2"
    ],
    [
      "MerkleTree.New.High.Correct.mt_insert_ok",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.mto_inv",
        "equation_MerkleTree.New.High.mt_insert",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_olds",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_mt",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_olds",
        "refinement_interpretation_MerkleTree.New.High_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt"
      ],
      0,
      "0def8521f2c1999d3924da31565f94e0"
    ],
    [
      "MerkleTree.New.High.Correct.mt_flush_to_ok",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.mt_flush_to",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.nat",
        "primitive_Prims.op_LessThan",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.MT_hs",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_32c708e8003aa702efd9480633a3631c",
        "refinement_interpretation_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "refinement_interpretation_Tm_refine_9bcf7608e9c780de654070e916e3b081",
        "refinement_interpretation_Tm_refine_a890b6516b808fc1f746b2a0dd0cdc0f",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__j"
      ],
      0,
      "e8557729b95df03181d5776c75fd59e5"
    ],
    [
      "MerkleTree.New.High.Correct.mt_flush_to_ok",
      2,
      2,
      1,
      [
        "@fuel_correspondence_MerkleTree.New.High.Correct.Flushing.mt_flush_to_olds.fuel_instrumented",
        "@query", "equation_MerkleTree.New.High.Correct.mto_inv",
        "equation_MerkleTree.New.High.mt_flush_to",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_olds",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_mt",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_olds"
      ],
      0,
      "e1bab11d316c1852486118ec73e8483a"
    ],
    [
      "MerkleTree.New.High.Correct.mt_flush_ok",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.mt_flush_to",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "l_and-interp", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "proj_equation_MerkleTree.New.High.MT_rhs_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "refinement_interpretation_Tm_refine_32c708e8003aa702efd9480633a3631c",
        "refinement_interpretation_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_9bcf7608e9c780de654070e916e3b081",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__i",
        "typing_MerkleTree.New.High.__proj__MT__item__j"
      ],
      0,
      "51afd6cb23be8fa6dc0c254a448d11ff"
    ],
    [
      "MerkleTree.New.High.Correct.mt_flush_ok",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Flushing.mt_flush_to_olds.fuel_instrumented",
        "@query", "equation_MerkleTree.New.High.Correct.mto_inv",
        "equation_MerkleTree.New.High.mt_flush",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_olds",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_mt",
        "projection_inverse_MerkleTree.New.High.Correct.MTO_olds",
        "refinement_interpretation_MerkleTree.New.High_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt"
      ],
      0,
      "b1ed29280f7bc77cf31ff7d2b44cc61f"
    ],
    [
      "MerkleTree.New.High.Correct.mt_get_root_ok",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "data_elim_MerkleTree.New.High.Correct.MTO",
        "equation_MerkleTree.New.High.Correct.old_hashes",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.hash_ss",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "fuel_guarded_inversion_MerkleTree.New.High.Correct.mt_olds",
        "proj_equation_MerkleTree.New.High.Correct.MTO_mt",
        "proj_equation_MerkleTree.New.High.Correct.MTO_olds",
        "refinement_interpretation_Tm_refine_88aa594a996383bdf2b36e1a01a97181",
        "refinement_interpretation_Tm_refine_88b2421350c3a459eae3f69956c7e70c",
        "typing_MerkleTree.New.High.Correct.__proj__MTO__item__mt"
      ],
      0,
      "330147526a6cde0cc9967e922711e530"
    ],
    [
      "MerkleTree.New.High.Correct.mt_get_root_ok",
      2,
      2,
      1,
      [ "@query", "equation_MerkleTree.New.High.Correct.mto_inv" ],
      0,
      "afdbcc9ad5bfc3217933b9377afde751"
    ],
    [
      "MerkleTree.New.High.Correct.mt_get_path_ok",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.Correct.mto_base",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.path",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "fuel_guarded_inversion_MerkleTree.New.High.Correct.mt_olds",
        "function_token_typing_MerkleTree.New.High.hash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
        "refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_906c6795e9fdf151ce3da1c23a66fcb7",
        "refinement_interpretation_Tm_refine_a5a7fb1fc3218e358d5c574055166e92",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ed2ae499cd8c6fde3c635dcdab10145e",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_ff29f835becb67c2f7617c8e3df7c97e",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.mto_base",
        "typing_MerkleTree.New.High.mt_path_length"
      ],
      0,
      "ec76a845866d04bdecfd8e1410cb6e28"
    ],
    [
      "MerkleTree.New.High.Correct.mt_get_path_ok",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.mto_base",
        "equation_MerkleTree.New.High.Correct.mto_inv",
        "equation_MerkleTree.New.High.Correct.mto_spec",
        "fuel_guarded_inversion_MerkleTree.New.High.Correct.mt_olds"
      ],
      0,
      "3c83a029e808aaa70786e1232947e5ac"
    ],
    [
      "MerkleTree.New.High.Correct.mt_verify_ok",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.path", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "function_token_typing_MerkleTree.New.High.hash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
        "refinement_interpretation_Tm_refine_85e9bb54d06cdc6388e1f9b9ed33ad11",
        "refinement_interpretation_Tm_refine_a5a7fb1fc3218e358d5c574055166e92",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d75f77191dffd5455e47d8155177febe",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.mt_path_length"
      ],
      0,
      "9fe2bfdd7518cbb8125e104464978abb"
    ],
    [
      "MerkleTree.New.High.Correct.mt_verify_ok",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "1055221ff04e35c56e3756955d2e6e8a"
    ]
  ]
]