LU0012 · theorem body

lucas_repeated_prime_shift_below_base

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Every below-base binomial column is invariant modulo a prime under an arbitrary number of prime-row shifts.

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.

Statement with defined notation

∀ p. ∀ q. ∀ a. ∀ b. ∀ C. ∀ D. Prime(p) → Lt(b,p) → Choose(p · q + a,b,C) → Choose(a,b,D) → ModEq(p,C,D)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0008 ModEq PD0041 Choose

In local proof propositions

PD0008 ModEq PD0041 Choose
Exact expanded first-order statement
forall p q a b C D. ((~(p = 1) /\ forall frm_prime_left_lucas_low_digit_prime frm_prime_right_lucas_low_digit_prime. p = frm_prime_left_lucas_low_digit_prime * frm_prime_right_lucas_low_digit_prime -> frm_prime_left_lucas_low_digit_prime = 1 \/ frm_prime_right_lucas_low_digit_prime = 1)) -> (exists lld_gap_repeat_bound. lld_gap_repeat_bound + S (b) = (p)) -> (((exists bcf_lt_gap_lucas_low_digit_repeat_upper_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_upper_out_of_range + S (p * q + a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_upper_in_range. bcf_le_gap_lucas_low_digit_repeat_upper_in_range + (b) = p * q + a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_upper bcf_row_code_scale_lucas_low_digit_repeat_upper bcf_row_scale_code_lucas_low_digit_repeat_upper bcf_row_scale_scale_lucas_low_digit_repeat_upper bcf_row_code_lucas_low_digit_repeat_upper bcf_row_scale_lucas_low_digit_repeat_upper. ((forall bcf_row_index_lucas_low_digit_repeat_upper_table. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_upper_table) = S (p * q + a)) -> exists bcf_row_code_lucas_low_digit_repeat_upper_table bcf_row_scale_lucas_low_digit_repeat_upper_table. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_upper_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_row_code_lucas_low_digit_repeat_upper_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_upper_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_row_scale_lucas_low_digit_repeat_upper_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_upper_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_upper_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_upper_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_upper_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_upper_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_upper_table) + (bcf_value_lucas_low_digit_repeat_upper_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_upper_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table_zero_row. bcf_index_lucas_low_digit_repeat_upper_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_upper_table_zero_row /\ bcf_value_lucas_low_digit_repeat_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table bcf_previous_code_lucas_low_digit_repeat_upper_table bcf_previous_scale_lucas_low_digit_repeat_upper_table. bcf_row_index_lucas_low_digit_repeat_upper_table = S bcf_predecessor_lucas_low_digit_repeat_upper_table /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_upper_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_previous_code_lucas_low_digit_repeat_upper_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_upper_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_previous_scale_lucas_low_digit_repeat_upper_table))) /\ (forall bcf_index_lucas_low_digit_repeat_upper_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_upper_table_row_step) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_upper_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_entry. bcf_height_lucas_low_digit_repeat_upper_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_upper_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_upper_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_upper_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_upper_table) + (bcf_value_lucas_low_digit_repeat_upper_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_upper_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step bcf_left_lucas_low_digit_repeat_upper_table_row_step bcf_right_lucas_low_digit_repeat_upper_table_row_step. bcf_index_lucas_low_digit_repeat_upper_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_upper_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_upper_table) + (bcf_left_lucas_low_digit_repeat_upper_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_upper_table) + (bcf_right_lucas_low_digit_repeat_upper_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_upper_table_row_step = bcf_left_lucas_low_digit_repeat_upper_table_row_step + bcf_right_lucas_low_digit_repeat_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_decoded_row_code. bcf_height_lucas_low_digit_repeat_upper_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_upper) = S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_code * S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_row_code_lucas_low_digit_repeat_upper))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_decoded_row_scale. bcf_height_lucas_low_digit_repeat_upper_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_upper) = S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_scale * S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_row_scale_lucas_low_digit_repeat_upper))) /\ (((exists bcf_height_lucas_low_digit_repeat_upper_decoded_value. bcf_height_lucas_low_digit_repeat_upper_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_value. bcf_row_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_upper) + (C))))))))) -> (((exists bcf_lt_gap_lucas_low_digit_repeat_lower_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_lower_out_of_range + S (a) = b) /\ D = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_lower_in_range. bcf_le_gap_lucas_low_digit_repeat_lower_in_range + (b) = a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_lower bcf_row_code_scale_lucas_low_digit_repeat_lower bcf_row_scale_code_lucas_low_digit_repeat_lower bcf_row_scale_scale_lucas_low_digit_repeat_lower bcf_row_code_lucas_low_digit_repeat_lower bcf_row_scale_lucas_low_digit_repeat_lower. ((forall bcf_row_index_lucas_low_digit_repeat_lower_table. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_lower_table) = S (a)) -> exists bcf_row_code_lucas_low_digit_repeat_lower_table bcf_row_scale_lucas_low_digit_repeat_lower_table. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_lower_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_row_code_lucas_low_digit_repeat_lower_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_lower_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_row_scale_lucas_low_digit_repeat_lower_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_lower_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_lower_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_lower_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_lower_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_lower_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_lower_table) + (bcf_value_lucas_low_digit_repeat_lower_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_lower_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_lower_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table_zero_row. bcf_index_lucas_low_digit_repeat_lower_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_lower_table_zero_row /\ bcf_value_lucas_low_digit_repeat_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table bcf_previous_code_lucas_low_digit_repeat_lower_table bcf_previous_scale_lucas_low_digit_repeat_lower_table. bcf_row_index_lucas_low_digit_repeat_lower_table = S bcf_predecessor_lucas_low_digit_repeat_lower_table /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_lower_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_previous_code_lucas_low_digit_repeat_lower_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_lower_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_previous_scale_lucas_low_digit_repeat_lower_table))) /\ (forall bcf_index_lucas_low_digit_repeat_lower_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_lower_table_row_step) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_lower_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_entry. bcf_height_lucas_low_digit_repeat_lower_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_lower_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_lower_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_lower_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_lower_table) + (bcf_value_lucas_low_digit_repeat_lower_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_lower_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_lower_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step bcf_left_lucas_low_digit_repeat_lower_table_row_step bcf_right_lucas_low_digit_repeat_lower_table_row_step. bcf_index_lucas_low_digit_repeat_lower_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_lower_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_lower_table) + (bcf_left_lucas_low_digit_repeat_lower_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_lower_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_lower_table) + (bcf_right_lucas_low_digit_repeat_lower_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_lower_table_row_step = bcf_left_lucas_low_digit_repeat_lower_table_row_step + bcf_right_lucas_low_digit_repeat_lower_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_decoded_row_code. bcf_height_lucas_low_digit_repeat_lower_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_lower) = S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_row_code_lucas_low_digit_repeat_lower))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_decoded_row_scale. bcf_height_lucas_low_digit_repeat_lower_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_lower) = S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_row_scale_lucas_low_digit_repeat_lower))) /\ (((exists bcf_height_lucas_low_digit_repeat_lower_decoded_value. bcf_height_lucas_low_digit_repeat_lower_decoded_value + S (D) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_value. bcf_row_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_lower) + (D))))))))) -> (exists lld_left_repeat_result lld_right_repeat_result. (C) + (p) * lld_left_repeat_result = (D) + (p) * lld_right_repeat_result)

