[ "ÑÈ\"Ê2(w!P\u0003¯û=B6¡", [ [ "Vale.Math.Poly2.Lemmas.lemma_pointwise_equal", 1, 1, 0, [ "@query" ], 0, "64c2d31d9493abf50ab6a87adea81f11" ], [ "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, "7c3c8577a21cac67368cb548db7aadb5" ], [ "Vale.Math.Poly2.Lemmas.lemma_mask_define", 1, 1, 0, [ "@query" ], 0, "fb61664187c6c81f01433e80e25458fa" ], [ "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, "b022b789bb2296471936ca85c56de5b0" ], [ "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, "4581dbdc1d43e7e672b9911cdfa1cc79" ], [ "Vale.Math.Poly2.Lemmas.lemma_zero_degree", 1, 1, 0, [ "@query", "typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.zero" ], 0, "8b2b7208328ecae4b17037f19585ae72" ], [ "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, "eef1167d68d443d088abe3bcbe8f5394" ], [ "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, "e912537f08f2e41c9ba6c2b0328f2ea8" ], [ "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, "6b2b0e6fe87f347530a8fe597da5c3bc" ], [ "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, "9711bb444639a5924add30722e3676e6" ], [ "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, "c73125e17a544c7f05324e74c2567a7a" ], [ "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, "dda4b5cb06d71a177fab2945a3039860" ], [ "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, "da990679a545fe7099067ed14ba77f7f" ], [ "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, "85760beaa1b6ecab28ea1875c571c016" ], [ "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, "0d2cdcb55b435ac91c2e02e8756115a7" ], [ "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, "c0ba83bf667db5381840c71fb387a0fd" ], [ "Vale.Math.Poly2.Lemmas.lemma_add_zero_left", 1, 1, 0, [ "@query" ], 0, "6cac9a5edc257d0f738b4a87fa9e0be9" ], [ "Vale.Math.Poly2.Lemmas.lemma_add_all", 1, 1, 0, [ "@query" ], 0, "9e47d56473bb2c3e0b514f4e8596497e" ], [ "Vale.Math.Poly2.Lemmas.lemma_bitwise_all", 1, 1, 0, [ "@query" ], 0, "d51d1311a832ee9d8d99029ee950d914" ], [ "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, "20989f8c145b9ea1e7b006cfcf3587ac" ], [ "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, "4f99929fedb4efd1de6f9256d29a35fe" ], [ "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, "0cbcc1f559d3fb83babfb4a416c308c2" ], [ "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, "bf039ea933c161e5c7aec8f4389c6007" ], [ "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, "4064485010c0a2b00d0f5e5ea10a6069" ], [ "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, "6a356abd029c2c3b60554f78af0e5c1c" ], [ "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, "297cd7d5877a536a515e4e3858ce876f" ], [ "Vale.Math.Poly2.Lemmas.lemma_mul_distribute_left", 1, 1, 0, [ "@query" ], 0, "49be710576544500506d8a68621a64b6" ], [ "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, "d016e929d0bba2e398a5e989c42380c9" ], [ "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, "5c81137175e8a0aaccc04269ee6845b7" ], [ "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, "cd479e1b40c5d9ccda42e4059ed6628d" ], [ "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, "05bd269ce06321e42cfac476ca17733c" ], [ "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, "700c74bea4709c69ed4ea8c079b539cb" ], [ "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, "fd367e18f4d8f21695e98b72d61fc924" ], [ "Vale.Math.Poly2.Lemmas.lemma_shift_is_mul_left", 1, 1, 0, [ "@query" ], 0, "7d12c6b5a69fcbec1e8c89a5dd390916" ], [ "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, "2df0b58fef789000c4970da0e09b8c77" ], [ "Vale.Math.Poly2.Lemmas.lemma_mul_all", 1, 1, 0, [ "@query" ], 0, "ea00072356299d477c165daddbac35b8" ], [ "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, "a46dd892aba78e2414a509178aadc5e4" ], [ "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, "a52262bbb57f80b9d832884751a56d09" ], [ "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, "02ea6629f852a3b15e763f4283b61253" ], [ "Vale.Math.Poly2.Lemmas.lemma_mod_small", 1, 1, 0, [ "@query" ], 0, "8de4173f893928888417bb82456a2fdc" ], [ "Vale.Math.Poly2.Lemmas.lemma_mod_mod", 1, 1, 0, [ "@query", "lemma_Vale.Math.Poly2.lemma_mod_degree" ], 0, "9c777c78f2d867823a6d5597efb655ab" ], [ "Vale.Math.Poly2.Lemmas.lemma_mod_cancel", 1, 1, 0, [ "@query" ], 0, "5c0f99e2e5ea1e16d7e2cd434346d996" ], [ "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, "0763bb97c5e447cf93cf2939d9fcc607" ], [ "Vale.Math.Poly2.Lemmas.lemma_mod_mul_mod_right", 1, 1, 0, [ "@query", "typing_Vale.Math.Poly2_s.mod" ], 0, "c8114d48ef789f24611e9103f6894352" ], [ "Vale.Math.Poly2.Lemmas.lemma_shift_mod", 1, 1, 0, [ "@query" ], 0, "3af40ec8d117be34aee9a9902ad48de7" ], [ "Vale.Math.Poly2.Lemmas.lemma_mod_reduce", 1, 1, 0, [ "@query", "typing_Vale.Math.Poly2_s.add" ], 0, "b37032a6c7be26eb6028aa732d41a1dd" ], [ "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, "fb0e72c18ee96a7e4cec2f0906e0afa4" ], [ "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, "1c78b1b0c00c44899e8a3fd6158210ba" ], [ "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, "bf640644e1be79c04501503d1d982d6f" ], [ "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, "7da74a183c4a09d7376155d33a13a659" ], [ "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, "dc3dbaaaeb4e411a834bff224e8d1d08" ], [ "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, "43dc16e06a861e1f4f79d066413f8ded" ] ] ]