LU001F

lucas_choose_prefix_extend

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Beta-prefix extension and relational binomial totality append the exact coefficient for the next two decoded source entries.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall qb qc db dc z t l. (forall lmd_choose_index_choose_before. (exists lmd_gap_choose_before_bound. lmd_gap_choose_before_bound + S (lmd_choose_index_choose_before) = (l)) -> exists lmd_choose_upper_choose_before lmd_choose_lower_choose_before lmd_choose_value_choose_before. ((((exists ff_h_lmd_choose_before_upper. ff_h_lmd_choose_before_upper + S (lmd_choose_upper_choose_before) = S ((S (lmd_choose_index_choose_before)) * qc)) /\ exists ff_q_lmd_choose_before_upper. qb = ff_q_lmd_choose_before_upper * S ((S (lmd_choose_index_choose_before)) * qc) + (lmd_choose_upper_choose_before))) /\ ((((exists ff_h_lmd_choose_before_lower. ff_h_lmd_choose_before_lower + S (lmd_choose_lower_choose_before) = S ((S (lmd_choose_index_choose_before)) * dc)) /\ exists ff_q_lmd_choose_before_lower. db = ff_q_lmd_choose_before_lower * S ((S (lmd_choose_index_choose_before)) * dc) + (lmd_choose_lower_choose_before))) /\ ((((exists ff_h_lmd_choose_before_result. ff_h_lmd_choose_before_result + S (lmd_choose_value_choose_before) = S ((S (lmd_choose_index_choose_before)) * t)) /\ exists ff_q_lmd_choose_before_result. z = ff_q_lmd_choose_before_result * S ((S (lmd_choose_index_choose_before)) * t) + (lmd_choose_value_choose_before))) /\ (((exists bcf_lt_gap_lmd_choose_before_choose_out_of_range. bcf_lt_gap_lmd_choose_before_choose_out_of_range + S (lmd_choose_upper_choose_before) = lmd_choose_lower_choose_before) /\ lmd_choose_value_choose_before = 0) \/ ((exists bcf_le_gap_lmd_choose_before_choose_in_range. bcf_le_gap_lmd_choose_before_choose_in_range + (lmd_choose_lower_choose_before) = lmd_choose_upper_choose_before) /\ (exists bcf_row_code_code_lmd_choose_before_choose bcf_row_code_scale_lmd_choose_before_choose bcf_row_scale_code_lmd_choose_before_choose bcf_row_scale_scale_lmd_choose_before_choose bcf_row_code_lmd_choose_before_choose bcf_row_scale_lmd_choose_before_choose. ((forall bcf_row_index_lmd_choose_before_choose_table. (exists bcf_lt_gap_lmd_choose_before_choose_table_row_bound. bcf_lt_gap_lmd_choose_before_choose_table_row_bound + S (bcf_row_index_lmd_choose_before_choose_table) = S (lmd_choose_upper_choose_before)) -> exists bcf_row_code_lmd_choose_before_choose_table bcf_row_scale_lmd_choose_before_choose_table. ((((exists bcf_height_lmd_choose_before_choose_table_decoded_row_code. bcf_height_lmd_choose_before_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_before_choose_table) = S ((S (bcf_row_index_lmd_choose_before_choose_table)) * bcf_row_code_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_before_choose_table)) * bcf_row_code_scale_lmd_choose_before_choose) + (bcf_row_code_lmd_choose_before_choose_table))) /\ ((((exists bcf_height_lmd_choose_before_choose_table_decoded_row_scale. bcf_height_lmd_choose_before_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_before_choose_table) = S ((S (bcf_row_index_lmd_choose_before_choose_table)) * bcf_row_scale_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_before_choose_table)) * bcf_row_scale_scale_lmd_choose_before_choose) + (bcf_row_scale_lmd_choose_before_choose_table))) /\ ((bcf_row_index_lmd_choose_before_choose_table = 0 /\ (forall bcf_index_lmd_choose_before_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_before_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_before_choose_table_zero_row_bound + S (bcf_index_lmd_choose_before_choose_table_zero_row) = S (lmd_choose_upper_choose_before)) -> exists bcf_value_lmd_choose_before_choose_table_zero_row. ((((exists bcf_height_lmd_choose_before_choose_table_zero_row_entry. bcf_height_lmd_choose_before_choose_table_zero_row_entry + S (bcf_value_lmd_choose_before_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_before_choose_table_zero_row)) * bcf_row_scale_lmd_choose_before_choose_table)) /\ exists bcf_quotient_lmd_choose_before_choose_table_zero_row_entry. bcf_row_code_lmd_choose_before_choose_table = bcf_quotient_lmd_choose_before_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_before_choose_table_zero_row)) * bcf_row_scale_lmd_choose_before_choose_table) + (bcf_value_lmd_choose_before_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_before_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_before_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_before_choose_table_zero_row. bcf_index_lmd_choose_before_choose_table_zero_row = S bcf_predecessor_lmd_choose_before_choose_table_zero_row /\ bcf_value_lmd_choose_before_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_before_choose_table bcf_previous_code_lmd_choose_before_choose_table bcf_previous_scale_lmd_choose_before_choose_table. bcf_row_index_lmd_choose_before_choose_table = S bcf_predecessor_lmd_choose_before_choose_table /\ ((((exists bcf_height_lmd_choose_before_choose_table_decoded_previous_code. bcf_height_lmd_choose_before_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_before_choose_table) = S ((S (bcf_predecessor_lmd_choose_before_choose_table)) * bcf_row_code_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_before_choose_table)) * bcf_row_code_scale_lmd_choose_before_choose) + (bcf_previous_code_lmd_choose_before_choose_table))) /\ ((((exists bcf_height_lmd_choose_before_choose_table_decoded_previous_scale. bcf_height_lmd_choose_before_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_before_choose_table) = S ((S (bcf_predecessor_lmd_choose_before_choose_table)) * bcf_row_scale_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_before_choose_table)) * bcf_row_scale_scale_lmd_choose_before_choose) + (bcf_previous_scale_lmd_choose_before_choose_table))) /\ (forall bcf_index_lmd_choose_before_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_before_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_before_choose_table_row_step_bound + S (bcf_index_lmd_choose_before_choose_table_row_step) = S (lmd_choose_upper_choose_before)) -> exists bcf_value_lmd_choose_before_choose_table_row_step. ((((exists bcf_height_lmd_choose_before_choose_table_row_step_entry. bcf_height_lmd_choose_before_choose_table_row_step_entry + S (bcf_value_lmd_choose_before_choose_table_row_step) = S ((S (bcf_index_lmd_choose_before_choose_table_row_step)) * bcf_row_scale_lmd_choose_before_choose_table)) /\ exists bcf_quotient_lmd_choose_before_choose_table_row_step_entry. bcf_row_code_lmd_choose_before_choose_table = bcf_quotient_lmd_choose_before_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_before_choose_table_row_step)) * bcf_row_scale_lmd_choose_before_choose_table) + (bcf_value_lmd_choose_before_choose_table_row_step))) /\ ((bcf_index_lmd_choose_before_choose_table_row_step = 0 /\ bcf_value_lmd_choose_before_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_before_choose_table_row_step bcf_left_lmd_choose_before_choose_table_row_step bcf_right_lmd_choose_before_choose_table_row_step. bcf_index_lmd_choose_before_choose_table_row_step = S bcf_predecessor_lmd_choose_before_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_before_choose_table_row_step_previous_left. bcf_height_lmd_choose_before_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_before_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_before_choose_table_row_step)) * bcf_previous_scale_lmd_choose_before_choose_table)) /\ exists bcf_quotient_lmd_choose_before_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_before_choose_table = bcf_quotient_lmd_choose_before_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_before_choose_table_row_step)) * bcf_previous_scale_lmd_choose_before_choose_table) + (bcf_left_lmd_choose_before_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_before_choose_table_row_step_previous_right. bcf_height_lmd_choose_before_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_before_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_before_choose_table_row_step))) * bcf_previous_scale_lmd_choose_before_choose_table)) /\ exists bcf_quotient_lmd_choose_before_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_before_choose_table = bcf_quotient_lmd_choose_before_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_before_choose_table_row_step))) * bcf_previous_scale_lmd_choose_before_choose_table) + (bcf_right_lmd_choose_before_choose_table_row_step))) /\ bcf_value_lmd_choose_before_choose_table_row_step = bcf_left_lmd_choose_before_choose_table_row_step + bcf_right_lmd_choose_before_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_before_choose_decoded_row_code. bcf_height_lmd_choose_before_choose_decoded_row_code + S (bcf_row_code_lmd_choose_before_choose) = S ((S (lmd_choose_upper_choose_before)) * bcf_row_code_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_decoded_row_code. bcf_row_code_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_before)) * bcf_row_code_scale_lmd_choose_before_choose) + (bcf_row_code_lmd_choose_before_choose))) /\ ((((exists bcf_height_lmd_choose_before_choose_decoded_row_scale. bcf_height_lmd_choose_before_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_before_choose) = S ((S (lmd_choose_upper_choose_before)) * bcf_row_scale_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_before)) * bcf_row_scale_scale_lmd_choose_before_choose) + (bcf_row_scale_lmd_choose_before_choose))) /\ (((exists bcf_height_lmd_choose_before_choose_decoded_value. bcf_height_lmd_choose_before_choose_decoded_value + S (lmd_choose_value_choose_before) = S ((S (lmd_choose_lower_choose_before)) * bcf_row_scale_lmd_choose_before_choose)) /\ exists bcf_quotient_lmd_choose_before_choose_decoded_value. bcf_row_code_lmd_choose_before_choose = bcf_quotient_lmd_choose_before_choose_decoded_value * S ((S (lmd_choose_lower_choose_before)) * bcf_row_scale_lmd_choose_before_choose) + (lmd_choose_value_choose_before))))))))))))) -> exists u v. (forall lmd_choose_index_choose_after. (exists lmd_gap_choose_after_bound. lmd_gap_choose_after_bound + S (lmd_choose_index_choose_after) = (S l)) -> exists lmd_choose_upper_choose_after lmd_choose_lower_choose_after lmd_choose_value_choose_after. ((((exists ff_h_lmd_choose_after_upper. ff_h_lmd_choose_after_upper + S (lmd_choose_upper_choose_after) = S ((S (lmd_choose_index_choose_after)) * qc)) /\ exists ff_q_lmd_choose_after_upper. qb = ff_q_lmd_choose_after_upper * S ((S (lmd_choose_index_choose_after)) * qc) + (lmd_choose_upper_choose_after))) /\ ((((exists ff_h_lmd_choose_after_lower. ff_h_lmd_choose_after_lower + S (lmd_choose_lower_choose_after) = S ((S (lmd_choose_index_choose_after)) * dc)) /\ exists ff_q_lmd_choose_after_lower. db = ff_q_lmd_choose_after_lower * S ((S (lmd_choose_index_choose_after)) * dc) + (lmd_choose_lower_choose_after))) /\ ((((exists ff_h_lmd_choose_after_result. ff_h_lmd_choose_after_result + S (lmd_choose_value_choose_after) = S ((S (lmd_choose_index_choose_after)) * v)) /\ exists ff_q_lmd_choose_after_result. u = ff_q_lmd_choose_after_result * S ((S (lmd_choose_index_choose_after)) * v) + (lmd_choose_value_choose_after))) /\ (((exists bcf_lt_gap_lmd_choose_after_choose_out_of_range. bcf_lt_gap_lmd_choose_after_choose_out_of_range + S (lmd_choose_upper_choose_after) = lmd_choose_lower_choose_after) /\ lmd_choose_value_choose_after = 0) \/ ((exists bcf_le_gap_lmd_choose_after_choose_in_range. bcf_le_gap_lmd_choose_after_choose_in_range + (lmd_choose_lower_choose_after) = lmd_choose_upper_choose_after) /\ (exists bcf_row_code_code_lmd_choose_after_choose bcf_row_code_scale_lmd_choose_after_choose bcf_row_scale_code_lmd_choose_after_choose bcf_row_scale_scale_lmd_choose_after_choose bcf_row_code_lmd_choose_after_choose bcf_row_scale_lmd_choose_after_choose. ((forall bcf_row_index_lmd_choose_after_choose_table. (exists bcf_lt_gap_lmd_choose_after_choose_table_row_bound. bcf_lt_gap_lmd_choose_after_choose_table_row_bound + S (bcf_row_index_lmd_choose_after_choose_table) = S (lmd_choose_upper_choose_after)) -> exists bcf_row_code_lmd_choose_after_choose_table bcf_row_scale_lmd_choose_after_choose_table. ((((exists bcf_height_lmd_choose_after_choose_table_decoded_row_code. bcf_height_lmd_choose_after_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_after_choose_table) = S ((S (bcf_row_index_lmd_choose_after_choose_table)) * bcf_row_code_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_after_choose_table)) * bcf_row_code_scale_lmd_choose_after_choose) + (bcf_row_code_lmd_choose_after_choose_table))) /\ ((((exists bcf_height_lmd_choose_after_choose_table_decoded_row_scale. bcf_height_lmd_choose_after_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_after_choose_table) = S ((S (bcf_row_index_lmd_choose_after_choose_table)) * bcf_row_scale_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_after_choose_table)) * bcf_row_scale_scale_lmd_choose_after_choose) + (bcf_row_scale_lmd_choose_after_choose_table))) /\ ((bcf_row_index_lmd_choose_after_choose_table = 0 /\ (forall bcf_index_lmd_choose_after_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_after_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_after_choose_table_zero_row_bound + S (bcf_index_lmd_choose_after_choose_table_zero_row) = S (lmd_choose_upper_choose_after)) -> exists bcf_value_lmd_choose_after_choose_table_zero_row. ((((exists bcf_height_lmd_choose_after_choose_table_zero_row_entry. bcf_height_lmd_choose_after_choose_table_zero_row_entry + S (bcf_value_lmd_choose_after_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_after_choose_table_zero_row)) * bcf_row_scale_lmd_choose_after_choose_table)) /\ exists bcf_quotient_lmd_choose_after_choose_table_zero_row_entry. bcf_row_code_lmd_choose_after_choose_table = bcf_quotient_lmd_choose_after_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_after_choose_table_zero_row)) * bcf_row_scale_lmd_choose_after_choose_table) + (bcf_value_lmd_choose_after_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_after_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_after_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_after_choose_table_zero_row. bcf_index_lmd_choose_after_choose_table_zero_row = S bcf_predecessor_lmd_choose_after_choose_table_zero_row /\ bcf_value_lmd_choose_after_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_after_choose_table bcf_previous_code_lmd_choose_after_choose_table bcf_previous_scale_lmd_choose_after_choose_table. bcf_row_index_lmd_choose_after_choose_table = S bcf_predecessor_lmd_choose_after_choose_table /\ ((((exists bcf_height_lmd_choose_after_choose_table_decoded_previous_code. bcf_height_lmd_choose_after_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_after_choose_table) = S ((S (bcf_predecessor_lmd_choose_after_choose_table)) * bcf_row_code_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_after_choose_table)) * bcf_row_code_scale_lmd_choose_after_choose) + (bcf_previous_code_lmd_choose_after_choose_table))) /\ ((((exists bcf_height_lmd_choose_after_choose_table_decoded_previous_scale. bcf_height_lmd_choose_after_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_after_choose_table) = S ((S (bcf_predecessor_lmd_choose_after_choose_table)) * bcf_row_scale_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_after_choose_table)) * bcf_row_scale_scale_lmd_choose_after_choose) + (bcf_previous_scale_lmd_choose_after_choose_table))) /\ (forall bcf_index_lmd_choose_after_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_after_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_after_choose_table_row_step_bound + S (bcf_index_lmd_choose_after_choose_table_row_step) = S (lmd_choose_upper_choose_after)) -> exists bcf_value_lmd_choose_after_choose_table_row_step. ((((exists bcf_height_lmd_choose_after_choose_table_row_step_entry. bcf_height_lmd_choose_after_choose_table_row_step_entry + S (bcf_value_lmd_choose_after_choose_table_row_step) = S ((S (bcf_index_lmd_choose_after_choose_table_row_step)) * bcf_row_scale_lmd_choose_after_choose_table)) /\ exists bcf_quotient_lmd_choose_after_choose_table_row_step_entry. bcf_row_code_lmd_choose_after_choose_table = bcf_quotient_lmd_choose_after_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_after_choose_table_row_step)) * bcf_row_scale_lmd_choose_after_choose_table) + (bcf_value_lmd_choose_after_choose_table_row_step))) /\ ((bcf_index_lmd_choose_after_choose_table_row_step = 0 /\ bcf_value_lmd_choose_after_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_after_choose_table_row_step bcf_left_lmd_choose_after_choose_table_row_step bcf_right_lmd_choose_after_choose_table_row_step. bcf_index_lmd_choose_after_choose_table_row_step = S bcf_predecessor_lmd_choose_after_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_after_choose_table_row_step_previous_left. bcf_height_lmd_choose_after_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_after_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_after_choose_table_row_step)) * bcf_previous_scale_lmd_choose_after_choose_table)) /\ exists bcf_quotient_lmd_choose_after_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_after_choose_table = bcf_quotient_lmd_choose_after_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_after_choose_table_row_step)) * bcf_previous_scale_lmd_choose_after_choose_table) + (bcf_left_lmd_choose_after_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_after_choose_table_row_step_previous_right. bcf_height_lmd_choose_after_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_after_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_after_choose_table_row_step))) * bcf_previous_scale_lmd_choose_after_choose_table)) /\ exists bcf_quotient_lmd_choose_after_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_after_choose_table = bcf_quotient_lmd_choose_after_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_after_choose_table_row_step))) * bcf_previous_scale_lmd_choose_after_choose_table) + (bcf_right_lmd_choose_after_choose_table_row_step))) /\ bcf_value_lmd_choose_after_choose_table_row_step = bcf_left_lmd_choose_after_choose_table_row_step + bcf_right_lmd_choose_after_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_after_choose_decoded_row_code. bcf_height_lmd_choose_after_choose_decoded_row_code + S (bcf_row_code_lmd_choose_after_choose) = S ((S (lmd_choose_upper_choose_after)) * bcf_row_code_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_decoded_row_code. bcf_row_code_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_after)) * bcf_row_code_scale_lmd_choose_after_choose) + (bcf_row_code_lmd_choose_after_choose))) /\ ((((exists bcf_height_lmd_choose_after_choose_decoded_row_scale. bcf_height_lmd_choose_after_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_after_choose) = S ((S (lmd_choose_upper_choose_after)) * bcf_row_scale_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_after)) * bcf_row_scale_scale_lmd_choose_after_choose) + (bcf_row_scale_lmd_choose_after_choose))) /\ (((exists bcf_height_lmd_choose_after_choose_decoded_value. bcf_height_lmd_choose_after_choose_decoded_value + S (lmd_choose_value_choose_after) = S ((S (lmd_choose_lower_choose_after)) * bcf_row_scale_lmd_choose_after_choose)) /\ exists bcf_quotient_lmd_choose_after_choose_decoded_value. bcf_row_code_lmd_choose_after_choose = bcf_quotient_lmd_choose_after_choose_decoded_value * S ((S (lmd_choose_lower_choose_after)) * bcf_row_scale_lmd_choose_after_choose) + (lmd_choose_value_choose_after)))))))))))))

