[ "t9ߵ LWjo", [ [ "Vale.Arch.Types.lemma_nat_to_two32", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "int_typing", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "fb1983705d96200f665def574a89ead6" ], [ "Vale.Arch.Types.lemma_nat_to_two32", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d657313e832f90b9da2597122651ce83" ], 0, "43f4adab77e671cceaac1f75904f58b8" ], [ "Vale.Arch.Types.lemma_BitwiseXorCommutative", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Vale.Def.Types_s.ixor" ], 0, "d3e01002d7c321a37fd49eaf878335f6" ], [ "Vale.Arch.Types.lemma_BitwiseXorWithZero", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Vale.Def.Types_s.ixor" ], 0, "ac9cc32c9e48d2afa83223d7d7c9df47" ], [ "Vale.Arch.Types.lemma_BitwiseXorCancel", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented", "function_token_typing_Prims.bool", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Prims.pow2" ], 0, "330642acf9a26df8ba03c4048446f964" ], [ "Vale.Arch.Types.lemma_BitwiseXorCancel64", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented", "function_token_typing_Prims.bool", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2897f455bd1a2e7bd7f8f1aa6ce63472", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6c6633917f79a67f4eaac4ed70320fc6", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Prims.pow2" ], 0, "18af831949bc726473fe61bec44cd352" ], [ "Vale.Arch.Types.lemma_BitwiseXorAssociative", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.bool", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Vale.Def.Types_s.ixor" ], 0, "529223a10504d866f0b1ce5c68f8a408" ], [ "Vale.Arch.Types.xor_lemmas", 1, 1, 0, [ "@query" ], 0, "4cc0f556896f7c98e8adb1fc7bc2bd76" ], [ "Vale.Arch.Types.lemma_quad32_xor", 1, 3, 3, [ "@MaxIFuel_assumption", "@query", "data_elim_Vale.Def.Words_s.Mkfour", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Types_s.quad32_xor_def", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Types_s.quad32_xor", "token_correspondence_Vale.Def.Types_s.quad32_xor_def" ], 0, "9cf6bdde17cac31ee1cfbe3f5849fa04" ], [ "Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2", "equation_Prims.nat", "equation_Vale.Def.Types_s.nat32_to_be_bytes", "equation_Vale.Def.Types_s.reverse_bytes_nat32_def", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.reverse_seq", "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_Vale.Lib.Seqs.reverse_reverse_seq", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa", "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c", "typing_Vale.Def.Types_s.nat32_to_be_bytes" ], 0, "3da35453c813defa1e9c9ea7da8121fe" ], [ "Vale.Arch.Types.lemma_reverse_bytes_quad32", 1, 3, 3, [ "@MaxIFuel_assumption", "@query", "data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_reverse", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion", "lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "636db239996cfac45a68defa8b218baf" ], [ "Vale.Arch.Types.lemma_reverse_bytes_nat32", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.be_bytes_to_nat32", "equation_Vale.Def.Types_s.nat32_to_be_bytes", "equation_Vale.Def.Types_s.reverse_bytes_nat32_def", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_BE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.reverse_seq", "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c", "lemma_FStar.Seq.Base.init_index_", "lemma_Vale.Def.Words.Seq.nat_to_four_to_nat", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_a", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa", "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def", "typing_FStar.Seq.Base.length", "typing_Prims.pow2", "typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c", "typing_Vale.Def.Types_s.nat32_to_be_bytes", "typing_Vale.Def.Words.Seq_s.four_to_seq_BE", "typing_Vale.Def.Words.Seq_s.seq_to_four_BE", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3" ], 0, "c24ca70cd307cdab0e0a51be280ad829" ], [ "Vale.Arch.Types.lemma_reverse_bytes_quad32_zero", 1, 1, 0, [ "@query", "equation_Vale.Def.Words.Four_s.four_reverse", "equation_Vale.Def.Words_s.nat32", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1" ], 0, "1e925d005ee33a86776323d3d1b39fbe" ], [ "Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_seq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_afc033f4783947c3d425ff758d5e540a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Types_s.reverse_bytes_nat32_seq" ], 0, "8fb24e49cd7fedc0d7bac998bbdba893" ], [ "Vale.Arch.Types.lemma_insert_nat64_properties", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.insert_nat64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Four_s.two_two_to_four", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words.Two_s.two_insert", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Types_s.insert_nat64", "int_inversion", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Def.Types_s.insert_nat64_def" ], 0, "7fb5da10c4230811c0430d733288597d" ], [ "Vale.Arch.Types.lemma_insert_nat64_nat32s", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.insert_nat64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Four_s.two_two_to_four", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words.Two_s.two_insert", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Types_s.insert_nat64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Two.nat_to_two_to_nat", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Def.Types_s.insert_nat64_def" ], 0, "9626a40ac40e62d80314577175a7ac67" ], [ "Vale.Arch.Types.lo64_reveal", 1, 1, 0, [ "@query" ], 0, "9e5d3e783382bed715746569e66c6443" ], [ "Vale.Arch.Types.hi64_reveal", 1, 1, 0, [ "@query" ], 0, "9ca8d9818bacd2a6ec770889773bacfd" ], [ "Vale.Arch.Types.lemma_lo64_properties", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Arch.Types.lo64", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Vale.Arch.Types.lo64_def" ], 0, "0bff6884812062e4bda344036dbbc59a" ], [ "Vale.Arch.Types.lemma_hi64_properties", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Arch.Types.hi64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Arch.Types.hi64", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Vale.Arch.Types.hi64_def" ], 0, "0f9e93e3842348de888eb2537fed3207" ], [ "Vale.Arch.Types.lemma_reverse_bytes_nat64_32", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.reverse_bytes_nat64_def", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Two.nat_to_two_to_nat", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat64_def", "typing_Prims.pow2" ], 0, "5a8b745d4d789f72c8ed6f1ee44a9412" ], [ "Vale.Arch.Types.lemma_reverse_bytes_quad32_64", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.Types.hi64_def", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.reverse_bytes_nat64_def", "equation_Vale.Def.Words.Four_s.four_reverse", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Arch.Types.hi64", "function_token_typing_Vale.Arch.Types.lo64", "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Two.nat_to_two_to_nat", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.Arch.Types.hi64_def", "token_correspondence_Vale.Arch.Types.lo64_def", "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat64_def", "typing_Prims.pow2" ], 0, "a40f060191025e393e2d4a00c56daa95" ], [ "Vale.Arch.Types.lemma_equality_check_helper", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "data_elim_Vale.Def.Words_s.Mkfour", "data_elim_Vale.Def.Words_s.Mktwo", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.Types.hi64_def", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.Def.Words_s.two", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.Types.hi64", "function_token_typing_Vale.Arch.Types.lo64", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.two@tok", "l_quant_interp_170d6477ea866701a90ae6e76923559c", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Arch.Types.hi64_def", "token_correspondence_Vale.Arch.Types.lo64_def", "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64", "typing_Vale.Def.Words.Four_s.four_to_two_two", "typing_Vale.Def.Words.Two_s.two_select", "typing_Vale.Def.Words_s.__proj__Mktwo__item__lo", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "e7fc9b792de99d9b82145402bed669a6" ], [ "Vale.Arch.Types.lemma_equality_check_helper_2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion", "primitive_Prims.op_Equality", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "1692da002c0cbcc9bedc560faea11516" ], [ "Vale.Arch.Types.push_pop_xmm", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "data_elim_Vale.Def.Words_s.Mkfour", "data_elim_Vale.Def.Words_s.Mktwo", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.Types.hi64_def", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.insert_nat64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Four_s.two_two_to_four", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words.Two_s.two_insert", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.Def.Words_s.two", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.Types.hi64", "function_token_typing_Vale.Arch.Types.lo64", "function_token_typing_Vale.Def.Types_s.insert_nat64", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.two@tok", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Two.nat_to_two_to_nat", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.Arch.Types.hi64_def", "token_correspondence_Vale.Arch.Types.lo64_def", "token_correspondence_Vale.Def.Types_s.insert_nat64_def", "typing_Prims.pow2", "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64", "typing_Vale.Def.Words.Four_s.four_to_two_two", "typing_Vale.Def.Words.Two_s.nat_to_two", "typing_Vale.Def.Words.Two_s.two_insert", "typing_Vale.Def.Words.Two_s.two_select", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "f8856b8e2b895519732d8c19cf683ecf" ], [ "Vale.Arch.Types.lemma_insrq_extrq_relations", 1, 3, 3, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat", "equation_Vale.Arch.Types.hi64_def", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.insert_nat64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Four_s.two_two_to_four", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words.Two_s.two_insert", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Arch.Types.hi64", "function_token_typing_Vale.Arch.Types.lo64", "function_token_typing_Vale.Arch.Types.lo64_def", "function_token_typing_Vale.Def.Types_s.insert_nat64", "function_token_typing_Vale.Def.Types_s.insert_nat64_def", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Arch.Types.lemma_insert_nat64_properties", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Arch.Types.hi64_def", "token_correspondence_Vale.Def.Types_s.insert_nat64_def", "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64_def", "typing_Vale.Def.Types_s.insert_nat64" ], 0, "5f7e5c088d7205bf91cd8900e91d0a7f" ], [ "Vale.Arch.Types.le_bytes_to_nat64_to_bytes", 1, 3, 3, [ "@query" ], 0, "bed92e6a9113f48db838bf831feb0fd7" ], [ "Vale.Arch.Types.le_bytes_to_nat64_to_bytes", 2, 3, 3, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "data_typing_intro_Vale.Def.Words_s.Mktwo@tok", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.le_bytes_to_nat64_def", "equation_Vale.Def.Types_s.le_nat64_to_bytes_def", "equation_Vale.Def.Words.Seq_s.seq2", "equation_Vale.Def.Words.Seq_s.seq_to_two_LE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words.Two_s.nat_to_two", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64", "function_token_typing_Vale.Def.Types_s.le_nat64_to_bytes", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE", "lemma_Vale.Def.Words.Two.two_to_nat_to_two", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb", "token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def", "token_correspondence_Vale.Def.Types_s.le_nat64_to_bytes_def", "typing_Prims.pow2", "typing_Vale.Def.Types_s.le_nat64_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "typing_Vale.Def.Words.Seq_s.two_to_seq_LE", "typing_Vale.Def.Words_s.natN" ], 0, "f7682e78fd98e941de6128fe8abb7c6c" ], [ "Vale.Arch.Types.le_nat64_to_bytes_to_nat64", 1, 3, 3, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619" ], 0, "4f95b96cdea7a781b37c7574da2a79b8" ], [ "Vale.Arch.Types.le_nat64_to_bytes_to_nat64", 2, 3, 3, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_bytes_to_nat64_def", "equation_Vale.Def.Types_s.le_nat64_to_bytes_def", "equation_Vale.Def.Words.Seq_s.seq2", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words.Seq_s.seq_to_two_LE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64", "function_token_typing_Vale.Def.Types_s.le_nat64_to_bytes", "function_token_typing_Vale.Def.Words.Four_s.four_to_nat", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE", "lemma_Vale.Def.Words.Seq.two_to_seq_to_two_LE", "lemma_Vale.Def.Words.Two.nat_to_two_to_nat", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def", "token_correspondence_Vale.Def.Types_s.le_nat64_to_bytes_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "6502718de273263f80a6f0e28969f4a6" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_empty", 1, 3, 3, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "73ae1fefa9da271b90c7df769eea14af" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_empty", 2, 3, 3, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "lemma_FStar.Seq.Base.lemma_init_len", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "05f99b42f516c9e6fd237daeb0c7af59" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad", 1, 0, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "d2d84c00c4d6d7c676f9d1aabd6919f4" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8", "lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6517d0c8716e159a40f752c583d756c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_a65d20b338845083fa7a7ab8518b0f7b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Prims.pow2", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "222641f87bd8fdf18f6d6c16efced7aa" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes", 1, 0, 0, [ "@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "projection_inverse_BoxInt_proj_0" ], 0, "9dc831a9121f84667f205e0a3e7d089f" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8", "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "9018511b88040b0bc4a6b7b2547fb357" ], [ "Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0" ], 0, "c6c61bcc6212c8717b11330cd40b9692" ], [ "Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "function_token_typing_Vale.Def.Words.Four_s.four_to_nat", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE", "lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "typing_Vale.Lib.Seqs_s.seq_map" ], 0, "cec1747aa69e04fbb5461ad08776d552" ], [ "Vale.Arch.Types.le_quad32_to_bytes_to_quad32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc" ], 0, "2bceb95cf1083508a72007e8827e04f2" ], [ "Vale.Arch.Types.le_quad32_to_bytes_to_quad32", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_bytes_to_quad32_def", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32", "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.nat_to_four_to_nat", "lemma_Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca" ], 0, "987608224239d2613e7d79d58b5ae3ed" ], [ "Vale.Arch.Types.le_seq_quad32_to_bytes_of_singleton", 1, 0, 0, [ "@query", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def" ], 0, "adc13b64ccc4766927606c184c803a0b" ], [ "Vale.Arch.Types.le_quad32_to_bytes_injective", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing", "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43", "lemma_FStar.Seq.Base.hasEq_lemma", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Equality", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE" ], 0, "4315a016e4cae5c5d9d26d5d8134e068" ], [ "Vale.Arch.Types.le_quad32_to_bytes_injective_specific", 1, 0, 0, [ "@query" ], 0, "5533c3a6e8fa6060be7915ce672aaea1" ], [ "Vale.Arch.Types.le_seq_quad32_to_bytes_injective", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "4758f46416dfce11f24008a83fdabe84" ], [ "Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e" ], 0, "d82f5038af11f6cf58c2e2bd307a440b" ], [ "Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Arch.Types_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344", "equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words.Seq_s.seqn", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "int_inversion", "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_create", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "typing_Vale.Def.Words.Seq_s.seq_to_four_LE" ], 0, "fc0aa1488c993c78e7b433da6c3e435e" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc" ], 0, "df5bc17830a18a24713f5c320a9d653b" ], [ "Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.le_bytes_to_quad32_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca" ], 0, "5465acbc89ad5fa514725c58ae195298" ], [ "Vale.Arch.Types.le_bytes_to_quad32_to_bytes", 1, 0, 0, [ "@query" ], 0, "d37d0c0b5a6ad69e3ab497142c5e5eeb" ], [ "Vale.Arch.Types.le_bytes_to_quad32_to_bytes", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.Seq.Base.create" ], 0, "d9db7410f88a00eefbe3a17312eaaac5" ], [ "Vale.Arch.Types.be_quad32_to_bytes", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_029dc40463b676c106e396144db4f6f0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.four_to_seq_BE" ], 0, "547a2774a101651319663f2b6f754adb" ], [ "Vale.Arch.Types.be_bytes_to_quad32_to_bytes", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.Types.be_quad32_to_bytes", "equation_Vale.Def.Words.Seq_s.seq16", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat8", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "typing_Vale.Arch.Types.be_quad32_to_bytes" ], 0, "abea357ef04a892f7ec4c46ad0212b48" ], [ "Vale.Arch.Types.be_bytes_to_quad32_to_bytes", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Arch.Types.be_quad32_to_bytes", "equation_Vale.Def.Types_s.be_bytes_to_quad32_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq16", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_BE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Types_s.be_bytes_to_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8", "lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_Vale.Def.Types_s.be_bytes_to_quad32_def", "token_correspondence_Vale.Def.Words.Four_s.four_to_nat", "token_correspondence_Vale.Def.Words.Four_s.nat_to_four", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Arch.Types.be_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.four_to_seq_BE", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1" ], 0, "cbd1d3899b2f92b6cc386b68972d8214" ], [ "Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Types_s.reverse_bytes_nat32", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Words_s.nat32", "lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_hi3", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_Vale.Def.Words_s.Mkfour_hi2", "projection_inverse_Vale.Def.Words_s.Mkfour_hi3", "projection_inverse_Vale.Def.Words_s.Mkfour_lo0", "projection_inverse_Vale.Def.Words_s.Mkfour_lo1", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1" ], 0, "a3448a193878ff5473b62cca2fde6447" ], [ "Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32_seq", 1, 0, 0, [ "@query", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq", "lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32" ], 0, "aa59bb311573d9bb3962da1cb64713be" ], [ "Vale.Arch.Types.lemma_reverse_reverse_bytes_quad32_seq", 1, 0, 0, [ "@query", "equation_Vale.Arch.Types.reverse_bytes_quad32_seq", "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32" ], 0, "15df6c015937df8171cba6e53d164eb9" ], [ "Vale.Arch.Types.lemma_le_seq_quad32_to_bytes_length", 1, 0, 0, [ "@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length" ], 0, "5c85c20e9732171ff5da416b12bc9bf9" ], [ "Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "kinding_Vale.Def.Words_s.four@tok", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc", "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "02658b41be590263b3857fc286646d05" ], [ "Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Arch.Types_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "equation_Prims.nat", "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "int_inversion", "int_typing", "interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b", "interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_21ef7f5ab4b8827eb094439f3acdea47", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f0e12f26859fbf7671f3fb2fdbdad52a", "typing_FStar.Seq.Base.length", "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "a414ffc704ae47e2f9bbd40b045b30bb" ], [ "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_3234ac1d1198c8b724cbaa98bc293002", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee" ], 0, "742515267d682283a035e1397a6753ef" ], [ "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_3234ac1d1198c8b724cbaa98bc293002", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "6ed1a0a35f7ae0de7b4a3f82de2087dc" ], [ "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee" ], 0, "6b97152e862313490f9f266dfc59341f" ], [ "Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "kinding_Vale.Def.Words_s.four@tok", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee", "typing_FStar.Seq.Base.length" ], 0, "99b52b701d6da14dc298e2e932ab8864" ], [ "Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "equation_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Def.Words_s.nat8", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0" ], 0, "a1bdade6cb395072274aec323d65ee4e" ], [ "Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.pos", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "444770a5996cac092e867c273da949a5" ], [ "Vale.Arch.Types.append_distributes_le_seq_quad32_to_bytes", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "int_typing", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def" ], 0, "c64c4f0f83cd377b426484466d1bef81" ] ] ]