https://github.com/project-everest/hacl-star
Tip revision: 7829770a46b5d5a167de0107af2127bbedf8fe3c authored by Marina Polubelova on 05 August 2020, 23:05:18 UTC
fix nacl-box
fix nacl-box
Tip revision: 7829770
Lib.LoopCombinators.fst.hints
[
"�$#�#��h6W�hq}h�",
[
[
"Lib.LoopCombinators.repeat_left",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"9d639330348caaa8bba96913b60b711c"
],
[
"Lib.LoopCombinators.repeat_left",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"2671cc0a5a25ed2ccf89e342f56286a1"
],
[
"Lib.LoopCombinators.repeat_left",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_ef3cff77d20be12dde95f0777a90f70e_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2eb00ca989f9ebed0ed65e52a78766e7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"c6125b86a4ea522405e5f3ee6424a360"
],
[
"Lib.LoopCombinators.repeat_left_all_ml",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"e88e06c47596877b50755a77f9419e65"
],
[
"Lib.LoopCombinators.repeat_left_all_ml",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"152bff9386a1673f3f05939495600d9a"
],
[
"Lib.LoopCombinators.repeat_left_all_ml",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.result",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913"
],
0,
"bc7b85166619a0b2cdac17a798cd4b10"
],
[
"Lib.LoopCombinators.repeat_right",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"0d7f783826550ab70e9f5f62d16d6307"
],
[
"Lib.LoopCombinators.repeat_right",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"8365dccfbb228829fcc158d29c43e1bc"
],
[
"Lib.LoopCombinators.repeat_right",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_ef3cff77d20be12dde95f0777a90f70e_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2eb00ca989f9ebed0ed65e52a78766e7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_68812a9442c7946d522ecd05c6a1a9af",
"well-founded-ordering-on-nat"
],
0,
"10f0fef5a90673906026f3511fd20301"
],
[
"Lib.LoopCombinators.repeat_right_all_ml",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"a2538b1fd14a95f49040953bb305d0ea"
],
[
"Lib.LoopCombinators.repeat_right_all_ml",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"ec494c0921529a452863eeba74a75c9b"
],
[
"Lib.LoopCombinators.repeat_right_all_ml",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.result",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913"
],
0,
"cb9b8e20e3ac9c06c679c1768a14f883"
],
[
"Lib.LoopCombinators.repeat_right_plus",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"4a9f422325879770ff3220685b7e6420"
],
[
"Lib.LoopCombinators.repeat_right_plus",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"10722d1c140c25be3e26776a7e988c4a"
],
[
"Lib.LoopCombinators.repeat_right_plus",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_475c5d8500e6c5accacf8430e17609c1",
"Lib.LoopCombinators_interpretation_Tm_arrow_d923f15fa51c1adf198e41a2a2b838b8",
"binder_x_1643872395c8718ea40fbc2752387c4d_5",
"binder_x_9c1467c8a1dc9d1a9cfdd135b2fced70_3",
"binder_x_af5edae8b4ff911e6a823e510ac6c756_6",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_e1b475a8738f7fad7118cc46529602ed_4",
"binder_x_ef3cff77d20be12dde95f0777a90f70e_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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_2eb00ca989f9ebed0ed65e52a78766e7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_64e0884aedfcc28624ca5710ec89a7e4",
"refinement_interpretation_Tm_refine_94b4e5d3116d0fdc2008285d6fe3b144",
"refinement_interpretation_Tm_refine_9f4b8102951be8af6f4ece9f995f631e",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"typing_Lib.LoopCombinators.repeat_right",
"well-founded-ordering-on-nat"
],
0,
"9aa5003d2a80355fbeafc8d0ba8c8e61"
],
[
"Lib.LoopCombinators.unfold_repeat_right",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"9de97d86dda0f9ef4ae61c4a07075414"
],
[
"Lib.LoopCombinators.unfold_repeat_right",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"2b067b3f53e2c8a23e04652eda392421"
],
[
"Lib.LoopCombinators.unfold_repeat_right",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"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_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795"
],
0,
"03d9321a976243ddafa66d84d7092a7f"
],
[
"Lib.LoopCombinators.eq_repeat_right",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"9ad002ea351f941e9f3e0605de3639a5"
],
[
"Lib.LoopCombinators.eq_repeat_right",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"ac4c71c43cc515c6818a48c49bee0297"
],
[
"Lib.LoopCombinators.eq_repeat_right",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795"
],
0,
"bf666671b8517d3cee5f5e232b251d27"
],
[
"Lib.LoopCombinators.repeat_left_right",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"64a2cb8e43d25050762be24c9d944106"
],
[
"Lib.LoopCombinators.repeat_left_right",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
],
0,
"796ba401263e5100b71550e18e5eee5d"
],
[
"Lib.LoopCombinators.repeat_left_right",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_73e03d6f682a7e8a0e2e4caa6e7e006f",
"Lib.LoopCombinators_interpretation_Tm_arrow_e54f60146c15ffc3c6fdfdf188f36184",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_15a2a2aa213729b179fdecca4d6d5fcf_5",
"binder_x_57098d7a08a5c655d3e755e495233706_3",
"binder_x_61db9e95f5c6e22c0f798a9af5990a12_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_ef3cff77d20be12dde95f0777a90f70e_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2eb00ca989f9ebed0ed65e52a78766e7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_5a9b6c458d60ee3d78bcb9cb8e632018",
"refinement_interpretation_Tm_refine_68812a9442c7946d522ecd05c6a1a9af",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"well-founded-ordering-on-nat"
],
0,
"e9c37bc9255f84caad512a1c200be6d0"
],
[
"Lib.LoopCombinators.repeat_gen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"3a318840e42af6261a6c945935d2c7e1"
],
[
"Lib.LoopCombinators.repeat_gen",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"217bd95f553727485e7816eb8b494258"
],
[
"Lib.LoopCombinators.repeat_gen",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"92b866e5aa726c2055855eb120d7e7b4"
],
[
"Lib.LoopCombinators.repeat_gen_all_ml",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"b711c57aa6471e80b9979a26c1296d3d"
],
[
"Lib.LoopCombinators.repeat_gen_all_ml",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"71ba1c5f79fafdc520e4b9b6fad685dd"
],
[
"Lib.LoopCombinators.repeat_gen_all_ml",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"30082674aa879d102d038a8cde116aa9"
],
[
"Lib.LoopCombinators.unfold_repeat_gen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"f002954af4b730ecfda8a2d868dc59e8"
],
[
"Lib.LoopCombinators.unfold_repeat_gen",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"dfb0809cd97c8947f37ee79d37eab08e"
],
[
"Lib.LoopCombinators.unfold_repeat_gen",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"equation_Lib.LoopCombinators.repeat_gen", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"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_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795"
],
0,
"0e977569a59599cd046b24e4c458beb5"
],
[
"Lib.LoopCombinators.eq_repeat_gen0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"c4a20385125bc52f989557f024a7394d"
],
[
"Lib.LoopCombinators.eq_repeat_gen0",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"3cba5f3f1cb41d60fcf60b734f0928f0"
],
[
"Lib.LoopCombinators.eq_repeat_gen0",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"equation_Lib.LoopCombinators.repeat_gen", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795"
],
0,
"c6fa9e22b55f8180ce41d8ca95126ccd"
],
[
"Lib.LoopCombinators.repeat_gen_def",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"7babc05d0588621788432cd735e47c18"
],
[
"Lib.LoopCombinators.repeat_gen_def",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"8963aba13526701273283a35162ea975"
],
[
"Lib.LoopCombinators.repeat_gen_def",
3,
2,
1,
[ "@query", "equation_Lib.LoopCombinators.repeat_gen" ],
0,
"98df8d0cd1d1e1fb5d3ba684682eaf2f"
],
[
"Lib.LoopCombinators.eq_repeati0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"09479fa93b81297845d28ce8c9e14c73"
],
[
"Lib.LoopCombinators.eq_repeati0",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_67c7b2626869cb316f118144000415b9",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.repeat_gen",
"equation_Lib.LoopCombinators.repeati", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"function_token_typing_Lib.LoopCombinators.fixed_a", "int_typing",
"primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"token_correspondence_Lib.LoopCombinators.fixed_a"
],
0,
"6784e53a150229bc72743280ba65564e"
],
[
"Lib.LoopCombinators.unfold_repeati",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"681a724014b27c4550fca73a4f0775dd"
],
[
"Lib.LoopCombinators.unfold_repeati",
2,
2,
1,
[
"@query", "equation_Lib.LoopCombinators.repeati",
"primitive_Prims.op_Addition"
],
0,
"264e3f7f1d23e162b28d0697f9bf4110"
],
[
"Lib.LoopCombinators.repeati_def",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"5fc053431a14971f92174639bc2dacc0"
],
[
"Lib.LoopCombinators.repeati_def",
2,
2,
1,
[
"@query", "equation_Lib.LoopCombinators.repeat_gen",
"equation_Lib.LoopCombinators.repeati"
],
0,
"ab58d5e03f4e683939afed8867192fe3"
],
[
"Lib.LoopCombinators.eq_repeat0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_67c7b2626869cb316f118144000415b9",
"Lib.LoopCombinators_interpretation_Tm_arrow_bfe22415bc48790397b6e21fcc88873f",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.repeat",
"equation_Lib.LoopCombinators.repeat_gen",
"equation_Lib.LoopCombinators.repeati", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"function_token_typing_Lib.LoopCombinators.fixed_a",
"function_token_typing_Lib.LoopCombinators.fixed_i", "int_typing",
"kinding_Tm_arrow_fcd589b21e6efcf1e5d17b07c282a015",
"primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"token_correspondence_Lib.LoopCombinators.fixed_a"
],
0,
"a6edecc749c35bacd06421d4a5f0a785"
],
[
"Lib.LoopCombinators.unfold_repeat",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"e268872e4b7c5b8f88759016752247b0"
],
[
"Lib.LoopCombinators.unfold_repeat",
2,
2,
1,
[
"@query", "equation_Lib.LoopCombinators.fixed_i",
"equation_Lib.LoopCombinators.repeat", "primitive_Prims.op_Addition",
"token_correspondence_Lib.LoopCombinators.fixed_i"
],
0,
"d3e2839548aac42772b549b57712ba78"
],
[
"Lib.LoopCombinators.repeat_range",
1,
2,
1,
[ "@query" ],
0,
"dc82086fdb7a43886125c64dfa74003b"
],
[
"Lib.LoopCombinators.repeat_range_all_ml",
1,
2,
1,
[ "@query" ],
0,
"66bc45193d7d1352966218e3291e462a"
],
[
"Lib.LoopCombinators.repeatable",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"3cb441f89d76e2dde71b6bf9d88c1c4e"
],
[
"Lib.LoopCombinators.repeat_range_inductive",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913"
],
0,
"30903aa2dae1def4c373224babed6501"
],
[
"Lib.LoopCombinators.repeat_range_inductive",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913"
],
0,
"067e8d19cd184ac40d0515d600ed529b"
],
[
"Lib.LoopCombinators.repeat_range_inductive",
3,
2,
1,
[ "@query" ],
0,
"164f29bbede65a74a58e82d5e0e227ff"
],
[
"Lib.LoopCombinators.repeati_inductive",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"1812d2f8833a02322fb29bb97bb91467"
],
[
"Lib.LoopCombinators.repeati_inductive",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b4d6875628d4f8ea4fcf73d3ca3bcadb"
],
[
"Lib.LoopCombinators.repeati_inductive",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"dcbc260340ad6350328e1a419b5b9a0c"
],
[
"Lib.LoopCombinators.repeati_inductive_repeat_gen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"c631f8e7d9fc8c364f28867a6f171ded"
],
[
"Lib.LoopCombinators.repeati_inductive_repeat_gen",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"16db3a1c47d576c2d2cbd30cdd221ca8"
],
[
"Lib.LoopCombinators.repeati_inductive_repeat_gen",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_9228bb88100b5a0762d39b5c83174ad9",
"Lib.LoopCombinators_interpretation_Tm_arrow_a5015036cf1762e788e4ccbba6a8d538",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"equation_Lib.LoopCombinators.repeat_gen", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_left.fuel_instrumented",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0e3034507692d95678dac3878d3c5d27",
"interpretation_Tm_abs_cf403a3c460d958924174d2b00a62cb3",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_08698b4b6e166624b5bf789ac071b4cf",
"refinement_interpretation_Tm_refine_0f5d287096bf7dd24d582019e4d18f0c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_574e14f4b9c774d5e61146c6d94cf593",
"refinement_interpretation_Tm_refine_909c0555fed853bc5dc1098d3dd63f21",
"refinement_interpretation_Tm_refine_96e65b2359ce32ff1f5ca9648c355aa6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"typing_Lib.LoopCombinators.repeat_gen",
"typing_Tm_abs_0e3034507692d95678dac3878d3c5d27"
],
0,
"f3526a526e4c62eab44c8ac2291daa2a"
],
[
"Lib.LoopCombinators.preserves_predicate",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0d54a6ac776e809e17c16d070e187012"
],
[
"Lib.LoopCombinators.preserves_predicate",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"94b53140691291b3d3bad0f50435552b"
],
[
"Lib.LoopCombinators.repeat_gen_inductive",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"dffc72a59339300ef8a6a0b42b68fdae"
],
[
"Lib.LoopCombinators.repeat_gen_inductive",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"35b20ac291c5ed1b0b528a391df135cf"
],
[
"Lib.LoopCombinators.repeat_gen_inductive",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"equation_Lib.LoopCombinators.preserves_predicate",
"equation_Lib.LoopCombinators.repeat_gen", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"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_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_695fc9bad57438f078f1918065bbd3eb",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795"
],
0,
"09f5c68434fd87d9bff5e03a403a02c0"
],
[
"Lib.LoopCombinators.preserves",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0defe91a1c8623410d781a535de05e3e"
],
[
"Lib.LoopCombinators.repeati_inductive'",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"595c1910f5ae1852f4ea289ab833c6fa"
],
[
"Lib.LoopCombinators.repeati_inductive'",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@fuel_irrelevance_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8",
"Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6",
"Lib.LoopCombinators_interpretation_Tm_arrow_67c7b2626869cb316f118144000415b9",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"equation_Lib.LoopCombinators.fixed_a",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.LoopCombinators.repeat_gen",
"equation_Lib.LoopCombinators.repeati", "equation_Prims.nat",
"equation_with_fuel_Lib.LoopCombinators.repeat_right.fuel_instrumented",
"function_token_typing_Lib.LoopCombinators.fixed_a", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"token_correspondence_Lib.LoopCombinators.fixed_a"
],
0,
"abf3b227b21d1cd9858326059cd0f7ee"
]
]
]