[
  "dՙ�\u001c�o���]\u0017�\u0018{�",
  [
    [
      "Hacl.Spec.Poly1305.Lemmas.pfelem",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "84b6ee859d15d16dfb2d63f727ff8bbd"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.zero",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "da1f97059ec688132c9e912baafb04fa"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.one",
      1,
      0,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "f9fe00892d09b200e81ff76045f8e943"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.nat",
        "equation_Prims.pos", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "9837adbad1583e8b228cf65b6a0f0e6f"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.nat",
        "equation_Prims.pos", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "8779bf668610964f0f846a7cb39b8d8d"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.op_Tilde_Percent",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.nat",
        "equation_Prims.pos", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "63a0092eb9d60d5243a5d9bdfad47623"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.add_identity",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.zero", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "typing_Hacl.Spec.Poly1305.Lemmas.zero"
      ],
      0,
      "92f804631421ec46835eb98b1804a251"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.mul_identity",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.one",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Hacl.Spec.Poly1305.Lemmas.one",
        "typing_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent"
      ],
      0,
      "52ddf18a360cbcb5bf660e15ee947def"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.add_associativity",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent"
      ],
      0,
      "0e076a677e4c6be167706ef0b8c1f6b9"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.add_commutativity",
      1,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "primitive_Prims.op_Addition"
      ],
      0,
      "9c018c825d1f5dae60420345ab0bba8c"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.mul_associativity",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "178b9365f9333b5c1994758c6fff2c56"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.mul_commutativity",
      1,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "primitive_Prims.op_Multiply"
      ],
      0,
      "c91bb0cbc2c8844289e46aab86f9dd82"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.mul_add_distr",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem_add_cm",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem_mul_cm",
        "equation_Prims.nat",
        "function_token_typing_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "function_token_typing_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus",
        "proj_equation_FStar.Algebra.CommMonoid.CM_mult",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Algebra.CommMonoid.CM_mult",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_FStar.Algebra.CommMonoid.__proj__CM__item__mult"
      ],
      0,
      "4b800abfd919092169e11149952694c5"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.mul_zero_l",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem_add_cm",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem_mul_cm",
        "equation_Prims.nat",
        "function_token_typing_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply",
        "proj_equation_FStar.Algebra.CommMonoid.CM_mult",
        "proj_equation_FStar.Algebra.CommMonoid.CM_unit",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Algebra.CommMonoid.CM_mult",
        "projection_inverse_FStar.Algebra.CommMonoid.CM_unit",
        "refinement_interpretation_Tm_refine_050542d050b31782e2f5a256a21d1330",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_FStar.Algebra.CommMonoid.__proj__CM__item__mult"
      ],
      0,
      "fd294b27c4fb9b37a7759e7322473bc5"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.add_opp",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.op_Tilde_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime",
        "equation_Hacl.Spec.Poly1305.Lemmas.zero", "equation_Prims.pos",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Minus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "c72671561ccd0e02f115e64b19ee1245"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.pfelem_cr",
      1,
      0,
      0,
      [
        "@query", "equation_Hacl.Spec.Poly1305.Lemmas.op_Tilde_Percent",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem",
        "equation_Hacl.Spec.Poly1305.Lemmas.pfelem_add_cm",
        "function_token_typing_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent",
        "proj_equation_FStar.Algebra.CommMonoid.CM_mult",
        "proj_equation_FStar.Algebra.CommMonoid.CM_unit",
        "projection_inverse_FStar.Algebra.CommMonoid.CM_mult",
        "projection_inverse_FStar.Algebra.CommMonoid.CM_unit",
        "token_correspondence_FStar.Algebra.CommMonoid.__proj__CM__item__mult"
      ],
      0,
      "2d8119d4bbcc2f85b7d8c0c8fa54d3ed"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify",
      1,
      0,
      0,
      [ "@query", "true_interp" ],
      0,
      "3643d798c8ad43549217956c782464d4"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_repeat_blocks_multi_lemma2_simplify",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "7f4ed3e99215ae875733e25f7c68f502"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b4b9f2caae6549e1c04b532818632080",
        "true_interp"
      ],
      0,
      "1b6eb352a8ce75756d4f9197321af66c"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_repeat_blocks_multi_lemma4_simplify",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "e4e37048ea6fb39a66883dc3b53039da"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_multi_lemma_load2_simplify",
      1,
      0,
      0,
      [ "@query", "true_interp" ],
      0,
      "8cbc47dadff3e9ffbd21ea3c6b675a73"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_multi_lemma_load2_simplify",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "a507ff96d87e23568ab81984c3ba02b0"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_multi_lemma_load4_simplify",
      1,
      0,
      0,
      [ "@query", "true_interp" ],
      0,
      "4c2f4e44c0c2d3b07752efeaec977e7e"
    ],
    [
      "Hacl.Spec.Poly1305.Lemmas.poly_update_multi_lemma_load4_simplify",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.Spec.Poly1305.Lemmas.prime"
      ],
      0,
      "ebde6a74c288cd0af16610dfaa7a2bc6"
    ]
  ]
]