Revision 9a1c35986c9ec0d91b29ce0fcc77700ae032310a authored by Aseem Rastogi on 01 April 2021, 08:46:33 UTC, committed by Aseem Rastogi on 01 April 2021, 08:46:33 UTC
1 parent 122750f
Lib.NatMod.fst.hints
[
"\u0019������z���h�D�",
[
[
"Lib.NatMod.mk_nat_group",
1,
2,
1,
[ "@query" ],
0,
"87280519a8e1d9366257f73b4eb47201"
],
[
"Lib.NatMod.pow",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"580eeef9192ec134655ba53cbcd88da9"
],
[
"Lib.NatMod.lemma_pow0",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"equation_with_fuel_Lib.NatMod.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"814a27652c3962b0e2d5a7bfa5b893c6"
],
[
"Lib.NatMod.lemma_pow1",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"equation_with_fuel_Lib.NatMod.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.NatMod.pow"
],
0,
"736f0f675438dc8b4a2ac5deb3c3d761"
],
[
"Lib.NatMod.lemma_pow_unfold",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"4d738ddd82899650aa7bb7211d37296f"
],
[
"Lib.NatMod.lemma_pow_unfold",
2,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented",
"@fuel_irrelevance_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Lib.NatMod.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"771dddbc34f1bc7463517ce508f54094"
],
[
"Lib.NatMod.lemma_pow_gt_zero",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"e3fb132b440619511942fb9e1176f744"
],
[
"Lib.NatMod.lemma_pow_ge_zero",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_Lib.NatMod.lemma_pow_gt_zero",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"1ce5380b9192bfe7d5aff4ae30dbf3b3"
],
[
"Lib.NatMod.lemma_pow_nat_is_pow",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Lib.Exponentiation.fmul",
"equation_Lib.Exponentiation.one",
"equation_Lib.NatMod.mk_nat_group", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_8043e4a8d64039a018f0a54c1c55af00",
"interpretation_Tm_abs_e7b0793a93fa8dd7eb00cf2e34267add",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"proj_equation_Lib.Exponentiation.Mkexp_fmul",
"proj_equation_Lib.Exponentiation.Mkexp_one",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Lib.Exponentiation.Mkexp_fmul",
"projection_inverse_Lib.Exponentiation.Mkexp_one",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Lib.Exponentiation.fmul",
"token_correspondence_Lib.Exponentiation.one",
"token_correspondence_Prims.op_Multiply",
"well-founded-ordering-on-nat"
],
0,
"ef4b85811b7f2047d9f0926dfd45ca44"
],
[
"Lib.NatMod.lemma_pow_add",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"26c6c326261ab87ddd605ebaf173a460"
],
[
"Lib.NatMod.lemma_pow_add",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Exponentiation.fmul",
"equation_Lib.NatMod.mk_nat_group", "equation_Prims.nat",
"interpretation_Tm_abs_8043e4a8d64039a018f0a54c1c55af00",
"primitive_Prims.op_Addition",
"proj_equation_Lib.Exponentiation.Mkexp_fmul",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Lib.Exponentiation.Mkexp_fmul",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Lib.Exponentiation.fmul",
"token_correspondence_Prims.op_Multiply"
],
0,
"a93c7342233991e57475b8bd49a9dfcd"
],
[
"Lib.NatMod.lemma_pow_mul",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"db9f525776b8e05764612387e96cc327"
],
[
"Lib.NatMod.lemma_pow_mul",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"e25be055037a1bc63f6d23e6317771e0"
],
[
"Lib.NatMod.lemma_pow_double",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"81cd8fec435b654e6058802ede9150a8"
],
[
"Lib.NatMod.lemma_pow_double",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Exponentiation.fmul",
"equation_Lib.NatMod.mk_nat_group", "equation_Prims.nat",
"int_inversion",
"interpretation_Tm_abs_8043e4a8d64039a018f0a54c1c55af00",
"primitive_Prims.op_Addition",
"proj_equation_Lib.Exponentiation.Mkexp_fmul",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Lib.Exponentiation.Mkexp_fmul",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Lib.Exponentiation.fmul",
"token_correspondence_Prims.op_Multiply"
],
0,
"7dc7aeb5f9168698904948a0fb5c8624"
],
[
"Lib.NatMod.lemma_pow_mul_base",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.Exponentiation.fmul",
"equation_Lib.NatMod.mk_nat_group", "int_inversion",
"interpretation_Tm_abs_8043e4a8d64039a018f0a54c1c55af00",
"proj_equation_Lib.Exponentiation.Mkexp_fmul",
"projection_inverse_Lib.Exponentiation.Mkexp_fmul",
"token_correspondence_Lib.Exponentiation.fmul",
"token_correspondence_Prims.op_Multiply"
],
0,
"e16bc9d5ee8618bf931d2bdd669973a7"
],
[
"Lib.NatMod.lemma_pow_mod_base",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3819eae404963ab27c3e5a04adf11f88"
],
[
"Lib.NatMod.lemma_pow_mod_base",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f9f88af3b1e2dbc99e38f49301940025"
],
0,
"1ed745b002df350031ce9eebbe52ca2c"
],
[
"Lib.NatMod.lemma_pow_mod_base",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"c0722159391a9aad5c78d88bac20664c"
],
[
"Lib.NatMod.one_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"fb1a52c06e921919e66ba901d73a4553"
],
[
"Lib.NatMod.mul_mod",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"032fb7f2b49339b4ff0ab0a63c2028ea"
],
[
"Lib.NatMod.lemma_one_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.mul_mod",
"equation_Lib.NatMod.nat_mod", "equation_Lib.NatMod.one_mod",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Lib.NatMod.mul_mod", "typing_Lib.NatMod.one_mod"
],
0,
"69aab60a25b80bfd35eb1bcccb5bf9a5"
],
[
"Lib.NatMod.lemma_mul_mod_assoc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.mul_mod",
"equation_Lib.NatMod.nat_mod", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"d42876849cd9380372d9949005384ed7"
],
[
"Lib.NatMod.lemma_mul_mod_comm",
1,
0,
0,
[
"@query", "equation_Lib.NatMod.mul_mod",
"primitive_Prims.op_Multiply"
],
0,
"db3fa90904c47382e5defd6a7b70aea0"
],
[
"Lib.NatMod.pow_mod_",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"4934de65499d11df02eb6cc97f20607f"
],
[
"Lib.NatMod.lemma_pow_mod1",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow_mod_.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Lib.NatMod.pow_mod", "equation_Prims.pos",
"equation_with_fuel_Lib.NatMod.pow_mod_.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9afbd5b8908985ec656f4dee747e9d60"
],
[
"Lib.NatMod.lemma_pow_mod_unfold0",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1da93ef63852a3a506544a292b2657a4"
],
0,
"a5a507511511ff0343a64ac4cae7656a"
],
[
"Lib.NatMod.lemma_pow_mod_unfold0",
2,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow_mod_.fuel_instrumented",
"@fuel_irrelevance_Lib.NatMod.pow_mod_.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.pow_mod",
"equation_Prims.pos",
"equation_with_fuel_Lib.NatMod.pow_mod_.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1da93ef63852a3a506544a292b2657a4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"711a4cf5cb3da71f4423d5c44033d2b3"
],
[
"Lib.NatMod.lemma_pow_mod_unfold1",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f"
],
0,
"7cdc77dfd7297e8f1aa73e82b1c63c49"
],
[
"Lib.NatMod.lemma_pow_mod_unfold1",
2,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow_mod_.fuel_instrumented",
"@fuel_irrelevance_Lib.NatMod.pow_mod_.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.pow_mod",
"equation_Prims.pos",
"equation_with_fuel_Lib.NatMod.pow_mod_.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2b060c198748ac61ad87847894b57f20"
],
[
"Lib.NatMod.lemma_pow_mod_",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"61d7ef46ac8dd3ecb607695de105ac03"
],
[
"Lib.NatMod.lemma_pow_mod_",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_6092045e3746216d4a7e28a7890a43dd",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b4858f57afdd2c4a1250246c8d1b0555"
],
[
"Lib.NatMod.lemma_pow_mod_",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_294bbd16ad656dcb9eba9c34cf7aac04_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Lib.NatMod.mul_mod",
"equation_Lib.NatMod.nat_mod", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"unit_inversion", "unit_typing", "well-founded-ordering-on-nat"
],
0,
"523820e70d540e7a7f6ed74923370875"
],
[
"Lib.NatMod.lemma_pow_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"74269a2f089a636b7c3f6c35c8fda4d6"
],
[
"Lib.NatMod.lemma_pow_mod",
2,
0,
0,
[ "@query" ],
0,
"b01fa71f3424d4df9735bd6d5ebb6265"
],
[
"Lib.NatMod.lemma_pow_nat_mod_is_pow",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ec42ef706ec63d6eb19e4995045b62c6"
],
[
"Lib.NatMod.lemma_pow_nat_mod_is_pow",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9940fd5216d1969f95f956276466686b"
],
0,
"7d731c33c260b4ca0fd30520e201a7d6"
],
[
"Lib.NatMod.lemma_pow_nat_mod_is_pow",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_294bbd16ad656dcb9eba9c34cf7aac04_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Lib.Exponentiation.fmul",
"equation_Lib.NatMod.mk_nat_mod_group",
"equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.nat_mod",
"equation_Lib.NatMod.one_mod", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_8043e4a8d64039a018f0a54c1c55af00",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_Lib.Exponentiation.Mkexp_fmul",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Lib.Exponentiation.Mkexp_fmul",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Lib.Exponentiation.__proj__Mkexp__item__fmul",
"token_correspondence_Lib.Exponentiation.fmul",
"token_correspondence_Lib.NatMod.mul_mod",
"well-founded-ordering-on-nat"
],
0,
"fe171f14efb82d3195d13cd861dcdc1c"
]
]
]
Computing file changes ...
