Revision aa211c2d5a40dd6969fe8a469fcadfd27e8c8fe3 authored by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC, committed by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC
1 parent 6f91754
Vale.Lib.Lists.fst.hints
[
"M\u0019�:���\u0011�\u0007�\nh���",
[
[
"Vale.Lib.Lists.singleton_list_rev",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.rev_acc.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"equation_FStar.List.Tot.Base.rev",
"equation_with_fuel_FStar.List.Tot.Base.rev_acc.fuel_instrumented",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a"
],
0,
"f77aa70279c54fe399c6d7bf4b91ed80"
],
[
"Vale.Lib.Lists.list_cons_is_append",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a"
],
0,
"6a7494690249dacab481ab87d0d8090b"
],
[
"Vale.Lib.Lists.singleton_list_seq",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok", "equation_FStar.List.Tot.Base.hd",
"equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_create",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_FStar.List.Tot.Base.index",
"typing_FStar.List.Tot.Base.length", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Properties.seq_of_list"
],
0,
"9a774d5edbdad4e0aa1240b6ec8af0c1"
],
[
"Vale.Lib.Lists.list_append_length",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
"binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3",
"binder_x_fe28d8bcde588226b4e538b35321de05_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Prims.list", "int_inversion",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.append",
"typing_FStar.List.Tot.Base.length"
],
0,
"64183bc16846ea05ab048f4046fed595"
],
[
"Vale.Lib.Lists.list_append_index",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.squash",
"int_inversion", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b6c4a0161e0c22e30fcaac04d58b3a70"
],
[
"Vale.Lib.Lists.list_append_index",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "equation_Prims.squash",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"8da77de3ae4eb75efdbcdd444a52c155"
],
[
"Vale.Lib.Lists.list_append_index",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
"binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_fe28d8bcde588226b4e538b35321de05_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_FStar.List.Tot.Base.hd",
"equation_FStar.List.Tot.Base.tail",
"equation_FStar.List.Tot.Base.tl", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_FStar.List.Tot.Base.append", "unit_inversion", "unit_typing"
],
0,
"027992777cde9351957e45e5b7fddbaa"
],
[
"Vale.Lib.Lists.append_list_seq",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
"binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3",
"binder_x_fe28d8bcde588226b4e538b35321de05_1",
"constructor_distinct_Tm_unit", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"refinement_interpretation_Tm_refine_29865b3e2df22a2c020de4bfd5a89179",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c4ff8e69afa98d84e6a0fb3bbbc650c0",
"refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.List.Tot.Base.append",
"typing_FStar.List.Tot.Base.length", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Properties.seq_of_list"
],
0,
"2495115c6c6ad9af4b377323cf2d6032"
],
[
"Vale.Lib.Lists.from_list_le",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_0ac2f7b25dff899a09cad33bdd7540a2_0", "bool_typing",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"fuel_guarded_inversion_Prims.list",
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
],
0,
"b62f934cd4cdfa763a990a5ed7b205d1"
],
[
"Vale.Lib.Lists.lemma_from_list_le",
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,
"71e53fef8da4586d8d7ddf5feeaf6a6c"
],
[
"Vale.Lib.Lists.lemma_from_list_le",
2,
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,
"173555c4dfe79433cd9349799f32f6f9"
],
[
"Vale.Lib.Lists.lemma_from_list_le",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.rev_acc.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_Vale.Lib.Lists.from_list_le.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_Vale.Lib.Lists.from_list_le.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_0ac2f7b25dff899a09cad33bdd7540a2_0", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_elim_Prims.Cons",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equation_FStar.BitVector.bv_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.List.Tot.Base.rev", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.rev_acc.fuel_instrumented",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"equation_with_fuel_Vale.Lib.Lists.from_list_le.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.List.Tot.Properties.append_length",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"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_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_3470787130ed719a6675e4c9599659d3",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4aa5c7e663f2b15889d438d88a10b639",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"token_correspondence_Vale.Lib.Lists.from_list_le.fuel_instrumented",
"typing_FStar.List.Tot.Base.length",
"typing_FStar.List.Tot.Base.rev",
"typing_FStar.List.Tot.Base.rev_acc",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_FStar.UInt.from_vec"
],
0,
"4d440986745cbcf54247193eae72bf7f"
],
[
"Vale.Lib.Lists.lemma_from_list_be",
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,
"f82fe68332da6ee7c9ae92bb0a1ec061"
],
[
"Vale.Lib.Lists.lemma_from_list_be",
2,
1,
0,
[ "@query", "equation_Vale.Lib.Lists.from_list_be" ],
0,
"0bb71ab75994a60d598e3063e9d7cab2"
]
]
]
Computing file changes ...
