Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Vale.Math.Poly2.Defs_s.fst.hints
[
"�\"s�MA\u001f_��\u00190���",
[
[
"Vale.Math.Poly2.Defs_s.valid",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.bool",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length"
],
0,
"a3b3635a07c6f7711f981a517a77e6cb"
],
[
"Vale.Math.Poly2.Defs_s.monomial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.one",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"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_BarBar",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"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",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.one"
],
0,
"97c41a36ab7835ff9a11f7ee02043291"
],
[
"Vale.Math.Poly2.Defs_s.lshift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"e98c173a69da27032b1af44a7f9bbbe7"
],
[
"Vale.Math.Poly2.Defs_s.rshift",
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.poly",
"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_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"aae8a56ee195cf61c08aa00b54cf1e80"
],
[
"Vale.Math.Poly2.Defs_s.shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid", "int_inversion",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"a1b22f010d47b47abf6b41a6e2aff2bc"
],
[
"Vale.Math.Poly2.Defs_s.poly_index",
1,
1,
0,
[
"@query", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"f9c74118e7c6375dbab5d1226ba26914"
],
[
"Vale.Math.Poly2.Defs_s.to_seq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_24e885e6455d3b15b3ea0660054abea4",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Defs_s.poly_index",
"int_inversion", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"054ed89077832e7300df1190bc913bdc"
],
[
"Vale.Math.Poly2.Defs_s.of_seq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_5c5fd3496cd194f4c678415e261a4775_0", "bool_inversion",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66810020e159bcdf1763fab2dde0de35",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"well-founded-ordering-on-nat"
],
0,
"676b9f4c1511b054faa5df21743a5531"
],
[
"Vale.Math.Poly2.Defs_s.of_fun",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_67d1eb0e2b2b0432bd883bf79e9b388c",
"bool_inversion", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len", "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_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.poly_index",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"f62b278a5be382a5f5854ded95a2a820"
],
[
"Vale.Math.Poly2.Defs_s.reverse",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b7f59fbe639567c5ab8ed10579365264",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_366d043f86c85bf294c13134c5ec2089",
"typing_Vale.Math.Poly2.Defs_s.of_fun",
"typing_Vale.Math.Poly2.Defs_s.poly_index",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"5488fd8c1ff8ea66116d1d492750b7b3"
],
[
"Vale.Math.Poly2.Defs_s.add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"refinement_interpretation_Tm_refine_f84738c4655c15110645e630f03fcac4",
"typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"01078fcd5ce6dde3b7080b5d5346d3b7"
],
[
"Vale.Math.Poly2.Defs_s.sum_of_bools",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
"int_typing", "primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"fc9db53e8df26de65b27b6e69bb65b56"
],
[
"Vale.Math.Poly2.Defs_s.mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Math.Poly2.Defs_s.poly",
"function_token_typing_Prims.bool",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.length"
],
0,
"b3ce89f9b8c2ea933e550a1f5f16b3e3"
],
[
"Vale.Math.Poly2.Defs_s.divmod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_3e94af60b2131294de5742284d9caf65_0",
"binder_x_d8f1a9de738227ae573ad709c2c8d006_1", "bool_inversion",
"bool_typing", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Math.Lib.max", "equation_Prims.eqtype",
"equation_Prims.nat", "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.shift",
"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_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_919a8154a884fef643f87583005a7c0a",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.poly_index",
"typing_Vale.Math.Poly2.Defs_s.shift",
"typing_Vale.Math.Poly2.Defs_s.valid", "well-founded-ordering-on-nat"
],
0,
"f57907538f1705edb09a84dbf1f61fc4"
],
[
"Vale.Math.Poly2.Defs_s.valid",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.bool",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length"
],
0,
"d42bb1cc265e94d12f63293f02b5115f"
],
[
"Vale.Math.Poly2.Defs_s.monomial",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.one",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"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_BarBar",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"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",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.one"
],
0,
"789c8b20fcd8778de3a5d16ee90ae7a1"
],
[
"Vale.Math.Poly2.Defs_s.lshift",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"392d9114a20ad5b1ef861bf1b4a60c91"
],
[
"Vale.Math.Poly2.Defs_s.rshift",
2,
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.poly",
"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_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"5ea561252c71a676c26b89e2b8e4b920"
],
[
"Vale.Math.Poly2.Defs_s.shift",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid", "int_inversion",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"4c9ffb20c076093eaade3d672e629972"
],
[
"Vale.Math.Poly2.Defs_s.poly_index",
2,
1,
0,
[
"@query", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"b8bb81814fd8e1908722a7e5ac070514"
],
[
"Vale.Math.Poly2.Defs_s.to_seq",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_24e885e6455d3b15b3ea0660054abea4",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Defs_s.poly_index",
"int_inversion", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"665d5117271d2b3dcc8c68f9d0b528ad"
],
[
"Vale.Math.Poly2.Defs_s.of_seq",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_5c5fd3496cd194f4c678415e261a4775_0", "bool_inversion",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66810020e159bcdf1763fab2dde0de35",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"well-founded-ordering-on-nat"
],
0,
"104e8fc85778b122240ac7c1ffbabc6f"
],
[
"Vale.Math.Poly2.Defs_s.of_fun",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_67d1eb0e2b2b0432bd883bf79e9b388c",
"bool_inversion", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len", "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_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.poly_index",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"2f7416c4b44ee026ef2d49500a6751c8"
],
[
"Vale.Math.Poly2.Defs_s.reverse",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b7f59fbe639567c5ab8ed10579365264",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_366d043f86c85bf294c13134c5ec2089",
"typing_Vale.Math.Poly2.Defs_s.of_fun",
"typing_Vale.Math.Poly2.Defs_s.poly_index",
"typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"405ebc864f2f25090afbdfbb8e2c50de"
],
[
"Vale.Math.Poly2.Defs_s.add",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Math.Poly2.Defs_s.poly",
"equation_Vale.Math.Poly2.Defs_s.poly_index",
"equation_Vale.Math.Poly2.Defs_s.valid",
"function_token_typing_Prims.bool", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"refinement_interpretation_Tm_refine_f84738c4655c15110645e630f03fcac4",
"typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.valid"
],
0,
"61988d18a3c85cdfe3e4c7625c79d9e5"
],
[
"Vale.Math.Poly2.Defs_s.sum_of_bools",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
"int_typing", "primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"d220ec4dd7e3a57b8ccb359ba369562e"
],
[
"Vale.Math.Poly2.Defs_s.mul",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Math.Poly2.Defs_s.poly",
"function_token_typing_Prims.bool",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Seq.Base.length"
],
0,
"c4c65577481ef1242e0342e4c5726957"
],
[
"Vale.Math.Poly2.Defs_s.divmod",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_3e94af60b2131294de5742284d9caf65_0",
"binder_x_d8f1a9de738227ae573ad709c2c8d006_1", "bool_inversion",
"bool_typing", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Math.Lib.max", "equation_Prims.eqtype",
"equation_Prims.nat", "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.shift",
"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_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_919a8154a884fef643f87583005a7c0a",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
"typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Defs_s.poly_index",
"typing_Vale.Math.Poly2.Defs_s.shift",
"typing_Vale.Math.Poly2.Defs_s.valid", "well-founded-ordering-on-nat"
],
0,
"13b89a31c46e4d6fbfda190f8a56ea7a"
]
]
]
Computing file changes ...
