LU000M

lucas_prime_block_digit_congruence

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

The complete prime-base Lucas one-digit block congruence holds for arbitrary upper and lower quotients and both bounded digits.

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 q r d e C A B. ((~(p = 1) /\ forall frm_prime_left_lucas_block_digit_prime frm_prime_right_lucas_block_digit_prime. p = frm_prime_left_lucas_block_digit_prime * frm_prime_right_lucas_block_digit_prime -> frm_prime_left_lucas_block_digit_prime = 1 \/ frm_prime_right_lucas_block_digit_prime = 1)) -> (exists lbd_gap_canonical_upper_bound. lbd_gap_canonical_upper_bound + S (d) = (p)) -> (exists lbd_gap_canonical_lower_bound. lbd_gap_canonical_lower_bound + S (e) = (p)) -> (((exists bcf_lt_gap_lucas_block_digit_canonical_whole_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_whole_out_of_range + S (p * q + d) = p * r + e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_whole_in_range. bcf_le_gap_lucas_block_digit_canonical_whole_in_range + (p * r + e) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_whole bcf_row_code_scale_lucas_block_digit_canonical_whole bcf_row_scale_code_lucas_block_digit_canonical_whole bcf_row_scale_scale_lucas_block_digit_canonical_whole bcf_row_code_lucas_block_digit_canonical_whole bcf_row_scale_lucas_block_digit_canonical_whole. ((forall bcf_row_index_lucas_block_digit_canonical_whole_table. (exists bcf_lt_gap_lucas_block_digit_canonical_whole_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_whole_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_whole_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_canonical_whole_table bcf_row_scale_lucas_block_digit_canonical_whole_table. ((((exists bcf_height_lucas_block_digit_canonical_whole_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_whole_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_whole_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_whole_table)) * bcf_row_code_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_whole_table)) * bcf_row_code_scale_lucas_block_digit_canonical_whole) + (bcf_row_code_lucas_block_digit_canonical_whole_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_whole_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_whole_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_whole_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_whole_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole) + (bcf_row_scale_lucas_block_digit_canonical_whole_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_whole_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_whole_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_whole_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_whole_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_whole_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_whole_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_whole_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_whole_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_whole_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_whole_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_whole_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_whole_table = bcf_quotient_lucas_block_digit_canonical_whole_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_whole_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_whole_table) + (bcf_value_lucas_block_digit_canonical_whole_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_whole_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_whole_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_whole_table_zero_row. bcf_index_lucas_block_digit_canonical_whole_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_whole_table_zero_row /\ bcf_value_lucas_block_digit_canonical_whole_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_whole_table bcf_previous_code_lucas_block_digit_canonical_whole_table bcf_previous_scale_lucas_block_digit_canonical_whole_table. bcf_row_index_lucas_block_digit_canonical_whole_table = S bcf_predecessor_lucas_block_digit_canonical_whole_table /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_whole_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_whole_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table)) * bcf_row_code_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table)) * bcf_row_code_scale_lucas_block_digit_canonical_whole) + (bcf_previous_code_lucas_block_digit_canonical_whole_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_whole_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_whole_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole) + (bcf_previous_scale_lucas_block_digit_canonical_whole_table))) /\ (forall bcf_index_lucas_block_digit_canonical_whole_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_whole_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_whole_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_whole_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_whole_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_whole_table_row_step_entry. bcf_height_lucas_block_digit_canonical_whole_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_whole_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_whole_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_whole_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_whole_table = bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_whole_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_whole_table) + (bcf_value_lucas_block_digit_canonical_whole_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_whole_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_whole_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step bcf_left_lucas_block_digit_canonical_whole_table_row_step bcf_right_lucas_block_digit_canonical_whole_table_row_step. bcf_index_lucas_block_digit_canonical_whole_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_whole_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_whole_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_whole_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_whole_table = bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_whole_table) + (bcf_left_lucas_block_digit_canonical_whole_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_whole_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_whole_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_whole_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_whole_table = bcf_quotient_lucas_block_digit_canonical_whole_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_whole_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_whole_table) + (bcf_right_lucas_block_digit_canonical_whole_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_whole_table_row_step = bcf_left_lucas_block_digit_canonical_whole_table_row_step + bcf_right_lucas_block_digit_canonical_whole_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_decoded_row_code. bcf_height_lucas_block_digit_canonical_whole_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_whole) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_whole) + (bcf_row_code_lucas_block_digit_canonical_whole))) /\ ((((exists bcf_height_lucas_block_digit_canonical_whole_decoded_row_scale. bcf_height_lucas_block_digit_canonical_whole_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_whole) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_whole) + (bcf_row_scale_lucas_block_digit_canonical_whole))) /\ (((exists bcf_height_lucas_block_digit_canonical_whole_decoded_value. bcf_height_lucas_block_digit_canonical_whole_decoded_value + S (C) = S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_canonical_whole)) /\ exists bcf_quotient_lucas_block_digit_canonical_whole_decoded_value. bcf_row_code_lucas_block_digit_canonical_whole = bcf_quotient_lucas_block_digit_canonical_whole_decoded_value * S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_canonical_whole) + (C))))))))) -> (((exists bcf_lt_gap_lucas_block_digit_canonical_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_quotient_out_of_range + S (q) = r) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_quotient_in_range. bcf_le_gap_lucas_block_digit_canonical_quotient_in_range + (r) = q) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_quotient bcf_row_code_scale_lucas_block_digit_canonical_quotient bcf_row_scale_code_lucas_block_digit_canonical_quotient bcf_row_scale_scale_lucas_block_digit_canonical_quotient bcf_row_code_lucas_block_digit_canonical_quotient bcf_row_scale_lucas_block_digit_canonical_quotient. ((forall bcf_row_index_lucas_block_digit_canonical_quotient_table. (exists bcf_lt_gap_lucas_block_digit_canonical_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_quotient_table) = S (q)) -> exists bcf_row_code_lucas_block_digit_canonical_quotient_table bcf_row_scale_lucas_block_digit_canonical_quotient_table. ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient) + (bcf_row_code_lucas_block_digit_canonical_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient) + (bcf_row_scale_lucas_block_digit_canonical_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_quotient_table_zero_row) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_quotient_table = bcf_quotient_lucas_block_digit_canonical_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_quotient_table) + (bcf_value_lucas_block_digit_canonical_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_quotient_table_zero_row. bcf_index_lucas_block_digit_canonical_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_quotient_table_zero_row /\ bcf_value_lucas_block_digit_canonical_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_quotient_table bcf_previous_code_lucas_block_digit_canonical_quotient_table bcf_previous_scale_lucas_block_digit_canonical_quotient_table. bcf_row_index_lucas_block_digit_canonical_quotient_table = S bcf_predecessor_lucas_block_digit_canonical_quotient_table /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient) + (bcf_previous_code_lucas_block_digit_canonical_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient) + (bcf_previous_scale_lucas_block_digit_canonical_quotient_table))) /\ (forall bcf_index_lucas_block_digit_canonical_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_quotient_table_row_step) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_row_step_entry. bcf_height_lucas_block_digit_canonical_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_quotient_table = bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_quotient_table) + (bcf_value_lucas_block_digit_canonical_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step bcf_left_lucas_block_digit_canonical_quotient_table_row_step bcf_right_lucas_block_digit_canonical_quotient_table_row_step. bcf_index_lucas_block_digit_canonical_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_quotient_table = bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_quotient_table) + (bcf_left_lucas_block_digit_canonical_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_quotient_table = bcf_quotient_lucas_block_digit_canonical_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_quotient_table) + (bcf_right_lucas_block_digit_canonical_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_quotient_table_row_step = bcf_left_lucas_block_digit_canonical_quotient_table_row_step + bcf_right_lucas_block_digit_canonical_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_decoded_row_code. bcf_height_lucas_block_digit_canonical_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_quotient) = S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_decoded_row_code * S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_quotient) + (bcf_row_code_lucas_block_digit_canonical_quotient))) /\ ((((exists bcf_height_lucas_block_digit_canonical_quotient_decoded_row_scale. bcf_height_lucas_block_digit_canonical_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_quotient) = S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_decoded_row_scale * S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_quotient) + (bcf_row_scale_lucas_block_digit_canonical_quotient))) /\ (((exists bcf_height_lucas_block_digit_canonical_quotient_decoded_value. bcf_height_lucas_block_digit_canonical_quotient_decoded_value + S (A) = S ((S (r)) * bcf_row_scale_lucas_block_digit_canonical_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_quotient_decoded_value. bcf_row_code_lucas_block_digit_canonical_quotient = bcf_quotient_lucas_block_digit_canonical_quotient_decoded_value * S ((S (r)) * bcf_row_scale_lucas_block_digit_canonical_quotient) + (A))))))))) -> (((exists bcf_lt_gap_lucas_block_digit_canonical_digit_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_digit_out_of_range + S (d) = e) /\ B = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_digit_in_range. bcf_le_gap_lucas_block_digit_canonical_digit_in_range + (e) = d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_digit bcf_row_code_scale_lucas_block_digit_canonical_digit bcf_row_scale_code_lucas_block_digit_canonical_digit bcf_row_scale_scale_lucas_block_digit_canonical_digit bcf_row_code_lucas_block_digit_canonical_digit bcf_row_scale_lucas_block_digit_canonical_digit. ((forall bcf_row_index_lucas_block_digit_canonical_digit_table. (exists bcf_lt_gap_lucas_block_digit_canonical_digit_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_digit_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_digit_table) = S (d)) -> exists bcf_row_code_lucas_block_digit_canonical_digit_table bcf_row_scale_lucas_block_digit_canonical_digit_table. ((((exists bcf_height_lucas_block_digit_canonical_digit_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_digit_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_digit_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_digit_table)) * bcf_row_code_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_digit_table)) * bcf_row_code_scale_lucas_block_digit_canonical_digit) + (bcf_row_code_lucas_block_digit_canonical_digit_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_digit_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_digit_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_digit_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_digit_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit) + (bcf_row_scale_lucas_block_digit_canonical_digit_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_digit_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_digit_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_digit_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_digit_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_digit_table_zero_row) = S (d)) -> exists bcf_value_lucas_block_digit_canonical_digit_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_digit_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_digit_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_digit_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_digit_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_digit_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_digit_table = bcf_quotient_lucas_block_digit_canonical_digit_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_digit_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_digit_table) + (bcf_value_lucas_block_digit_canonical_digit_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_digit_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_digit_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_digit_table_zero_row. bcf_index_lucas_block_digit_canonical_digit_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_digit_table_zero_row /\ bcf_value_lucas_block_digit_canonical_digit_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_digit_table bcf_previous_code_lucas_block_digit_canonical_digit_table bcf_previous_scale_lucas_block_digit_canonical_digit_table. bcf_row_index_lucas_block_digit_canonical_digit_table = S bcf_predecessor_lucas_block_digit_canonical_digit_table /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_digit_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_digit_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table)) * bcf_row_code_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table)) * bcf_row_code_scale_lucas_block_digit_canonical_digit) + (bcf_previous_code_lucas_block_digit_canonical_digit_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_digit_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_digit_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit) + (bcf_previous_scale_lucas_block_digit_canonical_digit_table))) /\ (forall bcf_index_lucas_block_digit_canonical_digit_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_digit_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_digit_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_digit_table_row_step) = S (d)) -> exists bcf_value_lucas_block_digit_canonical_digit_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_digit_table_row_step_entry. bcf_height_lucas_block_digit_canonical_digit_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_digit_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_digit_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_digit_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_digit_table = bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_digit_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_digit_table) + (bcf_value_lucas_block_digit_canonical_digit_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_digit_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_digit_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step bcf_left_lucas_block_digit_canonical_digit_table_row_step bcf_right_lucas_block_digit_canonical_digit_table_row_step. bcf_index_lucas_block_digit_canonical_digit_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_digit_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_digit_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_digit_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_digit_table = bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_digit_table) + (bcf_left_lucas_block_digit_canonical_digit_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_digit_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_digit_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_digit_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_digit_table = bcf_quotient_lucas_block_digit_canonical_digit_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_digit_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_digit_table) + (bcf_right_lucas_block_digit_canonical_digit_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_digit_table_row_step = bcf_left_lucas_block_digit_canonical_digit_table_row_step + bcf_right_lucas_block_digit_canonical_digit_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_decoded_row_code. bcf_height_lucas_block_digit_canonical_digit_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_digit) = S ((S (d)) * bcf_row_code_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_decoded_row_code * S ((S (d)) * bcf_row_code_scale_lucas_block_digit_canonical_digit) + (bcf_row_code_lucas_block_digit_canonical_digit))) /\ ((((exists bcf_height_lucas_block_digit_canonical_digit_decoded_row_scale. bcf_height_lucas_block_digit_canonical_digit_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_digit) = S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_decoded_row_scale * S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_canonical_digit) + (bcf_row_scale_lucas_block_digit_canonical_digit))) /\ (((exists bcf_height_lucas_block_digit_canonical_digit_decoded_value. bcf_height_lucas_block_digit_canonical_digit_decoded_value + S (B) = S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_digit)) /\ exists bcf_quotient_lucas_block_digit_canonical_digit_decoded_value. bcf_row_code_lucas_block_digit_canonical_digit = bcf_quotient_lucas_block_digit_canonical_digit_decoded_value * S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_digit) + (B))))))))) -> (exists lbd_left_canonical_result lbd_right_canonical_result. (C) + (p) * lbd_left_canonical_result = (A * B) + (p) * lbd_right_canonical_result)

