[
"رب\"ت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"
]
]
]