[
  "��\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,
      "65f2b78ae0cc0fdd58e0397f143ef193"
    ],
    [
      "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,
      "9e5d06f0d085cdcbba77f65b586917a6"
    ],
    [
      "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,
      "ecfa594feb545b8f249e54901b9d020c"
    ],
    [
      "Lib.Loops.while",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "refinement_interpretation_Tm_refine_557d46919d3626ac17d05f14a46b11ea"
      ],
      0,
      "118ee07d83418be9ccde93708ed8aa2f"
    ],
    [
      "Lib.Loops.while",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "refinement_interpretation_Tm_refine_557d46919d3626ac17d05f14a46b11ea"
      ],
      0,
      "762e977d21d4763b2e4c6dca17166b4b"
    ],
    [
      "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,
      "3f313ea179e5b5fa996053d3f35afc1d"
    ]
  ]
]