Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Lib.Sequence.Lemmas.fst.hints
[
"6�t�q&\u001d�=��\u001cn���",
[
[
"Lib.Sequence.Lemmas.map_blocks_vec_equiv_pre",
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_Prims.nat",
"equation_Prims.pos", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "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_7d90ff2f12815f81a295a11e6f29235e",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"e6adae87cdac8de91a7ced39fa8e6b05"
],
[
"Lib.Sequence.Lemmas.map_blocks_vec_equiv_pre",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"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.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash", "equation_Prims.subtype_of",
"int_inversion", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_824da4eabc6ac6d5c984b1ec60534f76",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
"unit_typing"
],
0,
"93d94ce3c064ce669c4512883cd7bf3c"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec_i",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_824da4eabc6ac6d5c984b1ec60534f76",
"refinement_interpretation_Tm_refine_8710a3dcbb7aeecb1da33ddf8070b919",
"typing_Lib.Sequence.map_blocks"
],
0,
"ca2fbe1bc10995350f34f163ced5ce40"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec_i",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e"
],
0,
"f13befdedb96581e432e13fc9bb00d39"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec_i",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_42c7944beb4de731cb59df7bf03023e1",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_a3ec56f110c69b031a3e4ccd219d9b24",
"Lib.Sequence_interpretation_Tm_arrow_24d6c2eeed5985153dd3de637e4e9d92",
"Lib.Sequence_interpretation_Tm_arrow_332b1ea1a0cfec68b92823596eb548e6",
"Lib.Sequence_interpretation_Tm_arrow_e758e9123a587b0ffb58bf693a073014",
"Lib.Sequence_interpretation_Tm_arrow_efd714987712642bce73b6a439af3d22",
"eq2-interp",
"equation_Lib.Sequence.Lemmas.map_blocks_vec_equiv_pre",
"equation_Lib.Sequence.get_block", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.l_Forall",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"int_inversion", "int_typing",
"l_quant_interp_dd4a75b19ecd43121fc88e03becd8902",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1f6c16a51cd4ba3256b95ca590c832c5",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_3c95b2e85447abd45d87cb083c2241b1",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_44fce4eb41a71668f7b0d92c3f052579",
"refinement_interpretation_Tm_refine_4e46b18e6de7fd724da2ef45eb7b3ba2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6e46224416d7840217015521fce4453b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_824da4eabc6ac6d5c984b1ec60534f76",
"refinement_interpretation_Tm_refine_8710a3dcbb7aeecb1da33ddf8070b919",
"refinement_interpretation_Tm_refine_bb0b8197bb42e9a1aaebe59e97685233",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_f0c1e15a29e66147d883478f9bc4a727",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.get_block",
"typing_Lib.Sequence.get_last", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.length"
],
0,
"1ae95ece6d9db027dfdff737cb757297"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e"
],
0,
"c043d9e98ec0bf88e2c34052859ef9ef"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e"
],
0,
"d463cae61b791b4ecb3c3a3399eddc8e"
],
[
"Lib.Sequence.Lemmas.lemma_map_blocks_vec",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_42c7944beb4de731cb59df7bf03023e1",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_a3ec56f110c69b031a3e4ccd219d9b24",
"Lib.Sequence_interpretation_Tm_arrow_24d6c2eeed5985153dd3de637e4e9d92",
"Lib.Sequence_interpretation_Tm_arrow_efd714987712642bce73b6a439af3d22",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_intro",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1f6c16a51cd4ba3256b95ca590c832c5",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_3c95b2e85447abd45d87cb083c2241b1",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4e46b18e6de7fd724da2ef45eb7b3ba2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_824da4eabc6ac6d5c984b1ec60534f76",
"refinement_interpretation_Tm_refine_8710a3dcbb7aeecb1da33ddf8070b919",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd",
"typing_Lib.Sequence.map_blocks"
],
0,
"c07b0313bec1d38b5eb915d498e0407c"
],
[
"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,
"5f49439cf989e744f7f54dd104aaa909"
],
[
"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,
"a80e7acdc359f3a3ccc20033f4b61720"
],
[
"Lib.Sequence.Lemmas.repeati_right_extensionality",
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_54c3ba9c6cc0203b91208dbe209fe9b7",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"a2ee36f62be59f4473e8b0db6984858e"
],
[
"Lib.Sequence.Lemmas.repeati_right_extensionality",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Properties_interpretation_Tm_arrow_67c7b2626869cb316f118144000415b9",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.Sequence.Lemmas_interpretation_Tm_arrow_f715d9c45d58a4f120f57b15a310761a",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_a35d68fb210a5c8491a1fe21a78d90fe_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_bcc2f6f9f4295168fb705265fe290244_5",
"binder_x_e09860b75d8922ab497a3e5bc9347578_7",
"binder_x_fe28d8bcde588226b4e538b35321de05_1",
"equation_Lib.LoopCombinators.fixed_a", "equation_Prims.nat",
"function_token_typing_Lib.LoopCombinators.fixed_a",
"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_24e0f7a4ca49aa53202cb61b2d7edc7c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_622464fca245921c9ddd8551e6567101",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_e6651b74fd10aa11130b6626c647d515",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"refinement_interpretation_Tm_refine_fb92f957c6718b5dce11e5cb4a82332e",
"token_correspondence_Lib.LoopCombinators.fixed_a",
"typing_Lib.LoopCombinators.repeat_right",
"well-founded-ordering-on-nat"
],
0,
"1a1f0fcadb90e3f097df2d6874b87931"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
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_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",
"refinement_interpretation_Tm_refine_bb0b8197bb42e9a1aaebe59e97685233"
],
0,
"2b4d810e7710ccf881c07378922cd97c"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c9a804b1d55b34f376c2198ffde5c6b1"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"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",
"lemma_FStar.Seq.Properties.slice_length",
"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_1c325641987cce6783228428bd15a869",
"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",
"refinement_interpretation_Tm_refine_bb0b8197bb42e9a1aaebe59e97685233",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"d458deed0f1f93f1b3f4ab0da904108f"
],
[
"Lib.Sequence.Lemmas.lemma_aux",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"21e02fd8fb9a9ac110d28b46868da606"
],
[
"Lib.Sequence.Lemmas.lemma_aux",
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_Minus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f67136332d586762a9522b027e0cba8f"
],
[
"Lib.Sequence.Lemmas.lemma_aux2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7fb6a1c358810743a7e153a3c53a1807"
],
[
"Lib.Sequence.Lemmas.lemma_aux2",
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_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"94591cb2f64cb3862a4c50f2cc91c299"
],
[
"Lib.Sequence.Lemmas.lemma_aux3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e74e7bb4b2f54d7aed405508ec2c0a69"
],
[
"Lib.Sequence.Lemmas.lemma_aux3",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9edd3e1657d1e6be880115e98ae2a55c"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
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_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual",
"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_596ec1b41cf453090618f08b7bf62083",
"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,
"44db75bff944e74c2ba26592d4b257d6"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"68a36554e68cb8f683e8190c51a7925f"
],
[
"Lib.Sequence.Lemmas.aux_repeat_bf_s1",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length",
"equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"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_09378811719f1db9568e56774ba6685e",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2aa4ee2b8fa3e2c3e461553307b0a540",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_596ec1b41cf453090618f08b7bf62083",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_Lib.Sequence.length"
],
0,
"6f4102cde288e62e86d5008ce2fc3ca5"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split12",
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_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.length", "typing_Lib.Sequence.length"
],
0,
"fb226640aed97258a05db22e2ee6e50e"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split12",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"674df433ef8d0307fa386c2011228e7a"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split12",
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_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_596ec1b41cf453090618f08b7bf62083",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"cddbacc79d3ec1c9aa773aaa539f7c63"
],
[
"Lib.Sequence.Lemmas.lemma_aux4",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"48470fb7c55fc47a69ad9cbac2879291"
],
[
"Lib.Sequence.Lemmas.lemma_aux4",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Minus",
"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,
"a5cf2a2fc696e80a7c7762d77f3a5404"
],
[
"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,
"a4e89e3cb0eaacedafd1cff28ecc28f6"
],
[
"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,
"da384faedb1c3d6910d8c1c0d55aae67"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_multi_split",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_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_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_5839670106941c7a52e93e3779e15dba",
"refinement_interpretation_Tm_refine_5e9c3dad358c3890f342f5eeb42bb76e",
"refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.Sequence.length", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c53835f53f5b6cf7e89406b3c54fbb8c"
],
[
"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,
"3bdda38adddf4a99fd6c15062b150ad3"
],
[
"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,
"0fe1f7315684054af28db1a34074d5db"
],
[
"Lib.Sequence.Lemmas.repeat_blocks_split",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_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.Seq.Properties.slice_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_1ba8fd8bb363097813064c67740b2de5",
"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",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.Sequence.length", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"90e5ab3f2017dd290ab24a23ef8b5ad9"
],
[
"Lib.Sequence.Lemmas.repeat_w",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.lanes", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"ab2cab79645f378776f43daeb7e8ad88"
],
[
"Lib.Sequence.Lemmas.unfold_repeatw",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.lanes", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"979848267079b9b3c1d60a06295e4948"
],
[
"Lib.Sequence.Lemmas.unfold_repeatw",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.Sequence.Lemmas.lanes",
"equation_Lib.Sequence.Lemmas.repeat_w", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_Lib.IntTypes.pow2_2", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ee0890b9538254b053898937056d73dc"
],
[
"Lib.Sequence.Lemmas.lemma_repeati_vec",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.lanes", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"1aee782c7f57a15d08d255ca29a92205"
],
[
"Lib.Sequence.Lemmas.lemma_repeati_vec",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.lanes", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"018890ffa8d8a4daf3861f92e52ee326"
],
[
"Lib.Sequence.Lemmas.lemma_repeati_vec",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_f430f1421de1406ca4011434213a5489_2",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.lanes",
"equation_Lib.Sequence.Lemmas.repeat_w", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_214521be6835548f2f282adfe2372d8b",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_aacd5c5013e5b4b181bda5c667bdb087",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"well-founded-ordering-on-nat"
],
0,
"0b00e5a1f7e63a827b29501e4f58ab4e"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_load_acc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.lanes", "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_3015949e152d57179f3877cf7b8274b6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"edccf7ce511cdd1539ea54514c22eb58"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_load_acc",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.lanes", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"584871f165cded4a70486a52f7b48bcd"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_load_acc",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_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.Lemmas.lanes", "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_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"cae78626a6fc92550825965b0e27c277"
],
[
"Lib.Sequence.Lemmas.mul_assoc",
1,
0,
0,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"4889e9308bfce586455c6805d8fcaef6"
],
[
"Lib.Sequence.Lemmas.lemma_aux1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"beed502f1cbefe79770e172dfe596318"
],
[
"Lib.Sequence.Lemmas.lemma_aux1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "int_typing", "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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"4e30812a06fc9b6511f8d85c79159b86"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_vec",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.lanes", "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_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6",
"refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ecf83a296b6d78a99730a94b7c40973f"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_vec",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Lib.Sequence.Lemmas.lanes", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e"
],
0,
"04efb5bcc868c73729cf058b47060efe"
],
[
"Lib.Sequence.Lemmas.lemma_repeat_blocks_multi_vec",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.Lemmas.lanes", "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_3015949e152d57179f3877cf7b8274b6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bc66a0aecd55540258f8dcc397e03f9e",
"typing_Lib.Sequence.length"
],
0,
"28ece186163bfaf099d2cf260494af28"
]
]
]
Computing file changes ...
