Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.Math.Poly2.Lemmas.fst.hints
[
"��\"�2(w!P\u0003��=B6�",
[
[
"Vale.Math.Poly2.Lemmas.lemma_pointwise_equal",
1,
1,
0,
[ "@query" ],
0,
"c4ef691a4fdac18e43f8d23b95806f2d"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_define_forward",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxInt_proj_0",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"98c1d4013879827fcb7d27bc280acf5c"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mask_define",
1,
1,
0,
[ "@query" ],
0,
"725d6b372860f924bf4d077f9df32e57"
],
[
"Vale.Math.Poly2.Lemmas.lemma_degree_negative",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"c4eadb7b6bbc870df8e6ad2d89ae267b"
],
[
"Vale.Math.Poly2.Lemmas.lemma_degree_is",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "int_inversion",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "typing_Vale.Math.Poly2_s.degree"
],
0,
"e16aabfe0bcc048f3f926858d3119c3a"
],
[
"Vale.Math.Poly2.Lemmas.lemma_zero_degree",
1,
1,
0,
[
"@query", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"29c62cf3b07e6a9207d469f02dfb0f18"
],
[
"Vale.Math.Poly2.Lemmas.lemma_one_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"7932e2306113cbeb2e6566460319c265"
],
[
"Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f3ffb6ddd8b9fc0077f4298e27a6561d"
],
[
"Vale.Math.Poly2.Lemmas.lemma_ones_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"d10d65994664e7aff17f6547a6f7561b"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"2f912cc42817286ebca6b0c3336b3992"
],
[
"Vale.Math.Poly2.Lemmas.lemma_and_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "int_inversion",
"primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.degree"
],
0,
"932a537282bd482b424d5f8e0c894cee"
],
[
"Vale.Math.Poly2.Lemmas.lemma_or_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.Math.Lib.max", "int_inversion",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
"typing_FStar.Math.Lib.max", "typing_Vale.Math.Poly2.poly_or",
"typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"b761ed75dcd4c91f5817e4a219909c41"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mask_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.degree"
],
0,
"80cfa8f610dc6e0227a2a0f44827b423"
],
[
"Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.reverse"
],
0,
"ddf3c726620afcca312211f461d8a593"
],
[
"Vale.Math.Poly2.Lemmas.lemma_of_list_degree",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Prims.bool", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.List.Tot.Base.length"
],
0,
"9f7e3b5bc48d7fd40b8756b2641dce6a"
],
[
"Vale.Math.Poly2.Lemmas.lemma_of_list_degree",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "constructor_distinct_Tm_unit",
"disc_equation_Prims.Cons", "equation_FStar.List.Tot.Base.tail",
"equation_FStar.List.Tot.Base.tl", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Properties.lemma_seq_of_list_index",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_52187ccee49c0e09e68a24ca1902f0fc",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e",
"refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_FStar.List.Tot.Base.length", "typing_FStar.List.Tot.Base.tl",
"typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"9fac22dcb5c49bf55288f617f89a97db"
],
[
"Vale.Math.Poly2.Lemmas.lemma_add_zero_left",
1,
1,
0,
[ "@query" ],
0,
"97a31354c8c66846b8809ae0d65a7ddf"
],
[
"Vale.Math.Poly2.Lemmas.lemma_add_all",
1,
1,
0,
[ "@query" ],
0,
"de946d4988a44eda7e40c74ef3bde945"
],
[
"Vale.Math.Poly2.Lemmas.lemma_bitwise_all",
1,
1,
0,
[ "@query" ],
0,
"44ab83e6b070ba4246d88265c539e7c4"
],
[
"Vale.Math.Poly2.Lemmas.lemma_monomial_add_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"27663e4a1885a03ac1805ac5b29a6957"
],
[
"Vale.Math.Poly2.Lemmas.lemma_and_zero",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"primitive_Prims.op_AmpAmp", "typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"18ae36cf70eecaae6ac7519e2f5faf9b"
],
[
"Vale.Math.Poly2.Lemmas.lemma_and_ones",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"46679611617bacf98bbb3d751a1a0465"
],
[
"Vale.Math.Poly2.Lemmas.lemma_and_consts",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"98384ac37dd30f167ab35c50627de109"
],
[
"Vale.Math.Poly2.Lemmas.lemma_or_zero",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"primitive_Prims.op_BarBar", "typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"25e461e7025445d491d87597e35cd1ff"
],
[
"Vale.Math.Poly2.Lemmas.lemma_or_ones",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2.poly_or",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"d8bfb37d19cbed8cec99cc5aac70dcaf"
],
[
"Vale.Math.Poly2.Lemmas.lemma_or_consts",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e8199a6d21a43b2ed4819f7f1b47fb19"
],
0,
"29da3ddd4ee1414ec9b302e7513c9f5d"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_distribute_left",
1,
1,
0,
[ "@query" ],
0,
"0ac23c34f6d1db8900fb4bf1200ab328"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_smaller_is_zero",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"typing_Vale.Math.Poly2_s.degree"
],
0,
"23a59530d4af2799d571112b5c428800"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_monomials",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"99457385a1d64bcb4cf833c59d83c911"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_monomials",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"eddd22aab7a0fa79f5672595b723bf93"
],
[
"Vale.Math.Poly2.Lemmas.lemma_add_reverse",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse"
],
0,
"6a031ee0c2a4ffdf6874cf4f1cc4f1a5"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"3402ebb12f4b64ea7d1209d96d28cde4"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_typing",
"lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"d166f985a9ad20d81ccd4cd84635dd44"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_is_mul_left",
1,
1,
0,
[ "@query" ],
0,
"03ec89f92d10c2d0ef8402f9225a8ab4"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"04431a52d1e8f42f5c568089d960e89e"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mul_all",
1,
1,
0,
[ "@query" ],
0,
"41b50069df121c840acea6d5c9cfe684"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_distribute",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"4e64844dfa64689f74155bbea8688032"
],
[
"Vale.Math.Poly2.Lemmas.lemma_div_mod_unique",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "int_inversion",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"a285d5b8eb5beea3831893f7821a30ef"
],
[
"Vale.Math.Poly2.Lemmas.lemma_div_mod_exact",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303"
],
0,
"729547e90e4acb30653160a77c5e1ff7"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_small",
1,
1,
0,
[ "@query" ],
0,
"d1026561c43ce4979ecfa4cc1ba28cd9"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_mod",
1,
1,
0,
[ "@query", "lemma_Vale.Math.Poly2.lemma_mod_degree" ],
0,
"0299ac682fd15327b9f835aab5877125"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_cancel",
1,
1,
0,
[ "@query" ],
0,
"a61e71e9418ed6c2875be354afc12e8a"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_mul_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"int_inversion", "lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"96ff43fa03e6fe9abe23f7569046724a"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_mul_mod_right",
1,
1,
0,
[ "@query", "typing_Vale.Math.Poly2_s.mod" ],
0,
"f6bc9cca0158839e1dc905aa27ee05de"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_mod",
1,
1,
0,
[ "@query" ],
0,
"79413c965625cd618d53ad555d76ef11"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_reduce",
1,
1,
0,
[ "@query", "typing_Vale.Math.Poly2_s.add" ],
0,
"4697f33439284e2a4316de988c17d184"
],
[
"Vale.Math.Poly2.Lemmas.lemma_split_define",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"0a8fcab79932334a04633ff9f18702c0"
],
[
"Vale.Math.Poly2.Lemmas.lemma_split_define_forward",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"92527d94963dc86490e4ca8fe9c53d83"
],
[
"Vale.Math.Poly2.Lemmas.lemma_combine_define",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"881f82bde9df383942b8a1a7f5255b99"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mask_is_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"1e9fc87d8ffdcb7cfa868dff8eab1d83"
],
[
"Vale.Math.Poly2.Lemmas.lemma_shift_is_div",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"5bb44d929a8cf14639f37e756a6020d1"
],
[
"Vale.Math.Poly2.Lemmas.lemma_mod_monomial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_Prims.nat", "int_inversion",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"2179bc5f26f7cbe1bde0a1a128e21f00"
]
]
]
Computing file changes ...