Constructive proof overview

Generated structural guide

Beta-prefix extension and relational binomial totality append the exact coefficient for the next two decoded source entries.

The unchanged tactic script uses 4 declared prerequisites and contains 84 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized choose_exists Alpha theorem; checked-use authorized beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

LU001G lucas_choose_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

84 script commands · 30 reading checkpoints · 6 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro qb
  2. L2
    intro qc
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro z
  6. L6
    intro t
  7. L7
    intro l
  8. L8
    intro hprefix
02Establish hupperL9–13

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hupper : exists a. (((exists ff_h_lmd_choose_last_upper. ff_h_lmd_choose_last_upper + S (a) = S ((S (l)) * qc)) /\ exists ff_q_lmd_choose_last_upper. qb = ff_q_lmd_choose_last_upper * S ((S (l)) * qc) + (a)))
  2. L10
    specialize beta_at_exists qb
  3. L11
    specialize beta_at_exists qc
  4. L12
    specialize beta_at_exists l
  5. L13
    exact beta_at_exists
03Separate the logical casesL14–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hupper
04Establish hlowerL15–19

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have hlower : exists b. (((exists ff_h_lmd_choose_last_lower. ff_h_lmd_choose_last_lower + S (b) = S ((S (l)) * dc)) /\ exists ff_q_lmd_choose_last_lower. db = ff_q_lmd_choose_last_lower * S ((S (l)) * dc) + (b)))
  2. L16
    specialize beta_at_exists db
  3. L17
    specialize beta_at_exists dc
  4. L18
    specialize beta_at_exists l
  5. L19
    exact beta_at_exists
05Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases hlower
06Establish hchooseL21–24

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hchoose : ∃ C. Choose(x,x1,C)Definitions: Choose
  2. L22
    specialize choose_exists x
  3. L23
    specialize choose_exists x1
  4. L24
    exact choose_exists
07Separate the logical casesL25–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hchoose
08Establish hextendL26–31

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hextend : ∃ u. ∃ v. BetaAt(u,v,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(z,t,x,y) → BetaAt(u,v,x,y))Definitions: LtBetaAt
  2. L27
    specialize beta_prefix_extend l
  3. L28
    specialize beta_prefix_extend z
  4. L29
    specialize beta_prefix_extend t
  5. L30
    specialize beta_prefix_extend x2
  6. L31
    exact beta_prefix_extend
09Separate the logical casesL32–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    cases hextend
  2. L33
    cases hextend_witness
  3. L34
    cases hextend_witness_witness
10Construct an explicit witnessL35–36

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists x3
  2. L36
    exists x4
11Fix variables and assumptionsL37–38

Work with arbitrary variables or the premises of the current implication.

  1. L37
    intro i
  2. L38
    intro hi
12Establish hsplitL39–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L39
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L40
    specialize finite_lt_succ_eq_or_lt l
  3. L41
    specialize finite_lt_succ_eq_or_lt i
  4. L42
    apply finite_lt_succ_eq_or_lt
  5. L43
    exact hi
