[
  "\u0007øÛÃ\u0019(ZcïĨHá3{áØ",
  [
    [
      "Lib.UpdateMulti.Lemmas.split_at_last_lazy_nb_rem_spec",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "65b46e0a805c43732d1f7eeaf91aa768"
    ],
    [
      "Lib.UpdateMulti.Lemmas.split_at_last_lazy_nb_rem_spec",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "bool_inversion", "bool_typing",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "equation_Lib.UpdateMulti.split_at_last_nb_rem",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "typing_Lib.UpdateMulti.split_at_last_nb_rem", "unit_inversion",
        "unit_typing"
      ],
      0,
      "e95174b9ebee77c3b73a1cb04b60ab10"
    ],
    [
      "Lib.UpdateMulti.Lemmas.split_at_last_lazy_spec",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "64349d2d3f9f338e9224eed63e24404e"
    ],
    [
      "Lib.UpdateMulti.Lemmas.split_at_last_lazy_spec",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8",
        "equation_Lib.UpdateMulti.Lemmas.uint8",
        "equation_Lib.UpdateMulti.split_at_last_lazy",
        "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "equation_Lib.UpdateMulti.split_at_last_nb_rem",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_cc936e5a549dcdc2e3f9713145143490",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "typing_Lib.UpdateMulti.split_at_last_lazy",
        "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "typing_Lib.UpdateMulti.split_at_last_nb_rem"
      ],
      0,
      "909b42ec694e916b0da8491f834add75"
    ],
    [
      "Lib.UpdateMulti.Lemmas.repeat_f",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "5eaea60d2f232ed0db82aded3b2d511a"
    ],
    [
      "Lib.UpdateMulti.Lemmas.repeat_l",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45"
      ],
      0,
      "c70d8edce7cf2925604897c540f1801a"
    ],
    [
      "Lib.UpdateMulti.Lemmas.repeat_l_input",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Lib.UpdateMulti.Lemmas.repeat_l", "equation_Prims.pos",
        "int_inversion",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "747e4a2f9fa216c0918c914697d51d3f"
    ],
    [
      "Lib.UpdateMulti.Lemmas.update_full_is_repeat_blocks",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.UpdateMulti.Lemmas.uint8",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.pos",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "f621171ae063ac8f7bfb8a5183a740a9"
    ],
    [
      "Lib.UpdateMulti.Lemmas.update_full_is_repeat_blocks",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.UpdateMulti.Lemmas.uint8",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.pos",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1a630e99ddfba3fdbd16707c910c2e27"
    ],
    [
      "Lib.UpdateMulti.Lemmas.update_full_is_repeat_blocks",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_8a249fa91522e368ce1f88a8f21e1bc4_5",
        "binder_x_8a249fa91522e368ce1f88a8f21e1bc4_6",
        "binder_x_b72a68bdf8d51e4ab675643707e06c74_1",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.repeat_blocks_f",
        "equation_Lib.UpdateMulti.Lemmas.repeat_f",
        "equation_Lib.UpdateMulti.Lemmas.repeat_l",
        "equation_Lib.UpdateMulti.Lemmas.uint8",
        "equation_Lib.UpdateMulti.split_at_last",
        "equation_Lib.UpdateMulti.split_at_last_nb_rem",
        "equation_Lib.UpdateMulti.split_block",
        "equation_Lib.UpdateMulti.uint8",
        "equation_Lib.UpdateMulti.update_full", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_273466d1cf0308d7bacfa0935ec989e3",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_4e72460fd31ab6faf9d60fa0f6ecfff5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6418319cfc67d818d590ac71a5206b3d",
        "refinement_interpretation_Tm_refine_69505886a99bc48ceeb322f859e1df81",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b51f1fc8427c126fe38ed0de2545d4ec",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ebb6b88bcdebc331a6787f1f7d3095a2",
        "token_correspondence_Lib.UpdateMulti.Lemmas.repeat_f",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "well-founded-ordering-on-nat"
      ],
      0,
      "1c5480703f8aa273e24585f6a23c23ee"
    ]
  ]
]