Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Lib.Sequence.fsti.hints
[
"Po�rM�rӚ�4>E�\u0000�",
[
[
"Lib.Sequence.to_lseq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"refinement_interpretation_Tm_refine_63c2dd5c1d96d3ed77642e23ae97146c"
],
0,
"6eb73c1326b470d405a8c958da1cfd5b"
],
[
"Lib.Sequence.index",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"2e3cea4174e07908bb7cd9956fd3b398"
],
[
"Lib.Sequence.create",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"2141b0a0387d4a8ff8fc801c96343bf6"
],
[
"Lib.Sequence.concat",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
],
0,
"cfefb7cbbe69ae448e5ee69666ccb618"
],
[
"Lib.Sequence.to_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"8191284d73b96d9881f45fe3462e63c1"
],
[
"Lib.Sequence.of_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_f2f46e59ec8203b19b1042d057b66530"
],
0,
"c0a32c80454ff331a15f8512d7d2a89b"
],
[
"Lib.Sequence.of_list_index",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
"refinement_interpretation_Tm_refine_f2f46e59ec8203b19b1042d057b66530"
],
0,
"302caedd0183ad70cbe8e17f9ebc4f6e"
],
[
"Lib.Sequence.eq_intro",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq",
"refinement_interpretation_Tm_refine_42c42a38dac60cf556273cb50abc9e82",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"7b081c73e39f0ac681246601a89d57eb"
],
[
"Lib.Sequence.upd",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_62e53d9cfa59f3fc33281615a392dc08",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"40fe105bcd9bb3ddaa5481d2619dc087"
],
[
"Lib.Sequence.sub",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"f8b6dbf481d24d220b678e358cc7c1f6"
],
[
"Lib.Sequence.slice",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609"
],
0,
"4346d50a670458370d5a843052886679"
],
[
"Lib.Sequence.update_sub",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"ddbe10a5e877ed8cb1fe7ff212acc935"
],
[
"Lib.Sequence.lemma_update_sub",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03ea481677aa4f241e0fcf866da3eab4",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"042b18d723a29c3bf017e01993c584c5"
],
[
"Lib.Sequence.lemma_concat2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
],
0,
"d5ebf5042d21f121cf3280b766741048"
],
[
"Lib.Sequence.lemma_concat3",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00fa94391fe0cec5e77f0fd24a439f4e",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0"
],
0,
"ce2f01dca7babd96a80888dcc2d650b8"
],
[
"Lib.Sequence.update_slice",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609"
],
0,
"70e92186b64e86a7f87e414365479dcb"
],
[
"Lib.Sequence.update_slice",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609"
],
0,
"6b7805e60b76950187a138a80918f78b"
],
[
"Lib.Sequence.createi",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"07337fe540ed260c858ddfec967ca636"
],
[
"Lib.Sequence.mapi",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"3f926009923a96f74dda406decea5fa8"
],
[
"Lib.Sequence.map",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"991cd2069ad98d88a6be49c829cca34a"
],
[
"Lib.Sequence.map2i",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"bd73164bc09161470f77964cfdb19ba8"
],
[
"Lib.Sequence.map2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1"
],
0,
"6869f3c64b5d55e592fc96496b7d7c3b"
],
[
"Lib.Sequence.repeati_blocks",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_854ac88ba27f00b6ffd4e86ced11eaad"
],
0,
"709557ea24cb5c09ba339d8d4a25c005"
],
[
"Lib.Sequence.repeat_blocks_f",
1,
2,
1,
[ "@query" ],
0,
"6cab7fcaa9fa0833771cf575772568c0"
],
[
"Lib.Sequence.repeat_blocks_f",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_1c325641987cce6783228428bd15a869",
"refinement_interpretation_Tm_refine_1f6c16a51cd4ba3256b95ca590c832c5",
"refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length"
],
0,
"35d79737a19185b45563a385ad9f83d0"
],
[
"Lib.Sequence.repeat_blocks",
1,
2,
1,
[ "@query" ],
0,
"94d0c774431600cf8bcdd03e86110687"
],
[
"Lib.Sequence.lemma_repeat_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",
"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,
"d0887471c50f8d43662f495247ac9272"
],
[
"Lib.Sequence.repeat_blocks_multi",
1,
2,
1,
[ "@query" ],
0,
"ed10dc58dc16eea63cb84c52ff3cf3bd"
],
[
"Lib.Sequence.lemma_repeat_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"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_b14928a18ba707004108386997fed9d6",
"typing_Lib.Sequence.length"
],
0,
"61834ebbff8a18cec86d17f877fb1160"
],
[
"Lib.Sequence.generate_blocks",
1,
2,
1,
[
"@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_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"adeb7d10d85cd38dbc0af93a2f346ac9"
],
[
"Lib.Sequence.generate_blocks_simple",
1,
0,
0,
[ "@query" ],
0,
"a8b8556108b67ea704bb70098a2a329a"
],
[
"Lib.Sequence.div_interval",
1,
0,
0,
[ "@query" ],
0,
"543ba1c25c2446231dd291fe12637c1f"
],
[
"Lib.Sequence.mod_interval_lt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"62705474138df4ec869ed4b39866a1a8"
],
[
"Lib.Sequence.div_mul_lt",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"012cdd59f5a62d14df4933dc49d86c12"
],
[
"Lib.Sequence.mod_div_lt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8a6cb7b721d5bc5092c119854316423a"
],
[
"Lib.Sequence.div_mul_l",
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,
"46b2634239136527112604ceb4a50a13"
],
[
"Lib.Sequence.map_blocks_f",
1,
0,
0,
[ "@query" ],
0,
"f097774d8178160a145213e16c5d9311"
],
[
"Lib.Sequence.map_blocks_f",
2,
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.map_blocks_a",
"equation_Lib.Sequence.seq", "equation_Prims.nat", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"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_1c325641987cce6783228428bd15a869",
"refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
],
0,
"fdd9a1fbe9ab3247c234fa3ed20d1148"
],
[
"Lib.Sequence.map_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"6c1254c328fee82c9fd2fa4a487bc7fa"
],
[
"Lib.Sequence.lemma_map_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"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_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"dc358678f081591b637efcc61ffe176e"
],
[
"Lib.Sequence.index_map_blocks_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"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_07295705544891065e7a01d318c0ba51",
"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_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.length"
],
0,
"0aa6cc8d626bd99b5a03dc1c1fb0e92c"
],
[
"Lib.Sequence.block",
1,
0,
0,
[ "@query" ],
0,
"69c5664651990ec8e881f624a2af5b49"
],
[
"Lib.Sequence.last",
1,
0,
0,
[ "@query" ],
0,
"2166fbda297fd121f155b59566ade410"
],
[
"Lib.Sequence.map_blocks",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_854ac88ba27f00b6ffd4e86ced11eaad"
],
0,
"5fd63cdf8b17721d7180de32deb08674"
],
[
"Lib.Sequence.lemma_map_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_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,
"b28775d56eb095b5e494b7d02a818c99"
],
[
"Lib.Sequence.get_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e4082c6287043c8ddc6398742434f6ba"
],
[
"Lib.Sequence.get_block",
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",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"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"
],
0,
"faaf24b0b347551eef0a3d5fae1aad50"
],
[
"Lib.Sequence.get_last",
1,
0,
0,
[ "@query" ],
0,
"8086547c11c30d635f6dbdc77eee684c"
],
[
"Lib.Sequence.get_last",
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_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_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_eeb59caff9a959bab0eef3a399bf14b7",
"typing_FStar.Seq.Base.length"
],
0,
"b64f5b45c20296ef6c3994150e6012e8"
],
[
"Lib.Sequence.index_map_blocks",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"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_824da4eabc6ac6d5c984b1ec60534f76",
"refinement_interpretation_Tm_refine_8710a3dcbb7aeecb1da33ddf8070b919",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.Sequence.map_blocks"
],
0,
"d15c5483fa52a7df740644af472019de"
],
[
"Lib.Sequence.eq_generate_blocks0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"9dcf6072646a82cb13caef73e32062fe"
],
[
"Lib.Sequence.unfold_generate_blocks",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat", "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_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length"
],
0,
"2d1f983a75c763afb51d8d9450101fdf"
],
[
"Lib.Sequence.index_generate_blocks",
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.Sequence.length", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_Lib.IntTypes.pow2_values", "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_07295705544891065e7a01d318c0ba51",
"refinement_interpretation_Tm_refine_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_642416fe6039ccdba55bf60d260af469",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
"unit_typing"
],
0,
"dd57bf218c4dd19c9cf5fb15072a4270"
]
]
]
Computing file changes ...
