Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.Math.Lemmas.Int.fsti.hints
[
"�lj�\u0003\u0013�\u001bh�G\u001e�Ⳮ",
[
[
"Vale.Math.Lemmas.Int.multiply_fractions",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"636648b5dcd7938c554e9ae1d2ffe84e"
],
[
"Vale.Math.Lemmas.Int.lemma_div_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9ff671a39af150428ad61501f6aababb"
],
[
"Vale.Math.Lemmas.Int.lemma_div_lt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"aadd2b609c94fe5abe231c9e59dbc40d"
],
[
"Vale.Math.Lemmas.Int.small_div",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"98f1035ba4801a9211a51d9ecedce496"
],
[
"Vale.Math.Lemmas.Int.small_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d43b1f6c0b7fe03aae5f0d31e723702e"
],
[
"Vale.Math.Lemmas.Int.lemma_div_plus",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"486500afd8d383249613cc2625c08a3e"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_plus",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3238afb343ad412e871677e282fc203c"
],
[
"Vale.Math.Lemmas.Int.cancel_mul_div",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"15e71328e62f5a52961e2a078b1d4785"
],
[
"Vale.Math.Lemmas.Int.cancel_mul_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f71e4fbf4ccd33193552734f4416c6f4"
],
[
"Vale.Math.Lemmas.Int.mod_add_both",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ea306a80e24498699c14033e71a21391"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_add_distr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"5ce869944c9bb381ddd2133d6a3139b8"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_sub_distr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"aae9ce1cdb24f1ec9baf8550ed067f9a"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_mul_distr_l",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0eada4a49a24350f3b33f90787a49601"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_mul_distr_r",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"dd6bac3be6248aea949d10a4bf6391e6"
],
[
"Vale.Math.Lemmas.Int.lemma_div_exact",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8298db96ebbf386ae1ef55cf0f6db32b"
],
[
"Vale.Math.Lemmas.Int.div_exact_r",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"fbc465a14cd5f2f6090b290ca755b292"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_spec",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"cffd6d009b5094cab63d7728f1933ec3"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_spec2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"39e86f58f32ca4483026e1f4b4fde63b"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_plus_distr_l",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8a2585535dbeb7af6ba2e095e8b96d73"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_plus_distr_r",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"afefff65b3a313d52044175d784b5b0b"
],
[
"Vale.Math.Lemmas.Int.small_division_lemma_2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b90b70c37471e6f38bf51689fcb828b7"
],
[
"Vale.Math.Lemmas.Int.division_propriety",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2af292bfd6a15f279307381a51ca2000"
],
[
"Vale.Math.Lemmas.Int.division_definition",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8462cf5cce1875dfbd373e3439d95663"
],
[
"Vale.Math.Lemmas.Int.multiple_division_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b9988271b3dcd8726ae4249e6ab6cdf2"
],
[
"Vale.Math.Lemmas.Int.multiple_modulo_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"da5763d69c6176663400b55bf64d9071"
],
[
"Vale.Math.Lemmas.Int.division_addition_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"26df52d82795b9768f268e97befb7b4f"
],
[
"Vale.Math.Lemmas.Int.division_sub_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7592f5a0a1d6244c2e0ed4291c5f0759"
],
[
"Vale.Math.Lemmas.Int.modulo_distributivity",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"790310984bc57370bfec5367187904ff"
],
[
"Vale.Math.Lemmas.Int.modulo_addition_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3784009374d0ad3ba10419e69b3e5844"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_sub",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a3a89be12755404202f40e8b514bb33c"
],
[
"Vale.Math.Lemmas.Int.mod_mult_exact",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ed1c2506c1786143a1a6de9771abdb29"
],
[
"Vale.Math.Lemmas.Int.mod_mul_div_exact",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.pos",
"equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d1e859906c7b412ec794b5c9a15bb00a"
],
[
"Vale.Math.Lemmas.Int.mod_pow2_div2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a456b6c35fdc7e2a3137bf576c4d94f0"
],
[
"Vale.Math.Lemmas.Int.division_multiplication_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"93b99977608b328b9062df04d92970df"
],
[
"Vale.Math.Lemmas.Int.modulo_modulo_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9523b149c5786ce3e881e4abc83a7fa0"
],
[
"Vale.Math.Lemmas.Int.lemma_mod_plus_injective",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3525b23674f4cb46cab2a4ac10adb107"
]
]
]
Computing file changes ...
