[
  "��\u0004'��zpl<�͜�8k",
  [
    [
      "Lib.Loops.for",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b64ab56da311d7423a716ac175775c0",
        "refinement_interpretation_Tm_refine_24a2e4e4002dd35f896b1f3735743821",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "933910a405652d5c5d9d287d61b40c76"
    ],
    [
      "Lib.Loops.for",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b64ab56da311d7423a716ac175775c0",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5ffa7cb512a09f549b0f8556ab8c9408"
    ],
    [
      "Lib.Loops.for",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0b8220cf7e7ff415083e158443454dd5",
        "refinement_interpretation_Tm_refine_1b0248fedbadce73896fd7f3ff619e7d",
        "refinement_interpretation_Tm_refine_1b64ab56da311d7423a716ac175775c0",
        "refinement_interpretation_Tm_refine_24a2e4e4002dd35f896b1f3735743821",
        "refinement_interpretation_Tm_refine_61fd6148accc5adbb68c65bd9eda0ba2",
        "refinement_interpretation_Tm_refine_92416b39f687a537c60d4066b8811ee9",
        "refinement_interpretation_Tm_refine_b491442e9e2be77ffc95941336b90d77",
        "refinement_interpretation_Tm_refine_c60d5c4708a8d5fbe46629889520a08c",
        "refinement_interpretation_Tm_refine_ca99ef8fc06619f214d1a3dfb5454c98",
        "refinement_interpretation_Tm_refine_dc6d0f6877796d0e4cc71dde2abea33b",
        "typing_Lib.RawIntTypes.size_from_UInt32",
        "typing_Lib.RawIntTypes.size_to_UInt32"
      ],
      0,
      "69a12aacedb926a02e6716826f2cb6e5"
    ],
    [
      "Lib.Loops.while",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "refinement_interpretation_Tm_refine_557d46919d3626ac17d05f14a46b11ea"
      ],
      0,
      "ebcc6034f94cd28db578e5b29ed873e0"
    ],
    [
      "Lib.Loops.while",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "refinement_interpretation_Tm_refine_557d46919d3626ac17d05f14a46b11ea"
      ],
      0,
      "f8bba57a957003313729ec4eef19980a"
    ],
    [
      "Lib.Loops.while",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "lemma_FStar.Map.lemma_ContainsDom",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_acfe154edf7116150a3423acd08e4fdc",
        "refinement_interpretation_Tm_refine_fe39771c35a4b4c696cab447d642fea7",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip"
      ],
      0,
      "6fb7dd7e7645370453b90c41a234dc16"
    ]
  ]
]