[
  "ÙæW‹çÜ\u0017mŽY‚Íš¨tñ",
  [
    [
      "Vale.X64.Flags.upd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Vale.X64.Flags.flag_val_t", "int_inversion",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_intro",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "typing_FStar.Map.domain", "typing_FStar.Map.upd",
        "typing_FStar.Set.complement", "typing_FStar.Set.empty",
        "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "0b37ad8377b771cb5457be60458f2720"
    ],
    [
      "Vale.X64.Flags.of_fun",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
        "data_typing_intro_FStar.Pervasives.Native.None@tok",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Prims.bool",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.X64.Flags.flag_val_t",
        "haseqTm_refine_a29663a141e931174462ff96f2d1bbb5", "int_inversion",
        "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomConstMap",
        "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
        "lemma_FStar.Map.lemma_UpdDomain",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_intro",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
        "lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
        "refinement_kinding_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
        "typing_FStar.Map.const", "typing_FStar.Map.domain",
        "typing_FStar.Map.upd", "typing_FStar.Set.complement",
        "typing_FStar.Set.empty", "typing_FStar.Set.singleton",
        "typing_FStar.Set.union", "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "000117beee9e81ceac18074ffb9e2e12"
    ],
    [
      "Vale.X64.Flags.lemma_upd_eq",
      1,
      1,
      0,
      [
        "@query", "function_token_typing_Vale.X64.Flags.sel",
        "function_token_typing_Vale.X64.Flags.upd",
        "interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
        "interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
      ],
      0,
      "227bd76bc4d1017ecf6af92b32bce864"
    ],
    [
      "Vale.X64.Flags.lemma_upd_ne",
      1,
      1,
      0,
      [
        "@query", "function_token_typing_Vale.X64.Flags.sel",
        "function_token_typing_Vale.X64.Flags.upd",
        "interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
        "interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
      ],
      0,
      "b97b5ecc4a83ba0e9a07178a972be44f"
    ],
    [
      "Vale.X64.Flags.lemma_equal_intro",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.X64.Flags.equal",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Vale.X64.Flags.flag_val_t",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_elim",
        "refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
        "typing_FStar.Map.domain", "typing_FStar.Set.complement",
        "typing_FStar.Set.empty", "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "2897cc772503c1007c16f6dc5cd12be3"
    ],
    [
      "Vale.X64.Flags.lemma_equal_elim",
      1,
      1,
      0,
      [
        "@query", "eq2-interp", "equation_Vale.X64.Flags.equal",
        "equation_Vale.X64.Flags.t"
      ],
      0,
      "716ace1af786f86086135414a7fe653d"
    ]
  ]
]