[
  "\"™N\u0005’ƒ×dê*(ï/SëŽ",
  [
    [
      "Vale.Poly1305.Math.lowerUpper128_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "f911ab3cbd2b5fa5416579209d896879"
    ],
    [
      "Vale.Poly1305.Math.lowerUpper128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "529c046ae541142df65a9a9d03b43929"
    ],
    [
      "Vale.Poly1305.Math.lowerUpper192_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "32af324f6c483cdcaec4ac3adc78e9fd"
    ],
    [
      "Vale.Poly1305.Math.lemma_poly_multiply",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "4b311324bcc2503aba2c6433befa469d"
    ],
    [
      "Vale.Poly1305.Math.lemma_poly_reduce",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "int_inversion", "l_and-interp", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "af5ec75be5302b2f8dcffa6fadec8d31"
    ],
    [
      "Vale.Poly1305.Math.lemma_bytes_shift_power2",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "53023ce1edd85d7cae22d628b3a3f256"
    ],
    [
      "Vale.Poly1305.Math.lemma_bytes_and_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Types_s.ishl"
      ],
      0,
      "85edb22983c4f5ec619aa6807ff36efd"
    ],
    [
      "Vale.Poly1305.Math.lemma_mod_power2_lo",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "int_inversion", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "d3973aee8681fb775bac550723752f09"
    ],
    [
      "Vale.Poly1305.Math.lemma_power2_add64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c122067a423d935bf7e73cfd5787a02b"
    ],
    [
      "Vale.Poly1305.Math.lemma_mod_hi",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "60ff73658210d318c228fb8887f4821a"
    ],
    [
      "Vale.Poly1305.Math.lemma_poly_demod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "0bff2a91eab0a6127ce8b5fce8832cde"
    ]
  ]
]