13Separate the logical casesL44–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L44
    cases hsplit
14Calculate and transport equalitiesL45–50

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L45
    rewrite hsplit_left
  2. L46
    rewrite hsplit_left
  3. L47
    rewrite hsplit_left
  4. L48
    rewrite hsplit_left
  5. L49
    rewrite hsplit_left
  6. L50
    rewrite hsplit_left
15Construct an explicit witnessL51–53

Supply the displayed value, then prove that it has the required property.

  1. L51
    exists x
  2. L52
    exists x1
  3. L53
    exists x2
16Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    split
17Use earlier factsL55–55

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L55
    exact hupper_witness
18Separate the logical casesL56–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L56
    split
19Use earlier factsL57–57

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L57
    exact hlower_witness
20Separate the logical casesL58–58

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L58
    split
21Use earlier factsL59–60

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    exact hextend_witness_witness_left
  2. L60
    exact hchoose_witness
22Establish holdL61–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L61
    have hold : ∃ a. ∃ b. ∃ C. BetaAt(qb,qc,i,a) ∧ (BetaAt(db,dc,i,b) ∧ (BetaAt(z,t,i,C) ∧ Choose(a,b,C)))Definitions: BetaAtChoose
  2. L62
    specialize hprefix i
  3. L63
    apply hprefix
  4. L64
    exact hsplit_right