Proof neighborhood

Direct theorem prerequisites

LU0010 lucas_prime_block_zero_reassociation LU0011 lucas_prime_block_successor_reassociation choose_upper_eq_transport · Alpha closed choose_functional · Alpha closed mod_eq_refl · Stable closed choose_exists · Alpha closed LU000W lucas_prime_shift_below_base mod_eq_trans · Stable closed

Direct theorem dependents

LU0013 lucas_low_digit_congruence

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

75 script commands · 12 reading checkpoints · 6 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
lucas prime block zero reassociationlucas prime block successor reassociationlucas prime shift below base
01Fix variables and assumptionsL1–1

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

  1. L1
    intro p
02Induction on qL2–10

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 a
  3. L4
    intro b
  4. L5
    intro C
  5. L6
    intro D
  6. L7
    intro hprime
  7. L8
    intro hbound
  8. L9
    intro hupper
  9. L10
    intro hlower
03Establish hnormalizedL11–18

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

  1. L11
    have hnormalized : Choose(a,b,C)Definitions: Choose(a,b,C)Original native command in the exact edition
  2. L12
    specialize choose_upper_eq_transport (p * 0 + a)
  3. L13
    specialize choose_upper_eq_transport a
  4. L14
    specialize choose_upper_eq_transport b
  5. L15
    specialize choose_upper_eq_transport C
  6. L16
    apply choose_upper_eq_transport
  7. L17
    apply lucas_prime_block_zero_reassociation
  8. L18
    exact hupper