Constructive proof overview

Generated structural guide

The complete prime-base Lucas one-digit block congruence holds for arbitrary upper and lower quotients and both bounded digits.

The unchanged tactic script uses 18 declared prerequisites and contains 255 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

eq_decidable Stable theorem; checked-use authorized LU000O lucas_choose_lower_eq_transport LU0010 lucas_prime_block_zero_reassociation LU0014 lucas_low_digit_product_congruence LU000L lucas_zero_upper_quotient_high_column_vanishes LU000Q lucas_choose_zero_upper_positive_is_zero mul_zero_left Stable theorem; checked-use authorized mod_eq_refl Stable theorem; checked-use authorized nonzero_is_succ Stable theorem; checked-use authorized choose_upper_eq_transport Alpha theorem; checked-use authorized LU0011 lucas_prime_block_successor_reassociation choose_exists Alpha theorem; checked-use authorized LU000Z lucas_prime_shift_high_column choose_succ_succ Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized mod_eq_add Stable theorem; checked-use authorized add_mul Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized

Direct dependents

LU000N lucas_one_step_division_congruence

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

255 script commands · 48 reading checkpoints · 27 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.

Named ingredients (7)
lucas choose lower eq transportlucas prime block zero reassociationlucas low digit product congruencelucas zero upper quotient high column vanisheslucas choose zero upper positive is zerolucas prime block successor reassociationlucas prime shift high column

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–1

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

  1. L1
    intro p
02Induction on qL2–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction q
  2. L3
    intro r
  3. L4
    intro d
  4. L5
    intro e
  5. L6
    intro C
  6. L7
    intro A
  7. L8
    intro B
  8. L9
    intro hprime
  9. L10
    intro hdigit
  10. L11
    intro he_digit
03Fix variables and assumptionsL12–14

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

  1. L12
    intro hwhole
  2. L13
    intro hquotient
  3. L14
    intro hfactor
04Establish hcaseL15–18

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

  1. L15
    have hcase : r = 0 \/ ~(r = 0)
  2. L16
    specialize eq_decidable r
  3. L17
    specialize eq_decidable 0
  4. L18
    exact eq_decidable
05Separate the logical casesL19–19

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

  1. L19
    cases hcase
06Establish hindexL20–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime block zero reassociation.

  1. L20
    have hindex : p * r + e = e
  2. L21
    rewrite hcase_left
  3. L22
    apply lucas_prime_block_zero_reassociation
07Establish hnormalizedL23–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L23
    have hnormalized : Choose(p · 0 + d,e,C)Definitions: Choose
  2. L24
    specialize lucas_choose_lower_eq_transport (p * 0 + d)
  3. L25
    specialize lucas_choose_lower_eq_transport (p * r + e)
  4. L26
    specialize lucas_choose_lower_eq_transport e
  5. L27
    specialize lucas_choose_lower_eq_transport C
  6. L28
    apply lucas_choose_lower_eq_transport
  7. L29
    exact hindex
  8. L30
    exact hwhole
08Establish hquotient_zeroL31–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L31
    have hquotient_zero : Choose(0,0,A)Definitions: Choose
  2. L32
    specialize lucas_choose_lower_eq_transport 0
  3. L33
    specialize lucas_choose_lower_eq_transport r
  4. L34
    specialize lucas_choose_lower_eq_transport 0
  5. L35
    specialize lucas_choose_lower_eq_transport A
  6. L36
    apply lucas_choose_lower_eq_transport
  7. L37
    exact hcase_left
  8. L38
    exact hquotient
  9. L39
    specialize lucas_low_digit_product_congruence p
  10. L40
    specialize lucas_low_digit_product_congruence 0
09Use earlier factsL41–50

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

  1. L41
    specialize lucas_low_digit_product_congruence d
  2. L42
    specialize lucas_low_digit_product_congruence e
  3. L43
    specialize lucas_low_digit_product_congruence C
  4. L44
    specialize lucas_low_digit_product_congruence A
  5. L45
    specialize lucas_low_digit_product_congruence B
  6. L46
    apply lucas_low_digit_product_congruence
  7. L47
    exact hprime
  8. L48
    exact hdigit
  9. L49
    exact he_digit
  10. L50
    exact hnormalized
10Use earlier factsL51–52

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

  1. L51
    exact hquotient_zero
  2. L52
    exact hfactor
11Establish hwhole_zeroL53–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas zero upper quotient high column vanishes.

  1. L53
    have hwhole_zero : C = 0
  2. L54
    specialize lucas_zero_upper_quotient_high_column_vanishes p
  3. L55
    specialize lucas_zero_upper_quotient_high_column_vanishes r
  4. L56
    specialize lucas_zero_upper_quotient_high_column_vanishes d
  5. L57
    specialize lucas_zero_upper_quotient_high_column_vanishes e
  6. L58
    specialize lucas_zero_upper_quotient_high_column_vanishes C
  7. L59
    apply lucas_zero_upper_quotient_high_column_vanishes
  8. L60
    exact hdigit
  9. L61
    exact hcase_right
  10. L62
    exact hwhole
12Establish hquotient_zeroL63–72

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose zero upper positive is zero.

  1. L63
    have hquotient_zero : A = 0
  2. L64
    specialize lucas_choose_zero_upper_positive_is_zero r
  3. L65
    specialize lucas_choose_zero_upper_positive_is_zero A
  4. L66
    apply lucas_choose_zero_upper_positive_is_zero
  5. L67
    exact hcase_right
  6. L68
    exact hquotient
  7. L69
    rewrite hwhole_zero
  8. L70
    rewrite hquotient_zero
  9. L71
    specialize mul_zero_left B
  10. L72
    rewrite mul_zero_left
13Use earlier factsL73–73

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

  1. L73
    apply mod_eq_refl
14Fix variables and assumptionsL74–83

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

  1. L74
    intro r
  2. L75
    intro d
  3. L76
    intro e
  4. L77
    intro C
  5. L78
    intro A
  6. L79
    intro B
  7. L80
    intro hprime
  8. L81
    intro hdigit
  9. L82
    intro he_digit
  10. L83
    intro hwhole
15Fix variables and assumptionsL84–85

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

  1. L84
    intro hquotient
  2. L85
    intro hfactor
16Establish hcaseL86–89

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

  1. L86
    have hcase : r = 0 \/ ~(r = 0)
  2. L87
    specialize eq_decidable r
  3. L88
    specialize eq_decidable 0
  4. L89
    exact eq_decidable
17Separate the logical casesL90–90

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

  1. L90
    cases hcase
18Establish hindexL91–93

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime block zero reassociation.

  1. L91
    have hindex : p * r + e = e
  2. L92
    rewrite hcase_left
  3. L93
    apply lucas_prime_block_zero_reassociation
19Establish hnormalizedL94–101

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L94
    have hnormalized : Choose(p · S q + d,e,C)Definitions: Choose
  2. L95
    specialize lucas_choose_lower_eq_transport (p * S q + d)
  3. L96
    specialize lucas_choose_lower_eq_transport (p * r + e)
  4. L97
    specialize lucas_choose_lower_eq_transport e
  5. L98
    specialize lucas_choose_lower_eq_transport C
  6. L99
    apply lucas_choose_lower_eq_transport
  7. L100
    exact hindex
  8. L101
    exact hwhole
