[ "¯Šï\"OÍ€\\Ær}9\u0002?\u0003s", [ [ "Vale.Def.Words.Seq.two_to_seq_to_two_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq2", "equation_Vale.Def.Words.Seq_s.seq_to_two_LE", "equation_Vale.Def.Words.Seq_s.seqn", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb", "typing_Vale.Def.Words.Seq_s.seq_to_two_LE", "typing_Vale.Def.Words.Seq_s.two_to_seq_LE" ], 0, "479aadefb7ae6f0c646002ecab68de1c" ], [ "Vale.Def.Words.Seq.seq_to_two_to_seq_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words.Seq_s.seq_to_two_LE", "fuel_guarded_inversion_Vale.Def.Words_s.two", "proj_equation_Vale.Def.Words_s.Mktwo_hi", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb", "typing_Vale.Def.Words.Seq_s.two_to_seq_LE" ], 0, "b0e028fe72b1a9c7c0e09cc8da9e0f92" ], [ "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "a6bb30c70c41ce45135836472614fb82" ], [ "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344", "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "int_inversion", "int_typing", "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d", "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", "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_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e1f5e45cb61463bd8d5304890121db69", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34" ], 0, "c459a78f31e5729794c95a9dc41a1c29" ], [ "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "dc565c4a92691a3178065b1cc6f48eb7" ], [ "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344", "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_BE", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_BE", "int_inversion", "int_typing", "interpretation_Tm_abs_2fc6b3ab64c18b145a616e44e8d8d874", "interpretation_Tm_abs_68712397230d19f3062e360c964e25da", "interpretation_Tm_abs_9cd3a42bbbd0f67ce68082a0bbce4cf2", "interpretation_Tm_abs_df2053a244470cdb2ac13b7c0c00e093", "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", "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_lo0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_abd944e669f79e6af0f86cf95ccb27ea", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_Tm_abs_2fc6b3ab64c18b145a616e44e8d8d874", "typing_Tm_abs_68712397230d19f3062e360c964e25da", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_BE" ], 0, "88cffd22fc146ab4b8bbb23f5cf9f8a4" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE", 1, 1, 0, [ "@query" ], 0, "a1774ef13b86231228b9848023cc974e" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344", "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select", "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "int_inversion", "int_typing", "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d", "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", "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_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_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.length", "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "af7a6fb08d616e72c49c4e2b138d66f6" ], [ "Vale.Def.Words.Seq.lemma_fundamental_div_mod_4", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "276c5a89dd9521d8a5ca1e5865c11d50" ], [ "Vale.Def.Words.Seq.four_to_nat_to_four_8", 1, 1, 0, [ "@query" ], 0, "08999125b0190fa3879cb2b4ba60b487" ], [ "Vale.Def.Words.Seq.four_to_nat_to_four_8", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "a08e3646f75d65b478aa506dffa0ac99" ], [ "Vale.Def.Words.Seq.nat_to_four_to_nat", 1, 1, 0, [ "@query" ], 0, "e9281c3dcb6f4a34157b8d26f85ad9e0" ], [ "Vale.Def.Words.Seq.nat_to_four_to_nat", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "49c7b99cd93d5f9c21ca40caa550a248" ], [ "Vale.Def.Words.Seq.four_to_seq_to_four_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "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", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "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_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_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE", "typing_Vale.Def.Words.Seq_s.seq_to_four_LE" ], 0, "89849c375358a3aa177b0f87902d9b1c" ], [ "Vale.Def.Words.Seq.seq_to_four_to_seq_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE" ], 0, "7a0ebdca99b4f7a3295c0b3d518b1f89" ], [ "Vale.Def.Words.Seq.four_to_seq_to_four_BE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_BE", "equation_Vale.Def.Words.Seq_s.seqn", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "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_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_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_Vale.Def.Words.Seq_s.four_to_seq_BE", "typing_Vale.Def.Words.Seq_s.seq_to_four_BE" ], 0, "2013eed0fd72107817dcfff75d540255" ], [ "Vale.Def.Words.Seq.seq_to_four_to_seq_BE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words.Seq_s.seq_to_four_BE", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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", "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1", "typing_Vale.Def.Words.Seq_s.four_to_seq_BE" ], 0, "f72efcce0404c17f7b59e10ee7040ef5" ], [ "Vale.Def.Words.Seq.four_to_seq_LE_is_seq_four_to_seq_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "fuel_guarded_inversion_Vale.Def.Words_s.four", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e" ], 0, "9ec201d7dd5a00a97d31faa3994d39fd" ], [ "Vale.Def.Words.Seq.four_to_seq_LE_is_seq_four_to_seq_LE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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_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_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "aa75cb5ed22e0c42d2fdf2ce25a73fc4" ], [ "Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "equation_Prims.nat", "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.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "kinding_Vale.Def.Words_s.four@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "0bac225869487d97b60052b09861595c" ], [ "Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "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_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "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_init_len", "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_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_Vale.Def.Words.Four_s.four_to_nat", "token_correspondence_Vale.Def.Words.Four_s.nat_to_four", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "c8ddda62e57d78e48e4b0f0caffdfb91" ], [ "Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f", "Vale.Def.Words.Seq_interpretation_Tm_arrow_d99575c656699ec1bf0db12d4bfb9bae", "Vale.Def.Words.Seq_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "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.Def.Words_s.natN", "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.Seq_s.seq_four_to_seq_LE", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5", "interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c", "interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3", "interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac", "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_init_len", "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_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_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b75956299d71331caf39bdc95ee7a81c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_Vale.Def.Words.Four_s.four_to_nat", "token_correspondence_Vale.Def.Words.Four_s.nat_to_four", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Tm_abs_4f03474956a6a2311e7d7bb19e902da5", "typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c", "typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac", "typing_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "8eb0ffb72dba87db380b8dc5b409c863" ], [ "Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "equation_Vale.Def.Words_s.nat8", "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.nat8", "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_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt8.uv_inv", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_FStar.UInt8.uint_to_t", "token_correspondence_FStar.UInt8.v", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8" ], 0, "d3df9a945a0f1606e35ed7c19ffbb7e3" ], [ "Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "b2t_def", "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_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "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_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "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_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_FStar.Seq.Base.index", "token_correspondence_FStar.UInt8.uint_to_t", "token_correspondence_FStar.UInt8.v", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8" ], 0, "e003ba3972a430b58c641f5f55ace939" ], [ "Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_injective", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "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_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt8.t", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8" ], 0, "641b0a02b838e5dec9a605dc0bca03bf" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective", 1, 1, 0, [ "@query" ], 0, "622be686a9101951ff965a638d384c85" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "assumption_Vale.Def.Words_s.four__uu___haseq", "equation_Prims.eqtype", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.hasEq_lemma", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "6334bcf967fa82d9bdff5350fe3456d1" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective_specific", 1, 1, 0, [ "@query" ], 0, "d23bb5d028bab45373ae601f24384f37" ], [ "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective_specific", 2, 1, 0, [ "@query" ], 0, "e3a8eaef8cd500bcb221671bccfad0c6" ], [ "Vale.Def.Words.Seq.four_to_seq_LE_injective", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "assumption_Vale.Def.Words_s.four__uu___haseq", "equation_Prims.eqtype", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "haseqTm_refine_a0cd7d06c5da6444b6b51b319febde8e", "lemma_FStar.Seq.Base.hasEq_lemma", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "73948f85666231700ffb09981fe2f522" ], [ "Vale.Def.Words.Seq.four_to_nat_8_injective", 1, 1, 0, [ "@query" ], 0, "d448ff0ece0c9d0adee25275b64ce46e" ], [ "Vale.Def.Words.Seq.four_to_nat_8_injective", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "assumption_Vale.Def.Words_s.four__uu___haseq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "9597d8582164f7eb4f7086111f678a3f" ], [ "Vale.Def.Words.Seq.nat_to_four_8_injective", 1, 1, 0, [ "@query" ], 0, "2ec6b49f349c5f12678132751d86d6af" ], [ "Vale.Def.Words.Seq.nat_to_four_8_injective", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "assumption_Vale.Def.Words_s.four__uu___haseq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "f2f14a5887f65cb90e7f353176d85748" ], [ "Vale.Def.Words.Seq.append_distributes_seq_to_seq_four_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac" ], 0, "871cb978f53e4d92eeb328b0c9e8aa5f" ], [ "Vale.Def.Words.Seq.append_distributes_seq_to_seq_four_LE", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "int_inversion", "int_typing", "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_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_387c17e1c2128da0ffe38534dd5bf717", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "530bb96f577eb980fac80bc098dd1717" ], [ "Vale.Def.Words.Seq.append_distributes_seq_four_to_seq_LE", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat", "fuel_guarded_inversion_Vale.Def.Words_s.four", "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_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "d6cd150d84955213e2ab7167c26b3bf6" ] ] ]