[
"Eｾ!\f広欄 ;w｡T徴",
[
[
"Lib.Sequence.Lemmas.get_block_s",
1,
2,
1,
[ "@query" ],
0,
"86cbab7738ec6884dc3d3c53ecc0ef1f"
],
[
"Lib.Sequence.Lemmas.get_block_s",
2,
8,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ade7773d9cd7cd1a2abc2fe3f191b9e0",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"7722efdeac4bd8bfd8a2acb1f6a436e1"
],
[
"Lib.Sequence.Lemmas.get_last_s",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "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",
"refinement_interpretation_Tm_refine_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bfc5057f18c06463ef12f29d59d8a1f8"
],
[
"Lib.Sequence.Lemmas.repeati_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_e7e6bda13570450ba98cae3dc5e7dd42",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_6781041e5072f14a03af8b07643f1f30_4",
"binder_x_b3a9ce008df0278184098b1a723bca0c_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_fe28d8bcde588226b4e538b35321de05_0", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3e839a4d245a3beb00e03b7402cb44c7",
"refinement_interpretation_Tm_refine_49c0ba66edcf02816cc411af6df0f144",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.LoopCombinators.repeati", "well-founded-ordering-on-nat"
],
0,
"ee488cd538f4bbe3dbd24670d8f49337"
],
[
"Lib.Sequence.Lemmas.repeat_right_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.squash", "int_inversion", "l_and-interp",
"l_quant_interp_36cc075b8d0bea9b5aba146210641116",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12aaa86fce4296e5ca537def690c90b7",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2"
],
0,
"8fbcc32259014d8e99b440fb9aa2806d"
],
[
"Lib.Sequence.Lemmas.repeat_right_extensionality",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.squash", "int_inversion", "l_and-interp",
"l_quant_interp_36cc075b8d0bea9b5aba146210641116",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12aaa86fce4296e5ca537def690c90b7",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c56ecf2214201c8b90e8cb243b13f511",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2"
],
0,
"435d3f521ccfa918aa1103dc6b8d1f08"
],
[
"Lib.Sequence.Lemmas.repeat_right_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_3c9ffd2296420cd469cf20686505163b",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_bd7c7ab284b6accd96708c0ff3164304",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_03d51f0b26b266821854328111855af2_3",
"binder_x_b730587d8140e227a7f8adbd92d65106_5",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_d26ec331d6bcfdfd046bf0c1c673bcf9_7", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_303b9c87ad41f9e78fc62ab2390b0125",
"refinement_interpretation_Tm_refine_3e9b52cb3027f42e52803d569c244fcb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_57bc50f9aa6e93b9844a8bd63512cb1c",
"refinement_interpretation_Tm_refine_94dd066518be63a31245723626aaa707",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"typing_Lib.LoopCombinators.repeat_right",
"well-founded-ordering-on-nat"
],
0,
"ca807fd835c32cee973be1cedd1b2665"
],
[
"Lib.Sequence.Lemmas.repeat_gen_right_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.squash", "int_inversion", "int_typing",
"l_and-interp", "l_quant_interp_761ad16230b0f948d65f71b7fddfa556",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2"
],
0,
"e7098cfb18eb94b3c0e65ab27cbc0b7d"
],
[
"Lib.Sequence.Lemmas.repeat_gen_right_extensionality",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.squash", "int_inversion", "int_typing",
"l_and-interp", "l_quant_interp_761ad16230b0f948d65f71b7fddfa556",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_dd2dcd8a3f5ccd37362555d4349c15e4",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2"
],
0,
"287dd8db050d9b371ca847814c58359c"
],
[
"Lib.Sequence.Lemmas.repeat_gen_right_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_27ab71f0fb6c81f0fa9dbba5ba46be75",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_809f84adfa1ee74319c7b9bd8825d36a",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_759fff43cce3e9ec96895cb58a55ec68_3",
"binder_x_82e1062e5a8fb0849c9f621f85a4d628_5",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_de4df547607739c850b1e55a67a124fe_7", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3e839a4d245a3beb00e03b7402cb44c7",
"refinement_interpretation_Tm_refine_49c0ba66edcf02816cc411af6df0f144",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_5d8689c3031a6af8b5491cc44c84ab43",
"refinement_interpretation_Tm_refine_6536ede8f313b115412245fc854378bd",
"refinement_interpretation_Tm_refine_b61962d44f25224004938818b1c4cd7b",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"typing_Lib.LoopCombinators.repeat_right",
"well-founded-ordering-on-nat"
],
0,
"ab4983e2b0cd0008078de9704da1c7a2"
],
[
"Lib.Sequence.Lemmas.repeati_right_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_54c3ba9c6cc0203b91208dbe209fe9b7",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"dc7df921313a4e1bc9af4a8370ab1cd4"
],
[
"Lib.Sequence.Lemmas.repeati_right_extensionality",
2,
0,
0,
[ "@query", "equation_Lib.LoopCombinators.fixed_a" ],
0,
"5f520f9f8d8214986cd498696943865a"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_f",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"67003ac3a24e7b06e116cff1272bda7d"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_f",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bbe86a0a6209b8c07083cd4c9f7f9aa5",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803"
],
0,
"383d7196d292f62310f5311ecb2caddc"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"6991de8de2c70dffa6031a8ceb17553a"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"06dc275660fbea717344a4de6f30ec53"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953"
],
0,
"9b7512b40d843d8a9bac959d7f3249d0"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"a5caa9dc2fc792498e86119cfd7bf2e5"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"1eb9cf80e090306dd960c6be47120e79"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks_multi",
3,
0,
0,
[ "@query", "equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi" ],
0,
"900d9788d532ef4e1886bd9b829dba54"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.Sequence.length"
],
0,
"0b3687672ccb5cc7289eced2a2fb9f20"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.Sequence.length"
],
0,
"91e9a46a998b8f1b96e9bc5e344cd2bd"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"f288a9c3d0f22ec76c1c824e514845d8"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"0fe5d02de75b8f8c7fa302bb13676792"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.Sequence.length"
],
0,
"26efb1b3626e7eff4c4562e3fad5b60b"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_gen_blocks",
3,
0,
0,
[ "@query", "equation_Lib.Sequence.Lemmas.repeat_gen_blocks" ],
0,
"b3a0ad067610090ddaf930d16d79c1a7"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_extensionality_zero",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash", "int_inversion",
"int_typing", "l_and-interp",
"l_quant_interp_e0c135c0d1d2d760fb7f155318d559d0",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"29ef5ecba0dfca0d4b934fc1b503b357"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_extensionality_zero",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"4f19c88833709aba3a61146d97ed32f7"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_extensionality_zero",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_f",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ba24c249c2bac9c9652dccf45aee8033",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice"
],
0,
"3ce25ccd67eca958c1ee52434dcf593a"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_extensionality_zero",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash", "int_inversion",
"int_typing", "l_and-interp",
"l_quant_interp_e0c135c0d1d2d760fb7f155318d559d0",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d0b9c0d9bab47c0f00a15221dd05c4"
],
0,
"1ac5614de2f4a1540eb6770f2bbfd14b"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_extensionality_zero",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"4178b3cd06c5ac9420933a125b3d8f25"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_extensionality_zero",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_46d0490fc1bcee17b1822abbbaec9be9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d0b9c0d9bab47c0f00a15221dd05c4",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"12753e7a2e975b1b12eea6b656de1e37"
],
[
"Lib.Sequence.Lemmas.len0_div_bs",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"cdae7dde3449ccb53d24809dd87b6a4c"
],
[
"Lib.Sequence.Lemmas.len0_div_bs",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ec9b1ae71ab6b37453f23913b719be17"
],
[
"Lib.Sequence.Lemmas.split_len_lemma0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"dfd7929aa143da98da9a499413c2a137"
],
[
"Lib.Sequence.Lemmas.split_len_lemma0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"adb2ef728b04223215fb5ad1e0a8a67d"
],
[
"Lib.Sequence.Lemmas.split_len_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"fc75c0f53ada351073fb237f851a53c7"
],
[
"Lib.Sequence.Lemmas.split_len_lemma",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f3718dda107305b0915ccc30515a8e1b"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_3b00410d9ccdeee0a4c7af332e73ce2f",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b859045a8681d0937b4cb9681dd787b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"typing_Lib.Sequence.length"
],
0,
"0fa1c45be1d4b3857e6376aa51001005"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"b6492eae468635372f04db3a4f898fba"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_f",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_3b00410d9ccdeee0a4c7af332e73ce2f",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b859045a8681d0937b4cb9681dd787b",
"refinement_interpretation_Tm_refine_bbe86a0a6209b8c07083cd4c9f7f9aa5",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"1dbd05075d9f4ee2bba8e9eb6a13553c"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c215e983d7915709bebb4fb7be5bb946",
"refinement_interpretation_Tm_refine_d478cde3e691462712f56114befc57a5",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"typing_Lib.Sequence.length"
],
0,
"b3c1b96b16c94981a8c9ae174e521078"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"1300e9f931b99e3a3d954301c1469f53"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_f",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bbe86a0a6209b8c07083cd4c9f7f9aa5",
"refinement_interpretation_Tm_refine_c215e983d7915709bebb4fb7be5bb946",
"refinement_interpretation_Tm_refine_d478cde3e691462712f56114befc57a5",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"typing_Lib.Sequence.length"
],
0,
"36f70891ed31f65f7eb756c6b88c7133"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.Sequence.length"
],
0,
"c02483b5c6058fba9c7951830081c7a8"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"b10923729a3d2007e7c2ad2375fb9ddf"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_24813cd65ccef7cf8c09228ba9bdbf64",
"refinement_interpretation_Tm_refine_3b00410d9ccdeee0a4c7af332e73ce2f",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b859045a8681d0937b4cb9681dd787b",
"refinement_interpretation_Tm_refine_c215e983d7915709bebb4fb7be5bb946",
"refinement_interpretation_Tm_refine_d478cde3e691462712f56114befc57a5",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"typing_Lib.Sequence.length"
],
0,
"08b4481b3d7f608421b1c708f3965c72"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split_slice",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_784bfde0144e58d81243bc1b47b4f0ec",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337"
],
0,
"df078790264376a994b289d487744d7f"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split_slice",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_784bfde0144e58d81243bc1b47b4f0ec",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"e9fe6e31a1dc50ec30edd553fb7f0793"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_multi_split_slice",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_784bfde0144e58d81243bc1b47b4f0ec",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_Lib.Sequence.length"
],
0,
"7c0ca19dc5e1c4732e5d9c25e50236ca"
],
[
"Lib.Sequence.Lemmas.slice_slice_last",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Lib.Sequence.length"
],
0,
"9f0c1f558fac585e8f190517d2a6142c"
],
[
"Lib.Sequence.Lemmas.slice_slice_last",
2,
0,
0,
[ "@query" ],
0,
"825d535492a704b4f046fdcbf9995319"
],
[
"Lib.Sequence.Lemmas.slice_slice_last",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_refl",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.slice", "typing_Lib.Sequence.length"
],
0,
"82de60f7a59b84571c910856112b2cc2"
],
[
"Lib.Sequence.Lemmas.len0_le_len_fraction",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"98e5616f3e2f321f3aced9cdf72b29cd"
],
[
"Lib.Sequence.Lemmas.len0_le_len_fraction",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e7c50dfae11cf4610d8aef722e9c5400"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_split",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_fcf14b481b3a84f47b67fc1dd0096ca5",
"typing_Lib.Sequence.length"
],
0,
"88b9f60f4ef3f2ef5278399b506ea3d1"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_split",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"d1c2e10881c112de50397ee1dccacdcc"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_split",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_75e501c8cccef1c521502f88a4640586",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_fcf14b481b3a84f47b67fc1dd0096ca5",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"f9742241fd3a1a24c2d673d6b922d1c4"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"7b6cfa24d38debb75017036d33fb3866"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_extensionality",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ec5ed995f9ce0b678554c57783401dcf"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ec36165acc8b3b8a1f151af217f53b8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.slice", "typing_Lib.Sequence.length"
],
0,
"ef5dccd0c888efad50942cadc03a1230"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_via_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Division", "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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"d8ad05675ff3524e376a5456739b3fb7"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_via_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2c2fc31df0b237dd032ca40f1efb51af"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_via_multi",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"typing_Lib.Sequence.length"
],
0,
"29bcf201b006e05be362bdbf225dccc5"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_is_repeat_gen_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_dc64ef62fd3101207c953516420ca99f",
"typing_Lib.Sequence.length"
],
0,
"a54da8555df38c60d0a8534c977093af"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_is_repeat_gen_blocks_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"bfdc912a1dc7b2b5390f527e63317c11"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_is_repeat_gen_blocks_multi",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.fixed_i",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_f",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"equation_Lib.Sequence.length",
"equation_Lib.Sequence.repeat_blocks_f", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7a73c35877b307cf436e11329be9e855",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_dc64ef62fd3101207c953516420ca99f",
"token_correspondence_Lib.LoopCombinators.fixed_i",
"typing_Lib.Sequence.length"
],
0,
"4c52a1e49b2ba638792bd6f274390611"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_is_repeat_gen_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f571f2610f867b24665eec96f119e18c"
],
0,
"dd9499c580703ded8d0ca9a556cf3b13"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_is_repeat_gen_blocks",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"cb8669c3929a74371c90f2fbb63d433d"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_is_repeat_gen_blocks",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.LoopCombinators.fixed_i",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"refinement_interpretation_Tm_refine_f571f2610f867b24665eec96f119e18c",
"token_correspondence_Lib.LoopCombinators.fixed_i",
"typing_Lib.Sequence.length"
],
0,
"a1691f4306a8f406e540c28000633548"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_split",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Minus",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e9c3dad358c3890f342f5eeb42bb76e",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Lib.Sequence.length"
],
0,
"cb3b800fab1de1c59a9a8292f0245393"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_split",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"39e0ce4b3a592efe1006be305d405b49"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_split",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.fixed_i",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e9c3dad358c3890f342f5eeb42bb76e",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"token_correspondence_Lib.LoopCombinators.fixed_i",
"typing_Lib.Sequence.length"
],
0,
"1b5580bbdaeffaecc17556b156dc1bfb"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Minus", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"40fb18f7713fac4a7892664b8f2ee83e"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"6883c8657a4d242e2a0eb61fffb3da9f"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.fixed_i",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"token_correspondence_Lib.LoopCombinators.fixed_i",
"typing_Lib.Sequence.length"
],
0,
"0ad5a935f383796cbb125449d54fab98"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a2b843812e379caba2433f5840048866"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_extensionality",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e171588ce471ccc7735bce5d4ead26cb"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_a203639a647d7d28da9a0faccf0492b8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.map_blocks_a",
"equation_Lib.Sequence.map_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Lib.Sequence.map_blocks_f", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ba24c249c2bac9c9652dccf45aee8033",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.slice",
"typing_Lib.Sequence.length"
],
0,
"ab989a029b8d86ea5f581ed65f835f0d"
],
[
"Lib.Sequence.Lemmas.map_blocks_extensionality",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Division", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.Sequence.length"
],
0,
"5453114231c5f5c707a311c8305c6274"
],
[
"Lib.Sequence.Lemmas.map_blocks_extensionality",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"fe966000e03bcf4dce9a22627119b354"
],
[
"Lib.Sequence.Lemmas.map_blocks_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Division", "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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.slice", "typing_Lib.Sequence.length"
],
0,
"8841769ee97b14128b803b618d1c6f80"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8de8e35110e3a286c7b5ebd97df26dfd"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.Sequence_interpretation_Tm_arrow_d3b9c37343cabe37d3e11c0a1cafa7da",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length"
],
0,
"364576c76615ad00afb7683a28646a7c"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d9f3b7c825a458d6bdbd80a2e4cce5f9"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_l_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"5001145b55425dd2ae0dea68eb71a2e6"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_l_length",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"1426b03773dffc7d60ce61b3d5603653"
],
[
"Lib.Sequence.Lemmas.repeat_gen_blocks_map_l_length",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_9dbede814c7e09cf989d879ebca4b33a",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803"
],
0,
"59450652dc1b7dcffbd94fa91923cb35"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"53dbe43eebf79d8fae5270e33519d6ee"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"bbbd8d5f723ac10d8ebef79a608ba8d4"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.map_blocks_a", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803"
],
0,
"8a25e2c4a12379469fb6fb635afb977d"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"4ad33283208ebc06e0a8c8bf73f701e9"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"8154c136ac7898860c37b1a344200ec1"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc",
3,
0,
0,
[ "@query" ],
0,
"d551794be313904d3f56da8f192a199d"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_length",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"0096e13027080df7d2f34ee37eedf0bd"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_length",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"9771fb9bc54b2f583f4f63c12f9b189c"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_length",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_9dbede814c7e09cf989d879ebca4b33a",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_ad45ae83d88485c5735bdf0782e8440e",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_f0f2eb385217bc59a5339bff3d4fdc88",
"Lib.Sequence_interpretation_Tm_arrow_7a0e6fdd04f738fd5fc5c4a3221f6c0a",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.map_blocks_acc",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
"function_token_typing_Lib.Sequence.map_blocks_a", "int_inversion",
"int_typing", "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_GreaterThan",
"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",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"token_correspondence_Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
"token_correspondence_Lib.Sequence.map_blocks_a",
"typing_FStar.Seq.Base.slice",
"typing_Lib.Sequence.Lemmas.map_blocks_acc",
"typing_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"typing_Lib.Sequence.length"
],
0,
"a13d14efe2ceb3e3e76be0ce42d93251"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_repeat_gen_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ac974e177b7398442be6245342bd2ca7"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_repeat_gen_blocks_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8c932e3618b035ed56bf9e4bb4c0d5aa"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_repeat_gen_blocks_multi",
3,
0,
0,
[ "@query", "equation_Lib.Sequence.Lemmas.map_blocks_multi_acc" ],
0,
"ab31576e630727b882a86f1ff0e8734b"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_repeat_gen_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"13028a408fd491d60ca398feabaefd38"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_repeat_gen_blocks",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"3dcf2f9f221f6b42567be170c0affefb"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_repeat_gen_blocks",
3,
0,
0,
[ "@query", "equation_Lib.Sequence.Lemmas.map_blocks_acc" ],
0,
"0e34c15f4e28d82d3703bc3828640f03"
],
[
"Lib.Sequence.Lemmas.f_shift",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3e62de47257cea2fd43f97d413cf4f9d"
],
[
"Lib.Sequence.Lemmas.f_shift",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"92488f9f9f2ad94db1231bff8b4f21a5"
],
[
"Lib.Sequence.Lemmas.l_shift",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f"
],
0,
"4db54197df79bc00c8e5edd4637efe82"
],
[
"Lib.Sequence.Lemmas.l_shift",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"fce077a3df6742226a1bad37467e1632"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi_",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cedbfc1f9a0199ea1d2d039a83d0b50f",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.empty", "typing_Lib.Sequence.length"
],
0,
"c2fe0e84ca25740086e92f82e29527e7"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi_",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cedbfc1f9a0199ea1d2d039a83d0b50f",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"refinement_interpretation_Tm_refine_ed72a44b20a4857da5ae5cff5caa2c1d",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.empty", "typing_Lib.Sequence.length"
],
0,
"2df8bc19db5b107d646969eb491fd32c"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi_",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_f0aa2cd0cbd21d2c0749d4335c90581f",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_13a49770a881677ceb1fe0f760f300ae_1",
"binder_x_9caa9576d4c1ad3b0e97ef91b12afd21_5",
"binder_x_b31f2920fae1acea0665a8c14fa2054d_8",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_e1f78ce4a255666a7d239c31149b8f55_6",
"binder_x_fe28d8bcde588226b4e538b35321de05_0",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.f_shift",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_f",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.map_blocks_a",
"equation_Lib.Sequence.map_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals",
"equation_Prims.pos",
"function_token_typing_Lib.Sequence.map_blocks_a",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_19ff6668eed655f035f7f58d5d2659b6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8a6506292ccc20eb5c4cf1d8460ddbdb",
"refinement_interpretation_Tm_refine_a4a397079d7ea76ab85443b1137ac121",
"refinement_interpretation_Tm_refine_aacd5c5013e5b4b181bda5c667bdb087",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_db4109dc6119e88b617d40a03dd5557c",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"token_correspondence_Lib.Sequence.Lemmas.f_shift",
"token_correspondence_Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Lib.Sequence.length", "well-founded-ordering-on-nat"
],
0,
"1f3b42e7d994a2a406494e69b8daeb23"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f68cffa6dba4aabede1c709f3440fc0a"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f81833a6e606cb93ecb0dca7775b6c39"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.map_blocks_multi_acc",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.map_blocks_a",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Lib.Sequence.map_blocks_a", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e7fccb01210c2efde8affa46b16abcf2",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.empty"
],
0,
"14fcc30a6799227f57adb8a6cd0726f5"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"d7c3cd462c1b0bed1c208309ba210de7"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"typing_Lib.Sequence.length"
],
0,
"e6ce81bb7de04a226169822b2ef168e4"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_1c8e3695441d6e943fd420c55a9c2714",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_412ce3d8acd0125f78456a0e770dea0e",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_53c1cff0fc95f4065a8aa916a14dae1d",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_707f1100325826b024437354577c9bb0",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_8f12e8ab379230615398022b448d6596",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_9dbede814c7e09cf989d879ebca4b33a",
"Lib.Sequence_interpretation_Tm_arrow_24d6c2eeed5985153dd3de637e4e9d92",
"Lib.Sequence_interpretation_Tm_arrow_d3b9c37343cabe37d3e11c0a1cafa7da",
"Lib.Sequence_interpretation_Tm_arrow_efd714987712642bce73b6a439af3d22",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.l_shift",
"equation_Lib.Sequence.Lemmas.map_blocks_acc",
"equation_Lib.Sequence.Lemmas.map_blocks_multi_acc",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks",
"equation_Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Lib.Sequence.Lemmas.f_shift",
"function_token_typing_Lib.Sequence.Lemmas.l_shift", "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_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.Sequence.Lemmas.map_blocks_acc_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThan",
"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",
"refinement_interpretation_Tm_refine_1f6c16a51cd4ba3256b95ca590c832c5",
"refinement_interpretation_Tm_refine_25699f4de0c949c68e992e5573c8bf6d",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_54983c851ed3fe2f8809dd4f73bd5ffb",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8710a3dcbb7aeecb1da33ddf8070b919",
"refinement_interpretation_Tm_refine_8dd1dd228be3e5b616c46def4cb5b9b8",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_ef88cbfd1f224cec1819e89cfa0f6a00",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"token_correspondence_Lib.Sequence.Lemmas.f_shift",
"token_correspondence_Lib.Sequence.Lemmas.l_shift",
"token_correspondence_Lib.Sequence.Lemmas.repeat_gen_blocks_map_l",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.slice",
"typing_Lib.Sequence.Lemmas.map_blocks_acc",
"typing_Lib.Sequence.Lemmas.map_blocks_multi_acc",
"typing_Lib.Sequence.length", "typing_Lib.Sequence.map_blocks",
"typing_Lib.Sequence.map_blocks_multi"
],
0,
"566dd1e2bdf4ebb9e9d0ff0fb04b5dd1"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"75ea6f7c1c6df35ec8f7ec71e2083bd1"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"04f48f47b4e70a1ba946a1a31fb95624"
],
[
"Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_ad45ae83d88485c5735bdf0782e8440e",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_f0f2eb385217bc59a5339bff3d4fdc88",
"Lib.Sequence_interpretation_Tm_arrow_7a0e6fdd04f738fd5fc5c4a3221f6c0a",
"equation_Lib.Sequence.Lemmas.f_shift",
"equation_Lib.Sequence.Lemmas.map_blocks_multi_acc",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.map_blocks_a",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Lib.Sequence.Lemmas.repeat_gen_blocks_map_f",
"function_token_typing_Lib.Sequence.map_blocks_a", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_361ceade980020b5c15ebf36d114dc78",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f684e27d6af9965634108bcfe981953",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"token_correspondence_Lib.Sequence.Lemmas.f_shift",
"token_correspondence_Lib.Sequence.map_blocks_a",
"typing_FStar.Seq.Base.empty",
"typing_Lib.Sequence.Lemmas.repeat_gen_blocks_multi",
"typing_Lib.Sequence.length"
],
0,
"63471c503f4ba248bc16dcc91aa8ca8c"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f571f2610f867b24665eec96f119e18c"
],
0,
"34c3fc1034c5e695526218d7b19e3db6"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"97bb1cf6b8c76730d95a43377a924168"
],
[
"Lib.Sequence.Lemmas.map_blocks_acc_is_map_blocks0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.f_shift",
"equation_Lib.Sequence.Lemmas.l_shift",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.map_blocks_a",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"refinement_interpretation_Tm_refine_f571f2610f867b24665eec96f119e18c",
"token_correspondence_Lib.Sequence.Lemmas.f_shift",
"token_correspondence_Lib.Sequence.Lemmas.l_shift",
"typing_FStar.Seq.Base.empty", "typing_Lib.Sequence.length"
],
0,
"c331ff1704b6612a2d33781ec7e99034"
],
[
"Lib.Sequence.Lemmas.map_blocks_is_empty",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7ad90407dad3095183eb4d692b62fd08"
],
0,
"eb09639dfad0d7a25f81dce9b3b6de5c"
],
[
"Lib.Sequence.Lemmas.map_blocks_is_empty",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0b982abf2c3b4cac65966093b2a2a21a"
],
[
"Lib.Sequence.Lemmas.map_blocks_is_empty",
3,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.Sequence_interpretation_Tm_arrow_d3b9c37343cabe37d3e11c0a1cafa7da",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.map_blocks_a", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"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",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7ad90407dad3095183eb4d692b62fd08",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_Lib.Sequence.length", "typing_Lib.Sequence.map_blocks_multi"
],
0,
"7cdb15f5ad022d2fe28845edb0d9499e"
]
]
]