Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Vale.Lib.MapTree.fst.hints
[
"h42��\u0003��Ԙ��R�\u0018�",
[
[
"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,
"532b7fce3ace213266487253f028177f"
],
[
"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,
"646cb81d6147ed70b0b0ca54fddc07bf"
],
[
"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,
"ad46b2a521df7ea9cf4a613926e53a9f"
],
[
"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,
"98d3b542197682ed833d2017879743fa"
],
[
"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,
"1f1cd1948e140d6fdbb2c93f9a8cdfe1"
],
[
"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,
"6fbba35936c8aec771f61362bc22230c"
],
[
"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,
"345d0d3bd9e52c6dcd21f53100b4fc4b"
],
[
"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,
"21a114a1aaabd45420ae1edca1a5c0c9"
],
[
"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,
"211ef4d6904eb855718c30aefb1f502a"
],
[
"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,
"a63fc18440289abf24cdd21c696bd038"
],
[
"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,
"5a8bfbe231ef3444e178339d208d0388"
],
[
"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,
"06192b097f1fb4fe69e655e838966111"
],
[
"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,
"5d26c181f161ed2f03d159d0313dab46"
],
[
"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,
"e2fe6a7058cd674df44787ca65389c05"
],
[
"Vale.Lib.MapTree.__proj__Map__item__invs",
1,
1,
0,
[
"@query", "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"
],
0,
"450bc4d31fc4ce5283f3db94d8ef883e"
],
[
"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,
"d973230723093482aa338a8a038cb487"
],
[
"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,
"c0aa1f34c2c90f4f840c6a1c00af5644"
],
[
"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,
"da91727a58a71945bf1a1afeca5a31db"
],
[
"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,
"b42307f55411a342ff4ca57cdaf44bc7"
],
[
"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,
"17dfecc3ef5be4076856322a19ff78e0"
],
[
"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,
"f44aa7cbf3d7f57337d8b706f435a318"
]
]
]
Computing file changes ...
