Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.Lib.MapTree.fst.hints
[
"k��\u0003H�G�o�r&F���",
[
[
"Vale.Lib.MapTree.tree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"50740afd6a94099c266177b0df720449"
],
[
"Vale.Lib.MapTree.__proj__Node__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Node",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_131752844997e94d70cad487765e1288"
],
0,
"94c7a1f7f9f49be82d2e8af39ba2f1c0"
],
[
"Vale.Lib.MapTree.__proj__Node__item___1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Node",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_131752844997e94d70cad487765e1288"
],
0,
"d31f248b576eec240c03793e78ff2c57"
],
[
"Vale.Lib.MapTree.__proj__Node__item___2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Node",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_131752844997e94d70cad487765e1288"
],
0,
"38407f9efccc042cd754f0065d4a3bfb"
],
[
"Vale.Lib.MapTree.__proj__Node__item___3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Node",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_131752844997e94d70cad487765e1288"
],
0,
"2dfb96c0dd7d41b832fe32be02c63a3e"
],
[
"Vale.Lib.MapTree.__proj__Node__item___4",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Node",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_131752844997e94d70cad487765e1288"
],
0,
"fa61ae335b9db1262dca66341412da4f"
],
[
"Vale.Lib.MapTree.height",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree"
],
0,
"742889dd79efac7b4e0aba626ae7a7f3"
],
[
"Vale.Lib.MapTree.mkNode",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Lib.MapTree.height", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Lib.MapTree.height"
],
0,
"e8055fb6dc61951773878d951e51f657"
],
[
"Vale.Lib.MapTree.get",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"subterm_ordering_Vale.Lib.MapTree.Node"
],
0,
"08b61baf68cf453171fe0e00f133bcb1"
],
[
"Vale.Lib.MapTree.put",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"subterm_ordering_Vale.Lib.MapTree.Node"
],
0,
"3129d2a79fa3d39eeb743d641db224f6"
],
[
"Vale.Lib.MapTree.inv",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"subterm_ordering_Vale.Lib.MapTree.Node"
],
0,
"fcced979f259f8e3b263d1d444e02f02"
],
[
"Vale.Lib.MapTree.lemma_put_inv",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.put.fuel_instrumented", "@query",
"Vale.Lib.MapTree_interpretation_Tm_arrow_87fd7148829c07e8da0b20a2d843ccc0",
"Vale.Lib.MapTree_interpretation_Tm_arrow_c8126b87a2c25bb477df4a7a6b0eea9e",
"b2t_def", "binder_x_2e56f0f7014d6393bf76ee12c1ce5313_3",
"binder_x_64a6f2da4341770a4dee8aa1d0d4ae69_6",
"binder_x_9cd1733a5204f989dbb2f01d5984df93_1",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_7",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_8",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"binder_x_d3faed7bbec7b3b3d41ce73e2f001f5c_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_2", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.Lib.MapTree.Empty",
"constructor_distinct_Vale.Lib.MapTree.Node",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Lib.MapTree.Node",
"data_typing_intro_FStar.Pervasives.Native.Some@tok",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Vale.Lib.MapTree.balance",
"equation_Vale.Lib.MapTree.height",
"equation_Vale.Lib.MapTree.is_cmp",
"equation_Vale.Lib.MapTree.is_lt_option",
"equation_Vale.Lib.MapTree.mkNode",
"equation_Vale.Lib.MapTree.rotate_l",
"equation_Vale.Lib.MapTree.rotate_r",
"equation_with_fuel_Vale.Lib.MapTree.inv.fuel_instrumented",
"equation_with_fuel_Vale.Lib.MapTree.put.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree", "l_and-interp",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.Lib.MapTree.Empty_a",
"projection_inverse_Vale.Lib.MapTree.Empty_b",
"projection_inverse_Vale.Lib.MapTree.Node__0",
"projection_inverse_Vale.Lib.MapTree.Node__1",
"projection_inverse_Vale.Lib.MapTree.Node__2",
"projection_inverse_Vale.Lib.MapTree.Node__3",
"projection_inverse_Vale.Lib.MapTree.Node__4",
"projection_inverse_Vale.Lib.MapTree.Node_a",
"projection_inverse_Vale.Lib.MapTree.Node_b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c66edbccc6e0e4db18678f27ad0c5d10",
"subterm_ordering_Vale.Lib.MapTree.Node",
"token_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"true_interp", "typing_Vale.Lib.MapTree.height",
"typing_Vale.Lib.MapTree.is_lt_option",
"typing_Vale.Lib.MapTree.put", "unit_inversion", "unit_typing"
],
0,
"ab9e6f16389b1f98aae0f7b61715e97f"
],
[
"Vale.Lib.MapTree.lemma_get_put_self",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.get.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.put.fuel_instrumented", "@query",
"FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Lib.MapTree_interpretation_Tm_arrow_87fd7148829c07e8da0b20a2d843ccc0",
"Vale.Lib.MapTree_interpretation_Tm_arrow_c8126b87a2c25bb477df4a7a6b0eea9e",
"b2t_def", "binder_x_2e56f0f7014d6393bf76ee12c1ce5313_3",
"binder_x_64a6f2da4341770a4dee8aa1d0d4ae69_6",
"binder_x_9cd1733a5204f989dbb2f01d5984df93_1",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_7",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_8",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"binder_x_d3faed7bbec7b3b3d41ce73e2f001f5c_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_2", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_FStar.Pervasives.Native.option",
"constructor_distinct_Prims.unit",
"constructor_distinct_Vale.Lib.MapTree.Empty",
"constructor_distinct_Vale.Lib.MapTree.Node",
"data_elim_Vale.Lib.MapTree.Node",
"data_typing_intro_FStar.Pervasives.Native.Some@tok",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Lib.MapTree.balance",
"equation_Vale.Lib.MapTree.height",
"equation_Vale.Lib.MapTree.is_cmp",
"equation_Vale.Lib.MapTree.is_lt_option",
"equation_Vale.Lib.MapTree.mkNode",
"equation_Vale.Lib.MapTree.rotate_l",
"equation_Vale.Lib.MapTree.rotate_r",
"equation_with_fuel_Vale.Lib.MapTree.get.fuel_instrumented",
"equation_with_fuel_Vale.Lib.MapTree.inv.fuel_instrumented",
"equation_with_fuel_Vale.Lib.MapTree.put.fuel_instrumented",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree", "l_and-interp",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.Lib.MapTree.Empty_a",
"projection_inverse_Vale.Lib.MapTree.Empty_b",
"projection_inverse_Vale.Lib.MapTree.Node__0",
"projection_inverse_Vale.Lib.MapTree.Node__1",
"projection_inverse_Vale.Lib.MapTree.Node__2",
"projection_inverse_Vale.Lib.MapTree.Node__3",
"projection_inverse_Vale.Lib.MapTree.Node__4",
"projection_inverse_Vale.Lib.MapTree.Node_a",
"projection_inverse_Vale.Lib.MapTree.Node_b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_edd9870507b375cb58b236820b0502a7",
"subterm_ordering_Vale.Lib.MapTree.Node",
"token_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"token_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"typing_Vale.Lib.MapTree.get",
"typing_Vale.Lib.MapTree.is_lt_option",
"typing_Vale.Lib.MapTree.mkNode", "typing_Vale.Lib.MapTree.put",
"unit_inversion", "unit_typing"
],
0,
"3c2beb42fd0fb42b2c47091bb2169299"
],
[
"Vale.Lib.MapTree.lemma_get_put_other",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.get.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.inv.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.MapTree.put.fuel_instrumented", "@query",
"Vale.Lib.MapTree_interpretation_Tm_arrow_87fd7148829c07e8da0b20a2d843ccc0",
"Vale.Lib.MapTree_interpretation_Tm_arrow_c8126b87a2c25bb477df4a7a6b0eea9e",
"b2t_def", "binder_x_2e56f0f7014d6393bf76ee12c1ce5313_3",
"binder_x_64a6f2da4341770a4dee8aa1d0d4ae69_7",
"binder_x_9cd1733a5204f989dbb2f01d5984df93_1",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_8",
"binder_x_b44871c1c4c7134db582f31d4f8332b2_9",
"binder_x_d367b870ff7533df600153f672bdeb06_4",
"binder_x_d3faed7bbec7b3b3d41ce73e2f001f5c_5",
"binder_x_d3faed7bbec7b3b3d41ce73e2f001f5c_6",
"binder_x_fe28d8bcde588226b4e538b35321de05_2", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.Lib.MapTree.Empty",
"constructor_distinct_Vale.Lib.MapTree.Node",
"data_elim_Vale.Lib.MapTree.Node",
"data_typing_intro_FStar.Pervasives.Native.Some@tok",
"disc_equation_Vale.Lib.MapTree.Empty",
"disc_equation_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Lib.MapTree.balance",
"equation_Vale.Lib.MapTree.height",
"equation_Vale.Lib.MapTree.is_cmp",
"equation_Vale.Lib.MapTree.is_lt_option",
"equation_Vale.Lib.MapTree.mkNode",
"equation_Vale.Lib.MapTree.rotate_l",
"equation_Vale.Lib.MapTree.rotate_r",
"equation_with_fuel_Vale.Lib.MapTree.get.fuel_instrumented",
"equation_with_fuel_Vale.Lib.MapTree.inv.fuel_instrumented",
"equation_with_fuel_Vale.Lib.MapTree.put.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree", "l_and-interp",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.Lib.MapTree.Empty_a",
"projection_inverse_Vale.Lib.MapTree.Empty_b",
"projection_inverse_Vale.Lib.MapTree.Node__0",
"projection_inverse_Vale.Lib.MapTree.Node__1",
"projection_inverse_Vale.Lib.MapTree.Node__2",
"projection_inverse_Vale.Lib.MapTree.Node__3",
"projection_inverse_Vale.Lib.MapTree.Node__4",
"projection_inverse_Vale.Lib.MapTree.Node_a",
"projection_inverse_Vale.Lib.MapTree.Node_b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55b4cf9b5f83165eee7c0f721c450034",
"subterm_ordering_Vale.Lib.MapTree.Node",
"token_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"token_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"typing_Vale.Lib.MapTree.get", "typing_Vale.Lib.MapTree.height",
"typing_Vale.Lib.MapTree.is_lt_option",
"typing_Vale.Lib.MapTree.mkNode", "typing_Vale.Lib.MapTree.put",
"unit_inversion", "unit_typing"
],
0,
"4ddf637bbe550f885938a4e91b35387b"
],
[
"Vale.Lib.MapTree.map'",
1,
1,
2,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.Lib.MapTree.Empty",
"data_elim_Vale.Lib.MapTree.Node", "equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"86c55789e96fc8c9f5a0c44b68916fca"
],
[
"Vale.Lib.MapTree.__proj__Map__item__t",
1,
1,
2,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.Lib.MapTree.Empty",
"data_elim_Vale.Lib.MapTree.Map", "data_elim_Vale.Lib.MapTree.Node",
"equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.map_",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0b8f9567ca9637a95432de4566bc75a8"
],
[
"Vale.Lib.MapTree.__proj__Map__item__t",
2,
1,
2,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.Lib.MapTree.Empty",
"data_elim_Vale.Lib.MapTree.Map", "data_elim_Vale.Lib.MapTree.Node",
"equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.map_",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4c8198c2cdce52534bd2b977406c71b0"
],
[
"Vale.Lib.MapTree.__proj__Map__item__invs",
1,
1,
2,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.Lib.MapTree.Empty",
"data_elim_Vale.Lib.MapTree.Map", "data_elim_Vale.Lib.MapTree.Node",
"equation_Prims.eqtype",
"fuel_guarded_inversion_Vale.Lib.MapTree.map_",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"cd8a68ac22147aa08eacd51cf483e17a"
],
[
"Vale.Lib.MapTree.__proj__Map__item__invs",
2,
1,
2,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.Lib.MapTree.Empty",
"data_elim_Vale.Lib.MapTree.Map", "data_elim_Vale.Lib.MapTree.Node",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.squash",
"fuel_guarded_inversion_Vale.Lib.MapTree.map_",
"fuel_guarded_inversion_Vale.Lib.MapTree.tree", "l_and-interp",
"proj_equation_Vale.Lib.MapTree.Map_is_le",
"proj_equation_Vale.Lib.MapTree.Map_t",
"projection_inverse_Vale.Lib.MapTree.Map_is_le",
"projection_inverse_Vale.Lib.MapTree.Map_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"04d3147bbe298beaa033f98159a113d6"
],
[
"Vale.Lib.MapTree.const",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.inv.fuel_instrumented",
"@query", "constructor_distinct_Vale.Lib.MapTree.Empty",
"data_typing_intro_FStar.Pervasives.Native.None@tok",
"data_typing_intro_Vale.Lib.MapTree.Empty@tok",
"equation_Prims.eqtype",
"equation_with_fuel_Vale.Lib.MapTree.inv.fuel_instrumented",
"projection_inverse_Vale.Lib.MapTree.Empty_a",
"projection_inverse_Vale.Lib.MapTree.Empty_b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_45141b9abce5adf1299e1d7ad7f1fcef",
"true_interp"
],
0,
"8284b51c918506718fbfec6beea90d0a"
],
[
"Vale.Lib.MapTree.sel",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_with_fuel_Vale.Lib.MapTree.get.fuel_instrumented",
"lemma_FStar.Pervasives.invertOption",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Lib.MapTree.get"
],
0,
"5ae6b5f6f49997a9a190a3431c547e21"
],
[
"Vale.Lib.MapTree.upd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Pervasives.Native.None",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Vale.Lib.MapTree.is_lt_option", "l_and-interp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"a43d3a970a4b40bcf38043083fcd4a5a"
],
[
"Vale.Lib.MapTree.lemma_const",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.get.fuel_instrumented",
"@query", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Lib.MapTree.Empty",
"data_typing_intro_Vale.Lib.MapTree.Empty@tok",
"equation_Vale.Lib.MapTree.const", "equation_Vale.Lib.MapTree.sel",
"equation_with_fuel_Vale.Lib.MapTree.get.fuel_instrumented",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_Vale.Lib.MapTree.Empty_a",
"projection_inverse_Vale.Lib.MapTree.Empty_b",
"projection_inverse_Vale.Lib.MapTree.Map_default_v",
"projection_inverse_Vale.Lib.MapTree.Map_is_le",
"projection_inverse_Vale.Lib.MapTree.Map_t",
"refinement_interpretation_Tm_refine_45141b9abce5adf1299e1d7ad7f1fcef"
],
0,
"6ee577fc12fd4402f50d640a4b13d445"
],
[
"Vale.Lib.MapTree.lemma_sel_upd_self",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"@query", "constructor_distinct_FStar.Pervasives.Native.Some",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Vale.Lib.MapTree.sel", "equation_Vale.Lib.MapTree.upd",
"l_and-interp", "projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.Lib.MapTree.Map_default_v",
"projection_inverse_Vale.Lib.MapTree.Map_is_le",
"projection_inverse_Vale.Lib.MapTree.Map_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"unit_inversion"
],
0,
"17b01d6a66093ab90ca602b868fa252d"
],
[
"Vale.Lib.MapTree.lemma_sel_upd_other",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Lib.MapTree.put.fuel_instrumented",
"@query", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Vale.Lib.MapTree.is_lt_option",
"equation_Vale.Lib.MapTree.sel", "equation_Vale.Lib.MapTree.upd",
"l_and-interp", "lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.Lib.MapTree.Map_default_v",
"projection_inverse_Vale.Lib.MapTree.Map_is_le",
"projection_inverse_Vale.Lib.MapTree.Map_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"typing_Vale.Lib.MapTree.get", "unit_inversion"
],
0,
"d2080f3be18b0e13fbc13166d02a7cc8"
]
]
]
Computing file changes ...