20Establish hquotient_zeroL102–111

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L102
    have hquotient_zero : Choose(S q,0,A)Definitions: Choose
  2. L103
    specialize lucas_choose_lower_eq_transport (S q)
  3. L104
    specialize lucas_choose_lower_eq_transport r
  4. L105
    specialize lucas_choose_lower_eq_transport 0
  5. L106
    specialize lucas_choose_lower_eq_transport A
  6. L107
    apply lucas_choose_lower_eq_transport
  7. L108
    exact hcase_left
  8. L109
    exact hquotient
  9. L110
    specialize lucas_low_digit_product_congruence p
  10. L111
    specialize lucas_low_digit_product_congruence (S q)
21Use earlier factsL112–121

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

  1. L112
    specialize lucas_low_digit_product_congruence d
  2. L113
    specialize lucas_low_digit_product_congruence e
  3. L114
    specialize lucas_low_digit_product_congruence C
  4. L115
    specialize lucas_low_digit_product_congruence A
  5. L116
    specialize lucas_low_digit_product_congruence B
  6. L117
    apply lucas_low_digit_product_congruence
  7. L118
    exact hprime
  8. L119
    exact hdigit
  9. L120
    exact he_digit
  10. L121
    exact hnormalized
22Use earlier factsL122–123

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

  1. L122
    exact hquotient_zero
  2. L123
    exact hfactor
23Establish hsuccessorL124–127

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

  1. L124
    have hsuccessor : exists t. r = S t
  2. L125
    specialize nonzero_is_succ r
  3. L126
    apply nonzero_is_succ
  4. L127
    exact hcase_right
24Separate the logical casesL128–128

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

  1. L128
    cases hsuccessor
25Establish hupper_normalL129–136

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose upper eq transport.

  1. L129
    have hupper_normal : Choose(p + (p · q + d),p · r + e,C)Definitions: Choose
  2. L130
    specialize choose_upper_eq_transport (p * S q + d)
  3. L131
    specialize choose_upper_eq_transport (p + (p * q + d))
  4. L132
    specialize choose_upper_eq_transport (p * r + e)
  5. L133
    specialize choose_upper_eq_transport C
  6. L134
    apply choose_upper_eq_transport
  7. L135
    apply lucas_prime_block_successor_reassociation
  8. L136
    exact hwhole
26Establish hindexL137–139

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime block successor reassociation.

  1. L137
    have hindex : p * r + e = p + (p * x + e)
  2. L138
    rewrite hsuccessor_witness
  3. L139
    apply lucas_prime_block_successor_reassociation
27Establish hnormalL140–147

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L140
    have hnormal : Choose(p + (p · q + d),p + (p · x + e),C)Definitions: Choose
  2. L141
    specialize lucas_choose_lower_eq_transport (p + (p * q + d))
  3. L142
    specialize lucas_choose_lower_eq_transport (p * r + e)
  4. L143
    specialize lucas_choose_lower_eq_transport (p + (p * x + e))
  5. L144
    specialize lucas_choose_lower_eq_transport C
  6. L145
    apply lucas_choose_lower_eq_transport
  7. L146
    exact hindex
  8. L147
    exact hupper_normal
28Establish hleftL148–149

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

  1. L148
    have hleft : ∃ A. Choose(p · q + d,p + (p · x + e),A)Definitions: Choose
  2. L149
    apply choose_exists
29Separate the logical casesL150–150

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

  1. L150
    cases hleft
30Establish hrightL151–152

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

  1. L151
    have hright : ∃ A. Choose(p · q + d,p · x + e,A)Definitions: Choose
  2. L152
    apply choose_exists
31Separate the logical casesL153–153

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

  1. L153
    cases hright
32Establish hleft_quotientL154–155

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

  1. L154
    have hleft_quotient : ∃ A. Choose(q,S x,A)Definitions: Choose
  2. L155
    apply choose_exists
33Separate the logical casesL156–156

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

  1. L156
    cases hleft_quotient
34Establish hright_quotientL157–158

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

  1. L157
    have hright_quotient : ∃ A. Choose(q,x,A)Definitions: Choose
  2. L158
    apply choose_exists
35Separate the logical casesL159–159

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

  1. L159
    cases hright_quotient
36Establish hshiftL160–169

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime shift high column.

  1. L160
    have hshift : exists lbd_left_canonical_high_shift lbd_right_canonical_high_shift. (C) + (p) * lbd_left_canonical_high_shift = (x1 + x2) + (p) * lbd_right_canonical_high_shift
  2. L161
    specialize lucas_prime_shift_high_column p
  3. L162
    specialize lucas_prime_shift_high_column (p * q + d)
  4. L163
    specialize lucas_prime_shift_high_column (p * x + e)
  5. L164
    specialize lucas_prime_shift_high_column C
  6. L165
    specialize lucas_prime_shift_high_column x1
  7. L166
    specialize lucas_prime_shift_high_column x2
  8. L167
    apply lucas_prime_shift_high_column
  9. L168
    exact hprime
  10. L169
    exact hnormal
37Use earlier factsL170–171

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

  1. L170
    exact hleft_witness
  2. L171
    exact hright_witness
38Establish hleft_normalL172–180

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L172
    have hleft_normal : Choose(p · q + d,p · S x + e,x1)Definitions: Choose
  2. L173
    specialize lucas_choose_lower_eq_transport (p * q + d)
  3. L174
    specialize lucas_choose_lower_eq_transport (p + (p * x + e))
  4. L175
    specialize lucas_choose_lower_eq_transport (p * S x + e)
  5. L176
    specialize lucas_choose_lower_eq_transport x1
  6. L177
    apply lucas_choose_lower_eq_transport
  7. L178
    symm
  8. L179
    apply lucas_prime_block_successor_reassociation
  9. L180
    exact hleft_witness
39Establish hleft_modL181–190

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

  1. L181
    have hleft_mod : exists lbd_left_canonical_high_left_mod lbd_right_canonical_high_left_mod. (x1) + (p) * lbd_left_canonical_high_left_mod = (x3 * B) + (p) * lbd_right_canonical_high_left_mod
  2. L182
    specialize IH (S x)
  3. L183
    specialize IH d
  4. L184
    specialize IH e
  5. L185
    specialize IH x1
  6. L186
    specialize IH x3
  7. L187
    specialize IH B
  8. L188
    apply IH
  9. L189
    exact hprime
  10. L190
    exact hdigit
40Use earlier factsL191–194

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

  1. L191
    exact he_digit
  2. L192
    exact hleft_normal
  3. L193
    exact hleft_quotient_witness
  4. L194
    exact hfactor
41Establish hright_modL195–204

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

  1. L195
    have hright_mod : exists lbd_left_canonical_high_right_mod lbd_right_canonical_high_right_mod. (x2) + (p) * lbd_left_canonical_high_right_mod = (x4 * B) + (p) * lbd_right_canonical_high_right_mod
  2. L196
    specialize IH x
  3. L197
    specialize IH d
  4. L198
    specialize IH e
  5. L199
    specialize IH x2
  6. L200
    specialize IH x4
  7. L201
    specialize IH B
  8. L202
    apply IH
  9. L203
    exact hprime
  10. L204
    exact hdigit
42Use earlier factsL205–208

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

  1. L205
    exact he_digit
  2. L206
    exact hright_witness
  3. L207
    exact hright_quotient_witness
  4. L208
    exact hfactor
43Establish hsum_modL209–217

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

  1. L209
    have hsum_mod : exists lbd_left_canonical_high_sum_mod lbd_right_canonical_high_sum_mod. (x1 + x2) + (p) * lbd_left_canonical_high_sum_mod = (x3 * B + x4 * B) + (p) * lbd_right_canonical_high_sum_mod
  2. L210
    specialize mod_eq_add p
  3. L211
    specialize mod_eq_add x1
  4. L212
    specialize mod_eq_add (x3 * B)
  5. L213
    specialize mod_eq_add x2
  6. L214
    specialize mod_eq_add (x4 * B)
  7. L215
    apply mod_eq_add
  8. L216
    exact hleft_mod
  9. L217
    exact hright_mod
44Establish hquotient_normalL218–225

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L218
    have hquotient_normal : Choose(S q,S x,A)Definitions: Choose
  2. L219
    specialize lucas_choose_lower_eq_transport (S q)
  3. L220
    specialize lucas_choose_lower_eq_transport r
  4. L221
    specialize lucas_choose_lower_eq_transport (S x)
  5. L222
    specialize lucas_choose_lower_eq_transport A
  6. L223
    apply lucas_choose_lower_eq_transport
  7. L224
    exact hsuccessor_witness
  8. L225
    exact hquotient
45Establish hpascalL226–235

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

  1. L226
    have hpascal : A = x4 + x3
  2. L227
    specialize choose_succ_succ q
  3. L228
    specialize choose_succ_succ x
  4. L229
    specialize choose_succ_succ x4
  5. L230
    specialize choose_succ_succ x3
  6. L231
    specialize choose_succ_succ A
  7. L232
    apply choose_succ_succ
  8. L233
    exact hright_quotient_witness
  9. L234
    exact hleft_quotient_witness
  10. L235
    exact hquotient_normal
46Establish hsumL236–240

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

  1. L236
    have hsum : x3 + x4 = A
  2. L237
    trans x4 + x3
  3. L238
    apply add_comm
  4. L239
    symm
  5. L240
    exact hpascal
47Establish hfactorizedL241–250

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

  1. L241
    have hfactorized : x3 * B + x4 * B = A * B
  2. L242
    trans (x3 + x4) * B
  3. L243
    symm
  4. L244
    apply add_mul
  5. L245
    congr
  6. L246
    exact hsum
  7. L247
    refl
  8. L248
    rewrite hfactorized at hsum_mod
  9. L249
    specialize mod_eq_trans p
  10. L250
    specialize mod_eq_trans C
48Use earlier factsL251–255

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

  1. L251
    specialize mod_eq_trans (x1 + x2)
  2. L252
    specialize mod_eq_trans (A * B)
  3. L253
    apply mod_eq_trans
  4. L254
    exact hshift
  5. L255
    exact hsum_mod

Library-wide reading audit