23Separate the logical casesL65–70

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L65
    cases hold
  2. L66
    cases hold_witness
  3. L67
    cases hold_witness_witness
  4. L68
    cases hold_witness_witness_witness
  5. L69
    cases hold_witness_witness_witness_right
  6. L70
    cases hold_witness_witness_witness_right_right
24Construct an explicit witnessL71–73

Supply the displayed value, then prove that it has the required property.

  1. L71
    exists x5
  2. L72
    exists x6
  3. L73
    exists x7
25Separate the logical casesL74–74

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L74
    split
26Use earlier factsL75–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L75
    exact hold_witness_witness_witness_left
27Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    split
28Use earlier factsL77–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L77
    exact hold_witness_witness_witness_right_left
29Separate the logical casesL78–78

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L78
    split
30Use earlier factsL79–84

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L79
    specialize hextend_witness_witness_right i
  2. L80
    specialize hextend_witness_witness_right x7
  3. L81
    apply hextend_witness_witness_right
  4. L82
    exact hsplit_right
  5. L83
    exact hold_witness_witness_witness_right_right_left
  6. L84
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 84 lines
  1. 0001intro qb
  2. 0002intro qc
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro z
  6. 0006intro t
  7. 0007intro l
  8. 0008intro hprefix
  9. 0009have hupper : exists a. (((exists ff_h_lmd_choose_last_upper. ff_h_lmd_choose_last_upper + S (a) = S ((S (l)) * qc)) /\ exists ff_q_lmd_choose_last_upper. qb = ff_q_lmd_choose_last_upper * S ((S (l)) * qc) + (a)))
  10. 0010specialize beta_at_exists qb
  11. 0011specialize beta_at_exists qc
  12. 0012specialize beta_at_exists l
  13. 0013exact beta_at_exists
  14. 0014cases hupper
  15. 0015have hlower : exists b. (((exists ff_h_lmd_choose_last_lower. ff_h_lmd_choose_last_lower + S (b) = S ((S (l)) * dc)) /\ exists ff_q_lmd_choose_last_lower. db = ff_q_lmd_choose_last_lower * S ((S (l)) * dc) + (b)))
  16. 0016specialize beta_at_exists db
  17. 0017specialize beta_at_exists dc
  18. 0018specialize beta_at_exists l
  19. 0019exact beta_at_exists
  20. 0020cases hlower
  21. 0021have hchoose : exists C. (((exists bcf_lt_gap_lmd_last_choose_out_of_range. bcf_lt_gap_lmd_last_choose_out_of_range + S (x) = x1) /\ C = 0) \/ ((exists bcf_le_gap_lmd_last_choose_in_range. bcf_le_gap_lmd_last_choose_in_range + (x1) = x) /\ (exists bcf_row_code_code_lmd_last_choose bcf_row_code_scale_lmd_last_choose bcf_row_scale_code_lmd_last_choose bcf_row_scale_scale_lmd_last_choose bcf_row_code_lmd_last_choose bcf_row_scale_lmd_last_choose. ((forall bcf_row_index_lmd_last_choose_table. (exists bcf_lt_gap_lmd_last_choose_table_row_bound. bcf_lt_gap_lmd_last_choose_table_row_bound + S (bcf_row_index_lmd_last_choose_table) = S (x)) -> exists bcf_row_code_lmd_last_choose_table bcf_row_scale_lmd_last_choose_table. ((((exists bcf_height_lmd_last_choose_table_decoded_row_code. bcf_height_lmd_last_choose_table_decoded_row_code + S (bcf_row_code_lmd_last_choose_table) = S ((S (bcf_row_index_lmd_last_choose_table)) * bcf_row_code_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_table_decoded_row_code. bcf_row_code_code_lmd_last_choose = bcf_quotient_lmd_last_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_last_choose_table)) * bcf_row_code_scale_lmd_last_choose) + (bcf_row_code_lmd_last_choose_table))) /\ ((((exists bcf_height_lmd_last_choose_table_decoded_row_scale. bcf_height_lmd_last_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_last_choose_table) = S ((S (bcf_row_index_lmd_last_choose_table)) * bcf_row_scale_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_last_choose = bcf_quotient_lmd_last_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_last_choose_table)) * bcf_row_scale_scale_lmd_last_choose) + (bcf_row_scale_lmd_last_choose_table))) /\ ((bcf_row_index_lmd_last_choose_table = 0 /\ (forall bcf_index_lmd_last_choose_table_zero_row. (exists bcf_lt_gap_lmd_last_choose_table_zero_row_bound. bcf_lt_gap_lmd_last_choose_table_zero_row_bound + S (bcf_index_lmd_last_choose_table_zero_row) = S (x)) -> exists bcf_value_lmd_last_choose_table_zero_row. ((((exists bcf_height_lmd_last_choose_table_zero_row_entry. bcf_height_lmd_last_choose_table_zero_row_entry + S (bcf_value_lmd_last_choose_table_zero_row) = S ((S (bcf_index_lmd_last_choose_table_zero_row)) * bcf_row_scale_lmd_last_choose_table)) /\ exists bcf_quotient_lmd_last_choose_table_zero_row_entry. bcf_row_code_lmd_last_choose_table = bcf_quotient_lmd_last_choose_table_zero_row_entry * S ((S (bcf_index_lmd_last_choose_table_zero_row)) * bcf_row_scale_lmd_last_choose_table) + (bcf_value_lmd_last_choose_table_zero_row))) /\ ((bcf_index_lmd_last_choose_table_zero_row = 0 /\ bcf_value_lmd_last_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_last_choose_table_zero_row. bcf_index_lmd_last_choose_table_zero_row = S bcf_predecessor_lmd_last_choose_table_zero_row /\ bcf_value_lmd_last_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_last_choose_table bcf_previous_code_lmd_last_choose_table bcf_previous_scale_lmd_last_choose_table. bcf_row_index_lmd_last_choose_table = S bcf_predecessor_lmd_last_choose_table /\ ((((exists bcf_height_lmd_last_choose_table_decoded_previous_code. bcf_height_lmd_last_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_last_choose_table) = S ((S (bcf_predecessor_lmd_last_choose_table)) * bcf_row_code_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_table_decoded_previous_code. bcf_row_code_code_lmd_last_choose = bcf_quotient_lmd_last_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_last_choose_table)) * bcf_row_code_scale_lmd_last_choose) + (bcf_previous_code_lmd_last_choose_table))) /\ ((((exists bcf_height_lmd_last_choose_table_decoded_previous_scale. bcf_height_lmd_last_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_last_choose_table) = S ((S (bcf_predecessor_lmd_last_choose_table)) * bcf_row_scale_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_last_choose = bcf_quotient_lmd_last_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_last_choose_table)) * bcf_row_scale_scale_lmd_last_choose) + (bcf_previous_scale_lmd_last_choose_table))) /\ (forall bcf_index_lmd_last_choose_table_row_step. (exists bcf_lt_gap_lmd_last_choose_table_row_step_bound. bcf_lt_gap_lmd_last_choose_table_row_step_bound + S (bcf_index_lmd_last_choose_table_row_step) = S (x)) -> exists bcf_value_lmd_last_choose_table_row_step. ((((exists bcf_height_lmd_last_choose_table_row_step_entry. bcf_height_lmd_last_choose_table_row_step_entry + S (bcf_value_lmd_last_choose_table_row_step) = S ((S (bcf_index_lmd_last_choose_table_row_step)) * bcf_row_scale_lmd_last_choose_table)) /\ exists bcf_quotient_lmd_last_choose_table_row_step_entry. bcf_row_code_lmd_last_choose_table = bcf_quotient_lmd_last_choose_table_row_step_entry * S ((S (bcf_index_lmd_last_choose_table_row_step)) * bcf_row_scale_lmd_last_choose_table) + (bcf_value_lmd_last_choose_table_row_step))) /\ ((bcf_index_lmd_last_choose_table_row_step = 0 /\ bcf_value_lmd_last_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_last_choose_table_row_step bcf_left_lmd_last_choose_table_row_step bcf_right_lmd_last_choose_table_row_step. bcf_index_lmd_last_choose_table_row_step = S bcf_predecessor_lmd_last_choose_table_row_step /\ ((((exists bcf_height_lmd_last_choose_table_row_step_previous_left. bcf_height_lmd_last_choose_table_row_step_previous_left + S (bcf_left_lmd_last_choose_table_row_step) = S ((S (bcf_predecessor_lmd_last_choose_table_row_step)) * bcf_previous_scale_lmd_last_choose_table)) /\ exists bcf_quotient_lmd_last_choose_table_row_step_previous_left. bcf_previous_code_lmd_last_choose_table = bcf_quotient_lmd_last_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_last_choose_table_row_step)) * bcf_previous_scale_lmd_last_choose_table) + (bcf_left_lmd_last_choose_table_row_step))) /\ ((((exists bcf_height_lmd_last_choose_table_row_step_previous_right. bcf_height_lmd_last_choose_table_row_step_previous_right + S (bcf_right_lmd_last_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_last_choose_table_row_step))) * bcf_previous_scale_lmd_last_choose_table)) /\ exists bcf_quotient_lmd_last_choose_table_row_step_previous_right. bcf_previous_code_lmd_last_choose_table = bcf_quotient_lmd_last_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_last_choose_table_row_step))) * bcf_previous_scale_lmd_last_choose_table) + (bcf_right_lmd_last_choose_table_row_step))) /\ bcf_value_lmd_last_choose_table_row_step = bcf_left_lmd_last_choose_table_row_step + bcf_right_lmd_last_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_last_choose_decoded_row_code. bcf_height_lmd_last_choose_decoded_row_code + S (bcf_row_code_lmd_last_choose) = S ((S (x)) * bcf_row_code_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_decoded_row_code. bcf_row_code_code_lmd_last_choose = bcf_quotient_lmd_last_choose_decoded_row_code * S ((S (x)) * bcf_row_code_scale_lmd_last_choose) + (bcf_row_code_lmd_last_choose))) /\ ((((exists bcf_height_lmd_last_choose_decoded_row_scale. bcf_height_lmd_last_choose_decoded_row_scale + S (bcf_row_scale_lmd_last_choose) = S ((S (x)) * bcf_row_scale_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_decoded_row_scale. bcf_row_scale_code_lmd_last_choose = bcf_quotient_lmd_last_choose_decoded_row_scale * S ((S (x)) * bcf_row_scale_scale_lmd_last_choose) + (bcf_row_scale_lmd_last_choose))) /\ (((exists bcf_height_lmd_last_choose_decoded_value. bcf_height_lmd_last_choose_decoded_value + S (C) = S ((S (x1)) * bcf_row_scale_lmd_last_choose)) /\ exists bcf_quotient_lmd_last_choose_decoded_value. bcf_row_code_lmd_last_choose = bcf_quotient_lmd_last_choose_decoded_value * S ((S (x1)) * bcf_row_scale_lmd_last_choose) + (C)))))))))
  22. 0022specialize choose_exists x
  23. 0023specialize choose_exists x1
  24. 0024exact choose_exists
  25. 0025cases hchoose
  26. 0026have hextend : exists u v. ((((exists ff_h_lmd_choose_extended_new. ff_h_lmd_choose_extended_new + S (x2) = S ((S (l)) * v)) /\ exists ff_q_lmd_choose_extended_new. u = ff_q_lmd_choose_extended_new * S ((S (l)) * v) + (x2))) /\ forall i y. (exists lmd_gap_choose_extended_bound. lmd_gap_choose_extended_bound + S (i) = (l)) -> (((exists ff_h_lmd_choose_extended_old. ff_h_lmd_choose_extended_old + S (y) = S ((S (i)) * t)) /\ exists ff_q_lmd_choose_extended_old. z = ff_q_lmd_choose_extended_old * S ((S (i)) * t) + (y))) -> (((exists ff_h_lmd_choose_extended_target. ff_h_lmd_choose_extended_target + S (y) = S ((S (i)) * v)) /\ exists ff_q_lmd_choose_extended_target. u = ff_q_lmd_choose_extended_target * S ((S (i)) * v) + (y))))
  27. 0027specialize beta_prefix_extend l
  28. 0028specialize beta_prefix_extend z
  29. 0029specialize beta_prefix_extend t
  30. 0030specialize beta_prefix_extend x2
  31. 0031exact beta_prefix_extend
  32. 0032cases hextend
  33. 0033cases hextend_witness
  34. 0034cases hextend_witness_witness
  35. 0035exists x3
  36. 0036exists x4
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hsplit : i = l \/ exists gap. gap + S i = l
  40. 0040specialize finite_lt_succ_eq_or_lt l
  41. 0041specialize finite_lt_succ_eq_or_lt i
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hsplit
  45. 0045rewrite hsplit_left
  46. 0046rewrite hsplit_left
  47. 0047rewrite hsplit_left
  48. 0048rewrite hsplit_left
  49. 0049rewrite hsplit_left
  50. 0050rewrite hsplit_left
  51. 0051exists x
  52. 0052exists x1
  53. 0053exists x2
  54. 0054split
  55. 0055exact hupper_witness
  56. 0056split
  57. 0057exact hlower_witness
  58. 0058split
  59. 0059exact hextend_witness_witness_left
  60. 0060exact hchoose_witness
  61. 0061have hold : exists a b C. ((((exists ff_h_lmd_choose_old_upper. ff_h_lmd_choose_old_upper + S (a) = S ((S (i)) * qc)) /\ exists ff_q_lmd_choose_old_upper. qb = ff_q_lmd_choose_old_upper * S ((S (i)) * qc) + (a))) /\ ((((exists ff_h_lmd_choose_old_lower. ff_h_lmd_choose_old_lower + S (b) = S ((S (i)) * dc)) /\ exists ff_q_lmd_choose_old_lower. db = ff_q_lmd_choose_old_lower * S ((S (i)) * dc) + (b))) /\ ((((exists ff_h_lmd_choose_old_value. ff_h_lmd_choose_old_value + S (C) = S ((S (i)) * t)) /\ exists ff_q_lmd_choose_old_value. z = ff_q_lmd_choose_old_value * S ((S (i)) * t) + (C))) /\ (((exists bcf_lt_gap_lmd_old_choose_out_of_range. bcf_lt_gap_lmd_old_choose_out_of_range + S (a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lmd_old_choose_in_range. bcf_le_gap_lmd_old_choose_in_range + (b) = a) /\ (exists bcf_row_code_code_lmd_old_choose bcf_row_code_scale_lmd_old_choose bcf_row_scale_code_lmd_old_choose bcf_row_scale_scale_lmd_old_choose bcf_row_code_lmd_old_choose bcf_row_scale_lmd_old_choose. ((forall bcf_row_index_lmd_old_choose_table. (exists bcf_lt_gap_lmd_old_choose_table_row_bound. bcf_lt_gap_lmd_old_choose_table_row_bound + S (bcf_row_index_lmd_old_choose_table) = S (a)) -> exists bcf_row_code_lmd_old_choose_table bcf_row_scale_lmd_old_choose_table. ((((exists bcf_height_lmd_old_choose_table_decoded_row_code. bcf_height_lmd_old_choose_table_decoded_row_code + S (bcf_row_code_lmd_old_choose_table) = S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_row_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose) + (bcf_row_code_lmd_old_choose_table))) /\ ((((exists bcf_height_lmd_old_choose_table_decoded_row_scale. bcf_height_lmd_old_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_old_choose_table) = S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_row_scale_lmd_old_choose_table))) /\ ((bcf_row_index_lmd_old_choose_table = 0 /\ (forall bcf_index_lmd_old_choose_table_zero_row. (exists bcf_lt_gap_lmd_old_choose_table_zero_row_bound. bcf_lt_gap_lmd_old_choose_table_zero_row_bound + S (bcf_index_lmd_old_choose_table_zero_row) = S (a)) -> exists bcf_value_lmd_old_choose_table_zero_row. ((((exists bcf_height_lmd_old_choose_table_zero_row_entry. bcf_height_lmd_old_choose_table_zero_row_entry + S (bcf_value_lmd_old_choose_table_zero_row) = S ((S (bcf_index_lmd_old_choose_table_zero_row)) * bcf_row_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_zero_row_entry. bcf_row_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_zero_row_entry * S ((S (bcf_index_lmd_old_choose_table_zero_row)) * bcf_row_scale_lmd_old_choose_table) + (bcf_value_lmd_old_choose_table_zero_row))) /\ ((bcf_index_lmd_old_choose_table_zero_row = 0 /\ bcf_value_lmd_old_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_old_choose_table_zero_row. bcf_index_lmd_old_choose_table_zero_row = S bcf_predecessor_lmd_old_choose_table_zero_row /\ bcf_value_lmd_old_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_old_choose_table bcf_previous_code_lmd_old_choose_table bcf_previous_scale_lmd_old_choose_table. bcf_row_index_lmd_old_choose_table = S bcf_predecessor_lmd_old_choose_table /\ ((((exists bcf_height_lmd_old_choose_table_decoded_previous_code. bcf_height_lmd_old_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_old_choose_table) = S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_previous_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose) + (bcf_previous_code_lmd_old_choose_table))) /\ ((((exists bcf_height_lmd_old_choose_table_decoded_previous_scale. bcf_height_lmd_old_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_old_choose_table) = S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_previous_scale_lmd_old_choose_table))) /\ (forall bcf_index_lmd_old_choose_table_row_step. (exists bcf_lt_gap_lmd_old_choose_table_row_step_bound. bcf_lt_gap_lmd_old_choose_table_row_step_bound + S (bcf_index_lmd_old_choose_table_row_step) = S (a)) -> exists bcf_value_lmd_old_choose_table_row_step. ((((exists bcf_height_lmd_old_choose_table_row_step_entry. bcf_height_lmd_old_choose_table_row_step_entry + S (bcf_value_lmd_old_choose_table_row_step) = S ((S (bcf_index_lmd_old_choose_table_row_step)) * bcf_row_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_entry. bcf_row_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_entry * S ((S (bcf_index_lmd_old_choose_table_row_step)) * bcf_row_scale_lmd_old_choose_table) + (bcf_value_lmd_old_choose_table_row_step))) /\ ((bcf_index_lmd_old_choose_table_row_step = 0 /\ bcf_value_lmd_old_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_old_choose_table_row_step bcf_left_lmd_old_choose_table_row_step bcf_right_lmd_old_choose_table_row_step. bcf_index_lmd_old_choose_table_row_step = S bcf_predecessor_lmd_old_choose_table_row_step /\ ((((exists bcf_height_lmd_old_choose_table_row_step_previous_left. bcf_height_lmd_old_choose_table_row_step_previous_left + S (bcf_left_lmd_old_choose_table_row_step) = S ((S (bcf_predecessor_lmd_old_choose_table_row_step)) * bcf_previous_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_previous_left. bcf_previous_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_old_choose_table_row_step)) * bcf_previous_scale_lmd_old_choose_table) + (bcf_left_lmd_old_choose_table_row_step))) /\ ((((exists bcf_height_lmd_old_choose_table_row_step_previous_right. bcf_height_lmd_old_choose_table_row_step_previous_right + S (bcf_right_lmd_old_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_old_choose_table_row_step))) * bcf_previous_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_previous_right. bcf_previous_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_old_choose_table_row_step))) * bcf_previous_scale_lmd_old_choose_table) + (bcf_right_lmd_old_choose_table_row_step))) /\ bcf_value_lmd_old_choose_table_row_step = bcf_left_lmd_old_choose_table_row_step + bcf_right_lmd_old_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_old_choose_decoded_row_code. bcf_height_lmd_old_choose_decoded_row_code + S (bcf_row_code_lmd_old_choose) = S ((S (a)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_row_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lmd_old_choose) + (bcf_row_code_lmd_old_choose))) /\ ((((exists bcf_height_lmd_old_choose_decoded_row_scale. bcf_height_lmd_old_choose_decoded_row_scale + S (bcf_row_scale_lmd_old_choose) = S ((S (a)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_row_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_row_scale_lmd_old_choose))) /\ (((exists bcf_height_lmd_old_choose_decoded_value. bcf_height_lmd_old_choose_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_value. bcf_row_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_value * S ((S (b)) * bcf_row_scale_lmd_old_choose) + (C))))))))))))
  62. 0062specialize hprefix i
  63. 0063apply hprefix
  64. 0064exact hsplit_right
  65. 0065cases hold
  66. 0066cases hold_witness
  67. 0067cases hold_witness_witness
  68. 0068cases hold_witness_witness_witness
  69. 0069cases hold_witness_witness_witness_right
  70. 0070cases hold_witness_witness_witness_right_right
  71. 0071exists x5
  72. 0072exists x6
  73. 0073exists x7
  74. 0074split
  75. 0075exact hold_witness_witness_witness_left
  76. 0076split
  77. 0077exact hold_witness_witness_witness_right_left
  78. 0078split
  79. 0079specialize hextend_witness_witness_right i
  80. 0080specialize hextend_witness_witness_right x7
  81. 0081apply hextend_witness_witness_right
  82. 0082exact hsplit_right
  83. 0083exact hold_witness_witness_witness_right_right_left
  84. 0084exact hold_witness_witness_witness_right_right_right