04Establish hequalL19–28

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

  1. L19
    have hequal : C = D
  2. L20
    specialize choose_functional a
  3. L21
    specialize choose_functional b
  4. L22
    specialize choose_functional C
  5. L23
    specialize choose_functional D
  6. L24
    apply choose_functional
  7. L25
    exact hnormalized
  8. L26
    exact hlower
  9. L27
    rewrite hequal
  10. L28
    apply mod_eq_refl
05Fix variables and assumptionsL29–36

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

  1. L29
    intro a
  2. L30
    intro b
  3. L31
    intro C
  4. L32
    intro D
  5. L33
    intro hprime
  6. L34
    intro hbound
  7. L35
    intro hupper
  8. L36
    intro hlower
06Establish hnormalizedL37–44

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

  1. L37
    have hnormalized : Choose(p + (p · q + a),b,C)Definitions: Choose(p + (p · q + a),b,C)Original native command in the exact edition
  2. L38
    specialize choose_upper_eq_transport (p * S q + a)
  3. L39
    specialize choose_upper_eq_transport (p + (p * q + a))
  4. L40
    specialize choose_upper_eq_transport b
  5. L41
    specialize choose_upper_eq_transport C
  6. L42
    apply choose_upper_eq_transport
  7. L43
    apply lucas_prime_block_successor_reassociation
  8. L44
    exact hupper
07Establish hmiddleL45–46

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

  1. L45
    have hmiddle : ∃ D. Choose(p · q + a,b,D)Definitions: Choose(p · q + a,b,D)Original native command in the exact edition
  2. L46
    apply choose_exists
08Separate the logical casesL47–47

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

  1. L47
    cases hmiddle
09Establish hshiftL48–57

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

  1. L48
    have hshift : ModEq(p,C,x)Definitions: ModEq(p,C,x)Original native command in the exact edition
  2. L49
    specialize lucas_prime_shift_below_base p
  3. L50
    specialize lucas_prime_shift_below_base (p * q + a)
  4. L51
    specialize lucas_prime_shift_below_base b
  5. L52
    specialize lucas_prime_shift_below_base C
  6. L53
    specialize lucas_prime_shift_below_base x
  7. L54
    apply lucas_prime_shift_below_base
  8. L55
    exact hprime
  9. L56
    exact hbound
  10. L57
    exact hnormalized
10Use earlier factsL58–58

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

  1. L58
    exact hmiddle_witness
11Establish hremainingL59–68

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

  1. L59
    have hremaining : ModEq(p,x,D)Definitions: ModEq(p,x,D)Original native command in the exact edition
  2. L60
    specialize IH a
  3. L61
    specialize IH b
  4. L62
    specialize IH x
  5. L63
    specialize IH D
  6. L64
    apply IH
  7. L65
    exact hprime
  8. L66
    exact hbound
  9. L67
    exact hmiddle_witness
  10. L68
    exact hlower