Original exact command ledger · 255 lines
  1. 0001intro p
  2. 0002induction q
  3. 0003intro r
  4. 0004intro d
  5. 0005intro e
  6. 0006intro C
  7. 0007intro A
  8. 0008intro B
  9. 0009intro hprime
  10. 0010intro hdigit
  11. 0011intro he_digit
  12. 0012intro hwhole
  13. 0013intro hquotient
  14. 0014intro hfactor
  15. 0015have hcase : r = 0 \/ ~(r = 0)
  16. 0016specialize eq_decidable r
  17. 0017specialize eq_decidable 0
  18. 0018exact eq_decidable
  19. 0019cases hcase
  20. 0020have hindex : p * r + e = e
  21. 0021rewrite hcase_left
  22. 0022apply lucas_prime_block_zero_reassociation
  23. 0023have hnormalized : ((exists bcf_lt_gap_lucas_block_digit_canonical_base_low_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_base_low_out_of_range + S (p * 0 + d) = e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_base_low_in_range. bcf_le_gap_lucas_block_digit_canonical_base_low_in_range + (e) = p * 0 + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_base_low bcf_row_code_scale_lucas_block_digit_canonical_base_low bcf_row_scale_code_lucas_block_digit_canonical_base_low bcf_row_scale_scale_lucas_block_digit_canonical_base_low bcf_row_code_lucas_block_digit_canonical_base_low bcf_row_scale_lucas_block_digit_canonical_base_low. ((forall bcf_row_index_lucas_block_digit_canonical_base_low_table. (exists bcf_lt_gap_lucas_block_digit_canonical_base_low_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_base_low_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_base_low_table) = S (p * 0 + d)) -> exists bcf_row_code_lucas_block_digit_canonical_base_low_table bcf_row_scale_lucas_block_digit_canonical_base_low_table. ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_base_low_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_base_low_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_base_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_base_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low) + (bcf_row_code_lucas_block_digit_canonical_base_low_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_base_low_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_base_low_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_base_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_base_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low) + (bcf_row_scale_lucas_block_digit_canonical_base_low_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_base_low_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_base_low_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_base_low_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_base_low_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_base_low_table_zero_row) = S (p * 0 + d)) -> exists bcf_value_lucas_block_digit_canonical_base_low_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_base_low_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_base_low_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_base_low_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_base_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_base_low_table = bcf_quotient_lucas_block_digit_canonical_base_low_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_base_low_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_base_low_table) + (bcf_value_lucas_block_digit_canonical_base_low_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_base_low_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_base_low_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_low_table_zero_row. bcf_index_lucas_block_digit_canonical_base_low_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_base_low_table_zero_row /\ bcf_value_lucas_block_digit_canonical_base_low_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_low_table bcf_previous_code_lucas_block_digit_canonical_base_low_table bcf_previous_scale_lucas_block_digit_canonical_base_low_table. bcf_row_index_lucas_block_digit_canonical_base_low_table = S bcf_predecessor_lucas_block_digit_canonical_base_low_table /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_base_low_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_base_low_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low) + (bcf_previous_code_lucas_block_digit_canonical_base_low_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_base_low_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_base_low_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low) + (bcf_previous_scale_lucas_block_digit_canonical_base_low_table))) /\ (forall bcf_index_lucas_block_digit_canonical_base_low_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_base_low_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_base_low_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_base_low_table_row_step) = S (p * 0 + d)) -> exists bcf_value_lucas_block_digit_canonical_base_low_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_row_step_entry. bcf_height_lucas_block_digit_canonical_base_low_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_base_low_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_base_low_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_base_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_base_low_table = bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_base_low_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_base_low_table) + (bcf_value_lucas_block_digit_canonical_base_low_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_base_low_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_base_low_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step bcf_left_lucas_block_digit_canonical_base_low_table_row_step bcf_right_lucas_block_digit_canonical_base_low_table_row_step. bcf_index_lucas_block_digit_canonical_base_low_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_base_low_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_base_low_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_base_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_base_low_table = bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_base_low_table) + (bcf_left_lucas_block_digit_canonical_base_low_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_base_low_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_base_low_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_base_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_base_low_table = bcf_quotient_lucas_block_digit_canonical_base_low_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_base_low_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_base_low_table) + (bcf_right_lucas_block_digit_canonical_base_low_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_base_low_table_row_step = bcf_left_lucas_block_digit_canonical_base_low_table_row_step + bcf_right_lucas_block_digit_canonical_base_low_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_decoded_row_code. bcf_height_lucas_block_digit_canonical_base_low_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_base_low) = S ((S (p * 0 + d)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_decoded_row_code * S ((S (p * 0 + d)) * bcf_row_code_scale_lucas_block_digit_canonical_base_low) + (bcf_row_code_lucas_block_digit_canonical_base_low))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_low_decoded_row_scale. bcf_height_lucas_block_digit_canonical_base_low_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_base_low) = S ((S (p * 0 + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_decoded_row_scale * S ((S (p * 0 + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_low) + (bcf_row_scale_lucas_block_digit_canonical_base_low))) /\ (((exists bcf_height_lucas_block_digit_canonical_base_low_decoded_value. bcf_height_lucas_block_digit_canonical_base_low_decoded_value + S (C) = S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_base_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_low_decoded_value. bcf_row_code_lucas_block_digit_canonical_base_low = bcf_quotient_lucas_block_digit_canonical_base_low_decoded_value * S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_base_low) + (C))))))))
  24. 0024specialize lucas_choose_lower_eq_transport (p * 0 + d)
  25. 0025specialize lucas_choose_lower_eq_transport (p * r + e)
  26. 0026specialize lucas_choose_lower_eq_transport e
  27. 0027specialize lucas_choose_lower_eq_transport C
  28. 0028apply lucas_choose_lower_eq_transport
  29. 0029exact hindex
  30. 0030exact hwhole
  31. 0031have hquotient_zero : ((exists bcf_lt_gap_lucas_block_digit_canonical_base_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_base_quotient_out_of_range + S (0) = 0) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_base_quotient_in_range. bcf_le_gap_lucas_block_digit_canonical_base_quotient_in_range + (0) = 0) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_base_quotient bcf_row_code_scale_lucas_block_digit_canonical_base_quotient bcf_row_scale_code_lucas_block_digit_canonical_base_quotient bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient bcf_row_code_lucas_block_digit_canonical_base_quotient bcf_row_scale_lucas_block_digit_canonical_base_quotient. ((forall bcf_row_index_lucas_block_digit_canonical_base_quotient_table. (exists bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_base_quotient_table) = S (0)) -> exists bcf_row_code_lucas_block_digit_canonical_base_quotient_table bcf_row_scale_lucas_block_digit_canonical_base_quotient_table. ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_base_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient) + (bcf_row_code_lucas_block_digit_canonical_base_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_base_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient) + (bcf_row_scale_lucas_block_digit_canonical_base_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_base_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row) = S (0)) -> exists bcf_value_lucas_block_digit_canonical_base_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_base_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_base_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_base_quotient_table = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient_table) + (bcf_value_lucas_block_digit_canonical_base_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_base_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_zero_row. bcf_index_lucas_block_digit_canonical_base_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_zero_row /\ bcf_value_lucas_block_digit_canonical_base_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_quotient_table bcf_previous_code_lucas_block_digit_canonical_base_quotient_table bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table. bcf_row_index_lucas_block_digit_canonical_base_quotient_table = S bcf_predecessor_lucas_block_digit_canonical_base_quotient_table /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_base_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient) + (bcf_previous_code_lucas_block_digit_canonical_base_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_base_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient) + (bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table))) /\ (forall bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_base_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step) = S (0)) -> exists bcf_value_lucas_block_digit_canonical_base_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_entry. bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_base_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_base_quotient_table = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient_table) + (bcf_value_lucas_block_digit_canonical_base_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_base_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step bcf_left_lucas_block_digit_canonical_base_quotient_table_row_step bcf_right_lucas_block_digit_canonical_base_quotient_table_row_step. bcf_index_lucas_block_digit_canonical_base_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_base_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_base_quotient_table = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table) + (bcf_left_lucas_block_digit_canonical_base_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_base_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_base_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_base_quotient_table = bcf_quotient_lucas_block_digit_canonical_base_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_base_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_base_quotient_table) + (bcf_right_lucas_block_digit_canonical_base_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_base_quotient_table_row_step = bcf_left_lucas_block_digit_canonical_base_quotient_table_row_step + bcf_right_lucas_block_digit_canonical_base_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_decoded_row_code. bcf_height_lucas_block_digit_canonical_base_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_base_quotient) = S ((S (0)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_row_code * S ((S (0)) * bcf_row_code_scale_lucas_block_digit_canonical_base_quotient) + (bcf_row_code_lucas_block_digit_canonical_base_quotient))) /\ ((((exists bcf_height_lucas_block_digit_canonical_base_quotient_decoded_row_scale. bcf_height_lucas_block_digit_canonical_base_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_base_quotient) = S ((S (0)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_row_scale * S ((S (0)) * bcf_row_scale_scale_lucas_block_digit_canonical_base_quotient) + (bcf_row_scale_lucas_block_digit_canonical_base_quotient))) /\ (((exists bcf_height_lucas_block_digit_canonical_base_quotient_decoded_value. bcf_height_lucas_block_digit_canonical_base_quotient_decoded_value + S (A) = S ((S (0)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_value. bcf_row_code_lucas_block_digit_canonical_base_quotient = bcf_quotient_lucas_block_digit_canonical_base_quotient_decoded_value * S ((S (0)) * bcf_row_scale_lucas_block_digit_canonical_base_quotient) + (A))))))))
  32. 0032specialize lucas_choose_lower_eq_transport 0
  33. 0033specialize lucas_choose_lower_eq_transport r
  34. 0034specialize lucas_choose_lower_eq_transport 0
  35. 0035specialize lucas_choose_lower_eq_transport A
  36. 0036apply lucas_choose_lower_eq_transport
  37. 0037exact hcase_left
  38. 0038exact hquotient
  39. 0039specialize lucas_low_digit_product_congruence p
  40. 0040specialize lucas_low_digit_product_congruence 0
  41. 0041specialize lucas_low_digit_product_congruence d
  42. 0042specialize lucas_low_digit_product_congruence e
  43. 0043specialize lucas_low_digit_product_congruence C
  44. 0044specialize lucas_low_digit_product_congruence A
  45. 0045specialize lucas_low_digit_product_congruence B
  46. 0046apply lucas_low_digit_product_congruence
  47. 0047exact hprime
  48. 0048exact hdigit
  49. 0049exact he_digit
  50. 0050exact hnormalized
  51. 0051exact hquotient_zero
  52. 0052exact hfactor
  53. 0053have hwhole_zero : C = 0
  54. 0054specialize lucas_zero_upper_quotient_high_column_vanishes p
  55. 0055specialize lucas_zero_upper_quotient_high_column_vanishes r
  56. 0056specialize lucas_zero_upper_quotient_high_column_vanishes d
  57. 0057specialize lucas_zero_upper_quotient_high_column_vanishes e
  58. 0058specialize lucas_zero_upper_quotient_high_column_vanishes C
  59. 0059apply lucas_zero_upper_quotient_high_column_vanishes
  60. 0060exact hdigit
  61. 0061exact hcase_right
  62. 0062exact hwhole
  63. 0063have hquotient_zero : A = 0
  64. 0064specialize lucas_choose_zero_upper_positive_is_zero r
  65. 0065specialize lucas_choose_zero_upper_positive_is_zero A
  66. 0066apply lucas_choose_zero_upper_positive_is_zero
  67. 0067exact hcase_right
  68. 0068exact hquotient
  69. 0069rewrite hwhole_zero
  70. 0070rewrite hquotient_zero
  71. 0071specialize mul_zero_left B
  72. 0072rewrite mul_zero_left
  73. 0073apply mod_eq_refl
  74. 0074intro r
  75. 0075intro d
  76. 0076intro e
  77. 0077intro C
  78. 0078intro A
  79. 0079intro B
  80. 0080intro hprime
  81. 0081intro hdigit
  82. 0082intro he_digit
  83. 0083intro hwhole
  84. 0084intro hquotient
  85. 0085intro hfactor
  86. 0086have hcase : r = 0 \/ ~(r = 0)
  87. 0087specialize eq_decidable r
  88. 0088specialize eq_decidable 0
  89. 0089exact eq_decidable
  90. 0090cases hcase
  91. 0091have hindex : p * r + e = e
  92. 0092rewrite hcase_left
  93. 0093apply lucas_prime_block_zero_reassociation
  94. 0094have hnormalized : ((exists bcf_lt_gap_lucas_block_digit_canonical_successor_low_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_successor_low_out_of_range + S (p * S q + d) = e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_successor_low_in_range. bcf_le_gap_lucas_block_digit_canonical_successor_low_in_range + (e) = p * S q + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_successor_low bcf_row_code_scale_lucas_block_digit_canonical_successor_low bcf_row_scale_code_lucas_block_digit_canonical_successor_low bcf_row_scale_scale_lucas_block_digit_canonical_successor_low bcf_row_code_lucas_block_digit_canonical_successor_low bcf_row_scale_lucas_block_digit_canonical_successor_low. ((forall bcf_row_index_lucas_block_digit_canonical_successor_low_table. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_successor_low_table) = S (p * S q + d)) -> exists bcf_row_code_lucas_block_digit_canonical_successor_low_table bcf_row_scale_lucas_block_digit_canonical_successor_low_table. ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_successor_low_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_successor_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_successor_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low) + (bcf_row_code_lucas_block_digit_canonical_successor_low_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_successor_low_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_successor_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_successor_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low) + (bcf_row_scale_lucas_block_digit_canonical_successor_low_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_successor_low_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row) = S (p * S q + d)) -> exists bcf_value_lucas_block_digit_canonical_successor_low_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_successor_low_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_successor_low_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_successor_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_successor_low_table = bcf_quotient_lucas_block_digit_canonical_successor_low_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_successor_low_table) + (bcf_value_lucas_block_digit_canonical_successor_low_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_successor_low_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_low_table_zero_row. bcf_index_lucas_block_digit_canonical_successor_low_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_successor_low_table_zero_row /\ bcf_value_lucas_block_digit_canonical_successor_low_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_low_table bcf_previous_code_lucas_block_digit_canonical_successor_low_table bcf_previous_scale_lucas_block_digit_canonical_successor_low_table. bcf_row_index_lucas_block_digit_canonical_successor_low_table = S bcf_predecessor_lucas_block_digit_canonical_successor_low_table /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_successor_low_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low) + (bcf_previous_code_lucas_block_digit_canonical_successor_low_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_successor_low_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_successor_low_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low) + (bcf_previous_scale_lucas_block_digit_canonical_successor_low_table))) /\ (forall bcf_index_lucas_block_digit_canonical_successor_low_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_low_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_successor_low_table_row_step) = S (p * S q + d)) -> exists bcf_value_lucas_block_digit_canonical_successor_low_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_entry. bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_successor_low_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_successor_low_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_successor_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_successor_low_table = bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_successor_low_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_successor_low_table) + (bcf_value_lucas_block_digit_canonical_successor_low_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_successor_low_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_successor_low_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step bcf_left_lucas_block_digit_canonical_successor_low_table_row_step bcf_right_lucas_block_digit_canonical_successor_low_table_row_step. bcf_index_lucas_block_digit_canonical_successor_low_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_successor_low_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_successor_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_successor_low_table = bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_successor_low_table) + (bcf_left_lucas_block_digit_canonical_successor_low_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_successor_low_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_successor_low_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_successor_low_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_successor_low_table = bcf_quotient_lucas_block_digit_canonical_successor_low_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_successor_low_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_successor_low_table) + (bcf_right_lucas_block_digit_canonical_successor_low_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_successor_low_table_row_step = bcf_left_lucas_block_digit_canonical_successor_low_table_row_step + bcf_right_lucas_block_digit_canonical_successor_low_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_decoded_row_code. bcf_height_lucas_block_digit_canonical_successor_low_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_successor_low) = S ((S (p * S q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_row_code * S ((S (p * S q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_low) + (bcf_row_code_lucas_block_digit_canonical_successor_low))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_low_decoded_row_scale. bcf_height_lucas_block_digit_canonical_successor_low_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_successor_low) = S ((S (p * S q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_row_scale * S ((S (p * S q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_low) + (bcf_row_scale_lucas_block_digit_canonical_successor_low))) /\ (((exists bcf_height_lucas_block_digit_canonical_successor_low_decoded_value. bcf_height_lucas_block_digit_canonical_successor_low_decoded_value + S (C) = S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_successor_low)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_value. bcf_row_code_lucas_block_digit_canonical_successor_low = bcf_quotient_lucas_block_digit_canonical_successor_low_decoded_value * S ((S (e)) * bcf_row_scale_lucas_block_digit_canonical_successor_low) + (C))))))))
  95. 0095specialize lucas_choose_lower_eq_transport (p * S q + d)
  96. 0096specialize lucas_choose_lower_eq_transport (p * r + e)
  97. 0097specialize lucas_choose_lower_eq_transport e
  98. 0098specialize lucas_choose_lower_eq_transport C
  99. 0099apply lucas_choose_lower_eq_transport
  100. 0100exact hindex
  101. 0101exact hwhole
  102. 0102have hquotient_zero : ((exists bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_out_of_range + S (S q) = 0) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_successor_zero_quotient_in_range. bcf_le_gap_lucas_block_digit_canonical_successor_zero_quotient_in_range + (0) = S q) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_successor_zero_quotient bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient bcf_row_scale_code_lucas_block_digit_canonical_successor_zero_quotient bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient. ((forall bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table) = S (S q)) -> exists bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient_table bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table. ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row) = S (S q)) -> exists bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient_table = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table) + (bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row. bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row /\ bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table bcf_previous_code_lucas_block_digit_canonical_successor_zero_quotient_table bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table. bcf_row_index_lucas_block_digit_canonical_successor_zero_quotient_table = S bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_successor_zero_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_previous_code_lucas_block_digit_canonical_successor_zero_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table))) /\ (forall bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step) = S (S q)) -> exists bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_entry. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient_table = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient_table) + (bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step bcf_left_lucas_block_digit_canonical_successor_zero_quotient_table_row_step bcf_right_lucas_block_digit_canonical_successor_zero_quotient_table_row_step. bcf_index_lucas_block_digit_canonical_successor_zero_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_successor_zero_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_successor_zero_quotient_table = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table) + (bcf_left_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_successor_zero_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_successor_zero_quotient_table = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_successor_zero_quotient_table) + (bcf_right_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_successor_zero_quotient_table_row_step = bcf_left_lucas_block_digit_canonical_successor_zero_quotient_table_row_step + bcf_right_lucas_block_digit_canonical_successor_zero_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_code. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient) = S ((S (S q)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_code * S ((S (S q)) * bcf_row_code_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient))) /\ ((((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_scale. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient) = S ((S (S q)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_row_scale * S ((S (S q)) * bcf_row_scale_scale_lucas_block_digit_canonical_successor_zero_quotient) + (bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient))) /\ (((exists bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_value. bcf_height_lucas_block_digit_canonical_successor_zero_quotient_decoded_value + S (A) = S ((S (0)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_value. bcf_row_code_lucas_block_digit_canonical_successor_zero_quotient = bcf_quotient_lucas_block_digit_canonical_successor_zero_quotient_decoded_value * S ((S (0)) * bcf_row_scale_lucas_block_digit_canonical_successor_zero_quotient) + (A))))))))
  103. 0103specialize lucas_choose_lower_eq_transport (S q)
  104. 0104specialize lucas_choose_lower_eq_transport r
  105. 0105specialize lucas_choose_lower_eq_transport 0
  106. 0106specialize lucas_choose_lower_eq_transport A
  107. 0107apply lucas_choose_lower_eq_transport
  108. 0108exact hcase_left
  109. 0109exact hquotient
  110. 0110specialize lucas_low_digit_product_congruence p
  111. 0111specialize lucas_low_digit_product_congruence (S q)
  112. 0112specialize lucas_low_digit_product_congruence d
  113. 0113specialize lucas_low_digit_product_congruence e
  114. 0114specialize lucas_low_digit_product_congruence C
  115. 0115specialize lucas_low_digit_product_congruence A
  116. 0116specialize lucas_low_digit_product_congruence B
  117. 0117apply lucas_low_digit_product_congruence
  118. 0118exact hprime
  119. 0119exact hdigit
  120. 0120exact he_digit
  121. 0121exact hnormalized
  122. 0122exact hquotient_zero
  123. 0123exact hfactor
  124. 0124have hsuccessor : exists t. r = S t
  125. 0125specialize nonzero_is_succ r
  126. 0126apply nonzero_is_succ
  127. 0127exact hcase_right
  128. 0128cases hsuccessor
  129. 0129have hupper_normal : ((exists bcf_lt_gap_lucas_block_digit_canonical_high_upper_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_upper_out_of_range + S (p + (p * q + d)) = p * r + e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_upper_in_range. bcf_le_gap_lucas_block_digit_canonical_high_upper_in_range + (p * r + e) = p + (p * q + d)) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_upper bcf_row_code_scale_lucas_block_digit_canonical_high_upper bcf_row_scale_code_lucas_block_digit_canonical_high_upper bcf_row_scale_scale_lucas_block_digit_canonical_high_upper bcf_row_code_lucas_block_digit_canonical_high_upper bcf_row_scale_lucas_block_digit_canonical_high_upper. ((forall bcf_row_index_lucas_block_digit_canonical_high_upper_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_upper_table) = S (p + (p * q + d))) -> exists bcf_row_code_lucas_block_digit_canonical_high_upper_table bcf_row_scale_lucas_block_digit_canonical_high_upper_table. ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_upper_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_upper_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_upper_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper) + (bcf_row_code_lucas_block_digit_canonical_high_upper_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_upper_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_upper_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_upper_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper) + (bcf_row_scale_lucas_block_digit_canonical_high_upper_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_upper_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row) = S (p + (p * q + d))) -> exists bcf_value_lucas_block_digit_canonical_high_upper_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_upper_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_upper_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_upper_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_upper_table = bcf_quotient_lucas_block_digit_canonical_high_upper_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_upper_table) + (bcf_value_lucas_block_digit_canonical_high_upper_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_upper_table_zero_row. bcf_index_lucas_block_digit_canonical_high_upper_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_upper_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_upper_table bcf_previous_code_lucas_block_digit_canonical_high_upper_table bcf_previous_scale_lucas_block_digit_canonical_high_upper_table. bcf_row_index_lucas_block_digit_canonical_high_upper_table = S bcf_predecessor_lucas_block_digit_canonical_high_upper_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_upper_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper) + (bcf_previous_code_lucas_block_digit_canonical_high_upper_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_upper_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper) + (bcf_previous_scale_lucas_block_digit_canonical_high_upper_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_upper_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_upper_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_upper_table_row_step) = S (p + (p * q + d))) -> exists bcf_value_lucas_block_digit_canonical_high_upper_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_upper_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_upper_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_upper_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_upper_table = bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_upper_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_upper_table) + (bcf_value_lucas_block_digit_canonical_high_upper_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_upper_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step bcf_left_lucas_block_digit_canonical_high_upper_table_row_step bcf_right_lucas_block_digit_canonical_high_upper_table_row_step. bcf_index_lucas_block_digit_canonical_high_upper_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_upper_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_upper_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_upper_table = bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_upper_table) + (bcf_left_lucas_block_digit_canonical_high_upper_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_upper_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_upper_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_upper_table = bcf_quotient_lucas_block_digit_canonical_high_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_upper_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_upper_table) + (bcf_right_lucas_block_digit_canonical_high_upper_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_upper_table_row_step = bcf_left_lucas_block_digit_canonical_high_upper_table_row_step + bcf_right_lucas_block_digit_canonical_high_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_upper_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_upper) = S ((S (p + (p * q + d))) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_row_code * S ((S (p + (p * q + d))) * bcf_row_code_scale_lucas_block_digit_canonical_high_upper) + (bcf_row_code_lucas_block_digit_canonical_high_upper))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_upper_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_upper_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_upper) = S ((S (p + (p * q + d))) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_row_scale * S ((S (p + (p * q + d))) * bcf_row_scale_scale_lucas_block_digit_canonical_high_upper) + (bcf_row_scale_lucas_block_digit_canonical_high_upper))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_upper_decoded_value. bcf_height_lucas_block_digit_canonical_high_upper_decoded_value + S (C) = S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_canonical_high_upper)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_upper = bcf_quotient_lucas_block_digit_canonical_high_upper_decoded_value * S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_canonical_high_upper) + (C))))))))
  130. 0130specialize choose_upper_eq_transport (p * S q + d)
  131. 0131specialize choose_upper_eq_transport (p + (p * q + d))
  132. 0132specialize choose_upper_eq_transport (p * r + e)
  133. 0133specialize choose_upper_eq_transport C
  134. 0134apply choose_upper_eq_transport
  135. 0135apply lucas_prime_block_successor_reassociation
  136. 0136exact hwhole
  137. 0137have hindex : p * r + e = p + (p * x + e)
  138. 0138rewrite hsuccessor_witness
  139. 0139apply lucas_prime_block_successor_reassociation
  140. 0140have hnormal : ((exists bcf_lt_gap_lucas_block_digit_canonical_high_normal_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_normal_out_of_range + S (p + (p * q + d)) = p + (p * x + e)) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_normal_in_range. bcf_le_gap_lucas_block_digit_canonical_high_normal_in_range + (p + (p * x + e)) = p + (p * q + d)) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_normal bcf_row_code_scale_lucas_block_digit_canonical_high_normal bcf_row_scale_code_lucas_block_digit_canonical_high_normal bcf_row_scale_scale_lucas_block_digit_canonical_high_normal bcf_row_code_lucas_block_digit_canonical_high_normal bcf_row_scale_lucas_block_digit_canonical_high_normal. ((forall bcf_row_index_lucas_block_digit_canonical_high_normal_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_normal_table) = S (p + (p * q + d))) -> exists bcf_row_code_lucas_block_digit_canonical_high_normal_table bcf_row_scale_lucas_block_digit_canonical_high_normal_table. ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal) + (bcf_row_code_lucas_block_digit_canonical_high_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_normal_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_normal_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row) = S (p + (p * q + d))) -> exists bcf_value_lucas_block_digit_canonical_high_normal_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_normal_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_normal_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_normal_table = bcf_quotient_lucas_block_digit_canonical_high_normal_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_normal_table) + (bcf_value_lucas_block_digit_canonical_high_normal_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_normal_table_zero_row. bcf_index_lucas_block_digit_canonical_high_normal_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_normal_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_normal_table bcf_previous_code_lucas_block_digit_canonical_high_normal_table bcf_previous_scale_lucas_block_digit_canonical_high_normal_table. bcf_row_index_lucas_block_digit_canonical_high_normal_table = S bcf_predecessor_lucas_block_digit_canonical_high_normal_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal) + (bcf_previous_code_lucas_block_digit_canonical_high_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal) + (bcf_previous_scale_lucas_block_digit_canonical_high_normal_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_normal_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_normal_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_normal_table_row_step) = S (p + (p * q + d))) -> exists bcf_value_lucas_block_digit_canonical_high_normal_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_normal_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_normal_table = bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_normal_table) + (bcf_value_lucas_block_digit_canonical_high_normal_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_normal_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step bcf_left_lucas_block_digit_canonical_high_normal_table_row_step bcf_right_lucas_block_digit_canonical_high_normal_table_row_step. bcf_index_lucas_block_digit_canonical_high_normal_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_normal_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_normal_table = bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_normal_table) + (bcf_left_lucas_block_digit_canonical_high_normal_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_normal_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_normal_table = bcf_quotient_lucas_block_digit_canonical_high_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_normal_table) + (bcf_right_lucas_block_digit_canonical_high_normal_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_normal_table_row_step = bcf_left_lucas_block_digit_canonical_high_normal_table_row_step + bcf_right_lucas_block_digit_canonical_high_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_normal_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_normal) = S ((S (p + (p * q + d))) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_row_code * S ((S (p + (p * q + d))) * bcf_row_code_scale_lucas_block_digit_canonical_high_normal) + (bcf_row_code_lucas_block_digit_canonical_high_normal))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_normal_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_normal_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_normal) = S ((S (p + (p * q + d))) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_row_scale * S ((S (p + (p * q + d))) * bcf_row_scale_scale_lucas_block_digit_canonical_high_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_normal))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_normal_decoded_value. bcf_height_lucas_block_digit_canonical_high_normal_decoded_value + S (C) = S ((S (p + (p * x + e))) * bcf_row_scale_lucas_block_digit_canonical_high_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_normal = bcf_quotient_lucas_block_digit_canonical_high_normal_decoded_value * S ((S (p + (p * x + e))) * bcf_row_scale_lucas_block_digit_canonical_high_normal) + (C))))))))
  141. 0141specialize lucas_choose_lower_eq_transport (p + (p * q + d))
  142. 0142specialize lucas_choose_lower_eq_transport (p * r + e)
  143. 0143specialize lucas_choose_lower_eq_transport (p + (p * x + e))
  144. 0144specialize lucas_choose_lower_eq_transport C
  145. 0145apply lucas_choose_lower_eq_transport
  146. 0146exact hindex
  147. 0147exact hupper_normal
  148. 0148have hleft : exists A. ((exists bcf_lt_gap_lucas_block_digit_canonical_high_left_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_left_out_of_range + S (p * q + d) = p + (p * x + e)) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_left_in_range. bcf_le_gap_lucas_block_digit_canonical_high_left_in_range + (p + (p * x + e)) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_left bcf_row_code_scale_lucas_block_digit_canonical_high_left bcf_row_scale_code_lucas_block_digit_canonical_high_left bcf_row_scale_scale_lucas_block_digit_canonical_high_left bcf_row_code_lucas_block_digit_canonical_high_left bcf_row_scale_lucas_block_digit_canonical_high_left. ((forall bcf_row_index_lucas_block_digit_canonical_high_left_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_left_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_canonical_high_left_table bcf_row_scale_lucas_block_digit_canonical_high_left_table. ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left) + (bcf_row_code_lucas_block_digit_canonical_high_left_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left) + (bcf_row_scale_lucas_block_digit_canonical_high_left_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_left_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_left_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_left_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_left_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_left_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_left_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_left_table = bcf_quotient_lucas_block_digit_canonical_high_left_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_table) + (bcf_value_lucas_block_digit_canonical_high_left_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_table_zero_row. bcf_index_lucas_block_digit_canonical_high_left_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_left_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_left_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_table bcf_previous_code_lucas_block_digit_canonical_high_left_table bcf_previous_scale_lucas_block_digit_canonical_high_left_table. bcf_row_index_lucas_block_digit_canonical_high_left_table = S bcf_predecessor_lucas_block_digit_canonical_high_left_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_left_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_left_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left) + (bcf_previous_code_lucas_block_digit_canonical_high_left_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_left_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_left_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left) + (bcf_previous_scale_lucas_block_digit_canonical_high_left_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_left_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_left_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_left_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_left_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_left_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_left_table = bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_table) + (bcf_value_lucas_block_digit_canonical_high_left_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step bcf_left_lucas_block_digit_canonical_high_left_table_row_step bcf_right_lucas_block_digit_canonical_high_left_table_row_step. bcf_index_lucas_block_digit_canonical_high_left_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_left_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_left_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_left_table = bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_table) + (bcf_left_lucas_block_digit_canonical_high_left_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_left_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_left_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_left_table = bcf_quotient_lucas_block_digit_canonical_high_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_table) + (bcf_right_lucas_block_digit_canonical_high_left_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_left_table_row_step = bcf_left_lucas_block_digit_canonical_high_left_table_row_step + bcf_right_lucas_block_digit_canonical_high_left_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left) + (bcf_row_code_lucas_block_digit_canonical_high_left))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left) + (bcf_row_scale_lucas_block_digit_canonical_high_left))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_left_decoded_value. bcf_height_lucas_block_digit_canonical_high_left_decoded_value + S (A) = S ((S (p + (p * x + e))) * bcf_row_scale_lucas_block_digit_canonical_high_left)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_left = bcf_quotient_lucas_block_digit_canonical_high_left_decoded_value * S ((S (p + (p * x + e))) * bcf_row_scale_lucas_block_digit_canonical_high_left) + (A))))))))
  149. 0149apply choose_exists
  150. 0150cases hleft
  151. 0151have hright : exists A. ((exists bcf_lt_gap_lucas_block_digit_canonical_high_right_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_right_out_of_range + S (p * q + d) = p * x + e) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_right_in_range. bcf_le_gap_lucas_block_digit_canonical_high_right_in_range + (p * x + e) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_right bcf_row_code_scale_lucas_block_digit_canonical_high_right bcf_row_scale_code_lucas_block_digit_canonical_high_right bcf_row_scale_scale_lucas_block_digit_canonical_high_right bcf_row_code_lucas_block_digit_canonical_high_right bcf_row_scale_lucas_block_digit_canonical_high_right. ((forall bcf_row_index_lucas_block_digit_canonical_high_right_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_right_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_canonical_high_right_table bcf_row_scale_lucas_block_digit_canonical_high_right_table. ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_right_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_right_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right) + (bcf_row_code_lucas_block_digit_canonical_high_right_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_right_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_right_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right) + (bcf_row_scale_lucas_block_digit_canonical_high_right_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_right_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_right_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_right_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_right_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_right_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_right_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_right_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_right_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_right_table = bcf_quotient_lucas_block_digit_canonical_high_right_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_right_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_right_table) + (bcf_value_lucas_block_digit_canonical_high_right_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_right_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_right_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_table_zero_row. bcf_index_lucas_block_digit_canonical_high_right_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_right_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_right_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_table bcf_previous_code_lucas_block_digit_canonical_high_right_table bcf_previous_scale_lucas_block_digit_canonical_high_right_table. bcf_row_index_lucas_block_digit_canonical_high_right_table = S bcf_predecessor_lucas_block_digit_canonical_high_right_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_right_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_right_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right) + (bcf_previous_code_lucas_block_digit_canonical_high_right_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_right_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_right_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right) + (bcf_previous_scale_lucas_block_digit_canonical_high_right_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_right_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_right_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_right_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_right_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_right_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_right_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_right_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_right_table = bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_right_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_right_table) + (bcf_value_lucas_block_digit_canonical_high_right_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_right_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_right_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step bcf_left_lucas_block_digit_canonical_high_right_table_row_step bcf_right_lucas_block_digit_canonical_high_right_table_row_step. bcf_index_lucas_block_digit_canonical_high_right_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_right_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_right_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_right_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_right_table = bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_right_table) + (bcf_left_lucas_block_digit_canonical_high_right_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_right_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_right_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_right_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_right_table = bcf_quotient_lucas_block_digit_canonical_high_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_right_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_right_table) + (bcf_right_lucas_block_digit_canonical_high_right_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_right_table_row_step = bcf_left_lucas_block_digit_canonical_high_right_table_row_step + bcf_right_lucas_block_digit_canonical_high_right_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_right_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_right) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right) + (bcf_row_code_lucas_block_digit_canonical_high_right))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_right_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_right) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right) + (bcf_row_scale_lucas_block_digit_canonical_high_right))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_right_decoded_value. bcf_height_lucas_block_digit_canonical_high_right_decoded_value + S (A) = S ((S (p * x + e)) * bcf_row_scale_lucas_block_digit_canonical_high_right)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_right = bcf_quotient_lucas_block_digit_canonical_high_right_decoded_value * S ((S (p * x + e)) * bcf_row_scale_lucas_block_digit_canonical_high_right) + (A))))))))
  152. 0152apply choose_exists
  153. 0153cases hright
  154. 0154have hleft_quotient : exists A. ((exists bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_out_of_range + S (q) = S x) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_left_quotient_in_range. bcf_le_gap_lucas_block_digit_canonical_high_left_quotient_in_range + (S x) = q) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_left_quotient bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient bcf_row_scale_code_lucas_block_digit_canonical_high_left_quotient bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient bcf_row_code_lucas_block_digit_canonical_high_left_quotient bcf_row_scale_lucas_block_digit_canonical_high_left_quotient. ((forall bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table) = S (q)) -> exists bcf_row_code_lucas_block_digit_canonical_high_left_quotient_table bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table. ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_row_code_lucas_block_digit_canonical_high_left_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_high_left_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_left_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_left_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table) + (bcf_value_lucas_block_digit_canonical_high_left_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_zero_row. bcf_index_lucas_block_digit_canonical_high_left_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_left_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table bcf_previous_code_lucas_block_digit_canonical_high_left_quotient_table bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table. bcf_row_index_lucas_block_digit_canonical_high_left_quotient_table = S bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_left_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_previous_code_lucas_block_digit_canonical_high_left_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_high_left_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_left_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_left_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient_table) + (bcf_value_lucas_block_digit_canonical_high_left_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step bcf_left_lucas_block_digit_canonical_high_left_quotient_table_row_step bcf_right_lucas_block_digit_canonical_high_left_quotient_table_row_step. bcf_index_lucas_block_digit_canonical_high_left_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_left_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_left_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table) + (bcf_left_lucas_block_digit_canonical_high_left_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_left_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_left_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_quotient_table) + (bcf_right_lucas_block_digit_canonical_high_left_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_left_quotient_table_row_step = bcf_left_lucas_block_digit_canonical_high_left_quotient_table_row_step + bcf_right_lucas_block_digit_canonical_high_left_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left_quotient) = S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_row_code * S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_row_code_lucas_block_digit_canonical_high_left_quotient))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left_quotient) = S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_row_scale * S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_quotient) + (bcf_row_scale_lucas_block_digit_canonical_high_left_quotient))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_value. bcf_height_lucas_block_digit_canonical_high_left_quotient_decoded_value + S (A) = S ((S (S x)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_left_quotient = bcf_quotient_lucas_block_digit_canonical_high_left_quotient_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_block_digit_canonical_high_left_quotient) + (A))))))))
  155. 0155apply choose_exists
  156. 0156cases hleft_quotient
  157. 0157have hright_quotient : exists A. ((exists bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_out_of_range + S (q) = x) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_right_quotient_in_range. bcf_le_gap_lucas_block_digit_canonical_high_right_quotient_in_range + (x) = q) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_right_quotient bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient bcf_row_scale_code_lucas_block_digit_canonical_high_right_quotient bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient bcf_row_code_lucas_block_digit_canonical_high_right_quotient bcf_row_scale_lucas_block_digit_canonical_high_right_quotient. ((forall bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table) = S (q)) -> exists bcf_row_code_lucas_block_digit_canonical_high_right_quotient_table bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table. ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_right_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_row_code_lucas_block_digit_canonical_high_right_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_high_right_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_right_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_right_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table) + (bcf_value_lucas_block_digit_canonical_high_right_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_right_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_zero_row. bcf_index_lucas_block_digit_canonical_high_right_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_right_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table bcf_previous_code_lucas_block_digit_canonical_high_right_quotient_table bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table. bcf_row_index_lucas_block_digit_canonical_high_right_quotient_table = S bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_right_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_previous_code_lucas_block_digit_canonical_high_right_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_right_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step) = S (q)) -> exists bcf_value_lucas_block_digit_canonical_high_right_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_right_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_right_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient_table) + (bcf_value_lucas_block_digit_canonical_high_right_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_right_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step bcf_left_lucas_block_digit_canonical_high_right_quotient_table_row_step bcf_right_lucas_block_digit_canonical_high_right_quotient_table_row_step. bcf_index_lucas_block_digit_canonical_high_right_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_right_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_right_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table) + (bcf_left_lucas_block_digit_canonical_high_right_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_right_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_right_quotient_table = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_right_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_right_quotient_table) + (bcf_right_lucas_block_digit_canonical_high_right_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_right_quotient_table_row_step = bcf_left_lucas_block_digit_canonical_high_right_quotient_table_row_step + bcf_right_lucas_block_digit_canonical_high_right_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_right_quotient) = S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_row_code * S ((S (q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_row_code_lucas_block_digit_canonical_high_right_quotient))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_right_quotient) = S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_row_scale * S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_right_quotient) + (bcf_row_scale_lucas_block_digit_canonical_high_right_quotient))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_value. bcf_height_lucas_block_digit_canonical_high_right_quotient_decoded_value + S (A) = S ((S (x)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_right_quotient = bcf_quotient_lucas_block_digit_canonical_high_right_quotient_decoded_value * S ((S (x)) * bcf_row_scale_lucas_block_digit_canonical_high_right_quotient) + (A))))))))
  158. 0158apply choose_exists
  159. 0159cases hright_quotient
  160. 0160have hshift : exists lbd_left_canonical_high_shift lbd_right_canonical_high_shift. (C) + (p) * lbd_left_canonical_high_shift = (x1 + x2) + (p) * lbd_right_canonical_high_shift
  161. 0161specialize lucas_prime_shift_high_column p
  162. 0162specialize lucas_prime_shift_high_column (p * q + d)
  163. 0163specialize lucas_prime_shift_high_column (p * x + e)
  164. 0164specialize lucas_prime_shift_high_column C
  165. 0165specialize lucas_prime_shift_high_column x1
  166. 0166specialize lucas_prime_shift_high_column x2
  167. 0167apply lucas_prime_shift_high_column
  168. 0168exact hprime
  169. 0169exact hnormal
  170. 0170exact hleft_witness
  171. 0171exact hright_witness
  172. 0172have hleft_normal : ((exists bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_out_of_range + S (p * q + d) = p * S x + e) /\ x1 = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_left_normal_in_range. bcf_le_gap_lucas_block_digit_canonical_high_left_normal_in_range + (p * S x + e) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_left_normal bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal bcf_row_scale_code_lucas_block_digit_canonical_high_left_normal bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal bcf_row_code_lucas_block_digit_canonical_high_left_normal bcf_row_scale_lucas_block_digit_canonical_high_left_normal. ((forall bcf_row_index_lucas_block_digit_canonical_high_left_normal_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_left_normal_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_canonical_high_left_normal_table bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table. ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_row_code_lucas_block_digit_canonical_high_left_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_left_normal_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_left_normal_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_left_normal_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_left_normal_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_left_normal_table = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table) + (bcf_value_lucas_block_digit_canonical_high_left_normal_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_zero_row. bcf_index_lucas_block_digit_canonical_high_left_normal_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_left_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table bcf_previous_code_lucas_block_digit_canonical_high_left_normal_table bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table. bcf_row_index_lucas_block_digit_canonical_high_left_normal_table = S bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_left_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_previous_code_lucas_block_digit_canonical_high_left_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_left_normal_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_canonical_high_left_normal_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_left_normal_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_left_normal_table = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal_table) + (bcf_value_lucas_block_digit_canonical_high_left_normal_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_left_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step bcf_left_lucas_block_digit_canonical_high_left_normal_table_row_step bcf_right_lucas_block_digit_canonical_high_left_normal_table_row_step. bcf_index_lucas_block_digit_canonical_high_left_normal_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_left_normal_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_left_normal_table = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table) + (bcf_left_lucas_block_digit_canonical_high_left_normal_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_left_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_left_normal_table = bcf_quotient_lucas_block_digit_canonical_high_left_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_left_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_left_normal_table) + (bcf_right_lucas_block_digit_canonical_high_left_normal_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_left_normal_table_row_step = bcf_left_lucas_block_digit_canonical_high_left_normal_table_row_step + bcf_right_lucas_block_digit_canonical_high_left_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_left_normal) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_row_code_lucas_block_digit_canonical_high_left_normal))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_left_normal) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_left_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_left_normal))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_value. bcf_height_lucas_block_digit_canonical_high_left_normal_decoded_value + S (x1) = S ((S (p * S x + e)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_left_normal = bcf_quotient_lucas_block_digit_canonical_high_left_normal_decoded_value * S ((S (p * S x + e)) * bcf_row_scale_lucas_block_digit_canonical_high_left_normal) + (x1))))))))
  173. 0173specialize lucas_choose_lower_eq_transport (p * q + d)
  174. 0174specialize lucas_choose_lower_eq_transport (p + (p * x + e))
  175. 0175specialize lucas_choose_lower_eq_transport (p * S x + e)
  176. 0176specialize lucas_choose_lower_eq_transport x1
  177. 0177apply lucas_choose_lower_eq_transport
  178. 0178symm
  179. 0179apply lucas_prime_block_successor_reassociation
  180. 0180exact hleft_witness
  181. 0181have hleft_mod : exists lbd_left_canonical_high_left_mod lbd_right_canonical_high_left_mod. (x1) + (p) * lbd_left_canonical_high_left_mod = (x3 * B) + (p) * lbd_right_canonical_high_left_mod
  182. 0182specialize IH (S x)
  183. 0183specialize IH d
  184. 0184specialize IH e
  185. 0185specialize IH x1
  186. 0186specialize IH x3
  187. 0187specialize IH B
  188. 0188apply IH
  189. 0189exact hprime
  190. 0190exact hdigit
  191. 0191exact he_digit
  192. 0192exact hleft_normal
  193. 0193exact hleft_quotient_witness
  194. 0194exact hfactor
  195. 0195have hright_mod : exists lbd_left_canonical_high_right_mod lbd_right_canonical_high_right_mod. (x2) + (p) * lbd_left_canonical_high_right_mod = (x4 * B) + (p) * lbd_right_canonical_high_right_mod
  196. 0196specialize IH x
  197. 0197specialize IH d
  198. 0198specialize IH e
  199. 0199specialize IH x2
  200. 0200specialize IH x4
  201. 0201specialize IH B
  202. 0202apply IH
  203. 0203exact hprime
  204. 0204exact hdigit
  205. 0205exact he_digit
  206. 0206exact hright_witness
  207. 0207exact hright_quotient_witness
  208. 0208exact hfactor
  209. 0209have hsum_mod : exists lbd_left_canonical_high_sum_mod lbd_right_canonical_high_sum_mod. (x1 + x2) + (p) * lbd_left_canonical_high_sum_mod = (x3 * B + x4 * B) + (p) * lbd_right_canonical_high_sum_mod
  210. 0210specialize mod_eq_add p
  211. 0211specialize mod_eq_add x1
  212. 0212specialize mod_eq_add (x3 * B)
  213. 0213specialize mod_eq_add x2
  214. 0214specialize mod_eq_add (x4 * B)
  215. 0215apply mod_eq_add
  216. 0216exact hleft_mod
  217. 0217exact hright_mod
  218. 0218have hquotient_normal : ((exists bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_out_of_range. bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_out_of_range + S (S q) = S x) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_canonical_high_quotient_normal_in_range. bcf_le_gap_lucas_block_digit_canonical_high_quotient_normal_in_range + (S x) = S q) /\ (exists bcf_row_code_code_lucas_block_digit_canonical_high_quotient_normal bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal bcf_row_scale_code_lucas_block_digit_canonical_high_quotient_normal bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal bcf_row_code_lucas_block_digit_canonical_high_quotient_normal bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal. ((forall bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table. (exists bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_row_bound + S (bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table) = S (S q)) -> exists bcf_row_code_lucas_block_digit_canonical_high_quotient_normal_table bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table. ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_quotient_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_row_code_lucas_block_digit_canonical_high_quotient_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table) = S ((S (bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table))) /\ ((bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table = 0 /\ (forall bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_bound + S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row) = S (S q)) -> exists bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_zero_row. ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_entry. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_entry + S (bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_zero_row) = S ((S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_entry. bcf_row_code_lucas_block_digit_canonical_high_quotient_normal_table = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table) + (bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_zero_row))) /\ ((bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row = 0 /\ bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_zero_row. bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_zero_row = S bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_zero_row /\ bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table bcf_previous_code_lucas_block_digit_canonical_high_quotient_normal_table bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table. bcf_row_index_lucas_block_digit_canonical_high_quotient_normal_table = S bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_code. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_canonical_high_quotient_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_previous_code_lucas_block_digit_canonical_high_quotient_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_scale. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table))) /\ (forall bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step. (exists bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_row_step_bound. bcf_lt_gap_lucas_block_digit_canonical_high_quotient_normal_table_row_step_bound + S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step) = S (S q)) -> exists bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_row_step. ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_entry. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_entry + S (bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_row_step) = S ((S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_entry. bcf_row_code_lucas_block_digit_canonical_high_quotient_normal_table = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal_table) + (bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_row_step))) /\ ((bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step = 0 /\ bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step bcf_left_lucas_block_digit_canonical_high_quotient_normal_table_row_step bcf_right_lucas_block_digit_canonical_high_quotient_normal_table_row_step. bcf_index_lucas_block_digit_canonical_high_quotient_normal_table_row_step = S bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_left. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_left + S (bcf_left_lucas_block_digit_canonical_high_quotient_normal_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_canonical_high_quotient_normal_table = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table) + (bcf_left_lucas_block_digit_canonical_high_quotient_normal_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_right. bcf_height_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_right + S (bcf_right_lucas_block_digit_canonical_high_quotient_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_canonical_high_quotient_normal_table = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_canonical_high_quotient_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_canonical_high_quotient_normal_table) + (bcf_right_lucas_block_digit_canonical_high_quotient_normal_table_row_step))) /\ bcf_value_lucas_block_digit_canonical_high_quotient_normal_table_row_step = bcf_left_lucas_block_digit_canonical_high_quotient_normal_table_row_step + bcf_right_lucas_block_digit_canonical_high_quotient_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_row_code. bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_row_code + S (bcf_row_code_lucas_block_digit_canonical_high_quotient_normal) = S ((S (S q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_row_code. bcf_row_code_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_row_code * S ((S (S q)) * bcf_row_code_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_row_code_lucas_block_digit_canonical_high_quotient_normal))) /\ ((((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_row_scale. bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal) = S ((S (S q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_row_scale * S ((S (S q)) * bcf_row_scale_scale_lucas_block_digit_canonical_high_quotient_normal) + (bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal))) /\ (((exists bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_value. bcf_height_lucas_block_digit_canonical_high_quotient_normal_decoded_value + S (A) = S ((S (S x)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal)) /\ exists bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_value. bcf_row_code_lucas_block_digit_canonical_high_quotient_normal = bcf_quotient_lucas_block_digit_canonical_high_quotient_normal_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_block_digit_canonical_high_quotient_normal) + (A))))))))
  219. 0219specialize lucas_choose_lower_eq_transport (S q)
  220. 0220specialize lucas_choose_lower_eq_transport r
  221. 0221specialize lucas_choose_lower_eq_transport (S x)
  222. 0222specialize lucas_choose_lower_eq_transport A
  223. 0223apply lucas_choose_lower_eq_transport
  224. 0224exact hsuccessor_witness
  225. 0225exact hquotient
  226. 0226have hpascal : A = x4 + x3
  227. 0227specialize choose_succ_succ q
  228. 0228specialize choose_succ_succ x
  229. 0229specialize choose_succ_succ x4
  230. 0230specialize choose_succ_succ x3
  231. 0231specialize choose_succ_succ A
  232. 0232apply choose_succ_succ
  233. 0233exact hright_quotient_witness
  234. 0234exact hleft_quotient_witness
  235. 0235exact hquotient_normal
  236. 0236have hsum : x3 + x4 = A
  237. 0237trans x4 + x3
  238. 0238apply add_comm
  239. 0239symm
  240. 0240exact hpascal
  241. 0241have hfactorized : x3 * B + x4 * B = A * B
  242. 0242trans (x3 + x4) * B
  243. 0243symm
  244. 0244apply add_mul
  245. 0245congr
  246. 0246exact hsum
  247. 0247refl
  248. 0248rewrite hfactorized at hsum_mod
  249. 0249specialize mod_eq_trans p
  250. 0250specialize mod_eq_trans C
  251. 0251specialize mod_eq_trans (x1 + x2)
  252. 0252specialize mod_eq_trans (A * B)
  253. 0253apply mod_eq_trans
  254. 0254exact hshift
  255. 0255exact hsum_mod