[ "K/PΝӻ", [ [ "Vale.X64.Decls.va_if", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "projection_inverse_BoxBool_proj_0" ], 0, "c24b7720afe03b68acdd6c761894d2b2" ], [ "Vale.X64.Decls.total_thunk_if", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "projection_inverse_BoxBool_proj_0" ], 0, "b545432ceb699dd5c014c4a25b16493b" ], [ "Vale.X64.Decls.va_tl", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_1c9655c30deebdd07e36fb0790c48d70" ], 0, "d1f9861a362c758d1328dfb7b9097b4d" ], [ "Vale.X64.Decls.reg_operand", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9ef8214062f1b33af206dcc0a829bce1" ], [ "Vale.X64.Decls.va_operand_reg_opr64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a543eb44231ab30b4c7d43a4c2356b36" ], [ "Vale.X64.Decls.cmp_operand", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "aa4650759836395889dd360553f44ca8" ], [ "Vale.X64.Decls.get_reg", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "278995ede1f7063246e5a988d396a6d0" ], [ "Vale.X64.Decls.valid_operand", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d689c8c655d7006623eb0d48086d3b1a" ], [ "Vale.X64.Decls.valid_operand", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5c67a7642f382695b901a8f84c8253ed" ], [ "Vale.X64.Decls.valid_operand", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "431045989ced5dde72e7fe4728b3651c" ], [ "Vale.X64.Decls.valid_operand", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0713618f5cecfcec19ca78db65a09200" ], [ "Vale.X64.Decls.valid_operand128", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "575df1a24342eb0d99d22197f9a89731" ], [ "Vale.X64.Decls.valid_operand128", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "717b929128a3911922f4ec245c71beae" ], [ "Vale.X64.Decls.va_op_opr64_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ced65eba04977c77ba9065225cb91055" ], [ "Vale.X64.Decls.va_op_reg64_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5913a47a3ebe0e87e3ba341766efcd5a" ], [ "Vale.X64.Decls.va_op_opr128_xmm", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0bfa0fe7efc3533d5b11dbc1ead59e2e" ], [ "Vale.X64.Decls.va_const_opr64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "da05e86eb051693253673cbe12906431" ], [ "Vale.X64.Decls.va_const_shift_amt64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "b1a226650055ec2b3176fe25a71f91e0" ], [ "Vale.X64.Decls.va_op_shift_amt64_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ff40fa0a345d445abfd82d92b91cf706" ], [ "Vale.X64.Decls.va_op_cmp_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OMem", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "77444da956913cf14f07277135bdb245" ], [ "Vale.X64.Decls.va_const_cmp", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.X64.Machine_s.OConst", "disc_equation_Vale.X64.Machine_s.OMem", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9d014e8174686430a2381a33c1968f55" ], [ "Vale.X64.Decls.va_coerce_reg64_opr64_to_cmp", 1, 1, 0, [ "@query", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OReg", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.reg_64", "projection_inverse_BoxBool_proj_0" ], 0, "b81064bfa3babac0d3be70bd35d0349e" ], [ "Vale.X64.Decls.va_coerce_opr64_to_cmp", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c30ced905d3a0e5bd063a904f78829fb" ], [ "Vale.X64.Decls.va_op_reg_opr64_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OReg", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Machine_s.OReg_r", "projection_inverse_Vale.X64.Machine_s.OReg_tc", "projection_inverse_Vale.X64.Machine_s.OReg_tr", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9df0e0eb7ee024ffec6817d2231f2c1b" ], [ "Vale.X64.Decls.va_op_dst_opr64_reg64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "cb9f61a60a7297b30cbdf57b4f67a3c5" ], [ "Vale.X64.Decls.va_coerce_xmm_to_opr128", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "b1fe703a99f45b52d76f235516dc74d5" ], [ "Vale.X64.Decls.va_opr_code_Mem64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d" ], 0, "ad4aff9e82fe52a6146cc0ab8faef8cc" ], [ "Vale.X64.Decls.va_opr_code_Mem64", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "8cb0b07d2a7a0ea87e079d14242db49d" ], [ "Vale.X64.Decls.va_opr_code_Mem64", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ce99fc792f0d8ef5e331d9730bc21e0e" ], [ "Vale.X64.Decls.va_opr_code_Mem64", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "3ea73c6573359b49b7b42611879aa5f9" ], [ "Vale.X64.Decls.va_opr_code_Mem64", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "44e5920d12af95c2199a704a0adb4a0f" ], [ "Vale.X64.Decls.va_opr_code_Stack", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d" ], 0, "9ebf31a97d7fbf48752ebecec97c5111" ], [ "Vale.X64.Decls.va_opr_code_Stack", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "cfb13f849762548bd4bc08807e994ba1" ], [ "Vale.X64.Decls.va_opr_code_Stack", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "624fa9b19fe65324f1cc711fa5276f34" ], [ "Vale.X64.Decls.va_opr_code_Stack", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "994d6ae5ad87e3aea35b5244b5b7c36f" ], [ "Vale.X64.Decls.va_opr_code_Stack", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7f389e20f6e13e95032da70678d6572d" ], [ "Vale.X64.Decls.va_opr_code_Mem128", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d" ], 0, "b07c65f932f2075be901607c6692a2d3" ], [ "Vale.X64.Decls.va_opr_code_Mem128", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0d45bed3e5a545de43f61606df00f8bb" ], [ "Vale.X64.Decls.va_opr_code_Mem128", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "db07eaed6cbd6eab568ff4c72852d18e" ], [ "Vale.X64.Decls.va_is_dst_opr64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ff98d228290ed94f12d876a59231ac9f" ], [ "Vale.X64.Decls.va_is_dst_opr64", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "24f9d80e8831b16b905b231810534ba8" ], [ "Vale.X64.Decls.va_is_dst_opr64", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "2533171b24bb31aaa4c02a7fec97b9c5" ], [ "Vale.X64.Decls.va_is_src_reg_opr64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "31576fb3ed58919200ac9d103e0f3a21" ], [ "Vale.X64.Decls.va_is_dst_reg_opr64", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "25fd76bcd7f9116168d239f9861f3d26" ], [ "Vale.X64.Decls.update_operand", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.X64.Machine_s.OConst", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.X64.Machine_s.operand" ], 0, "38f213bb3fd42874715f0e32d1db73ed" ], [ "Vale.X64.Decls.update_operand", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ea45ae5f65139f5a63196d5bc4e5fbf9" ], [ "Vale.X64.Decls.update_operand", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "fb0f6ac6154c2994fb539196e6bfbec1" ], [ "Vale.X64.Decls.update_operand", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "49c9cb85fba5a9cd4365e58af4d07adf" ], [ "Vale.X64.Decls.update_operand", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "251e68bdc5171fde0025124f99215971" ], [ "Vale.X64.Decls.update_operand", 6, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "df3901cb95430842d2db527baf427566" ], [ "Vale.X64.Decls.update_operand", 7, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "69a31add82a87756abd1134a53bc7138" ], [ "Vale.X64.Decls.update_operand", 8, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "2b1dea3b6b9d35d9ccd7b8fe9b3e7eca" ], [ "Vale.X64.Decls.update_operand", 9, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "2cc6432504576634401515814775d17c" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.X64.Machine_s.OConst", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.X64.Machine_s.operand" ], 0, "3735243b87118940c653add07d9b6953" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f82bc99e397dc0419d01af5f82037fbe" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c790634204fa902a45eadfec602b1144" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ce5eb7a271ba0fbeaab154272ee0e543" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "94ef4c9d27421ad16169b6e81666c828" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 6, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "60a376c5fbd723e041040058ad6446f3" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 7, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9044c11bae6c55bb10302d8a745e1363" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 8, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7a71c8eb6aa5f7756c0c1e57d1fae1c9" ], [ "Vale.X64.Decls.va_upd_operand_dst_opr64", 9, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e5ed45323291c4ed332d54ff5b5bb7f0" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.X64.Machine_s.OConst", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OReg", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.X64.Machine_s.operand" ], 0, "1dcffcde1b8709912783cb187c625d08" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c81ca43499fd7de44c5cd3cc06138af7" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "1615cf9460953d51387fce34d01a2c7c" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "35bcc8054cb21a4dab791d65459f231b" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5b8b21d538160deb3426b2aadfc813ed" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 6, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "cfa8ceebaa661a1bbd8a650f92e07f85" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 7, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "af8d655a0c70e5445b76a5c7d89c98bf" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 8, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "764807b02d3fb219762597891fe78ef1" ], [ "Vale.X64.Decls.va_upd_operand_reg_opr64", 9, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "203db8e475db6e3409e633c19cda914f" ], [ "Vale.X64.Decls.va_lemma_upd_update", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.X64.Machine_s.OReg", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_upd_operand_dst_opr64", "equation_Vale.X64.Decls.va_upd_operand_reg_opr64", "equation_Vale.X64.Decls.va_upd_operand_xmm", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "fuel_guarded_inversion_Vale.X64.State.vale_state", "projection_inverse_BoxBool_proj_0" ], 0, "32bd71206ffa0d5e1c22f998fe3ba80c" ], [ "Vale.X64.Decls.va_cmp_eq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "eda1b16e1664eab123dbc809a72521c0" ], [ "Vale.X64.Decls.va_cmp_ne", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a4a5f5b57b328b350437c84ff4cbbfd4" ], [ "Vale.X64.Decls.va_cmp_le", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "df31de5c4eca0eba070144c313109797" ], [ "Vale.X64.Decls.va_cmp_ge", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f2ee8ed3cbcfd85b4231a8365616cd9d" ], [ "Vale.X64.Decls.va_cmp_lt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d85556d64e793076df1c7ba226dbf168" ], [ "Vale.X64.Decls.va_cmp_gt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "89d3f3e13ab245d4bb6b67e0d6224a56" ], [ "Vale.X64.Decls.buffers_readable", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_2ba196b19be26fed8bbff92956a16ea9_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok", "equation_Vale.X64.Memory.buffer64", "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons" ], 0, "91f5c2fe4fca0c15c5c86713ed5c81ab" ], [ "Vale.X64.Decls.loc_locs_disjoint_rec128", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_b6f06d207926310c35b5daa4508dea69_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, "f7c44c8bd9b98376adcc57daeb8d39e8" ], [ "Vale.X64.Decls.lemma_cmp_eq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d916f490e6138a16c0615cf492b211e2" ], [ "Vale.X64.Decls.lemma_cmp_ne", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "fab2b04c8fe6aee0e6de1c2935eb230d" ], [ "Vale.X64.Decls.lemma_cmp_le", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "bc61fd9dca2daaaad813e8b2f1801658" ], [ "Vale.X64.Decls.lemma_cmp_ge", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ef1ab460de7016fc74c827883e5b7ec1" ], [ "Vale.X64.Decls.lemma_cmp_lt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "8636491b83fdf21b775b5daa512ad96b" ], [ "Vale.X64.Decls.lemma_cmp_gt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ea117d77aeebc8cb65ee8b7aa411e947" ], [ "Vale.X64.Decls.lemma_valid_cmp_eq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c77f42b8bfa36e634b1f1d9a067258b7" ], [ "Vale.X64.Decls.lemma_valid_cmp_ne", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "1e6eb55bd4f0f9d7431ac8a1db044a42" ], [ "Vale.X64.Decls.lemma_valid_cmp_le", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "561dafcf1a81f911ae0f930263982ab2" ], [ "Vale.X64.Decls.lemma_valid_cmp_ge", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d6a6ca943aab858de44409b66d3d8f88" ], [ "Vale.X64.Decls.lemma_valid_cmp_lt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7381c26d85253f4f8948099060359345" ], [ "Vale.X64.Decls.lemma_valid_cmp_gt", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5857db89ea7ee29ed9af29b976f8ac9e" ], [ "Vale.X64.Decls.va_lemma_merge_total", 1, 1, 0, [ "@query" ], 0, "1f88ba575b45ba43ac7581520d5b3b03" ], [ "Vale.X64.Decls.va_lemma_whileMerge_total", 1, 1, 0, [ "@query" ], 0, "a23f7bf34fa55a2a00a42d93e79c5112" ], [ "Vale.X64.Decls.max_one_mem", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0dc253e5fd7d9e315efe072a00fd87c2" ], [ "Vale.X64.Decls.max_one_mem", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e7342aa29cc35d8d24252cdf9dda15f3" ], [ "Vale.X64.Decls.max_one_mem", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "6d9424ad2266e0fb144f7baf5812bfcb" ], [ "Vale.X64.Decls.max_one_mem", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e4377cbe386017623186c4eabc190749" ], [ "Vale.X64.Decls.max_one_mem", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "643d6685ae7339ac14ef6649b3a05f43" ], [ "Vale.X64.Decls.max_one_mem", 6, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d7fcb91e42b359c7339f305d7244d456" ], [ "Vale.X64.Decls.max_one_mem", 7, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "16f27ee4438d4f5fb34ccc25a0e63379" ], [ "Vale.X64.Decls.max_one_mem", 8, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ab415b2a9478ea25afbd76a22b0dc11e" ], [ "Vale.X64.Decls.max_one_mem", 9, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d14134b3674604ec2d571b792c75ac4d" ], [ "Vale.X64.Decls.max_one_mem", 10, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "bb3124badce3ea75503092428a400ec8" ], [ "Vale.X64.Decls.max_one_mem", 11, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "353ea3f5727fe7516ac2b2ea3cf12cfb" ], [ "Vale.X64.Decls.max_one_mem", 12, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e48361977b7271da3ed09572535a6b23" ], [ "Vale.X64.Decls.max_one_mem", 13, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "63343574c7d5420f0dfdbca5165bae8b" ], [ "Vale.X64.Decls.max_one_mem", 14, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9d649c42d425155308252508d94475fa" ], [ "Vale.X64.Decls.max_one_mem", 15, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "02e9feae71e5e31a2f37ec3cd1fe5a0d" ], [ "Vale.X64.Decls.max_one_mem", 16, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c37a6da2b58815cda5d94c7a68a90333" ], [ "Vale.X64.Decls.max_one_mem", 17, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7f731fcb2ec7b47df020b80d168c8416" ] ] ]