[
  "\\=\u001dN�D@N1&|�\u0011�\n&",
  [
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logand",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.l_not",
        "equation_Prims.squash", "l_not-interp", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned"
      ],
      0,
      "b72651797ad00233ee6b573236c3bb5a"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logand",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt128.n",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.logand", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "int_inversion",
        "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4a73301fbc41c8e432f23b6aef69a5eb",
        "refinement_interpretation_Tm_refine_6377d26335dc60c35078980c34caecb6",
        "refinement_interpretation_Tm_refine_71d1a346f76194fb038bba96302ce90d",
        "refinement_interpretation_Tm_refine_7afd5b0ca8e77c7f6870883658e19d63",
        "refinement_interpretation_Tm_refine_7cf5fd844874f3049d3067fe68a85256",
        "typing_FStar.UInt128.logand", "typing_FStar.UInt16.logand",
        "typing_FStar.UInt32.logand", "typing_FStar.UInt64.logand",
        "typing_FStar.UInt8.logand", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.unsigned", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "53592edc5b2da66996f5403c0684b718"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logor",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.l_not",
        "equation_Prims.squash", "l_not-interp", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned"
      ],
      0,
      "e68d389dcc0fbe4c3c845728a7299a12"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logor",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt128.n",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.logor", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "int_inversion",
        "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_3881ab512ff2d0d86d43bf57b0c61e75",
        "refinement_interpretation_Tm_refine_39cb18a1d289e559096741772432b24f",
        "refinement_interpretation_Tm_refine_6913af387cf2f30da0961ac60666f00f",
        "refinement_interpretation_Tm_refine_a7fcc8489f92354d1f8a101b7f900b3b",
        "refinement_interpretation_Tm_refine_be6bb0b9b6f3f07f3a5bb3ae3b56ec6a",
        "typing_FStar.UInt128.logor", "typing_FStar.UInt16.logor",
        "typing_FStar.UInt32.logor", "typing_FStar.UInt64.logor",
        "typing_FStar.UInt8.logor", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.unsigned", "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "356ca6aa39bbb7a4e419bc6ff693810d"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logxor",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.l_not",
        "equation_Prims.squash", "l_not-interp", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned"
      ],
      0,
      "dec3a806cac4f567e8a8caa73734f781"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_logxor",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_FStar.UInt128.n",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.logxor", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1e2a54f659380dff04459b91e600441e",
        "refinement_interpretation_Tm_refine_2b25e5c3b25bc06167200cbfa5d36b3e",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_97e4a63388ae45ee4261a689ecdcc635",
        "refinement_interpretation_Tm_refine_b87f471e80e3c2bc077d38b7026cfcf6",
        "refinement_interpretation_Tm_refine_e55be37d77d9b240b683ff3354ca439c",
        "typing_FStar.UInt128.logxor", "typing_FStar.UInt16.logxor",
        "typing_FStar.UInt32.logxor", "typing_FStar.UInt64.logxor",
        "typing_FStar.UInt8.logxor", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.SEC@tok"
      ],
      0,
      "8e785c95056b6ed4cbbd026e258369c3"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_eq_mask",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.S128", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5"
      ],
      0,
      "388dbcf48af9d0e4d05577bd7541d34c"
    ],
    [
      "Vale.Math.Poly2.Galois.IntTypes.define_eq_mask",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_Lib.IntTypes.S128", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.unsigned",
        "lemma_Lib.IntTypes.eq_mask_lemma", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7",
        "typing_Lib.IntTypes.unsigned"
      ],
      0,
      "31d5a3cb123efc93ae9dede26c985e73"
    ]
  ]
]