[ "EȣOFC]\u001b", [ [ "Vale.Math.Poly2.all_defs", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.one", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.Defs_s.zero", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_create", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.index", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.Defs_s.zero" ], 0, "588a53523f5c825a56b4ab9333f08950" ], [ "Vale.Math.Poly2.reveal_all_defs", 1, 1, 0, [ "@query", "equation_Vale.Math.Poly2.all_defs" ], 0, "7bbf010bb4131ec990e627a1841e8d89" ], [ "Vale.Math.Poly2.poly_and", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing", "equation_FStar.Math.Lib.max", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "equation_Vale.Math.Poly2.size", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.length" ], 0, "ae17d26ed0ad683d73ed01ed1c815f81" ], [ "Vale.Math.Poly2.poly_or", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "equation_Vale.Math.Poly2.size", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.length" ], 0, "8d450568c771a158c39944296df8d260" ], [ "Vale.Math.Poly2.power", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "well-founded-ordering-on-nat" ], 0, "63626e40ea58708d9b6e8fceaf14041a" ], [ "Vale.Math.Poly2.lemma_degree_at_least", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.length" ], 0, "bce7c3246d3c21a749daea13b577ff8b" ], [ "Vale.Math.Poly2.lemma_equal", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs.poly_equal", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "31f5f02b1e4b0e518b03c357e65f3807" ], [ "Vale.Math.Poly2.lemma_index_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "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_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "5a3d3dd3b8c37af394fc328c5ac7d631" ], [ "Vale.Math.Poly2.lemma_degree", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.one", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "f44238eb182166d5dbeaf1e209a6029c" ], [ "Vale.Math.Poly2.lemma_zero_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.zero", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Math.Poly2_s.poly_index", "typing_Vale.Math.Poly2_s.zero" ], 0, "99668073428401c50feb9a352ff81dd8" ], [ "Vale.Math.Poly2.lemma_one_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.one", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.Defs_s.zero", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_create", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.Defs_s.zero", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "c9aeb79c41005150c82ba51d6c628dcb" ], [ "Vale.Math.Poly2.lemma_monomial_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.monomial", "equation_Vale.Math.Poly2.Defs_s.one", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.Defs_s.zero", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.Defs_s.zero", "typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "6d8c32d52b35c42ea1eaf2ba4d5bded9" ], [ "Vale.Math.Poly2.lemma_shift_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.lshift", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.rshift", "equation_Vale.Math.Poly2.Defs_s.shift", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.Defs_s.zero", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index", "typing_Vale.Math.Poly2_s.shift" ], 0, "6678570461fb08e4fb49adacfbd246c2" ], [ "Vale.Math.Poly2.lemma_and_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "equation_FStar.Math.Lib.max", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.poly_and", "equation_Vale.Math.Poly2.reveal_all_defs", "equation_Vale.Math.Poly2.size", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "interpretation_Tm_abs_67ba49188d3741bb11ca039ce39f8753", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.length", "typing_Tm_abs_67ba49188d3741bb11ca039ce39f8753", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2.size", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "ddb029a55703ef3d785046eb1de1cfa1" ], [ "Vale.Math.Poly2.lemma_or_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "equation_FStar.Math.Lib.max", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.poly_or", "equation_Vale.Math.Poly2.reveal_all_defs", "equation_Vale.Math.Poly2.size", "function_token_typing_Prims.bool", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "interpretation_Tm_abs_1625bf73edea8a63924fef5f7a34bc2b", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.length", "typing_Tm_abs_1625bf73edea8a63924fef5f7a34bc2b", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.poly_or", "typing_Vale.Math.Poly2.size", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "f69f4130b5e9f60dec05c1835968fa5e" ], [ "Vale.Math.Poly2.lemma_mask_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.mask", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "interpretation_Tm_abs_f9a792c3df96aeff53663db14b2a8d7d", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "typing_Tm_abs_f9a792c3df96aeff53663db14b2a8d7d", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.one", "typing_Vale.Math.Poly2_s.poly_index" ], 0, "90bac986cd02c8c2ccd14479bf9f128a" ], [ "Vale.Math.Poly2.lemma_ones_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.Defs_s.poly", "equation_Vale.Math.Poly2.Defs_s.poly_index", "equation_Vale.Math.Poly2.Defs_s.valid", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.ones", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "interpretation_Tm_abs_09579966139f0077be0b3131f4faaf25", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f", "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0", "typing_Tm_abs_09579966139f0077be0b3131f4faaf25", "typing_Vale.Math.Poly2.Defs_s.one", "typing_Vale.Math.Poly2.Defs_s.valid", "typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.one" ], 0, "7b143891b05df361fc0e7dc69b3c869e" ], [ "Vale.Math.Poly2.lemma_reverse_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b1d28f840de949bc346d201a47c0cfe3", "typing_Vale.Math.Poly2.Defs_s.reverse", "typing_Vale.Math.Poly2_s.poly_index", "typing_Vale.Math.Poly2_s.reverse" ], 0, "7ea4da0d2f17160e343a398be2e6538d" ], [ "Vale.Math.Poly2.lemma_add_zero", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.zero" ], 0, "f2520e31c212752f13d1a27d445ed81f" ], [ "Vale.Math.Poly2.lemma_add_cancel", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2.Defs_s.add", "typing_Vale.Math.Poly2_s.zero" ], 0, "f4f99e284d03f31c21c77151a15e65d2" ], [ "Vale.Math.Poly2.lemma_add_cancel_eq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "9d99cbbf13b3326dc5670faf90687e77" ], [ "Vale.Math.Poly2.lemma_add_commute", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2.Defs_s.add" ], 0, "6aa9f502627628563394926589be2e9d" ], [ "Vale.Math.Poly2.lemma_add_associate", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.add" ], 0, "459a2e36f34c7e66a42bf158b1f5b52e" ], [ "Vale.Math.Poly2.lemma_add_define_i", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2.Defs_s.add", "typing_Vale.Math.Poly2_s.add" ], 0, "cd2498b01b641696bbb5f56dc4fe35b3" ], [ "Vale.Math.Poly2.lemma_add_degree", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Math.Lib.max", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2.Defs_s.add", "typing_Vale.Math.Poly2_s.add" ], 0, "b17c6e92a557f870b16b275f47139654" ], [ "Vale.Math.Poly2.lemma_mul_zero", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.zero" ], 0, "35cf653746ae4dc858eb91bbf2e84336" ], [ "Vale.Math.Poly2.lemma_mul_one", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.one" ], 0, "5d68483a6ed044b9f143ca80a466c89e" ], [ "Vale.Math.Poly2.lemma_mul_commute", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb", "typing_Vale.Math.Poly2.Defs_s.mul" ], 0, "5868b3d1c39768ab9aa239ee8bbead17" ], [ "Vale.Math.Poly2.lemma_mul_associate", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.mul" ], 0, "54d5e58c7d9d2c2adb1eb2173e2b2b72" ], [ "Vale.Math.Poly2.lemma_mul_distribute", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.mul" ], 0, "3b94ead47b82f04ae0f145f2ce889100" ], [ "Vale.Math.Poly2.lemma_mul_degree", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.mul" ], 0, "92f3d5d2323b270a44749f931d8978c0" ], [ "Vale.Math.Poly2.lemma_mul_reverse", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "b9f02b4b62aea8e49819374aa2de1a53" ], [ "Vale.Math.Poly2.lemma_mul_reverse", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.reverse" ], 0, "fdab99462101ddd8097fb57a55c6fe90" ], [ "Vale.Math.Poly2.lemma_shift_is_mul", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Math.Poly2.Defs_s.monomial", "typing_Vale.Math.Poly2.Defs_s.shift", "typing_Vale.Math.Poly2_s.mul" ], 0, "68e4064ad08e4029008b67917bc1db9b" ], [ "Vale.Math.Poly2.lemma_div_mod", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.mul" ], 0, "1ab29f900c1c5d02105dbcf850d03e21" ], [ "Vale.Math.Poly2.lemma_div_degree", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.div" ], 0, "ba887372feecc6b3171481e5e7bf9db3" ], [ "Vale.Math.Poly2.lemma_mod_degree", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.squash", "equation_Vale.Math.Poly2.Defs_s.degree", "equation_Vale.Math.Poly2.all_defs", "equation_Vale.Math.Poly2.reveal_all_defs", "function_token_typing_Vale.Math.Poly2.reveal_all_defs", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Vale.Math.Poly2_s.mod" ], 0, "a0ea9599b7783010b01bb4804bc12160" ] ] ]