12Use earlier factsL69–75

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

  1. L69
    specialize mod_eq_trans p
  2. L70
    specialize mod_eq_trans C
  3. L71
    specialize mod_eq_trans x
  4. L72
    specialize mod_eq_trans D
  5. L73
    apply mod_eq_trans
  6. L74
    exact hshift
  7. L75
    exact hremaining

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro p
  2. 0002induction q
  3. 0003intro a
  4. 0004intro b
  5. 0005intro C
  6. 0006intro D
  7. 0007intro hprime
  8. 0008intro hbound
  9. 0009intro hupper
  10. 0010intro hlower
  11. 0011have hnormalized : Choose(a,b,C)
    Exact native replay linehave hnormalized : ((exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_out_of_range + S (a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_zero_normalized_in_range. bcf_le_gap_lucas_low_digit_repeat_zero_normalized_in_range + (b) = a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_zero_normalized bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized bcf_row_code_lucas_low_digit_repeat_zero_normalized bcf_row_scale_lucas_low_digit_repeat_zero_normalized. ((forall bcf_row_index_lucas_low_digit_repeat_zero_normalized_table. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table) = S (a)) -> exists bcf_row_code_lucas_low_digit_repeat_zero_normalized_table bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_code_lucas_low_digit_repeat_zero_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_zero_normalized_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_zero_row. bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_zero_row /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table. bcf_row_index_lucas_low_digit_repeat_zero_normalized_table = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table))) /\ (forall bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_entry. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step. bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step = bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step + bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_code. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_zero_normalized) = S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_code_lucas_low_digit_repeat_zero_normalized))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_zero_normalized) = S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_scale_lucas_low_digit_repeat_zero_normalized))) /\ (((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_value. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_value. bcf_row_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized) + (C))))))))
  12. 0012specialize choose_upper_eq_transport (p * 0 + a)
  13. 0013specialize choose_upper_eq_transport a
  14. 0014specialize choose_upper_eq_transport b
  15. 0015specialize choose_upper_eq_transport C
  16. 0016apply choose_upper_eq_transport
  17. 0017apply lucas_prime_block_zero_reassociation
  18. 0018exact hupper
  19. 0019have hequal : C = D
  20. 0020specialize choose_functional a
  21. 0021specialize choose_functional b
  22. 0022specialize choose_functional C
  23. 0023specialize choose_functional D
  24. 0024apply choose_functional
  25. 0025exact hnormalized
  26. 0026exact hlower
  27. 0027rewrite hequal
  28. 0028apply mod_eq_refl
  29. 0029intro a
  30. 0030intro b
  31. 0031intro C
  32. 0032intro D
  33. 0033intro hprime
  34. 0034intro hbound
  35. 0035intro hupper
  36. 0036intro hlower
  37. 0037have hnormalized : Choose(p + (p · q + a),b,C)
    Exact native replay linehave hnormalized : ((exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_out_of_range + S (p + (p * q + a)) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_successor_normalized_in_range. bcf_le_gap_lucas_low_digit_repeat_successor_normalized_in_range + (b) = p + (p * q + a)) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_successor_normalized bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized bcf_row_code_lucas_low_digit_repeat_successor_normalized bcf_row_scale_lucas_low_digit_repeat_successor_normalized. ((forall bcf_row_index_lucas_low_digit_repeat_successor_normalized_table. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table) = S (p + (p * q + a))) -> exists bcf_row_code_lucas_low_digit_repeat_successor_normalized_table bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_code_lucas_low_digit_repeat_successor_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_successor_normalized_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row) = S (p + (p * q + a))) -> exists bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_zero_row. bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_zero_row /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table. bcf_row_index_lucas_low_digit_repeat_successor_normalized_table = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table))) /\ (forall bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step) = S (p + (p * q + a))) -> exists bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_entry. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step. bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step = bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step + bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_code. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_successor_normalized) = S ((S (p + (p * q + a))) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_code * S ((S (p + (p * q + a))) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_code_lucas_low_digit_repeat_successor_normalized))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_successor_normalized) = S ((S (p + (p * q + a))) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_scale * S ((S (p + (p * q + a))) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_scale_lucas_low_digit_repeat_successor_normalized))) /\ (((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_value. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_value. bcf_row_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized) + (C))))))))
  38. 0038specialize choose_upper_eq_transport (p * S q + a)
  39. 0039specialize choose_upper_eq_transport (p + (p * q + a))
  40. 0040specialize choose_upper_eq_transport b
  41. 0041specialize choose_upper_eq_transport C
  42. 0042apply choose_upper_eq_transport
  43. 0043apply lucas_prime_block_successor_reassociation
  44. 0044exact hupper
  45. 0045have hmiddle : ∃ D. Choose(p · q + a,b,D)
    Exact native replay linehave hmiddle : exists D. ((exists bcf_lt_gap_lucas_low_digit_repeat_middle_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_middle_out_of_range + S (p * q + a) = b) /\ D = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_middle_in_range. bcf_le_gap_lucas_low_digit_repeat_middle_in_range + (b) = p * q + a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_middle bcf_row_code_scale_lucas_low_digit_repeat_middle bcf_row_scale_code_lucas_low_digit_repeat_middle bcf_row_scale_scale_lucas_low_digit_repeat_middle bcf_row_code_lucas_low_digit_repeat_middle bcf_row_scale_lucas_low_digit_repeat_middle. ((forall bcf_row_index_lucas_low_digit_repeat_middle_table. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_middle_table) = S (p * q + a)) -> exists bcf_row_code_lucas_low_digit_repeat_middle_table bcf_row_scale_lucas_low_digit_repeat_middle_table. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_middle_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_row_code_lucas_low_digit_repeat_middle_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_middle_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_row_scale_lucas_low_digit_repeat_middle_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_middle_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_middle_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_middle_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_middle_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_middle_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_middle_table) + (bcf_value_lucas_low_digit_repeat_middle_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_middle_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_middle_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table_zero_row. bcf_index_lucas_low_digit_repeat_middle_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_middle_table_zero_row /\ bcf_value_lucas_low_digit_repeat_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table bcf_previous_code_lucas_low_digit_repeat_middle_table bcf_previous_scale_lucas_low_digit_repeat_middle_table. bcf_row_index_lucas_low_digit_repeat_middle_table = S bcf_predecessor_lucas_low_digit_repeat_middle_table /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_middle_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_previous_code_lucas_low_digit_repeat_middle_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_middle_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_previous_scale_lucas_low_digit_repeat_middle_table))) /\ (forall bcf_index_lucas_low_digit_repeat_middle_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_middle_table_row_step) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_middle_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_entry. bcf_height_lucas_low_digit_repeat_middle_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_middle_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_middle_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_middle_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_middle_table) + (bcf_value_lucas_low_digit_repeat_middle_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_middle_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_middle_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step bcf_left_lucas_low_digit_repeat_middle_table_row_step bcf_right_lucas_low_digit_repeat_middle_table_row_step. bcf_index_lucas_low_digit_repeat_middle_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_middle_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_middle_table) + (bcf_left_lucas_low_digit_repeat_middle_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_middle_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_middle_table) + (bcf_right_lucas_low_digit_repeat_middle_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_middle_table_row_step = bcf_left_lucas_low_digit_repeat_middle_table_row_step + bcf_right_lucas_low_digit_repeat_middle_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_decoded_row_code. bcf_height_lucas_low_digit_repeat_middle_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_middle) = S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_code * S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_row_code_lucas_low_digit_repeat_middle))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_decoded_row_scale. bcf_height_lucas_low_digit_repeat_middle_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_middle) = S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_scale * S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_row_scale_lucas_low_digit_repeat_middle))) /\ (((exists bcf_height_lucas_low_digit_repeat_middle_decoded_value. bcf_height_lucas_low_digit_repeat_middle_decoded_value + S (D) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_value. bcf_row_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_middle) + (D))))))))
  46. 0046apply choose_exists
  47. 0047cases hmiddle
  48. 0048have hshift : ModEq(p,C,x)
    Exact native replay linehave hshift : exists lld_left_repeat_shift lld_right_repeat_shift. (C) + (p) * lld_left_repeat_shift = (x) + (p) * lld_right_repeat_shift
  49. 0049specialize lucas_prime_shift_below_base p
  50. 0050specialize lucas_prime_shift_below_base (p * q + a)
  51. 0051specialize lucas_prime_shift_below_base b
  52. 0052specialize lucas_prime_shift_below_base C
  53. 0053specialize lucas_prime_shift_below_base x
  54. 0054apply lucas_prime_shift_below_base
  55. 0055exact hprime
  56. 0056exact hbound
  57. 0057exact hnormalized
  58. 0058exact hmiddle_witness
  59. 0059have hremaining : ModEq(p,x,D)
    Exact native replay linehave hremaining : exists lld_left_repeat_remaining lld_right_repeat_remaining. (x) + (p) * lld_left_repeat_remaining = (D) + (p) * lld_right_repeat_remaining
  60. 0060specialize IH a
  61. 0061specialize IH b
  62. 0062specialize IH x
  63. 0063specialize IH D
  64. 0064apply IH
  65. 0065exact hprime
  66. 0066exact hbound
  67. 0067exact hmiddle_witness
  68. 0068exact hlower
  69. 0069specialize mod_eq_trans p
  70. 0070specialize mod_eq_trans C
  71. 0071specialize mod_eq_trans x
  72. 0072specialize mod_eq_trans D
  73. 0073apply mod_eq_trans
  74. 0074exact hshift
  75. 0075exact hremaining