[
  "@´\"\u0014½Á&m<\u0017�5\u0010êîS",
  [
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "typing_Spec.P256.Definitions.prime256"
      ],
      0,
      "3866b7ad0909a6b1d34229f65938cfed"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "740300c2c7186ffc138c3bf01dcf1e8c"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_8807a8a6db5cf1a86cc29f7b64a93885",
        "refinement_interpretation_Tm_refine_93e2420a1bc2654a04bc10881f331e3b",
        "refinement_interpretation_Tm_refine_a92851949b382679e8dc999df60d181e"
      ],
      0,
      "cf1885ceda07c15044df59291777167f"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "20417e3d7785fd5c6bc7b269d338290a"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "6b0083f29e24a7fe2389822db5ab9a3a"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double", "int_typing",
        "lemma_Spec.P256.MontgomeryMultiplication.lemmaToDomainAndBackIsTheSame",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a92851949b382679e8dc999df60d181e",
        "refinement_interpretation_Tm_refine_a9a8ee103221296ed130a43a8be51fb9",
        "refinement_interpretation_Tm_refine_ac652f9023b70de96af3f923ebf68db3",
        "refinement_interpretation_Tm_refine_cf60fc7ec5c165f556fc4bba108ab85b",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "a0081e1127c3a7c7e9143c1b352695ea"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
      ],
      0,
      "16e6124b1683557da6e8499874745984"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "3e8d2e3ea155b3156fbe9e2c1a50d5f1"
    ],
    [
      "Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
        "equation_Spec.P256._point_double",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_4429a03440a4f885fdd4b2268b6cb06f"
      ],
      0,
      "474a4f4707520245a98be1e97d67f00e"
    ]
  ]
]