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 p n k l qb qc db dc ub uc vb vc z t s w P C T. ((~(p = 1) /\ forall frm_prime_left_lmd_terminal_prime frm_prime_right_lmd_terminal_prime. p = frm_prime_left_lmd_terminal_prime * frm_prime_right_lmd_terminal_prime -> frm_prime_left_lmd_terminal_prime = 1 \/ frm_prime_right_lmd_terminal_prime = 1)) -> (((((exists ff_h_lmd_full_n_initial. ff_h_lmd_full_n_initial + S (n) = S ((S (0)) * qc)) /\ exists ff_q_lmd_full_n_initial. qb = ff_q_lmd_full_n_initial * S ((S (0)) * qc) + (n))) /\ forall lmd_index_full_n. (exists lmd_gap_full_n_index. lmd_gap_full_n_index + S (lmd_index_full_n) = (l)) -> exists lmd_current_full_n lmd_successor_full_n lmd_digit_full_n. ((((exists ff_h_lmd_full_n_current. ff_h_lmd_full_n_current + S (lmd_current_full_n) = S ((S (lmd_index_full_n)) * qc)) /\ exists ff_q_lmd_full_n_current. qb = ff_q_lmd_full_n_current * S ((S (lmd_index_full_n)) * qc) + (lmd_current_full_n))) /\ ((((exists ff_h_lmd_full_n_successor. ff_h_lmd_full_n_successor + S (lmd_successor_full_n) = S ((S (S lmd_index_full_n)) * qc)) /\ exists ff_q_lmd_full_n_successor. qb = ff_q_lmd_full_n_successor * S ((S (S lmd_index_full_n)) * qc) + (lmd_successor_full_n))) /\ ((((exists ff_h_lmd_full_n_digit. ff_h_lmd_full_n_digit + S (lmd_digit_full_n) = S ((S (lmd_index_full_n)) * dc)) /\ exists ff_q_lmd_full_n_digit. db = ff_q_lmd_full_n_digit * S ((S (lmd_index_full_n)) * dc) + (lmd_digit_full_n))) /\ ((lmd_current_full_n = (p) * (lmd_successor_full_n) + (lmd_digit_full_n)) /\ (exists lmd_gap_full_n_digit_bound. lmd_gap_full_n_digit_bound + S (lmd_digit_full_n) = (p)))))))) -> (((((exists ff_h_lmd_full_k_initial. ff_h_lmd_full_k_initial + S (k) = S ((S (0)) * uc)) /\ exists ff_q_lmd_full_k_initial. ub = ff_q_lmd_full_k_initial * S ((S (0)) * uc) + (k))) /\ forall lmd_index_full_k. (exists lmd_gap_full_k_index. lmd_gap_full_k_index + S (lmd_index_full_k) = (l)) -> exists lmd_current_full_k lmd_successor_full_k lmd_digit_full_k. ((((exists ff_h_lmd_full_k_current. ff_h_lmd_full_k_current + S (lmd_current_full_k) = S ((S (lmd_index_full_k)) * uc)) /\ exists ff_q_lmd_full_k_current. ub = ff_q_lmd_full_k_current * S ((S (lmd_index_full_k)) * uc) + (lmd_current_full_k))) /\ ((((exists ff_h_lmd_full_k_successor. ff_h_lmd_full_k_successor + S (lmd_successor_full_k) = S ((S (S lmd_index_full_k)) * uc)) /\ exists ff_q_lmd_full_k_successor. ub = ff_q_lmd_full_k_successor * S ((S (S lmd_index_full_k)) * uc) + (lmd_successor_full_k))) /\ ((((exists ff_h_lmd_full_k_digit. ff_h_lmd_full_k_digit + S (lmd_digit_full_k) = S ((S (lmd_index_full_k)) * vc)) /\ exists ff_q_lmd_full_k_digit. vb = ff_q_lmd_full_k_digit * S ((S (lmd_index_full_k)) * vc) + (lmd_digit_full_k))) /\ ((lmd_current_full_k = (p) * (lmd_successor_full_k) + (lmd_digit_full_k)) /\ (exists lmd_gap_full_k_digit_bound. lmd_gap_full_k_digit_bound + S (lmd_digit_full_k) = (p)))))))) -> (forall lmd_choose_index_full_quotient_choose. (exists lmd_gap_full_quotient_choose_bound. lmd_gap_full_quotient_choose_bound + S (lmd_choose_index_full_quotient_choose) = (S l)) -> exists lmd_choose_upper_full_quotient_choose lmd_choose_lower_full_quotient_choose lmd_choose_value_full_quotient_choose. ((((exists ff_h_lmd_full_quotient_choose_upper. ff_h_lmd_full_quotient_choose_upper + S (lmd_choose_upper_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * qc)) /\ exists ff_q_lmd_full_quotient_choose_upper. qb = ff_q_lmd_full_quotient_choose_upper * S ((S (lmd_choose_index_full_quotient_choose)) * qc) + (lmd_choose_upper_full_quotient_choose))) /\ ((((exists ff_h_lmd_full_quotient_choose_lower. ff_h_lmd_full_quotient_choose_lower + S (lmd_choose_lower_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * uc)) /\ exists ff_q_lmd_full_quotient_choose_lower. ub = ff_q_lmd_full_quotient_choose_lower * S ((S (lmd_choose_index_full_quotient_choose)) * uc) + (lmd_choose_lower_full_quotient_choose))) /\ ((((exists ff_h_lmd_full_quotient_choose_result. ff_h_lmd_full_quotient_choose_result + S (lmd_choose_value_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * t)) /\ exists ff_q_lmd_full_quotient_choose_result. z = ff_q_lmd_full_quotient_choose_result * S ((S (lmd_choose_index_full_quotient_choose)) * t) + (lmd_choose_value_full_quotient_choose))) /\ (((exists bcf_lt_gap_lmd_full_quotient_choose_choose_out_of_range. bcf_lt_gap_lmd_full_quotient_choose_choose_out_of_range + S (lmd_choose_upper_full_quotient_choose) = lmd_choose_lower_full_quotient_choose) /\ lmd_choose_value_full_quotient_choose = 0) \/ ((exists bcf_le_gap_lmd_full_quotient_choose_choose_in_range. bcf_le_gap_lmd_full_quotient_choose_choose_in_range + (lmd_choose_lower_full_quotient_choose) = lmd_choose_upper_full_quotient_choose) /\ (exists bcf_row_code_code_lmd_full_quotient_choose_choose bcf_row_code_scale_lmd_full_quotient_choose_choose bcf_row_scale_code_lmd_full_quotient_choose_choose bcf_row_scale_scale_lmd_full_quotient_choose_choose bcf_row_code_lmd_full_quotient_choose_choose bcf_row_scale_lmd_full_quotient_choose_choose. ((forall bcf_row_index_lmd_full_quotient_choose_choose_table. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_bound + S (bcf_row_index_lmd_full_quotient_choose_choose_table) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_row_code_lmd_full_quotient_choose_choose_table bcf_row_scale_lmd_full_quotient_choose_choose_table. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_code. bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_code + S (bcf_row_code_lmd_full_quotient_choose_choose_table) = S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_row_code_lmd_full_quotient_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_scale. bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_full_quotient_choose_choose_table) = S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_row_scale_lmd_full_quotient_choose_choose_table))) /\ ((bcf_row_index_lmd_full_quotient_choose_choose_table = 0 /\ (forall bcf_index_lmd_full_quotient_choose_choose_table_zero_row. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_zero_row_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_zero_row_bound + S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_value_lmd_full_quotient_choose_choose_table_zero_row. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_zero_row_entry. bcf_height_lmd_full_quotient_choose_choose_table_zero_row_entry + S (bcf_value_lmd_full_quotient_choose_choose_table_zero_row) = S ((S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_zero_row_entry. bcf_row_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_zero_row_entry * S ((S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_quotient_choose_choose_table) + (bcf_value_lmd_full_quotient_choose_choose_table_zero_row))) /\ ((bcf_index_lmd_full_quotient_choose_choose_table_zero_row = 0 /\ bcf_value_lmd_full_quotient_choose_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table_zero_row. bcf_index_lmd_full_quotient_choose_choose_table_zero_row = S bcf_predecessor_lmd_full_quotient_choose_choose_table_zero_row /\ bcf_value_lmd_full_quotient_choose_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table bcf_previous_code_lmd_full_quotient_choose_choose_table bcf_previous_scale_lmd_full_quotient_choose_choose_table. bcf_row_index_lmd_full_quotient_choose_choose_table = S bcf_predecessor_lmd_full_quotient_choose_choose_table /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_code. bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_full_quotient_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_previous_code_lmd_full_quotient_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_scale. bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_full_quotient_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_previous_scale_lmd_full_quotient_choose_choose_table))) /\ (forall bcf_index_lmd_full_quotient_choose_choose_table_row_step. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_step_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_step_bound + S (bcf_index_lmd_full_quotient_choose_choose_table_row_step) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_value_lmd_full_quotient_choose_choose_table_row_step. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_entry. bcf_height_lmd_full_quotient_choose_choose_table_row_step_entry + S (bcf_value_lmd_full_quotient_choose_choose_table_row_step) = S ((S (bcf_index_lmd_full_quotient_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_entry. bcf_row_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_entry * S ((S (bcf_index_lmd_full_quotient_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_quotient_choose_choose_table) + (bcf_value_lmd_full_quotient_choose_choose_table_row_step))) /\ ((bcf_index_lmd_full_quotient_choose_choose_table_row_step = 0 /\ bcf_value_lmd_full_quotient_choose_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step bcf_left_lmd_full_quotient_choose_choose_table_row_step bcf_right_lmd_full_quotient_choose_choose_table_row_step. bcf_index_lmd_full_quotient_choose_choose_table_row_step = S bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_left. bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_left + S (bcf_left_lmd_full_quotient_choose_choose_table_row_step) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_left. bcf_previous_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_quotient_choose_choose_table) + (bcf_left_lmd_full_quotient_choose_choose_table_row_step))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_right. bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_right + S (bcf_right_lmd_full_quotient_choose_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_right. bcf_previous_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_quotient_choose_choose_table) + (bcf_right_lmd_full_quotient_choose_choose_table_row_step))) /\ bcf_value_lmd_full_quotient_choose_choose_table_row_step = bcf_left_lmd_full_quotient_choose_choose_table_row_step + bcf_right_lmd_full_quotient_choose_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_decoded_row_code. bcf_height_lmd_full_quotient_choose_choose_decoded_row_code + S (bcf_row_code_lmd_full_quotient_choose_choose) = S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_code * S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_row_code_lmd_full_quotient_choose_choose))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_decoded_row_scale. bcf_height_lmd_full_quotient_choose_choose_decoded_row_scale + S (bcf_row_scale_lmd_full_quotient_choose_choose) = S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_scale * S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_row_scale_lmd_full_quotient_choose_choose))) /\ (((exists bcf_height_lmd_full_quotient_choose_choose_decoded_value. bcf_height_lmd_full_quotient_choose_choose_decoded_value + S (lmd_choose_value_full_quotient_choose) = S ((S (lmd_choose_lower_full_quotient_choose)) * bcf_row_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_value. bcf_row_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_value * S ((S (lmd_choose_lower_full_quotient_choose)) * bcf_row_scale_lmd_full_quotient_choose_choose) + (lmd_choose_value_full_quotient_choose))))))))))))) -> (forall lmd_choose_index_full_digit_choose. (exists lmd_gap_full_digit_choose_bound. lmd_gap_full_digit_choose_bound + S (lmd_choose_index_full_digit_choose) = (l)) -> exists lmd_choose_upper_full_digit_choose lmd_choose_lower_full_digit_choose lmd_choose_value_full_digit_choose. ((((exists ff_h_lmd_full_digit_choose_upper. ff_h_lmd_full_digit_choose_upper + S (lmd_choose_upper_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * dc)) /\ exists ff_q_lmd_full_digit_choose_upper. db = ff_q_lmd_full_digit_choose_upper * S ((S (lmd_choose_index_full_digit_choose)) * dc) + (lmd_choose_upper_full_digit_choose))) /\ ((((exists ff_h_lmd_full_digit_choose_lower. ff_h_lmd_full_digit_choose_lower + S (lmd_choose_lower_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * vc)) /\ exists ff_q_lmd_full_digit_choose_lower. vb = ff_q_lmd_full_digit_choose_lower * S ((S (lmd_choose_index_full_digit_choose)) * vc) + (lmd_choose_lower_full_digit_choose))) /\ ((((exists ff_h_lmd_full_digit_choose_result. ff_h_lmd_full_digit_choose_result + S (lmd_choose_value_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * w)) /\ exists ff_q_lmd_full_digit_choose_result. s = ff_q_lmd_full_digit_choose_result * S ((S (lmd_choose_index_full_digit_choose)) * w) + (lmd_choose_value_full_digit_choose))) /\ (((exists bcf_lt_gap_lmd_full_digit_choose_choose_out_of_range. bcf_lt_gap_lmd_full_digit_choose_choose_out_of_range + S (lmd_choose_upper_full_digit_choose) = lmd_choose_lower_full_digit_choose) /\ lmd_choose_value_full_digit_choose = 0) \/ ((exists bcf_le_gap_lmd_full_digit_choose_choose_in_range. bcf_le_gap_lmd_full_digit_choose_choose_in_range + (lmd_choose_lower_full_digit_choose) = lmd_choose_upper_full_digit_choose) /\ (exists bcf_row_code_code_lmd_full_digit_choose_choose bcf_row_code_scale_lmd_full_digit_choose_choose bcf_row_scale_code_lmd_full_digit_choose_choose bcf_row_scale_scale_lmd_full_digit_choose_choose bcf_row_code_lmd_full_digit_choose_choose bcf_row_scale_lmd_full_digit_choose_choose. ((forall bcf_row_index_lmd_full_digit_choose_choose_table. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_row_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_row_bound + S (bcf_row_index_lmd_full_digit_choose_choose_table) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_row_code_lmd_full_digit_choose_choose_table bcf_row_scale_lmd_full_digit_choose_choose_table. ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_row_code. bcf_height_lmd_full_digit_choose_choose_table_decoded_row_code + S (bcf_row_code_lmd_full_digit_choose_choose_table) = S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_row_code_lmd_full_digit_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_row_scale. bcf_height_lmd_full_digit_choose_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_full_digit_choose_choose_table) = S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_row_scale_lmd_full_digit_choose_choose_table))) /\ ((bcf_row_index_lmd_full_digit_choose_choose_table = 0 /\ (forall bcf_index_lmd_full_digit_choose_choose_table_zero_row. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_zero_row_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_zero_row_bound + S (bcf_index_lmd_full_digit_choose_choose_table_zero_row) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_value_lmd_full_digit_choose_choose_table_zero_row. ((((exists bcf_height_lmd_full_digit_choose_choose_table_zero_row_entry. bcf_height_lmd_full_digit_choose_choose_table_zero_row_entry + S (bcf_value_lmd_full_digit_choose_choose_table_zero_row) = S ((S (bcf_index_lmd_full_digit_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_zero_row_entry. bcf_row_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_zero_row_entry * S ((S (bcf_index_lmd_full_digit_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_digit_choose_choose_table) + (bcf_value_lmd_full_digit_choose_choose_table_zero_row))) /\ ((bcf_index_lmd_full_digit_choose_choose_table_zero_row = 0 /\ bcf_value_lmd_full_digit_choose_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table_zero_row. bcf_index_lmd_full_digit_choose_choose_table_zero_row = S bcf_predecessor_lmd_full_digit_choose_choose_table_zero_row /\ bcf_value_lmd_full_digit_choose_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table bcf_previous_code_lmd_full_digit_choose_choose_table bcf_previous_scale_lmd_full_digit_choose_choose_table. bcf_row_index_lmd_full_digit_choose_choose_table = S bcf_predecessor_lmd_full_digit_choose_choose_table /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_code. bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_full_digit_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_previous_code_lmd_full_digit_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_scale. bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_full_digit_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_previous_scale_lmd_full_digit_choose_choose_table))) /\ (forall bcf_index_lmd_full_digit_choose_choose_table_row_step. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_row_step_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_row_step_bound + S (bcf_index_lmd_full_digit_choose_choose_table_row_step) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_value_lmd_full_digit_choose_choose_table_row_step. ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_entry. bcf_height_lmd_full_digit_choose_choose_table_row_step_entry + S (bcf_value_lmd_full_digit_choose_choose_table_row_step) = S ((S (bcf_index_lmd_full_digit_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_entry. bcf_row_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_entry * S ((S (bcf_index_lmd_full_digit_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_digit_choose_choose_table) + (bcf_value_lmd_full_digit_choose_choose_table_row_step))) /\ ((bcf_index_lmd_full_digit_choose_choose_table_row_step = 0 /\ bcf_value_lmd_full_digit_choose_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table_row_step bcf_left_lmd_full_digit_choose_choose_table_row_step bcf_right_lmd_full_digit_choose_choose_table_row_step. bcf_index_lmd_full_digit_choose_choose_table_row_step = S bcf_predecessor_lmd_full_digit_choose_choose_table_row_step /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_left. bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_left + S (bcf_left_lmd_full_digit_choose_choose_table_row_step) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_left. bcf_previous_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_digit_choose_choose_table) + (bcf_left_lmd_full_digit_choose_choose_table_row_step))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_right. bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_right + S (bcf_right_lmd_full_digit_choose_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_right. bcf_previous_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_digit_choose_choose_table) + (bcf_right_lmd_full_digit_choose_choose_table_row_step))) /\ bcf_value_lmd_full_digit_choose_choose_table_row_step = bcf_left_lmd_full_digit_choose_choose_table_row_step + bcf_right_lmd_full_digit_choose_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_decoded_row_code. bcf_height_lmd_full_digit_choose_choose_decoded_row_code + S (bcf_row_code_lmd_full_digit_choose_choose) = S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_row_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_row_code * S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_row_code_lmd_full_digit_choose_choose))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_decoded_row_scale. bcf_height_lmd_full_digit_choose_choose_decoded_row_scale + S (bcf_row_scale_lmd_full_digit_choose_choose) = S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_row_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_row_scale * S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_row_scale_lmd_full_digit_choose_choose))) /\ (((exists bcf_height_lmd_full_digit_choose_choose_decoded_value. bcf_height_lmd_full_digit_choose_choose_decoded_value + S (lmd_choose_value_full_digit_choose) = S ((S (lmd_choose_lower_full_digit_choose)) * bcf_row_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_value. bcf_row_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_value * S ((S (lmd_choose_lower_full_digit_choose)) * bcf_row_scale_lmd_full_digit_choose_choose) + (lmd_choose_value_full_digit_choose))))))))))))) -> (exists ff_u_lmd_full_product ff_v_lmd_full_product. ((((exists ff_h_lmd_full_product_start. ff_h_lmd_full_product_start + S (1) = S ((S (0)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_start. ff_u_lmd_full_product = ff_q_lmd_full_product_start * S ((S (0)) * ff_v_lmd_full_product) + (1))) /\ ((((exists ff_h_lmd_full_product_terminal. ff_h_lmd_full_product_terminal + S (P) = S ((S (l)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_terminal. ff_u_lmd_full_product = ff_q_lmd_full_product_terminal * S ((S (l)) * ff_v_lmd_full_product) + (P))) /\ forall ff_i_lmd_full_product. (exists ff_lt_lmd_full_product_bound. ff_lt_lmd_full_product_bound + S ff_i_lmd_full_product = l) -> exists ff_p_lmd_full_product ff_r_lmd_full_product ff_s_lmd_full_product. ((((exists ff_h_lmd_full_product_factor. ff_h_lmd_full_product_factor + S (ff_p_lmd_full_product) = S ((S (ff_i_lmd_full_product)) * w)) /\ exists ff_q_lmd_full_product_factor. s = ff_q_lmd_full_product_factor * S ((S (ff_i_lmd_full_product)) * w) + (ff_p_lmd_full_product))) /\ ((((exists ff_h_lmd_full_product_partial. ff_h_lmd_full_product_partial + S (ff_r_lmd_full_product) = S ((S (ff_i_lmd_full_product)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_partial. ff_u_lmd_full_product = ff_q_lmd_full_product_partial * S ((S (ff_i_lmd_full_product)) * ff_v_lmd_full_product) + (ff_r_lmd_full_product))) /\ ((((exists ff_h_lmd_full_product_successor. ff_h_lmd_full_product_successor + S (ff_s_lmd_full_product) = S ((S (S ff_i_lmd_full_product)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_successor. ff_u_lmd_full_product = ff_q_lmd_full_product_successor * S ((S (S ff_i_lmd_full_product)) * ff_v_lmd_full_product) + (ff_s_lmd_full_product))) /\ ff_s_lmd_full_product = ff_r_lmd_full_product * ff_p_lmd_full_product)))))) -> (((exists ff_h_lmd_full_coefficient_start. ff_h_lmd_full_coefficient_start + S (C) = S ((S (0)) * t)) /\ exists ff_q_lmd_full_coefficient_start. z = ff_q_lmd_full_coefficient_start * S ((S (0)) * t) + (C))) -> (((exists ff_h_lmd_full_coefficient_end. ff_h_lmd_full_coefficient_end + S (T) = S ((S (l)) * t)) /\ exists ff_q_lmd_full_coefficient_end. z = ff_q_lmd_full_coefficient_end * S ((S (l)) * t) + (T))) -> (((exists ff_h_lmd_terminal_upper_zero. ff_h_lmd_terminal_upper_zero + S (0) = S ((S (l)) * qc)) /\ exists ff_q_lmd_terminal_upper_zero. qb = ff_q_lmd_terminal_upper_zero * S ((S (l)) * qc) + (0))) -> (((exists ff_h_lmd_terminal_lower_zero. ff_h_lmd_terminal_lower_zero + S (0) = S ((S (l)) * uc)) /\ exists ff_q_lmd_terminal_lower_zero. ub = ff_q_lmd_terminal_lower_zero * S ((S (l)) * uc) + (0))) -> (exists lmd_mod_left_terminal_final lmd_mod_right_terminal_final. (C) + (p) * lmd_mod_left_terminal_final = (P) + (p) * lmd_mod_right_terminal_final)Constructive proof overview
Generated structural guide
Unconditional constructive Lucas theorem for any two genuinely terminating beta-coded prime-base digit streams: Choose(n,k) is congruent to the entire digitwise binomial product modulo p.
The unchanged tactic script uses 2 declared prerequisites and contains 62 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
Proof neighborhood
Direct dependencies
Direct dependents
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
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.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Fix variables and assumptionsL21–29
04Establish hglobalL30–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas terminating multidigit theorem from one step.
- L30Definitions: DigitLtPrimeModEqBetaAtProductChoose
have hglobal · expand full local formula (728 characters)
have hglobal : ∀ p. ∀ n. ∀ k. ∀ l. ∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ z. ∀ t. ∀ s. ∀ w. ∀ P. ∀ C. ∀ T. Prime(p) → BetaAt(qb,qc,0,n) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ m. ∃ i. BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,m) ∧ (BetaAt(db,dc,x,i) ∧ Digit(p,y,m,i)))) → BetaAt(ub,uc,0,k) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ m. ∃ i. BetaAt(ub,uc,x,y) ∧ (BetaAt(ub,uc,S x,m) ∧ (BetaAt(vb,vc,x,i) ∧ Digit(p,y,m,i)))) → (∀ x. Lt(x,S l) → ∃ y. ∃ m. ∃ i. BetaAt(qb,qc,x,y) ∧ (BetaAt(ub,uc,x,m) ∧ (BetaAt(z,t,x,i) ∧ Choose(y,m,i)))) → (∀ x. Lt(x,l) → ∃ y. ∃ m. ∃ i. BetaAt(db,dc,x,y) ∧ (BetaAt(vb,vc,x,m) ∧ (BetaAt(s,w,x,i) ∧ Choose(y,m,i)))) → Product(s,w,l,P) → BetaAt(z,t,0,C) → BetaAt(z,t,l,T) → BetaAt(qb,qc,l,0) → BetaAt(ub,uc,l,0) → ModEq(p,C,P) - L31
apply lucas_terminating_multidigit_theorem_from_one_step - L32
exact lucas_one_step_division_congruence - L33
specialize hglobal p - L34
specialize hglobal n - L35
specialize hglobal k - L36
specialize hglobal l - L37
specialize hglobal qb - L38
specialize hglobal qc - L39
specialize hglobal db
05Use earlier factsL40–49
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Use earlier factsL50–59
Original exact command ledger · 62 lines
- 0001
intro p - 0002
intro n - 0003
intro k - 0004
intro l - 0005
intro qb - 0006
intro qc - 0007
intro db - 0008
intro dc - 0009
intro ub - 0010
intro uc - 0011
intro vb - 0012
intro vc - 0013
intro z - 0014
intro t - 0015
intro s - 0016
intro w - 0017
intro P - 0018
intro C - 0019
intro T - 0020
intro hprime - 0021
intro hnchain - 0022
intro hkchain - 0023
intro hquotientchoose - 0024
intro hdigitchoose - 0025
intro hproduct - 0026
intro hstart - 0027
intro hterminal - 0028
intro hnzero - 0029
intro hkzero - 0030
have hglobal : forall p n k l qb qc db dc ub uc vb vc z t s w P C T. ((~(p = 1) /\ forall frm_prime_left_lmd_terminal_prime frm_prime_right_lmd_terminal_prime. p = frm_prime_left_lmd_terminal_prime * frm_prime_right_lmd_terminal_prime -> frm_prime_left_lmd_terminal_prime = 1 \/ frm_prime_right_lmd_terminal_prime = 1)) -> (((((exists ff_h_lmd_full_n_initial. ff_h_lmd_full_n_initial + S (n) = S ((S (0)) * qc)) /\ exists ff_q_lmd_full_n_initial. qb = ff_q_lmd_full_n_initial * S ((S (0)) * qc) + (n))) /\ forall lmd_index_full_n. (exists lmd_gap_full_n_index. lmd_gap_full_n_index + S (lmd_index_full_n) = (l)) -> exists lmd_current_full_n lmd_successor_full_n lmd_digit_full_n. ((((exists ff_h_lmd_full_n_current. ff_h_lmd_full_n_current + S (lmd_current_full_n) = S ((S (lmd_index_full_n)) * qc)) /\ exists ff_q_lmd_full_n_current. qb = ff_q_lmd_full_n_current * S ((S (lmd_index_full_n)) * qc) + (lmd_current_full_n))) /\ ((((exists ff_h_lmd_full_n_successor. ff_h_lmd_full_n_successor + S (lmd_successor_full_n) = S ((S (S lmd_index_full_n)) * qc)) /\ exists ff_q_lmd_full_n_successor. qb = ff_q_lmd_full_n_successor * S ((S (S lmd_index_full_n)) * qc) + (lmd_successor_full_n))) /\ ((((exists ff_h_lmd_full_n_digit. ff_h_lmd_full_n_digit + S (lmd_digit_full_n) = S ((S (lmd_index_full_n)) * dc)) /\ exists ff_q_lmd_full_n_digit. db = ff_q_lmd_full_n_digit * S ((S (lmd_index_full_n)) * dc) + (lmd_digit_full_n))) /\ ((lmd_current_full_n = (p) * (lmd_successor_full_n) + (lmd_digit_full_n)) /\ (exists lmd_gap_full_n_digit_bound. lmd_gap_full_n_digit_bound + S (lmd_digit_full_n) = (p)))))))) -> (((((exists ff_h_lmd_full_k_initial. ff_h_lmd_full_k_initial + S (k) = S ((S (0)) * uc)) /\ exists ff_q_lmd_full_k_initial. ub = ff_q_lmd_full_k_initial * S ((S (0)) * uc) + (k))) /\ forall lmd_index_full_k. (exists lmd_gap_full_k_index. lmd_gap_full_k_index + S (lmd_index_full_k) = (l)) -> exists lmd_current_full_k lmd_successor_full_k lmd_digit_full_k. ((((exists ff_h_lmd_full_k_current. ff_h_lmd_full_k_current + S (lmd_current_full_k) = S ((S (lmd_index_full_k)) * uc)) /\ exists ff_q_lmd_full_k_current. ub = ff_q_lmd_full_k_current * S ((S (lmd_index_full_k)) * uc) + (lmd_current_full_k))) /\ ((((exists ff_h_lmd_full_k_successor. ff_h_lmd_full_k_successor + S (lmd_successor_full_k) = S ((S (S lmd_index_full_k)) * uc)) /\ exists ff_q_lmd_full_k_successor. ub = ff_q_lmd_full_k_successor * S ((S (S lmd_index_full_k)) * uc) + (lmd_successor_full_k))) /\ ((((exists ff_h_lmd_full_k_digit. ff_h_lmd_full_k_digit + S (lmd_digit_full_k) = S ((S (lmd_index_full_k)) * vc)) /\ exists ff_q_lmd_full_k_digit. vb = ff_q_lmd_full_k_digit * S ((S (lmd_index_full_k)) * vc) + (lmd_digit_full_k))) /\ ((lmd_current_full_k = (p) * (lmd_successor_full_k) + (lmd_digit_full_k)) /\ (exists lmd_gap_full_k_digit_bound. lmd_gap_full_k_digit_bound + S (lmd_digit_full_k) = (p)))))))) -> (forall lmd_choose_index_full_quotient_choose. (exists lmd_gap_full_quotient_choose_bound. lmd_gap_full_quotient_choose_bound + S (lmd_choose_index_full_quotient_choose) = (S l)) -> exists lmd_choose_upper_full_quotient_choose lmd_choose_lower_full_quotient_choose lmd_choose_value_full_quotient_choose. ((((exists ff_h_lmd_full_quotient_choose_upper. ff_h_lmd_full_quotient_choose_upper + S (lmd_choose_upper_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * qc)) /\ exists ff_q_lmd_full_quotient_choose_upper. qb = ff_q_lmd_full_quotient_choose_upper * S ((S (lmd_choose_index_full_quotient_choose)) * qc) + (lmd_choose_upper_full_quotient_choose))) /\ ((((exists ff_h_lmd_full_quotient_choose_lower. ff_h_lmd_full_quotient_choose_lower + S (lmd_choose_lower_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * uc)) /\ exists ff_q_lmd_full_quotient_choose_lower. ub = ff_q_lmd_full_quotient_choose_lower * S ((S (lmd_choose_index_full_quotient_choose)) * uc) + (lmd_choose_lower_full_quotient_choose))) /\ ((((exists ff_h_lmd_full_quotient_choose_result. ff_h_lmd_full_quotient_choose_result + S (lmd_choose_value_full_quotient_choose) = S ((S (lmd_choose_index_full_quotient_choose)) * t)) /\ exists ff_q_lmd_full_quotient_choose_result. z = ff_q_lmd_full_quotient_choose_result * S ((S (lmd_choose_index_full_quotient_choose)) * t) + (lmd_choose_value_full_quotient_choose))) /\ (((exists bcf_lt_gap_lmd_full_quotient_choose_choose_out_of_range. bcf_lt_gap_lmd_full_quotient_choose_choose_out_of_range + S (lmd_choose_upper_full_quotient_choose) = lmd_choose_lower_full_quotient_choose) /\ lmd_choose_value_full_quotient_choose = 0) \/ ((exists bcf_le_gap_lmd_full_quotient_choose_choose_in_range. bcf_le_gap_lmd_full_quotient_choose_choose_in_range + (lmd_choose_lower_full_quotient_choose) = lmd_choose_upper_full_quotient_choose) /\ (exists bcf_row_code_code_lmd_full_quotient_choose_choose bcf_row_code_scale_lmd_full_quotient_choose_choose bcf_row_scale_code_lmd_full_quotient_choose_choose bcf_row_scale_scale_lmd_full_quotient_choose_choose bcf_row_code_lmd_full_quotient_choose_choose bcf_row_scale_lmd_full_quotient_choose_choose. ((forall bcf_row_index_lmd_full_quotient_choose_choose_table. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_bound + S (bcf_row_index_lmd_full_quotient_choose_choose_table) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_row_code_lmd_full_quotient_choose_choose_table bcf_row_scale_lmd_full_quotient_choose_choose_table. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_code. bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_code + S (bcf_row_code_lmd_full_quotient_choose_choose_table) = S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_row_code_lmd_full_quotient_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_scale. bcf_height_lmd_full_quotient_choose_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_full_quotient_choose_choose_table) = S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_row_scale_lmd_full_quotient_choose_choose_table))) /\ ((bcf_row_index_lmd_full_quotient_choose_choose_table = 0 /\ (forall bcf_index_lmd_full_quotient_choose_choose_table_zero_row. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_zero_row_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_zero_row_bound + S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_value_lmd_full_quotient_choose_choose_table_zero_row. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_zero_row_entry. bcf_height_lmd_full_quotient_choose_choose_table_zero_row_entry + S (bcf_value_lmd_full_quotient_choose_choose_table_zero_row) = S ((S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_zero_row_entry. bcf_row_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_zero_row_entry * S ((S (bcf_index_lmd_full_quotient_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_quotient_choose_choose_table) + (bcf_value_lmd_full_quotient_choose_choose_table_zero_row))) /\ ((bcf_index_lmd_full_quotient_choose_choose_table_zero_row = 0 /\ bcf_value_lmd_full_quotient_choose_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table_zero_row. bcf_index_lmd_full_quotient_choose_choose_table_zero_row = S bcf_predecessor_lmd_full_quotient_choose_choose_table_zero_row /\ bcf_value_lmd_full_quotient_choose_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table bcf_previous_code_lmd_full_quotient_choose_choose_table bcf_previous_scale_lmd_full_quotient_choose_choose_table. bcf_row_index_lmd_full_quotient_choose_choose_table = S bcf_predecessor_lmd_full_quotient_choose_choose_table /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_code. bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_full_quotient_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_previous_code_lmd_full_quotient_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_scale. bcf_height_lmd_full_quotient_choose_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_full_quotient_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_previous_scale_lmd_full_quotient_choose_choose_table))) /\ (forall bcf_index_lmd_full_quotient_choose_choose_table_row_step. (exists bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_step_bound. bcf_lt_gap_lmd_full_quotient_choose_choose_table_row_step_bound + S (bcf_index_lmd_full_quotient_choose_choose_table_row_step) = S (lmd_choose_upper_full_quotient_choose)) -> exists bcf_value_lmd_full_quotient_choose_choose_table_row_step. ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_entry. bcf_height_lmd_full_quotient_choose_choose_table_row_step_entry + S (bcf_value_lmd_full_quotient_choose_choose_table_row_step) = S ((S (bcf_index_lmd_full_quotient_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_entry. bcf_row_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_entry * S ((S (bcf_index_lmd_full_quotient_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_quotient_choose_choose_table) + (bcf_value_lmd_full_quotient_choose_choose_table_row_step))) /\ ((bcf_index_lmd_full_quotient_choose_choose_table_row_step = 0 /\ bcf_value_lmd_full_quotient_choose_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step bcf_left_lmd_full_quotient_choose_choose_table_row_step bcf_right_lmd_full_quotient_choose_choose_table_row_step. bcf_index_lmd_full_quotient_choose_choose_table_row_step = S bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_left. bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_left + S (bcf_left_lmd_full_quotient_choose_choose_table_row_step) = S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_left. bcf_previous_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_quotient_choose_choose_table) + (bcf_left_lmd_full_quotient_choose_choose_table_row_step))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_right. bcf_height_lmd_full_quotient_choose_choose_table_row_step_previous_right + S (bcf_right_lmd_full_quotient_choose_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_quotient_choose_choose_table)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_right. bcf_previous_code_lmd_full_quotient_choose_choose_table = bcf_quotient_lmd_full_quotient_choose_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_full_quotient_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_quotient_choose_choose_table) + (bcf_right_lmd_full_quotient_choose_choose_table_row_step))) /\ bcf_value_lmd_full_quotient_choose_choose_table_row_step = bcf_left_lmd_full_quotient_choose_choose_table_row_step + bcf_right_lmd_full_quotient_choose_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_decoded_row_code. bcf_height_lmd_full_quotient_choose_choose_decoded_row_code + S (bcf_row_code_lmd_full_quotient_choose_choose) = S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_code_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_code. bcf_row_code_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_code * S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_code_scale_lmd_full_quotient_choose_choose) + (bcf_row_code_lmd_full_quotient_choose_choose))) /\ ((((exists bcf_height_lmd_full_quotient_choose_choose_decoded_row_scale. bcf_height_lmd_full_quotient_choose_choose_decoded_row_scale + S (bcf_row_scale_lmd_full_quotient_choose_choose) = S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_scale. bcf_row_scale_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_row_scale * S ((S (lmd_choose_upper_full_quotient_choose)) * bcf_row_scale_scale_lmd_full_quotient_choose_choose) + (bcf_row_scale_lmd_full_quotient_choose_choose))) /\ (((exists bcf_height_lmd_full_quotient_choose_choose_decoded_value. bcf_height_lmd_full_quotient_choose_choose_decoded_value + S (lmd_choose_value_full_quotient_choose) = S ((S (lmd_choose_lower_full_quotient_choose)) * bcf_row_scale_lmd_full_quotient_choose_choose)) /\ exists bcf_quotient_lmd_full_quotient_choose_choose_decoded_value. bcf_row_code_lmd_full_quotient_choose_choose = bcf_quotient_lmd_full_quotient_choose_choose_decoded_value * S ((S (lmd_choose_lower_full_quotient_choose)) * bcf_row_scale_lmd_full_quotient_choose_choose) + (lmd_choose_value_full_quotient_choose))))))))))))) -> (forall lmd_choose_index_full_digit_choose. (exists lmd_gap_full_digit_choose_bound. lmd_gap_full_digit_choose_bound + S (lmd_choose_index_full_digit_choose) = (l)) -> exists lmd_choose_upper_full_digit_choose lmd_choose_lower_full_digit_choose lmd_choose_value_full_digit_choose. ((((exists ff_h_lmd_full_digit_choose_upper. ff_h_lmd_full_digit_choose_upper + S (lmd_choose_upper_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * dc)) /\ exists ff_q_lmd_full_digit_choose_upper. db = ff_q_lmd_full_digit_choose_upper * S ((S (lmd_choose_index_full_digit_choose)) * dc) + (lmd_choose_upper_full_digit_choose))) /\ ((((exists ff_h_lmd_full_digit_choose_lower. ff_h_lmd_full_digit_choose_lower + S (lmd_choose_lower_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * vc)) /\ exists ff_q_lmd_full_digit_choose_lower. vb = ff_q_lmd_full_digit_choose_lower * S ((S (lmd_choose_index_full_digit_choose)) * vc) + (lmd_choose_lower_full_digit_choose))) /\ ((((exists ff_h_lmd_full_digit_choose_result. ff_h_lmd_full_digit_choose_result + S (lmd_choose_value_full_digit_choose) = S ((S (lmd_choose_index_full_digit_choose)) * w)) /\ exists ff_q_lmd_full_digit_choose_result. s = ff_q_lmd_full_digit_choose_result * S ((S (lmd_choose_index_full_digit_choose)) * w) + (lmd_choose_value_full_digit_choose))) /\ (((exists bcf_lt_gap_lmd_full_digit_choose_choose_out_of_range. bcf_lt_gap_lmd_full_digit_choose_choose_out_of_range + S (lmd_choose_upper_full_digit_choose) = lmd_choose_lower_full_digit_choose) /\ lmd_choose_value_full_digit_choose = 0) \/ ((exists bcf_le_gap_lmd_full_digit_choose_choose_in_range. bcf_le_gap_lmd_full_digit_choose_choose_in_range + (lmd_choose_lower_full_digit_choose) = lmd_choose_upper_full_digit_choose) /\ (exists bcf_row_code_code_lmd_full_digit_choose_choose bcf_row_code_scale_lmd_full_digit_choose_choose bcf_row_scale_code_lmd_full_digit_choose_choose bcf_row_scale_scale_lmd_full_digit_choose_choose bcf_row_code_lmd_full_digit_choose_choose bcf_row_scale_lmd_full_digit_choose_choose. ((forall bcf_row_index_lmd_full_digit_choose_choose_table. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_row_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_row_bound + S (bcf_row_index_lmd_full_digit_choose_choose_table) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_row_code_lmd_full_digit_choose_choose_table bcf_row_scale_lmd_full_digit_choose_choose_table. ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_row_code. bcf_height_lmd_full_digit_choose_choose_table_decoded_row_code + S (bcf_row_code_lmd_full_digit_choose_choose_table) = S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_row_code_lmd_full_digit_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_row_scale. bcf_height_lmd_full_digit_choose_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_full_digit_choose_choose_table) = S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_row_scale_lmd_full_digit_choose_choose_table))) /\ ((bcf_row_index_lmd_full_digit_choose_choose_table = 0 /\ (forall bcf_index_lmd_full_digit_choose_choose_table_zero_row. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_zero_row_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_zero_row_bound + S (bcf_index_lmd_full_digit_choose_choose_table_zero_row) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_value_lmd_full_digit_choose_choose_table_zero_row. ((((exists bcf_height_lmd_full_digit_choose_choose_table_zero_row_entry. bcf_height_lmd_full_digit_choose_choose_table_zero_row_entry + S (bcf_value_lmd_full_digit_choose_choose_table_zero_row) = S ((S (bcf_index_lmd_full_digit_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_zero_row_entry. bcf_row_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_zero_row_entry * S ((S (bcf_index_lmd_full_digit_choose_choose_table_zero_row)) * bcf_row_scale_lmd_full_digit_choose_choose_table) + (bcf_value_lmd_full_digit_choose_choose_table_zero_row))) /\ ((bcf_index_lmd_full_digit_choose_choose_table_zero_row = 0 /\ bcf_value_lmd_full_digit_choose_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table_zero_row. bcf_index_lmd_full_digit_choose_choose_table_zero_row = S bcf_predecessor_lmd_full_digit_choose_choose_table_zero_row /\ bcf_value_lmd_full_digit_choose_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table bcf_previous_code_lmd_full_digit_choose_choose_table bcf_previous_scale_lmd_full_digit_choose_choose_table. bcf_row_index_lmd_full_digit_choose_choose_table = S bcf_predecessor_lmd_full_digit_choose_choose_table /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_code. bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_full_digit_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_previous_code_lmd_full_digit_choose_choose_table))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_scale. bcf_height_lmd_full_digit_choose_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_full_digit_choose_choose_table) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_previous_scale_lmd_full_digit_choose_choose_table))) /\ (forall bcf_index_lmd_full_digit_choose_choose_table_row_step. (exists bcf_lt_gap_lmd_full_digit_choose_choose_table_row_step_bound. bcf_lt_gap_lmd_full_digit_choose_choose_table_row_step_bound + S (bcf_index_lmd_full_digit_choose_choose_table_row_step) = S (lmd_choose_upper_full_digit_choose)) -> exists bcf_value_lmd_full_digit_choose_choose_table_row_step. ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_entry. bcf_height_lmd_full_digit_choose_choose_table_row_step_entry + S (bcf_value_lmd_full_digit_choose_choose_table_row_step) = S ((S (bcf_index_lmd_full_digit_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_entry. bcf_row_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_entry * S ((S (bcf_index_lmd_full_digit_choose_choose_table_row_step)) * bcf_row_scale_lmd_full_digit_choose_choose_table) + (bcf_value_lmd_full_digit_choose_choose_table_row_step))) /\ ((bcf_index_lmd_full_digit_choose_choose_table_row_step = 0 /\ bcf_value_lmd_full_digit_choose_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_full_digit_choose_choose_table_row_step bcf_left_lmd_full_digit_choose_choose_table_row_step bcf_right_lmd_full_digit_choose_choose_table_row_step. bcf_index_lmd_full_digit_choose_choose_table_row_step = S bcf_predecessor_lmd_full_digit_choose_choose_table_row_step /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_left. bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_left + S (bcf_left_lmd_full_digit_choose_choose_table_row_step) = S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_left. bcf_previous_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step)) * bcf_previous_scale_lmd_full_digit_choose_choose_table) + (bcf_left_lmd_full_digit_choose_choose_table_row_step))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_right. bcf_height_lmd_full_digit_choose_choose_table_row_step_previous_right + S (bcf_right_lmd_full_digit_choose_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_digit_choose_choose_table)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_right. bcf_previous_code_lmd_full_digit_choose_choose_table = bcf_quotient_lmd_full_digit_choose_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_full_digit_choose_choose_table_row_step))) * bcf_previous_scale_lmd_full_digit_choose_choose_table) + (bcf_right_lmd_full_digit_choose_choose_table_row_step))) /\ bcf_value_lmd_full_digit_choose_choose_table_row_step = bcf_left_lmd_full_digit_choose_choose_table_row_step + bcf_right_lmd_full_digit_choose_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_decoded_row_code. bcf_height_lmd_full_digit_choose_choose_decoded_row_code + S (bcf_row_code_lmd_full_digit_choose_choose) = S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_code_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_row_code. bcf_row_code_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_row_code * S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_code_scale_lmd_full_digit_choose_choose) + (bcf_row_code_lmd_full_digit_choose_choose))) /\ ((((exists bcf_height_lmd_full_digit_choose_choose_decoded_row_scale. bcf_height_lmd_full_digit_choose_choose_decoded_row_scale + S (bcf_row_scale_lmd_full_digit_choose_choose) = S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_scale_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_row_scale. bcf_row_scale_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_row_scale * S ((S (lmd_choose_upper_full_digit_choose)) * bcf_row_scale_scale_lmd_full_digit_choose_choose) + (bcf_row_scale_lmd_full_digit_choose_choose))) /\ (((exists bcf_height_lmd_full_digit_choose_choose_decoded_value. bcf_height_lmd_full_digit_choose_choose_decoded_value + S (lmd_choose_value_full_digit_choose) = S ((S (lmd_choose_lower_full_digit_choose)) * bcf_row_scale_lmd_full_digit_choose_choose)) /\ exists bcf_quotient_lmd_full_digit_choose_choose_decoded_value. bcf_row_code_lmd_full_digit_choose_choose = bcf_quotient_lmd_full_digit_choose_choose_decoded_value * S ((S (lmd_choose_lower_full_digit_choose)) * bcf_row_scale_lmd_full_digit_choose_choose) + (lmd_choose_value_full_digit_choose))))))))))))) -> (exists ff_u_lmd_full_product ff_v_lmd_full_product. ((((exists ff_h_lmd_full_product_start. ff_h_lmd_full_product_start + S (1) = S ((S (0)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_start. ff_u_lmd_full_product = ff_q_lmd_full_product_start * S ((S (0)) * ff_v_lmd_full_product) + (1))) /\ ((((exists ff_h_lmd_full_product_terminal. ff_h_lmd_full_product_terminal + S (P) = S ((S (l)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_terminal. ff_u_lmd_full_product = ff_q_lmd_full_product_terminal * S ((S (l)) * ff_v_lmd_full_product) + (P))) /\ forall ff_i_lmd_full_product. (exists ff_lt_lmd_full_product_bound. ff_lt_lmd_full_product_bound + S ff_i_lmd_full_product = l) -> exists ff_p_lmd_full_product ff_r_lmd_full_product ff_s_lmd_full_product. ((((exists ff_h_lmd_full_product_factor. ff_h_lmd_full_product_factor + S (ff_p_lmd_full_product) = S ((S (ff_i_lmd_full_product)) * w)) /\ exists ff_q_lmd_full_product_factor. s = ff_q_lmd_full_product_factor * S ((S (ff_i_lmd_full_product)) * w) + (ff_p_lmd_full_product))) /\ ((((exists ff_h_lmd_full_product_partial. ff_h_lmd_full_product_partial + S (ff_r_lmd_full_product) = S ((S (ff_i_lmd_full_product)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_partial. ff_u_lmd_full_product = ff_q_lmd_full_product_partial * S ((S (ff_i_lmd_full_product)) * ff_v_lmd_full_product) + (ff_r_lmd_full_product))) /\ ((((exists ff_h_lmd_full_product_successor. ff_h_lmd_full_product_successor + S (ff_s_lmd_full_product) = S ((S (S ff_i_lmd_full_product)) * ff_v_lmd_full_product)) /\ exists ff_q_lmd_full_product_successor. ff_u_lmd_full_product = ff_q_lmd_full_product_successor * S ((S (S ff_i_lmd_full_product)) * ff_v_lmd_full_product) + (ff_s_lmd_full_product))) /\ ff_s_lmd_full_product = ff_r_lmd_full_product * ff_p_lmd_full_product)))))) -> (((exists ff_h_lmd_full_coefficient_start. ff_h_lmd_full_coefficient_start + S (C) = S ((S (0)) * t)) /\ exists ff_q_lmd_full_coefficient_start. z = ff_q_lmd_full_coefficient_start * S ((S (0)) * t) + (C))) -> (((exists ff_h_lmd_full_coefficient_end. ff_h_lmd_full_coefficient_end + S (T) = S ((S (l)) * t)) /\ exists ff_q_lmd_full_coefficient_end. z = ff_q_lmd_full_coefficient_end * S ((S (l)) * t) + (T))) -> (((exists ff_h_lmd_terminal_upper_zero. ff_h_lmd_terminal_upper_zero + S (0) = S ((S (l)) * qc)) /\ exists ff_q_lmd_terminal_upper_zero. qb = ff_q_lmd_terminal_upper_zero * S ((S (l)) * qc) + (0))) -> (((exists ff_h_lmd_terminal_lower_zero. ff_h_lmd_terminal_lower_zero + S (0) = S ((S (l)) * uc)) /\ exists ff_q_lmd_terminal_lower_zero. ub = ff_q_lmd_terminal_lower_zero * S ((S (l)) * uc) + (0))) -> (exists lmd_mod_left_terminal_final lmd_mod_right_terminal_final. (C) + (p) * lmd_mod_left_terminal_final = (P) + (p) * lmd_mod_right_terminal_final) - 0031
apply lucas_terminating_multidigit_theorem_from_one_step - 0032
exact lucas_one_step_division_congruence - 0033
specialize hglobal p - 0034
specialize hglobal n - 0035
specialize hglobal k - 0036
specialize hglobal l - 0037
specialize hglobal qb - 0038
specialize hglobal qc - 0039
specialize hglobal db - 0040
specialize hglobal dc - 0041
specialize hglobal ub - 0042
specialize hglobal uc - 0043
specialize hglobal vb - 0044
specialize hglobal vc - 0045
specialize hglobal z - 0046
specialize hglobal t - 0047
specialize hglobal s - 0048
specialize hglobal w - 0049
specialize hglobal P - 0050
specialize hglobal C - 0051
specialize hglobal T - 0052
apply hglobal - 0053
exact hprime - 0054
exact hnchain - 0055
exact hkchain - 0056
exact hquotientchoose - 0057
exact hdigitchoose - 0058
exact hproduct - 0059
exact hstart - 0060
exact hterminal - 0061
exact hnzero - 0062
exact hkzero