Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
CanonCommMonoid.fst.hints
[
"��k\u0019'a��֚89�*�\u001a",
[
[
"CanonCommMonoid.var",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"25bd3fcfe7c7846e5b9490182a9810c5"
],
[
"CanonCommMonoid.exp",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_CanonCommMonoid.var",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"74e4aebc4d49a14bfba0591042a57e59"
],
[
"CanonCommMonoid.__proj__Var__item___0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_CanonCommMonoid.Var",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0ce029e55357168c7b2f4890c83d006f"
],
0,
"e0fe693e37a192aaad6a355d782e0b61"
],
[
"CanonCommMonoid.__proj__Mult__item___0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_CanonCommMonoid.Mult",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_81ce976ce6cdc1820c6b0b8dcaaaa29c"
],
0,
"4dc3a53a0df30f4857b8621f3aca0788"
],
[
"CanonCommMonoid.__proj__Mult__item___1",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_CanonCommMonoid.Mult",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_81ce976ce6cdc1820c6b0b8dcaaaa29c"
],
0,
"81097a21b7ade2be636cdff5561b85f1"
],
[
"CanonCommMonoid.exp_to_string",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"CanonCommMonoid_pretyping_04ca1c898b2ee941b4d5e76a7044c379",
"binder_x_04ca1c898b2ee941b4d5e76a7044c379_0",
"disc_equation_CanonCommMonoid.Mult",
"disc_equation_CanonCommMonoid.Unit",
"disc_equation_CanonCommMonoid.Var",
"equality_tok_CanonCommMonoid.Unit@tok",
"fuel_guarded_inversion_CanonCommMonoid.exp",
"subterm_ordering_CanonCommMonoid.Mult",
"typing_tok_CanonCommMonoid.Unit@tok"
],
0,
"665df4dc51cd46360d7160a916b2c179"
],
[
"CanonCommMonoid.mdenote",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"CanonCommMonoid_pretyping_04ca1c898b2ee941b4d5e76a7044c379",
"binder_x_04ca1c898b2ee941b4d5e76a7044c379_6",
"binder_x_29bc033fbf136376eadf5c2199fe83d8_4",
"binder_x_a597e8b39b6549dcdad766448921454a_5",
"disc_equation_CanonCommMonoid.Mult",
"disc_equation_CanonCommMonoid.Unit",
"disc_equation_CanonCommMonoid.Var",
"equality_tok_CanonCommMonoid.Unit@tok",
"equality_tok_Prims.LexTop@tok", "equation_CanonCommMonoid.vmap",
"fuel_guarded_inversion_CanonCommMonoid.exp",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"subterm_ordering_CanonCommMonoid.Mult",
"typing_tok_CanonCommMonoid.Unit@tok"
],
0,
"02e87270ec29f086a9eafb1f6aac32c2"
],
[
"CanonCommMonoid.xsdenote",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_29bc033fbf136376eadf5c2199fe83d8_4",
"binder_x_a2a1950e8630eae361cf9493762886a6_6",
"binder_x_a597e8b39b6549dcdad766448921454a_5",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_CanonCommMonoid.var",
"equation_CanonCommMonoid.vmap", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
],
0,
"541a55469a24dd71ef144807eeefcf0f"
],
[
"CanonCommMonoid.flatten",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"CanonCommMonoid_pretyping_04ca1c898b2ee941b4d5e76a7044c379",
"binder_x_04ca1c898b2ee941b4d5e76a7044c379_0",
"disc_equation_CanonCommMonoid.Mult",
"disc_equation_CanonCommMonoid.Unit",
"disc_equation_CanonCommMonoid.Var",
"equality_tok_CanonCommMonoid.Unit@tok",
"fuel_guarded_inversion_CanonCommMonoid.exp",
"subterm_ordering_CanonCommMonoid.Mult",
"typing_tok_CanonCommMonoid.Unit@tok"
],
0,
"c6f95e7fa93774ebc2eee78a7b31fd6f"
],
[
"CanonCommMonoid.flatten_correct_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_CanonCommMonoid.xsdenote.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_CanonCommMonoid.xsdenote.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@query", "binder_x_29bc033fbf136376eadf5c2199fe83d8_4",
"binder_x_a2a1950e8630eae361cf9493762886a6_6",
"binder_x_a2a1950e8630eae361cf9493762886a6_7",
"binder_x_a597e8b39b6549dcdad766448921454a_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_2",
"binder_x_fe28d8bcde588226b4e538b35321de05_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_CanonCommMonoid.var", "equation_CanonCommMonoid.vmap",
"equation_FStar.List.Tot.Base.op_At", "equation_Prims.nat",
"equation_with_fuel_CanonCommMonoid.xsdenote.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Prims.nat",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_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_7aac12c24449a22c34d98a0ea8ed4a32",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.op_At",
"typing_Prims.__proj__Cons__item__tl", "unit_inversion",
"unit_typing"
],
0,
"8211e1819d5bdcd36b34cf756cd7b28e"
],
[
"CanonCommMonoid.flatten_correct",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_CanonCommMonoid.flatten.fuel_instrumented",
"@fuel_correspondence_CanonCommMonoid.mdenote.fuel_instrumented",
"@fuel_correspondence_CanonCommMonoid.xsdenote.fuel_instrumented",
"@fuel_irrelevance_CanonCommMonoid.flatten.fuel_instrumented",
"@fuel_irrelevance_CanonCommMonoid.mdenote.fuel_instrumented",
"@query",
"CanonCommMonoid_pretyping_04ca1c898b2ee941b4d5e76a7044c379",
"binder_x_04ca1c898b2ee941b4d5e76a7044c379_6",
"binder_x_29bc033fbf136376eadf5c2199fe83d8_4",
"binder_x_a597e8b39b6549dcdad766448921454a_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_2",
"binder_x_fe28d8bcde588226b4e538b35321de05_3",
"constructor_distinct_CanonCommMonoid.Mult",
"constructor_distinct_CanonCommMonoid.Unit",
"constructor_distinct_CanonCommMonoid.Var",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"disc_equation_CanonCommMonoid.Mult",
"disc_equation_CanonCommMonoid.Unit",
"disc_equation_CanonCommMonoid.Var",
"equality_tok_CanonCommMonoid.Unit@tok",
"equality_tok_Prims.LexTop@tok", "equation_CanonCommMonoid.var",
"equation_CanonCommMonoid.vmap", "equation_Prims.nat",
"equation_with_fuel_CanonCommMonoid.flatten.fuel_instrumented",
"equation_with_fuel_CanonCommMonoid.mdenote.fuel_instrumented",
"equation_with_fuel_CanonCommMonoid.xsdenote.fuel_instrumented",
"fuel_guarded_inversion_CanonCommMonoid.exp",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_CanonCommMonoid.Mult__0",
"projection_inverse_CanonCommMonoid.Mult__1",
"projection_inverse_CanonCommMonoid.Var__0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"subterm_ordering_CanonCommMonoid.Mult",
"typing_CanonCommMonoid.flatten",
"typing_tok_CanonCommMonoid.Unit@tok"
],
0,
"c236cfc9e6b71bcd12b61fa72027f3be"
],
[
"CanonCommMonoid.apply_swap_aux_correct",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_CanonCommMonoid.var", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.nat", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.List.Tot.Base.length"
],
0,
"29b653a40cf587a507b4ad5b7c040c00"
],
[
"CanonCommMonoid.apply_swap_aux_correct",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_CanonCommMonoid.xsdenote.fuel_instrumented",
"@fuel_correspondence_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_CanonCommMonoid.xsdenote.fuel_instrumented",
"@fuel_irrelevance_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_29bc033fbf136376eadf5c2199fe83d8_5",
"binder_x_6abf175ef8030db79e1c78df8dc1c80f_8",
"binder_x_a2a1950e8630eae361cf9493762886a6_7",
"binder_x_a597e8b39b6549dcdad766448921454a_6",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_fe28d8bcde588226b4e538b35321de05_2",
"binder_x_fe28d8bcde588226b4e538b35321de05_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok",
"equation_CanonCommMonoid.var", "equation_CanonCommMonoid.vmap",
"equation_CanonCommSwaps.swap", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_CanonCommMonoid.xsdenote.fuel_instrumented",
"equation_with_fuel_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.nat", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction", "proj_equation_Prims.Cons_tl",
"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_090a06f8cdcdd6c3a2b22a117754681d",
"refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"subterm_ordering_Prims.Cons",
"token_correspondence_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_CanonCommMonoid.var", "typing_CanonCommSwaps.apply_swap_aux",
"typing_Prims.__proj__Cons__item__tl", "unit_inversion",
"unit_typing"
],
0,
"9fa26dcbc1ce81071759741e279b68e4"
],
[
"CanonCommMonoid.apply_swap_correct",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "equation_CanonCommMonoid.var",
"equation_CanonCommSwaps.apply_swap", "equation_CanonCommSwaps.swap",
"equation_Prims.nat",
"function_token_typing_CanonCommSwaps.apply_swap_aux",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_CanonCommSwaps_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_CanonCommSwaps.apply_swap"
],
0,
"cf6e2eb63b33cb5ae645dbe6c730c19d"
],
[
"CanonCommMonoid.apply_swaps_correct",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_CanonCommSwaps.apply_swaps.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_CanonCommSwaps.apply_swaps.fuel_instrumented",
"@query", "binder_x_a2a1950e8630eae361cf9493762886a6_6",
"binder_x_ca8dfc9730af6816dc21afe9b47d8c5a_7",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_CanonCommMonoid.var",
"equation_CanonCommSwaps.swap", "equation_Prims.nat",
"equation_with_fuel_CanonCommSwaps.apply_swaps.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Prims.nat", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "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_CanonCommSwaps_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
"subterm_ordering_Prims.Cons"
],
0,
"7a020661292dcb27724eba818cdea248"
],
[
"CanonCommMonoid.permute_via_swaps_correct_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_CanonCommMonoid.var",
"equation_Prims.nat",
"refinement_interpretation_Tm_refine_ef576a15b66f69e4ba5235543526c6d8"
],
0,
"3247c20151ce635e328dde2d0e7fc642"
],
[
"CanonCommMonoid.sort_via_swaps",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"equation_CanonCommMonoid.sort", "equation_CanonCommMonoid.var",
"equation_CanonCommMonoid.vmap",
"equation_CanonCommSwaps.equal_counts", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_CanonCommMonoid.var", "unit_typing"
],
0,
"08fc70e39bc5470868436c25b1b34994"
],
[
"CanonCommMonoid.sortWith_via_swaps",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"equation_CanonCommMonoid.sortWith", "equation_CanonCommMonoid.var",
"equation_CanonCommMonoid.vmap",
"equation_CanonCommSwaps.equal_counts", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"interpretation_Tm_abs_130f50af3b9642a0c7778eaf13263cff",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"token_correspondence_CanonCommMonoid.sortWith",
"token_correspondence_FStar.List.Tot.Base.sortWith",
"typing_CanonCommMonoid.var"
],
0,
"0c80aa8aa4902736a025d864b937080e"
],
[
"CanonCommMonoid.canon_correct",
1,
2,
1,
[ "@query", "equation_CanonCommMonoid.canon" ],
0,
"ecfd1782c52126de3a9d1cbfffe88b19"
],
[
"CanonCommMonoid.monoid_reflect",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"bbe205e889cbed1d4d3fc3f8ce4b16fe"
],
[
"CanonCommMonoid.where_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_54b8d13345a0876202ad05586d3a7a11_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_0",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"fuel_guarded_inversion_Prims.list", "int_inversion",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"subterm_ordering_Prims.Cons"
],
0,
"6d30d12fbf93ebf1359ee835db012500"
],
[
"CanonCommMonoid.reification_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_CanonCommMonoid.where", "equation_Prims.nat",
"function_token_typing_Prims.nat",
"lemma_FStar.Pervasives.invertOption",
"typing_CanonCommMonoid.where",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"4aeb58bf676e9fcdfb2a9264e4f8d602"
],
[
"CanonCommMonoid.term_mem",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_54b8d13345a0876202ad05586d3a7a11_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "fuel_guarded_inversion_Prims.list",
"subterm_ordering_Prims.Cons"
],
0,
"8fa5b26bc988b6d71291d562b7a590c2"
],
[
"CanonCommMonoid.quote_list",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "fuel_guarded_inversion_Prims.list"
],
0,
"e576dba0f649c996cbb4a5dfc576cdc3"
],
[
"CanonCommMonoid.quote_exp",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_CanonCommMonoid.Mult",
"disc_equation_CanonCommMonoid.Unit",
"disc_equation_CanonCommMonoid.Var",
"fuel_guarded_inversion_CanonCommMonoid.exp"
],
0,
"0f709ae90d498bec66d6ef7c305c9e89"
],
[
"CanonCommMonoid.const_compare",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"equation_CanonCommMonoid.var", "equation_CanonCommMonoid.vmap",
"equation_Prims.eqtype", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"function_token_typing_Prims.bool", "int_inversion",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_CanonCommMonoid.select_extra"
],
0,
"36c11a48f2822a0e0bd0a517ef507688"
],
[
"CanonCommMonoid.lem1",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_CanonCommMonoid.const_last",
"equation_CanonCommMonoid.sortWith", "equation_CanonCommMonoid.var",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"function_token_typing_FStar.List.Tot.Base.sortWith",
"interpretation_Tm_abs_130f50af3b9642a0c7778eaf13263cff",
"token_correspondence_CanonCommMonoid.sortWith"
],
0,
"7a7a6cd602df7108b53d7c600d630d97"
],
[
"CanonCommMonoid.lem1",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_CanonCommMonoid.const_last",
"equation_CanonCommMonoid.sortWith", "equation_CanonCommMonoid.var",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"function_token_typing_FStar.List.Tot.Base.sortWith",
"interpretation_Tm_abs_130f50af3b9642a0c7778eaf13263cff",
"token_correspondence_CanonCommMonoid.sortWith", "true_interp"
],
0,
"1d77fb9c4cee42f620578bde8504be5c"
],
[
"CanonCommMonoid.lem1",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_CanonCommMonoid.const_last",
"equation_CanonCommMonoid.sortWith", "equation_CanonCommMonoid.var",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"function_token_typing_FStar.List.Tot.Base.sortWith",
"interpretation_Tm_abs_130f50af3b9642a0c7778eaf13263cff",
"token_correspondence_CanonCommMonoid.sortWith"
],
0,
"0eef5570cdd55c2723487a8fbc8c3af7"
],
[
"CanonCommMonoid.special_compare",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"equation_CanonCommMonoid.var", "equation_CanonCommMonoid.vmap",
"equation_Prims.eqtype", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"function_token_typing_Prims.bool", "int_inversion",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_CanonCommMonoid.select_extra"
],
0,
"8cd76757ec5bb26fc3737fd69d7dcfe6"
],
[
"CanonCommMonoid.special_first_correct",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_CanonCommMonoid.sortWith",
"equation_CanonCommMonoid.special_first",
"equation_CanonCommMonoid.var", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Algebra.CommMonoid.cm",
"function_token_typing_FStar.List.Tot.Base.sortWith",
"interpretation_Tm_abs_130f50af3b9642a0c7778eaf13263cff",
"token_correspondence_CanonCommMonoid.sortWith"
],
0,
"bab10e2a84bbd423fd69b22ee728d571"
]
]
]
Computing file changes ...
