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. ∀ a. ∀ b. ∀ C. ∀ D. Prime(p) → Lt(b,p) → Choose(p + 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
In local proof propositions
Exact expanded first-order statement
forall p a b C D. ((~(p = 1) /\ forall frm_prime_left_lucas_convolution_prime frm_prime_right_lucas_convolution_prime. p = frm_prime_left_lucas_convolution_prime * frm_prime_right_lucas_convolution_prime -> frm_prime_left_lucas_convolution_prime = 1 \/ frm_prime_right_lucas_convolution_prime = 1)) -> (exists lcv_gap_shift_bound. lcv_gap_shift_bound + S (b) = (p)) -> (((exists bcf_lt_gap_lucas_convolution_shift_upper_out_of_range. bcf_lt_gap_lucas_convolution_shift_upper_out_of_range + S (p + a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_upper_in_range. bcf_le_gap_lucas_convolution_shift_upper_in_range + (b) = p + a) /\ (exists bcf_row_code_code_lucas_convolution_shift_upper bcf_row_code_scale_lucas_convolution_shift_upper bcf_row_scale_code_lucas_convolution_shift_upper bcf_row_scale_scale_lucas_convolution_shift_upper bcf_row_code_lucas_convolution_shift_upper bcf_row_scale_lucas_convolution_shift_upper. ((forall bcf_row_index_lucas_convolution_shift_upper_table. (exists bcf_lt_gap_lucas_convolution_shift_upper_table_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_table_row_bound + S (bcf_row_index_lucas_convolution_shift_upper_table) = S (p + a)) -> exists bcf_row_code_lucas_convolution_shift_upper_table bcf_row_scale_lucas_convolution_shift_upper_table. ((((exists bcf_height_lucas_convolution_shift_upper_table_decoded_row_code. bcf_height_lucas_convolution_shift_upper_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_upper) + (bcf_row_code_lucas_convolution_shift_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_table_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper) + (bcf_row_scale_lucas_convolution_shift_upper_table))) /\ ((bcf_row_index_lucas_convolution_shift_upper_table = 0 /\ (forall bcf_index_lucas_convolution_shift_upper_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_upper_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_upper_table_zero_row) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_upper_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_upper_table_zero_row_entry. bcf_height_lucas_convolution_shift_upper_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_upper_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_upper_table = bcf_quotient_lucas_convolution_shift_upper_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_table) + (bcf_value_lucas_convolution_shift_upper_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_upper_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_table_zero_row. bcf_index_lucas_convolution_shift_upper_table_zero_row = S bcf_predecessor_lucas_convolution_shift_upper_table_zero_row /\ bcf_value_lucas_convolution_shift_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_upper_table bcf_previous_code_lucas_convolution_shift_upper_table bcf_previous_scale_lucas_convolution_shift_upper_table. bcf_row_index_lucas_convolution_shift_upper_table = S bcf_predecessor_lucas_convolution_shift_upper_table /\ ((((exists bcf_height_lucas_convolution_shift_upper_table_decoded_previous_code. bcf_height_lucas_convolution_shift_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_upper) + (bcf_previous_code_lucas_convolution_shift_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper) + (bcf_previous_scale_lucas_convolution_shift_upper_table))) /\ (forall bcf_index_lucas_convolution_shift_upper_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_upper_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_upper_table_row_step_bound + S (bcf_index_lucas_convolution_shift_upper_table_row_step) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_upper_table_row_step. ((((exists bcf_height_lucas_convolution_shift_upper_table_row_step_entry. bcf_height_lucas_convolution_shift_upper_table_row_step_entry + S (bcf_value_lucas_convolution_shift_upper_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_row_step_entry. bcf_row_code_lucas_convolution_shift_upper_table = bcf_quotient_lucas_convolution_shift_upper_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_table) + (bcf_value_lucas_convolution_shift_upper_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_upper_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_table_row_step bcf_left_lucas_convolution_shift_upper_table_row_step bcf_right_lucas_convolution_shift_upper_table_row_step. bcf_index_lucas_convolution_shift_upper_table_row_step = S bcf_predecessor_lucas_convolution_shift_upper_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_upper_table_row_step_previous_left. bcf_height_lucas_convolution_shift_upper_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_upper_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_upper_table = bcf_quotient_lucas_convolution_shift_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_table) + (bcf_left_lucas_convolution_shift_upper_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_table_row_step_previous_right. bcf_height_lucas_convolution_shift_upper_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_upper_table = bcf_quotient_lucas_convolution_shift_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_table) + (bcf_right_lucas_convolution_shift_upper_table_row_step))) /\ bcf_value_lucas_convolution_shift_upper_table_row_step = bcf_left_lucas_convolution_shift_upper_table_row_step + bcf_right_lucas_convolution_shift_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_decoded_row_code. bcf_height_lucas_convolution_shift_upper_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper) = S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_decoded_row_code * S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_upper) + (bcf_row_code_lucas_convolution_shift_upper))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper) = S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_decoded_row_scale * S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_upper) + (bcf_row_scale_lucas_convolution_shift_upper))) /\ (((exists bcf_height_lucas_convolution_shift_upper_decoded_value. bcf_height_lucas_convolution_shift_upper_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_convolution_shift_upper)) /\ exists bcf_quotient_lucas_convolution_shift_upper_decoded_value. bcf_row_code_lucas_convolution_shift_upper = bcf_quotient_lucas_convolution_shift_upper_decoded_value * S ((S (b)) * bcf_row_scale_lucas_convolution_shift_upper) + (C))))))))) -> (((exists bcf_lt_gap_lucas_convolution_shift_lower_out_of_range. bcf_lt_gap_lucas_convolution_shift_lower_out_of_range + S (a) = b) /\ D = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_lower_in_range. bcf_le_gap_lucas_convolution_shift_lower_in_range + (b) = a) /\ (exists bcf_row_code_code_lucas_convolution_shift_lower bcf_row_code_scale_lucas_convolution_shift_lower bcf_row_scale_code_lucas_convolution_shift_lower bcf_row_scale_scale_lucas_convolution_shift_lower bcf_row_code_lucas_convolution_shift_lower bcf_row_scale_lucas_convolution_shift_lower. ((forall bcf_row_index_lucas_convolution_shift_lower_table. (exists bcf_lt_gap_lucas_convolution_shift_lower_table_row_bound. bcf_lt_gap_lucas_convolution_shift_lower_table_row_bound + S (bcf_row_index_lucas_convolution_shift_lower_table) = S (a)) -> exists bcf_row_code_lucas_convolution_shift_lower_table bcf_row_scale_lucas_convolution_shift_lower_table. ((((exists bcf_height_lucas_convolution_shift_lower_table_decoded_row_code. bcf_height_lucas_convolution_shift_lower_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_lower) + (bcf_row_code_lucas_convolution_shift_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_table_decoded_row_scale. bcf_height_lucas_convolution_shift_lower_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower) + (bcf_row_scale_lucas_convolution_shift_lower_table))) /\ ((bcf_row_index_lucas_convolution_shift_lower_table = 0 /\ (forall bcf_index_lucas_convolution_shift_lower_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_lower_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_lower_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_lower_table_zero_row) = S (a)) -> exists bcf_value_lucas_convolution_shift_lower_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_lower_table_zero_row_entry. bcf_height_lucas_convolution_shift_lower_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_lower_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_lower_table = bcf_quotient_lucas_convolution_shift_lower_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_lower_table) + (bcf_value_lucas_convolution_shift_lower_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_lower_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_lower_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_lower_table_zero_row. bcf_index_lucas_convolution_shift_lower_table_zero_row = S bcf_predecessor_lucas_convolution_shift_lower_table_zero_row /\ bcf_value_lucas_convolution_shift_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_lower_table bcf_previous_code_lucas_convolution_shift_lower_table bcf_previous_scale_lucas_convolution_shift_lower_table. bcf_row_index_lucas_convolution_shift_lower_table = S bcf_predecessor_lucas_convolution_shift_lower_table /\ ((((exists bcf_height_lucas_convolution_shift_lower_table_decoded_previous_code. bcf_height_lucas_convolution_shift_lower_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_lower) + (bcf_previous_code_lucas_convolution_shift_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_lower_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower) + (bcf_previous_scale_lucas_convolution_shift_lower_table))) /\ (forall bcf_index_lucas_convolution_shift_lower_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_lower_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_lower_table_row_step_bound + S (bcf_index_lucas_convolution_shift_lower_table_row_step) = S (a)) -> exists bcf_value_lucas_convolution_shift_lower_table_row_step. ((((exists bcf_height_lucas_convolution_shift_lower_table_row_step_entry. bcf_height_lucas_convolution_shift_lower_table_row_step_entry + S (bcf_value_lucas_convolution_shift_lower_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_row_step_entry. bcf_row_code_lucas_convolution_shift_lower_table = bcf_quotient_lucas_convolution_shift_lower_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_lower_table) + (bcf_value_lucas_convolution_shift_lower_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_lower_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_lower_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_lower_table_row_step bcf_left_lucas_convolution_shift_lower_table_row_step bcf_right_lucas_convolution_shift_lower_table_row_step. bcf_index_lucas_convolution_shift_lower_table_row_step = S bcf_predecessor_lucas_convolution_shift_lower_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_lower_table_row_step_previous_left. bcf_height_lucas_convolution_shift_lower_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_lower_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_lower_table = bcf_quotient_lucas_convolution_shift_lower_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_lower_table) + (bcf_left_lucas_convolution_shift_lower_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_table_row_step_previous_right. bcf_height_lucas_convolution_shift_lower_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_lower_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_lower_table = bcf_quotient_lucas_convolution_shift_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_lower_table) + (bcf_right_lucas_convolution_shift_lower_table_row_step))) /\ bcf_value_lucas_convolution_shift_lower_table_row_step = bcf_left_lucas_convolution_shift_lower_table_row_step + bcf_right_lucas_convolution_shift_lower_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_decoded_row_code. bcf_height_lucas_convolution_shift_lower_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_lower) = S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_lower) + (bcf_row_code_lucas_convolution_shift_lower))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_decoded_row_scale. bcf_height_lucas_convolution_shift_lower_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_lower) = S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_lower) + (bcf_row_scale_lucas_convolution_shift_lower))) /\ (((exists bcf_height_lucas_convolution_shift_lower_decoded_value. bcf_height_lucas_convolution_shift_lower_decoded_value + S (D) = S ((S (b)) * bcf_row_scale_lucas_convolution_shift_lower)) /\ exists bcf_quotient_lucas_convolution_shift_lower_decoded_value. bcf_row_code_lucas_convolution_shift_lower = bcf_quotient_lucas_convolution_shift_lower_decoded_value * S ((S (b)) * bcf_row_scale_lucas_convolution_shift_lower) + (D))))))))) -> (exists lcv_left_shift_result lcv_right_shift_result. (C) + (p) * lcv_left_shift_result = (D) + (p) * lcv_right_shift_result)Proof neighborhood
Direct theorem prerequisites
eq_decidable · Stable closed
LU000P lucas_choose_zero_index_is_one mod_eq_refl · Stable closed choose_upper_eq_transport · Alpha closed LU000T lucas_prime_row_interior_zero_mod LU000Q lucas_choose_zero_upper_positive_is_zero nonzero_is_succ · Stable closed LU000V lucas_predecessor_digit_below_base choose_exists · Alpha closed LU000O lucas_choose_lower_eq_transport choose_succ_succ · Alpha closed LU000U lucas_pascal_congruence_stepDirect theorem dependents
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
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 (6)
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro p
02Induction on aL2–9
03Establish hcaseL10–13
04Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases hcase
05Establish hCL15–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose zero index is one.
06Establish hDL22–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose zero index is one.
07Use earlier factsL32–33
08Establish hDzeroL34–39
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.
09Establish hprime_rowL40–49
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose upper eq transport.
- L40
have hprime_row : Choose(p,b,C)Definitions: Choose(p,b,C)Original native command in the exact edition - L41
specialize choose_upper_eq_transport (p + 0) - L42
specialize choose_upper_eq_transport p - L43
specialize choose_upper_eq_transport b - L44
specialize choose_upper_eq_transport C - L45
apply choose_upper_eq_transport - L46
apply PA3 - L47
exact hupper - L48
rewrite hDzero - L49
specialize lucas_prime_row_interior_zero_mod p
10Use earlier factsL50–56
11Fix variables and assumptionsL57–63
12Establish hcaseL64–67
13Separate the logical casesL68–68
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L68
cases hcase
14Establish hCL69–75
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose zero index is one.
15Establish hDL76–85
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose zero index is one.
16Use earlier factsL86–87
17Establish hsuccessorL88–91
18Separate the logical casesL92–92
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L92
cases hsuccessor
19Establish hsuccessor_boundL93–95
Establish this local claim before using it. It is not an additional assumption.
20Establish hpredecessor_boundL96–100
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas predecessor digit below base.
21Establish hleft_upperL101–102
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose exists.
- L101
have hleft_upper : ∃ C. Choose(p + a,x,C)Definitions: Choose(p + a,x,C)Original native command in the exact edition - L102
apply choose_exists
22Separate the logical casesL103–103
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L103
cases hleft_upper
23Establish hright_upperL104–105
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose exists.
- L104
have hright_upper : ∃ C. Choose(p + a,S x,C)Definitions: Choose(p + a,S x,C)Original native command in the exact edition - L105
apply choose_exists
24Separate the logical casesL106–106
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L106
cases hright_upper
25Establish hleft_lowerL107–108
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose exists.
- L107
have hleft_lower : ∃ C. Choose(a,x,C)Definitions: Choose(a,x,C)Original native command in the exact edition - L108
apply choose_exists
26Separate the logical casesL109–109
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L109
cases hleft_lower
27Establish hright_lowerL110–111
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose exists.
- L110
have hright_lower : ∃ C. Choose(a,S x,C)Definitions: Choose(a,S x,C)Original native command in the exact edition - L111
apply choose_exists
28Separate the logical casesL112–112
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L112
cases hright_lower
29Establish hleft_modL113–121
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
30Establish hright_modL122–130
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
31Establish hupper_indexL131–138
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.
- L131
have hupper_index : Choose(p + S a,S x,C)Definitions: Choose(p + S a,S x,C)Original native command in the exact edition - L132
specialize lucas_choose_lower_eq_transport (p + S a) - L133
specialize lucas_choose_lower_eq_transport b - L134
specialize lucas_choose_lower_eq_transport (S x) - L135
specialize lucas_choose_lower_eq_transport C - L136
apply lucas_choose_lower_eq_transport - L137
exact hsuccessor_witness - L138
exact hupper
32Establish hupper_normalL139–146
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose upper eq transport.
- L139
have hupper_normal : Choose(S (p + a),S x,C)Definitions: Choose(S (p + a),S x,C)Original native command in the exact edition - L140
specialize choose_upper_eq_transport (p + S a) - L141
specialize choose_upper_eq_transport (S (p + a)) - L142
specialize choose_upper_eq_transport (S x) - L143
specialize choose_upper_eq_transport C - L144
apply choose_upper_eq_transport - L145
apply PA4 - L146
exact hupper_index
33Establish hlower_normalL147–154
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.
- L147
have hlower_normal : Choose(S a,S x,D)Definitions: Choose(S a,S x,D)Original native command in the exact edition - L148
specialize lucas_choose_lower_eq_transport (S a) - L149
specialize lucas_choose_lower_eq_transport b - L150
specialize lucas_choose_lower_eq_transport (S x) - L151
specialize lucas_choose_lower_eq_transport D - L152
apply lucas_choose_lower_eq_transport - L153
exact hsuccessor_witness - L154
exact hlower
34Establish hlower_sumL155–164
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose succ succ.
- L155
have hlower_sum : D = x3 + x4 - L156
specialize choose_succ_succ a - L157
specialize choose_succ_succ x - L158
specialize choose_succ_succ x3 - L159
specialize choose_succ_succ x4 - L160
specialize choose_succ_succ D - L161
apply choose_succ_succ - L162
exact hleft_lower_witness - L163
exact hright_lower_witness - L164
exact hlower_normal
35Calculate and transport equalitiesL165–165
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L165
rewrite hlower_sum
36Use earlier factsL166–175
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L166
specialize lucas_pascal_congruence_step p - L167
specialize lucas_pascal_congruence_step (p + a) - L168
specialize lucas_pascal_congruence_step x - L169
specialize lucas_pascal_congruence_step x1 - L170
specialize lucas_pascal_congruence_step x2 - L171
specialize lucas_pascal_congruence_step C - L172
specialize lucas_pascal_congruence_step x3 - L173
specialize lucas_pascal_congruence_step x4 - L174
apply lucas_pascal_congruence_step - L175
exact hleft_upper_witness
Original defined command ledger · 179 lines
- 0001
intro p - 0002
induction a - 0003
intro b - 0004
intro C - 0005
intro D - 0006
intro hprime - 0007
intro hbound - 0008
intro hupper - 0009
intro hlower - 0010
have hcase : b = 0 \/ ~(b = 0) - 0011
specialize eq_decidable b - 0012
specialize eq_decidable 0 - 0013
exact eq_decidable - 0014
cases hcase - 0015
have hC : C = 1 - 0016
specialize lucas_choose_zero_index_is_one (p + 0) - 0017
specialize lucas_choose_zero_index_is_one b - 0018
specialize lucas_choose_zero_index_is_one C - 0019
apply lucas_choose_zero_index_is_one - 0020
exact hcase_left - 0021
exact hupper - 0022
have hD : D = 1 - 0023
specialize lucas_choose_zero_index_is_one 0 - 0024
specialize lucas_choose_zero_index_is_one b - 0025
specialize lucas_choose_zero_index_is_one D - 0026
apply lucas_choose_zero_index_is_one - 0027
exact hcase_left - 0028
exact hlower - 0029
rewrite hC - 0030
rewrite hD - 0031
specialize mod_eq_refl p - 0032
specialize mod_eq_refl 1 - 0033
exact mod_eq_refl - 0034
have hDzero : D = 0 - 0035
specialize lucas_choose_zero_upper_positive_is_zero b - 0036
specialize lucas_choose_zero_upper_positive_is_zero D - 0037
apply lucas_choose_zero_upper_positive_is_zero - 0038
exact hcase_right - 0039
exact hlower - 0040
have hprime_row : Choose(p,b,C)Exact native replay line
have hprime_row : ((exists bcf_lt_gap_lucas_convolution_shift_prime_row_out_of_range. bcf_lt_gap_lucas_convolution_shift_prime_row_out_of_range + S (p) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_prime_row_in_range. bcf_le_gap_lucas_convolution_shift_prime_row_in_range + (b) = p) /\ (exists bcf_row_code_code_lucas_convolution_shift_prime_row bcf_row_code_scale_lucas_convolution_shift_prime_row bcf_row_scale_code_lucas_convolution_shift_prime_row bcf_row_scale_scale_lucas_convolution_shift_prime_row bcf_row_code_lucas_convolution_shift_prime_row bcf_row_scale_lucas_convolution_shift_prime_row. ((forall bcf_row_index_lucas_convolution_shift_prime_row_table. (exists bcf_lt_gap_lucas_convolution_shift_prime_row_table_row_bound. bcf_lt_gap_lucas_convolution_shift_prime_row_table_row_bound + S (bcf_row_index_lucas_convolution_shift_prime_row_table) = S (p)) -> exists bcf_row_code_lucas_convolution_shift_prime_row_table bcf_row_scale_lucas_convolution_shift_prime_row_table. ((((exists bcf_height_lucas_convolution_shift_prime_row_table_decoded_row_code. bcf_height_lucas_convolution_shift_prime_row_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_prime_row_table) = S ((S (bcf_row_index_lucas_convolution_shift_prime_row_table)) * bcf_row_code_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_prime_row_table)) * bcf_row_code_scale_lucas_convolution_shift_prime_row) + (bcf_row_code_lucas_convolution_shift_prime_row_table))) /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_table_decoded_row_scale. bcf_height_lucas_convolution_shift_prime_row_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_prime_row_table) = S ((S (bcf_row_index_lucas_convolution_shift_prime_row_table)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_prime_row_table)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row) + (bcf_row_scale_lucas_convolution_shift_prime_row_table))) /\ ((bcf_row_index_lucas_convolution_shift_prime_row_table = 0 /\ (forall bcf_index_lucas_convolution_shift_prime_row_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_prime_row_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_prime_row_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_prime_row_table_zero_row) = S (p)) -> exists bcf_value_lucas_convolution_shift_prime_row_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_prime_row_table_zero_row_entry. bcf_height_lucas_convolution_shift_prime_row_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_prime_row_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_prime_row_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_prime_row_table)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_prime_row_table = bcf_quotient_lucas_convolution_shift_prime_row_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_prime_row_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_prime_row_table) + (bcf_value_lucas_convolution_shift_prime_row_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_prime_row_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_prime_row_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_prime_row_table_zero_row. bcf_index_lucas_convolution_shift_prime_row_table_zero_row = S bcf_predecessor_lucas_convolution_shift_prime_row_table_zero_row /\ bcf_value_lucas_convolution_shift_prime_row_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_prime_row_table bcf_previous_code_lucas_convolution_shift_prime_row_table bcf_previous_scale_lucas_convolution_shift_prime_row_table. bcf_row_index_lucas_convolution_shift_prime_row_table = S bcf_predecessor_lucas_convolution_shift_prime_row_table /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_table_decoded_previous_code. bcf_height_lucas_convolution_shift_prime_row_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_prime_row_table) = S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table)) * bcf_row_code_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table)) * bcf_row_code_scale_lucas_convolution_shift_prime_row) + (bcf_previous_code_lucas_convolution_shift_prime_row_table))) /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_prime_row_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_prime_row_table) = S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row) + (bcf_previous_scale_lucas_convolution_shift_prime_row_table))) /\ (forall bcf_index_lucas_convolution_shift_prime_row_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_prime_row_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_prime_row_table_row_step_bound + S (bcf_index_lucas_convolution_shift_prime_row_table_row_step) = S (p)) -> exists bcf_value_lucas_convolution_shift_prime_row_table_row_step. ((((exists bcf_height_lucas_convolution_shift_prime_row_table_row_step_entry. bcf_height_lucas_convolution_shift_prime_row_table_row_step_entry + S (bcf_value_lucas_convolution_shift_prime_row_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_prime_row_table_row_step)) * bcf_row_scale_lucas_convolution_shift_prime_row_table)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_entry. bcf_row_code_lucas_convolution_shift_prime_row_table = bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_prime_row_table_row_step)) * bcf_row_scale_lucas_convolution_shift_prime_row_table) + (bcf_value_lucas_convolution_shift_prime_row_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_prime_row_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_prime_row_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step bcf_left_lucas_convolution_shift_prime_row_table_row_step bcf_right_lucas_convolution_shift_prime_row_table_row_step. bcf_index_lucas_convolution_shift_prime_row_table_row_step = S bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_table_row_step_previous_left. bcf_height_lucas_convolution_shift_prime_row_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_prime_row_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_prime_row_table)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_prime_row_table = bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_prime_row_table) + (bcf_left_lucas_convolution_shift_prime_row_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_table_row_step_previous_right. bcf_height_lucas_convolution_shift_prime_row_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_prime_row_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_prime_row_table)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_prime_row_table = bcf_quotient_lucas_convolution_shift_prime_row_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_prime_row_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_prime_row_table) + (bcf_right_lucas_convolution_shift_prime_row_table_row_step))) /\ bcf_value_lucas_convolution_shift_prime_row_table_row_step = bcf_left_lucas_convolution_shift_prime_row_table_row_step + bcf_right_lucas_convolution_shift_prime_row_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_decoded_row_code. bcf_height_lucas_convolution_shift_prime_row_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_prime_row) = S ((S (p)) * bcf_row_code_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_decoded_row_code * S ((S (p)) * bcf_row_code_scale_lucas_convolution_shift_prime_row) + (bcf_row_code_lucas_convolution_shift_prime_row))) /\ ((((exists bcf_height_lucas_convolution_shift_prime_row_decoded_row_scale. bcf_height_lucas_convolution_shift_prime_row_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_prime_row) = S ((S (p)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_decoded_row_scale * S ((S (p)) * bcf_row_scale_scale_lucas_convolution_shift_prime_row) + (bcf_row_scale_lucas_convolution_shift_prime_row))) /\ (((exists bcf_height_lucas_convolution_shift_prime_row_decoded_value. bcf_height_lucas_convolution_shift_prime_row_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_convolution_shift_prime_row)) /\ exists bcf_quotient_lucas_convolution_shift_prime_row_decoded_value. bcf_row_code_lucas_convolution_shift_prime_row = bcf_quotient_lucas_convolution_shift_prime_row_decoded_value * S ((S (b)) * bcf_row_scale_lucas_convolution_shift_prime_row) + (C)))))))) - 0041
specialize choose_upper_eq_transport (p + 0) - 0042
specialize choose_upper_eq_transport p - 0043
specialize choose_upper_eq_transport b - 0044
specialize choose_upper_eq_transport C - 0045
apply choose_upper_eq_transport - 0046
apply PA3 - 0047
exact hupper - 0048
rewrite hDzero - 0049
specialize lucas_prime_row_interior_zero_mod p - 0050
specialize lucas_prime_row_interior_zero_mod b - 0051
specialize lucas_prime_row_interior_zero_mod C - 0052
apply lucas_prime_row_interior_zero_mod - 0053
exact hprime - 0054
exact hcase_right - 0055
exact hbound - 0056
exact hprime_row - 0057
intro b - 0058
intro C - 0059
intro D - 0060
intro hprime - 0061
intro hbound - 0062
intro hupper - 0063
intro hlower - 0064
have hcase : b = 0 \/ ~(b = 0) - 0065
specialize eq_decidable b - 0066
specialize eq_decidable 0 - 0067
exact eq_decidable - 0068
cases hcase - 0069
have hC : C = 1 - 0070
specialize lucas_choose_zero_index_is_one (p + S a) - 0071
specialize lucas_choose_zero_index_is_one b - 0072
specialize lucas_choose_zero_index_is_one C - 0073
apply lucas_choose_zero_index_is_one - 0074
exact hcase_left - 0075
exact hupper - 0076
have hD : D = 1 - 0077
specialize lucas_choose_zero_index_is_one (S a) - 0078
specialize lucas_choose_zero_index_is_one b - 0079
specialize lucas_choose_zero_index_is_one D - 0080
apply lucas_choose_zero_index_is_one - 0081
exact hcase_left - 0082
exact hlower - 0083
rewrite hC - 0084
rewrite hD - 0085
specialize mod_eq_refl p - 0086
specialize mod_eq_refl 1 - 0087
exact mod_eq_refl - 0088
have hsuccessor : exists k. b = S k - 0089
specialize nonzero_is_succ b - 0090
apply nonzero_is_succ - 0091
exact hcase_right - 0092
cases hsuccessor - 0093
have hsuccessor_bound : Lt(S x,p)Exact native replay line
have hsuccessor_bound : exists lcv_gap_shift_successor_bound. lcv_gap_shift_successor_bound + S (S x) = (p) - 0094
rewrite <- hsuccessor_witness - 0095
exact hbound - 0096
have hpredecessor_bound : Lt(x,p)Exact native replay line
have hpredecessor_bound : exists lcv_gap_shift_predecessor_bound. lcv_gap_shift_predecessor_bound + S (x) = (p) - 0097
specialize lucas_predecessor_digit_below_base p - 0098
specialize lucas_predecessor_digit_below_base x - 0099
apply lucas_predecessor_digit_below_base - 0100
exact hsuccessor_bound - 0101
have hleft_upper : ∃ C. Choose(p + a,x,C)Exact native replay line
have hleft_upper : exists C. ((exists bcf_lt_gap_lucas_convolution_shift_left_upper_out_of_range. bcf_lt_gap_lucas_convolution_shift_left_upper_out_of_range + S (p + a) = x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_left_upper_in_range. bcf_le_gap_lucas_convolution_shift_left_upper_in_range + (x) = p + a) /\ (exists bcf_row_code_code_lucas_convolution_shift_left_upper bcf_row_code_scale_lucas_convolution_shift_left_upper bcf_row_scale_code_lucas_convolution_shift_left_upper bcf_row_scale_scale_lucas_convolution_shift_left_upper bcf_row_code_lucas_convolution_shift_left_upper bcf_row_scale_lucas_convolution_shift_left_upper. ((forall bcf_row_index_lucas_convolution_shift_left_upper_table. (exists bcf_lt_gap_lucas_convolution_shift_left_upper_table_row_bound. bcf_lt_gap_lucas_convolution_shift_left_upper_table_row_bound + S (bcf_row_index_lucas_convolution_shift_left_upper_table) = S (p + a)) -> exists bcf_row_code_lucas_convolution_shift_left_upper_table bcf_row_scale_lucas_convolution_shift_left_upper_table. ((((exists bcf_height_lucas_convolution_shift_left_upper_table_decoded_row_code. bcf_height_lucas_convolution_shift_left_upper_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_left_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_left_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_left_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_left_upper) + (bcf_row_code_lucas_convolution_shift_left_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_table_decoded_row_scale. bcf_height_lucas_convolution_shift_left_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_left_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_left_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_left_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper) + (bcf_row_scale_lucas_convolution_shift_left_upper_table))) /\ ((bcf_row_index_lucas_convolution_shift_left_upper_table = 0 /\ (forall bcf_index_lucas_convolution_shift_left_upper_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_left_upper_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_left_upper_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_left_upper_table_zero_row) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_left_upper_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_left_upper_table_zero_row_entry. bcf_height_lucas_convolution_shift_left_upper_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_left_upper_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_left_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_left_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_left_upper_table = bcf_quotient_lucas_convolution_shift_left_upper_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_left_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_left_upper_table) + (bcf_value_lucas_convolution_shift_left_upper_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_left_upper_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_left_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_left_upper_table_zero_row. bcf_index_lucas_convolution_shift_left_upper_table_zero_row = S bcf_predecessor_lucas_convolution_shift_left_upper_table_zero_row /\ bcf_value_lucas_convolution_shift_left_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_left_upper_table bcf_previous_code_lucas_convolution_shift_left_upper_table bcf_previous_scale_lucas_convolution_shift_left_upper_table. bcf_row_index_lucas_convolution_shift_left_upper_table = S bcf_predecessor_lucas_convolution_shift_left_upper_table /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_table_decoded_previous_code. bcf_height_lucas_convolution_shift_left_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_left_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_left_upper) + (bcf_previous_code_lucas_convolution_shift_left_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_left_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_left_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper) + (bcf_previous_scale_lucas_convolution_shift_left_upper_table))) /\ (forall bcf_index_lucas_convolution_shift_left_upper_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_left_upper_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_left_upper_table_row_step_bound + S (bcf_index_lucas_convolution_shift_left_upper_table_row_step) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_left_upper_table_row_step. ((((exists bcf_height_lucas_convolution_shift_left_upper_table_row_step_entry. bcf_height_lucas_convolution_shift_left_upper_table_row_step_entry + S (bcf_value_lucas_convolution_shift_left_upper_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_left_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_left_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_entry. bcf_row_code_lucas_convolution_shift_left_upper_table = bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_left_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_left_upper_table) + (bcf_value_lucas_convolution_shift_left_upper_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_left_upper_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_left_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step bcf_left_lucas_convolution_shift_left_upper_table_row_step bcf_right_lucas_convolution_shift_left_upper_table_row_step. bcf_index_lucas_convolution_shift_left_upper_table_row_step = S bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_table_row_step_previous_left. bcf_height_lucas_convolution_shift_left_upper_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_left_upper_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_left_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_left_upper_table = bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_left_upper_table) + (bcf_left_lucas_convolution_shift_left_upper_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_table_row_step_previous_right. bcf_height_lucas_convolution_shift_left_upper_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_left_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_left_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_left_upper_table = bcf_quotient_lucas_convolution_shift_left_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_left_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_left_upper_table) + (bcf_right_lucas_convolution_shift_left_upper_table_row_step))) /\ bcf_value_lucas_convolution_shift_left_upper_table_row_step = bcf_left_lucas_convolution_shift_left_upper_table_row_step + bcf_right_lucas_convolution_shift_left_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_decoded_row_code. bcf_height_lucas_convolution_shift_left_upper_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_left_upper) = S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_decoded_row_code * S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_left_upper) + (bcf_row_code_lucas_convolution_shift_left_upper))) /\ ((((exists bcf_height_lucas_convolution_shift_left_upper_decoded_row_scale. bcf_height_lucas_convolution_shift_left_upper_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_left_upper) = S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_decoded_row_scale * S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_left_upper) + (bcf_row_scale_lucas_convolution_shift_left_upper))) /\ (((exists bcf_height_lucas_convolution_shift_left_upper_decoded_value. bcf_height_lucas_convolution_shift_left_upper_decoded_value + S (C) = S ((S (x)) * bcf_row_scale_lucas_convolution_shift_left_upper)) /\ exists bcf_quotient_lucas_convolution_shift_left_upper_decoded_value. bcf_row_code_lucas_convolution_shift_left_upper = bcf_quotient_lucas_convolution_shift_left_upper_decoded_value * S ((S (x)) * bcf_row_scale_lucas_convolution_shift_left_upper) + (C)))))))) - 0102
apply choose_exists - 0103
cases hleft_upper - 0104
have hright_upper : ∃ C. Choose(p + a,S x,C)Exact native replay line
have hright_upper : exists C. ((exists bcf_lt_gap_lucas_convolution_shift_right_upper_out_of_range. bcf_lt_gap_lucas_convolution_shift_right_upper_out_of_range + S (p + a) = S x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_right_upper_in_range. bcf_le_gap_lucas_convolution_shift_right_upper_in_range + (S x) = p + a) /\ (exists bcf_row_code_code_lucas_convolution_shift_right_upper bcf_row_code_scale_lucas_convolution_shift_right_upper bcf_row_scale_code_lucas_convolution_shift_right_upper bcf_row_scale_scale_lucas_convolution_shift_right_upper bcf_row_code_lucas_convolution_shift_right_upper bcf_row_scale_lucas_convolution_shift_right_upper. ((forall bcf_row_index_lucas_convolution_shift_right_upper_table. (exists bcf_lt_gap_lucas_convolution_shift_right_upper_table_row_bound. bcf_lt_gap_lucas_convolution_shift_right_upper_table_row_bound + S (bcf_row_index_lucas_convolution_shift_right_upper_table) = S (p + a)) -> exists bcf_row_code_lucas_convolution_shift_right_upper_table bcf_row_scale_lucas_convolution_shift_right_upper_table. ((((exists bcf_height_lucas_convolution_shift_right_upper_table_decoded_row_code. bcf_height_lucas_convolution_shift_right_upper_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_right_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_right_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_right_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_right_upper) + (bcf_row_code_lucas_convolution_shift_right_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_table_decoded_row_scale. bcf_height_lucas_convolution_shift_right_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_right_upper_table) = S ((S (bcf_row_index_lucas_convolution_shift_right_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_right_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper) + (bcf_row_scale_lucas_convolution_shift_right_upper_table))) /\ ((bcf_row_index_lucas_convolution_shift_right_upper_table = 0 /\ (forall bcf_index_lucas_convolution_shift_right_upper_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_right_upper_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_right_upper_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_right_upper_table_zero_row) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_right_upper_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_right_upper_table_zero_row_entry. bcf_height_lucas_convolution_shift_right_upper_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_right_upper_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_right_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_right_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_right_upper_table = bcf_quotient_lucas_convolution_shift_right_upper_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_right_upper_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_right_upper_table) + (bcf_value_lucas_convolution_shift_right_upper_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_right_upper_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_right_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_right_upper_table_zero_row. bcf_index_lucas_convolution_shift_right_upper_table_zero_row = S bcf_predecessor_lucas_convolution_shift_right_upper_table_zero_row /\ bcf_value_lucas_convolution_shift_right_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_right_upper_table bcf_previous_code_lucas_convolution_shift_right_upper_table bcf_previous_scale_lucas_convolution_shift_right_upper_table. bcf_row_index_lucas_convolution_shift_right_upper_table = S bcf_predecessor_lucas_convolution_shift_right_upper_table /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_table_decoded_previous_code. bcf_height_lucas_convolution_shift_right_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_right_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table)) * bcf_row_code_scale_lucas_convolution_shift_right_upper) + (bcf_previous_code_lucas_convolution_shift_right_upper_table))) /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_right_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_right_upper_table) = S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper) + (bcf_previous_scale_lucas_convolution_shift_right_upper_table))) /\ (forall bcf_index_lucas_convolution_shift_right_upper_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_right_upper_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_right_upper_table_row_step_bound + S (bcf_index_lucas_convolution_shift_right_upper_table_row_step) = S (p + a)) -> exists bcf_value_lucas_convolution_shift_right_upper_table_row_step. ((((exists bcf_height_lucas_convolution_shift_right_upper_table_row_step_entry. bcf_height_lucas_convolution_shift_right_upper_table_row_step_entry + S (bcf_value_lucas_convolution_shift_right_upper_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_right_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_right_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_entry. bcf_row_code_lucas_convolution_shift_right_upper_table = bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_right_upper_table_row_step)) * bcf_row_scale_lucas_convolution_shift_right_upper_table) + (bcf_value_lucas_convolution_shift_right_upper_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_right_upper_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_right_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step bcf_left_lucas_convolution_shift_right_upper_table_row_step bcf_right_lucas_convolution_shift_right_upper_table_row_step. bcf_index_lucas_convolution_shift_right_upper_table_row_step = S bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_table_row_step_previous_left. bcf_height_lucas_convolution_shift_right_upper_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_right_upper_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_right_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_right_upper_table = bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_right_upper_table) + (bcf_left_lucas_convolution_shift_right_upper_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_table_row_step_previous_right. bcf_height_lucas_convolution_shift_right_upper_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_right_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_right_upper_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_right_upper_table = bcf_quotient_lucas_convolution_shift_right_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_right_upper_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_right_upper_table) + (bcf_right_lucas_convolution_shift_right_upper_table_row_step))) /\ bcf_value_lucas_convolution_shift_right_upper_table_row_step = bcf_left_lucas_convolution_shift_right_upper_table_row_step + bcf_right_lucas_convolution_shift_right_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_decoded_row_code. bcf_height_lucas_convolution_shift_right_upper_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_right_upper) = S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_decoded_row_code * S ((S (p + a)) * bcf_row_code_scale_lucas_convolution_shift_right_upper) + (bcf_row_code_lucas_convolution_shift_right_upper))) /\ ((((exists bcf_height_lucas_convolution_shift_right_upper_decoded_row_scale. bcf_height_lucas_convolution_shift_right_upper_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_right_upper) = S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_decoded_row_scale * S ((S (p + a)) * bcf_row_scale_scale_lucas_convolution_shift_right_upper) + (bcf_row_scale_lucas_convolution_shift_right_upper))) /\ (((exists bcf_height_lucas_convolution_shift_right_upper_decoded_value. bcf_height_lucas_convolution_shift_right_upper_decoded_value + S (C) = S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_right_upper)) /\ exists bcf_quotient_lucas_convolution_shift_right_upper_decoded_value. bcf_row_code_lucas_convolution_shift_right_upper = bcf_quotient_lucas_convolution_shift_right_upper_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_right_upper) + (C)))))))) - 0105
apply choose_exists - 0106
cases hright_upper - 0107
have hleft_lower : ∃ C. Choose(a,x,C)Exact native replay line
have hleft_lower : exists C. ((exists bcf_lt_gap_lucas_convolution_shift_left_lower_out_of_range. bcf_lt_gap_lucas_convolution_shift_left_lower_out_of_range + S (a) = x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_left_lower_in_range. bcf_le_gap_lucas_convolution_shift_left_lower_in_range + (x) = a) /\ (exists bcf_row_code_code_lucas_convolution_shift_left_lower bcf_row_code_scale_lucas_convolution_shift_left_lower bcf_row_scale_code_lucas_convolution_shift_left_lower bcf_row_scale_scale_lucas_convolution_shift_left_lower bcf_row_code_lucas_convolution_shift_left_lower bcf_row_scale_lucas_convolution_shift_left_lower. ((forall bcf_row_index_lucas_convolution_shift_left_lower_table. (exists bcf_lt_gap_lucas_convolution_shift_left_lower_table_row_bound. bcf_lt_gap_lucas_convolution_shift_left_lower_table_row_bound + S (bcf_row_index_lucas_convolution_shift_left_lower_table) = S (a)) -> exists bcf_row_code_lucas_convolution_shift_left_lower_table bcf_row_scale_lucas_convolution_shift_left_lower_table. ((((exists bcf_height_lucas_convolution_shift_left_lower_table_decoded_row_code. bcf_height_lucas_convolution_shift_left_lower_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_left_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_left_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_left_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_left_lower) + (bcf_row_code_lucas_convolution_shift_left_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_table_decoded_row_scale. bcf_height_lucas_convolution_shift_left_lower_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_left_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_left_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_left_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower) + (bcf_row_scale_lucas_convolution_shift_left_lower_table))) /\ ((bcf_row_index_lucas_convolution_shift_left_lower_table = 0 /\ (forall bcf_index_lucas_convolution_shift_left_lower_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_left_lower_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_left_lower_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_left_lower_table_zero_row) = S (a)) -> exists bcf_value_lucas_convolution_shift_left_lower_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_left_lower_table_zero_row_entry. bcf_height_lucas_convolution_shift_left_lower_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_left_lower_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_left_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_left_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_left_lower_table = bcf_quotient_lucas_convolution_shift_left_lower_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_left_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_left_lower_table) + (bcf_value_lucas_convolution_shift_left_lower_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_left_lower_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_left_lower_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_left_lower_table_zero_row. bcf_index_lucas_convolution_shift_left_lower_table_zero_row = S bcf_predecessor_lucas_convolution_shift_left_lower_table_zero_row /\ bcf_value_lucas_convolution_shift_left_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_left_lower_table bcf_previous_code_lucas_convolution_shift_left_lower_table bcf_previous_scale_lucas_convolution_shift_left_lower_table. bcf_row_index_lucas_convolution_shift_left_lower_table = S bcf_predecessor_lucas_convolution_shift_left_lower_table /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_table_decoded_previous_code. bcf_height_lucas_convolution_shift_left_lower_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_left_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_left_lower) + (bcf_previous_code_lucas_convolution_shift_left_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_left_lower_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_left_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower) + (bcf_previous_scale_lucas_convolution_shift_left_lower_table))) /\ (forall bcf_index_lucas_convolution_shift_left_lower_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_left_lower_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_left_lower_table_row_step_bound + S (bcf_index_lucas_convolution_shift_left_lower_table_row_step) = S (a)) -> exists bcf_value_lucas_convolution_shift_left_lower_table_row_step. ((((exists bcf_height_lucas_convolution_shift_left_lower_table_row_step_entry. bcf_height_lucas_convolution_shift_left_lower_table_row_step_entry + S (bcf_value_lucas_convolution_shift_left_lower_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_left_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_left_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_entry. bcf_row_code_lucas_convolution_shift_left_lower_table = bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_left_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_left_lower_table) + (bcf_value_lucas_convolution_shift_left_lower_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_left_lower_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_left_lower_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step bcf_left_lucas_convolution_shift_left_lower_table_row_step bcf_right_lucas_convolution_shift_left_lower_table_row_step. bcf_index_lucas_convolution_shift_left_lower_table_row_step = S bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_table_row_step_previous_left. bcf_height_lucas_convolution_shift_left_lower_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_left_lower_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_left_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_left_lower_table = bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_left_lower_table) + (bcf_left_lucas_convolution_shift_left_lower_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_table_row_step_previous_right. bcf_height_lucas_convolution_shift_left_lower_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_left_lower_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_left_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_left_lower_table = bcf_quotient_lucas_convolution_shift_left_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_left_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_left_lower_table) + (bcf_right_lucas_convolution_shift_left_lower_table_row_step))) /\ bcf_value_lucas_convolution_shift_left_lower_table_row_step = bcf_left_lucas_convolution_shift_left_lower_table_row_step + bcf_right_lucas_convolution_shift_left_lower_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_decoded_row_code. bcf_height_lucas_convolution_shift_left_lower_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_left_lower) = S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_left_lower) + (bcf_row_code_lucas_convolution_shift_left_lower))) /\ ((((exists bcf_height_lucas_convolution_shift_left_lower_decoded_row_scale. bcf_height_lucas_convolution_shift_left_lower_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_left_lower) = S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_left_lower) + (bcf_row_scale_lucas_convolution_shift_left_lower))) /\ (((exists bcf_height_lucas_convolution_shift_left_lower_decoded_value. bcf_height_lucas_convolution_shift_left_lower_decoded_value + S (C) = S ((S (x)) * bcf_row_scale_lucas_convolution_shift_left_lower)) /\ exists bcf_quotient_lucas_convolution_shift_left_lower_decoded_value. bcf_row_code_lucas_convolution_shift_left_lower = bcf_quotient_lucas_convolution_shift_left_lower_decoded_value * S ((S (x)) * bcf_row_scale_lucas_convolution_shift_left_lower) + (C)))))))) - 0108
apply choose_exists - 0109
cases hleft_lower - 0110
have hright_lower : ∃ C. Choose(a,S x,C)Exact native replay line
have hright_lower : exists C. ((exists bcf_lt_gap_lucas_convolution_shift_right_lower_out_of_range. bcf_lt_gap_lucas_convolution_shift_right_lower_out_of_range + S (a) = S x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_right_lower_in_range. bcf_le_gap_lucas_convolution_shift_right_lower_in_range + (S x) = a) /\ (exists bcf_row_code_code_lucas_convolution_shift_right_lower bcf_row_code_scale_lucas_convolution_shift_right_lower bcf_row_scale_code_lucas_convolution_shift_right_lower bcf_row_scale_scale_lucas_convolution_shift_right_lower bcf_row_code_lucas_convolution_shift_right_lower bcf_row_scale_lucas_convolution_shift_right_lower. ((forall bcf_row_index_lucas_convolution_shift_right_lower_table. (exists bcf_lt_gap_lucas_convolution_shift_right_lower_table_row_bound. bcf_lt_gap_lucas_convolution_shift_right_lower_table_row_bound + S (bcf_row_index_lucas_convolution_shift_right_lower_table) = S (a)) -> exists bcf_row_code_lucas_convolution_shift_right_lower_table bcf_row_scale_lucas_convolution_shift_right_lower_table. ((((exists bcf_height_lucas_convolution_shift_right_lower_table_decoded_row_code. bcf_height_lucas_convolution_shift_right_lower_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_right_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_right_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_right_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_right_lower) + (bcf_row_code_lucas_convolution_shift_right_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_table_decoded_row_scale. bcf_height_lucas_convolution_shift_right_lower_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_right_lower_table) = S ((S (bcf_row_index_lucas_convolution_shift_right_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_right_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower) + (bcf_row_scale_lucas_convolution_shift_right_lower_table))) /\ ((bcf_row_index_lucas_convolution_shift_right_lower_table = 0 /\ (forall bcf_index_lucas_convolution_shift_right_lower_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_right_lower_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_right_lower_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_right_lower_table_zero_row) = S (a)) -> exists bcf_value_lucas_convolution_shift_right_lower_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_right_lower_table_zero_row_entry. bcf_height_lucas_convolution_shift_right_lower_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_right_lower_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_right_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_right_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_right_lower_table = bcf_quotient_lucas_convolution_shift_right_lower_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_right_lower_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_right_lower_table) + (bcf_value_lucas_convolution_shift_right_lower_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_right_lower_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_right_lower_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_right_lower_table_zero_row. bcf_index_lucas_convolution_shift_right_lower_table_zero_row = S bcf_predecessor_lucas_convolution_shift_right_lower_table_zero_row /\ bcf_value_lucas_convolution_shift_right_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_right_lower_table bcf_previous_code_lucas_convolution_shift_right_lower_table bcf_previous_scale_lucas_convolution_shift_right_lower_table. bcf_row_index_lucas_convolution_shift_right_lower_table = S bcf_predecessor_lucas_convolution_shift_right_lower_table /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_table_decoded_previous_code. bcf_height_lucas_convolution_shift_right_lower_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_right_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table)) * bcf_row_code_scale_lucas_convolution_shift_right_lower) + (bcf_previous_code_lucas_convolution_shift_right_lower_table))) /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_right_lower_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_right_lower_table) = S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower) + (bcf_previous_scale_lucas_convolution_shift_right_lower_table))) /\ (forall bcf_index_lucas_convolution_shift_right_lower_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_right_lower_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_right_lower_table_row_step_bound + S (bcf_index_lucas_convolution_shift_right_lower_table_row_step) = S (a)) -> exists bcf_value_lucas_convolution_shift_right_lower_table_row_step. ((((exists bcf_height_lucas_convolution_shift_right_lower_table_row_step_entry. bcf_height_lucas_convolution_shift_right_lower_table_row_step_entry + S (bcf_value_lucas_convolution_shift_right_lower_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_right_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_right_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_entry. bcf_row_code_lucas_convolution_shift_right_lower_table = bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_right_lower_table_row_step)) * bcf_row_scale_lucas_convolution_shift_right_lower_table) + (bcf_value_lucas_convolution_shift_right_lower_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_right_lower_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_right_lower_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step bcf_left_lucas_convolution_shift_right_lower_table_row_step bcf_right_lucas_convolution_shift_right_lower_table_row_step. bcf_index_lucas_convolution_shift_right_lower_table_row_step = S bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_table_row_step_previous_left. bcf_height_lucas_convolution_shift_right_lower_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_right_lower_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_right_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_right_lower_table = bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_right_lower_table) + (bcf_left_lucas_convolution_shift_right_lower_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_table_row_step_previous_right. bcf_height_lucas_convolution_shift_right_lower_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_right_lower_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_right_lower_table)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_right_lower_table = bcf_quotient_lucas_convolution_shift_right_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_right_lower_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_right_lower_table) + (bcf_right_lucas_convolution_shift_right_lower_table_row_step))) /\ bcf_value_lucas_convolution_shift_right_lower_table_row_step = bcf_left_lucas_convolution_shift_right_lower_table_row_step + bcf_right_lucas_convolution_shift_right_lower_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_decoded_row_code. bcf_height_lucas_convolution_shift_right_lower_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_right_lower) = S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_convolution_shift_right_lower) + (bcf_row_code_lucas_convolution_shift_right_lower))) /\ ((((exists bcf_height_lucas_convolution_shift_right_lower_decoded_row_scale. bcf_height_lucas_convolution_shift_right_lower_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_right_lower) = S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_convolution_shift_right_lower) + (bcf_row_scale_lucas_convolution_shift_right_lower))) /\ (((exists bcf_height_lucas_convolution_shift_right_lower_decoded_value. bcf_height_lucas_convolution_shift_right_lower_decoded_value + S (C) = S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_right_lower)) /\ exists bcf_quotient_lucas_convolution_shift_right_lower_decoded_value. bcf_row_code_lucas_convolution_shift_right_lower = bcf_quotient_lucas_convolution_shift_right_lower_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_right_lower) + (C)))))))) - 0111
apply choose_exists - 0112
cases hright_lower - 0113
have hleft_mod : ModEq(p,x1,x3)Exact native replay line
have hleft_mod : exists lcv_left_shift_left_mod lcv_right_shift_left_mod. (x1) + (p) * lcv_left_shift_left_mod = (x3) + (p) * lcv_right_shift_left_mod - 0114
specialize IH x - 0115
specialize IH x1 - 0116
specialize IH x3 - 0117
apply IH - 0118
exact hprime - 0119
exact hpredecessor_bound - 0120
exact hleft_upper_witness - 0121
exact hleft_lower_witness - 0122
have hright_mod : ModEq(p,x2,x4)Exact native replay line
have hright_mod : exists lcv_left_shift_right_mod lcv_right_shift_right_mod. (x2) + (p) * lcv_left_shift_right_mod = (x4) + (p) * lcv_right_shift_right_mod - 0123
specialize IH (S x) - 0124
specialize IH x2 - 0125
specialize IH x4 - 0126
apply IH - 0127
exact hprime - 0128
exact hsuccessor_bound - 0129
exact hright_upper_witness - 0130
exact hright_lower_witness - 0131
have hupper_index : Choose(p + S a,S x,C)Exact native replay line
have hupper_index : ((exists bcf_lt_gap_lucas_convolution_shift_upper_index_out_of_range. bcf_lt_gap_lucas_convolution_shift_upper_index_out_of_range + S (p + S a) = S x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_upper_index_in_range. bcf_le_gap_lucas_convolution_shift_upper_index_in_range + (S x) = p + S a) /\ (exists bcf_row_code_code_lucas_convolution_shift_upper_index bcf_row_code_scale_lucas_convolution_shift_upper_index bcf_row_scale_code_lucas_convolution_shift_upper_index bcf_row_scale_scale_lucas_convolution_shift_upper_index bcf_row_code_lucas_convolution_shift_upper_index bcf_row_scale_lucas_convolution_shift_upper_index. ((forall bcf_row_index_lucas_convolution_shift_upper_index_table. (exists bcf_lt_gap_lucas_convolution_shift_upper_index_table_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_index_table_row_bound + S (bcf_row_index_lucas_convolution_shift_upper_index_table) = S (p + S a)) -> exists bcf_row_code_lucas_convolution_shift_upper_index_table bcf_row_scale_lucas_convolution_shift_upper_index_table. ((((exists bcf_height_lucas_convolution_shift_upper_index_table_decoded_row_code. bcf_height_lucas_convolution_shift_upper_index_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper_index_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_index_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_upper_index_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_index) + (bcf_row_code_lucas_convolution_shift_upper_index_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_table_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_index_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper_index_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_index_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_upper_index_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index) + (bcf_row_scale_lucas_convolution_shift_upper_index_table))) /\ ((bcf_row_index_lucas_convolution_shift_upper_index_table = 0 /\ (forall bcf_index_lucas_convolution_shift_upper_index_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_upper_index_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_index_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_upper_index_table_zero_row) = S (p + S a)) -> exists bcf_value_lucas_convolution_shift_upper_index_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_upper_index_table_zero_row_entry. bcf_height_lucas_convolution_shift_upper_index_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_upper_index_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_upper_index_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_index_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_upper_index_table = bcf_quotient_lucas_convolution_shift_upper_index_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_upper_index_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_index_table) + (bcf_value_lucas_convolution_shift_upper_index_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_upper_index_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_upper_index_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_index_table_zero_row. bcf_index_lucas_convolution_shift_upper_index_table_zero_row = S bcf_predecessor_lucas_convolution_shift_upper_index_table_zero_row /\ bcf_value_lucas_convolution_shift_upper_index_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_upper_index_table bcf_previous_code_lucas_convolution_shift_upper_index_table bcf_previous_scale_lucas_convolution_shift_upper_index_table. bcf_row_index_lucas_convolution_shift_upper_index_table = S bcf_predecessor_lucas_convolution_shift_upper_index_table /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_table_decoded_previous_code. bcf_height_lucas_convolution_shift_upper_index_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_upper_index_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_index) + (bcf_previous_code_lucas_convolution_shift_upper_index_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_upper_index_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_upper_index_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index) + (bcf_previous_scale_lucas_convolution_shift_upper_index_table))) /\ (forall bcf_index_lucas_convolution_shift_upper_index_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_upper_index_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_upper_index_table_row_step_bound + S (bcf_index_lucas_convolution_shift_upper_index_table_row_step) = S (p + S a)) -> exists bcf_value_lucas_convolution_shift_upper_index_table_row_step. ((((exists bcf_height_lucas_convolution_shift_upper_index_table_row_step_entry. bcf_height_lucas_convolution_shift_upper_index_table_row_step_entry + S (bcf_value_lucas_convolution_shift_upper_index_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_upper_index_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_index_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_entry. bcf_row_code_lucas_convolution_shift_upper_index_table = bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_upper_index_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_index_table) + (bcf_value_lucas_convolution_shift_upper_index_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_upper_index_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_upper_index_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step bcf_left_lucas_convolution_shift_upper_index_table_row_step bcf_right_lucas_convolution_shift_upper_index_table_row_step. bcf_index_lucas_convolution_shift_upper_index_table_row_step = S bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_table_row_step_previous_left. bcf_height_lucas_convolution_shift_upper_index_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_upper_index_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_index_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_upper_index_table = bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_index_table) + (bcf_left_lucas_convolution_shift_upper_index_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_table_row_step_previous_right. bcf_height_lucas_convolution_shift_upper_index_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_upper_index_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_index_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_upper_index_table = bcf_quotient_lucas_convolution_shift_upper_index_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_index_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_index_table) + (bcf_right_lucas_convolution_shift_upper_index_table_row_step))) /\ bcf_value_lucas_convolution_shift_upper_index_table_row_step = bcf_left_lucas_convolution_shift_upper_index_table_row_step + bcf_right_lucas_convolution_shift_upper_index_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_decoded_row_code. bcf_height_lucas_convolution_shift_upper_index_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper_index) = S ((S (p + S a)) * bcf_row_code_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_decoded_row_code * S ((S (p + S a)) * bcf_row_code_scale_lucas_convolution_shift_upper_index) + (bcf_row_code_lucas_convolution_shift_upper_index))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_index_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_index_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper_index) = S ((S (p + S a)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_decoded_row_scale * S ((S (p + S a)) * bcf_row_scale_scale_lucas_convolution_shift_upper_index) + (bcf_row_scale_lucas_convolution_shift_upper_index))) /\ (((exists bcf_height_lucas_convolution_shift_upper_index_decoded_value. bcf_height_lucas_convolution_shift_upper_index_decoded_value + S (C) = S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_upper_index)) /\ exists bcf_quotient_lucas_convolution_shift_upper_index_decoded_value. bcf_row_code_lucas_convolution_shift_upper_index = bcf_quotient_lucas_convolution_shift_upper_index_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_upper_index) + (C)))))))) - 0132
specialize lucas_choose_lower_eq_transport (p + S a) - 0133
specialize lucas_choose_lower_eq_transport b - 0134
specialize lucas_choose_lower_eq_transport (S x) - 0135
specialize lucas_choose_lower_eq_transport C - 0136
apply lucas_choose_lower_eq_transport - 0137
exact hsuccessor_witness - 0138
exact hupper - 0139
have hupper_normal : Choose(S (p + a),S x,C)Exact native replay line
have hupper_normal : ((exists bcf_lt_gap_lucas_convolution_shift_upper_normal_out_of_range. bcf_lt_gap_lucas_convolution_shift_upper_normal_out_of_range + S (S (p + a)) = S x) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_upper_normal_in_range. bcf_le_gap_lucas_convolution_shift_upper_normal_in_range + (S x) = S (p + a)) /\ (exists bcf_row_code_code_lucas_convolution_shift_upper_normal bcf_row_code_scale_lucas_convolution_shift_upper_normal bcf_row_scale_code_lucas_convolution_shift_upper_normal bcf_row_scale_scale_lucas_convolution_shift_upper_normal bcf_row_code_lucas_convolution_shift_upper_normal bcf_row_scale_lucas_convolution_shift_upper_normal. ((forall bcf_row_index_lucas_convolution_shift_upper_normal_table. (exists bcf_lt_gap_lucas_convolution_shift_upper_normal_table_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_normal_table_row_bound + S (bcf_row_index_lucas_convolution_shift_upper_normal_table) = S (S (p + a))) -> exists bcf_row_code_lucas_convolution_shift_upper_normal_table bcf_row_scale_lucas_convolution_shift_upper_normal_table. ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_decoded_row_code. bcf_height_lucas_convolution_shift_upper_normal_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper_normal_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_upper_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_normal) + (bcf_row_code_lucas_convolution_shift_upper_normal_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper_normal_table) = S ((S (bcf_row_index_lucas_convolution_shift_upper_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_upper_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal) + (bcf_row_scale_lucas_convolution_shift_upper_normal_table))) /\ ((bcf_row_index_lucas_convolution_shift_upper_normal_table = 0 /\ (forall bcf_index_lucas_convolution_shift_upper_normal_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_upper_normal_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_upper_normal_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_upper_normal_table_zero_row) = S (S (p + a))) -> exists bcf_value_lucas_convolution_shift_upper_normal_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_zero_row_entry. bcf_height_lucas_convolution_shift_upper_normal_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_upper_normal_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_upper_normal_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_upper_normal_table = bcf_quotient_lucas_convolution_shift_upper_normal_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_upper_normal_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_upper_normal_table) + (bcf_value_lucas_convolution_shift_upper_normal_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_upper_normal_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_upper_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_normal_table_zero_row. bcf_index_lucas_convolution_shift_upper_normal_table_zero_row = S bcf_predecessor_lucas_convolution_shift_upper_normal_table_zero_row /\ bcf_value_lucas_convolution_shift_upper_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_upper_normal_table bcf_previous_code_lucas_convolution_shift_upper_normal_table bcf_previous_scale_lucas_convolution_shift_upper_normal_table. bcf_row_index_lucas_convolution_shift_upper_normal_table = S bcf_predecessor_lucas_convolution_shift_upper_normal_table /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_decoded_previous_code. bcf_height_lucas_convolution_shift_upper_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_upper_normal_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_upper_normal) + (bcf_previous_code_lucas_convolution_shift_upper_normal_table))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_upper_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_upper_normal_table) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal) + (bcf_previous_scale_lucas_convolution_shift_upper_normal_table))) /\ (forall bcf_index_lucas_convolution_shift_upper_normal_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_upper_normal_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_upper_normal_table_row_step_bound + S (bcf_index_lucas_convolution_shift_upper_normal_table_row_step) = S (S (p + a))) -> exists bcf_value_lucas_convolution_shift_upper_normal_table_row_step. ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_row_step_entry. bcf_height_lucas_convolution_shift_upper_normal_table_row_step_entry + S (bcf_value_lucas_convolution_shift_upper_normal_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_upper_normal_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_entry. bcf_row_code_lucas_convolution_shift_upper_normal_table = bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_upper_normal_table_row_step)) * bcf_row_scale_lucas_convolution_shift_upper_normal_table) + (bcf_value_lucas_convolution_shift_upper_normal_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_upper_normal_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_upper_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step bcf_left_lucas_convolution_shift_upper_normal_table_row_step bcf_right_lucas_convolution_shift_upper_normal_table_row_step. bcf_index_lucas_convolution_shift_upper_normal_table_row_step = S bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_row_step_previous_left. bcf_height_lucas_convolution_shift_upper_normal_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_upper_normal_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_upper_normal_table = bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_upper_normal_table) + (bcf_left_lucas_convolution_shift_upper_normal_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_table_row_step_previous_right. bcf_height_lucas_convolution_shift_upper_normal_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_upper_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_upper_normal_table = bcf_quotient_lucas_convolution_shift_upper_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_upper_normal_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_upper_normal_table) + (bcf_right_lucas_convolution_shift_upper_normal_table_row_step))) /\ bcf_value_lucas_convolution_shift_upper_normal_table_row_step = bcf_left_lucas_convolution_shift_upper_normal_table_row_step + bcf_right_lucas_convolution_shift_upper_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_decoded_row_code. bcf_height_lucas_convolution_shift_upper_normal_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_upper_normal) = S ((S (S (p + a))) * bcf_row_code_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_decoded_row_code * S ((S (S (p + a))) * bcf_row_code_scale_lucas_convolution_shift_upper_normal) + (bcf_row_code_lucas_convolution_shift_upper_normal))) /\ ((((exists bcf_height_lucas_convolution_shift_upper_normal_decoded_row_scale. bcf_height_lucas_convolution_shift_upper_normal_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_upper_normal) = S ((S (S (p + a))) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_decoded_row_scale * S ((S (S (p + a))) * bcf_row_scale_scale_lucas_convolution_shift_upper_normal) + (bcf_row_scale_lucas_convolution_shift_upper_normal))) /\ (((exists bcf_height_lucas_convolution_shift_upper_normal_decoded_value. bcf_height_lucas_convolution_shift_upper_normal_decoded_value + S (C) = S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_upper_normal)) /\ exists bcf_quotient_lucas_convolution_shift_upper_normal_decoded_value. bcf_row_code_lucas_convolution_shift_upper_normal = bcf_quotient_lucas_convolution_shift_upper_normal_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_upper_normal) + (C)))))))) - 0140
specialize choose_upper_eq_transport (p + S a) - 0141
specialize choose_upper_eq_transport (S (p + a)) - 0142
specialize choose_upper_eq_transport (S x) - 0143
specialize choose_upper_eq_transport C - 0144
apply choose_upper_eq_transport - 0145
apply PA4 - 0146
exact hupper_index - 0147
have hlower_normal : Choose(S a,S x,D)Exact native replay line
have hlower_normal : ((exists bcf_lt_gap_lucas_convolution_shift_lower_normal_out_of_range. bcf_lt_gap_lucas_convolution_shift_lower_normal_out_of_range + S (S a) = S x) /\ D = 0) \/ ((exists bcf_le_gap_lucas_convolution_shift_lower_normal_in_range. bcf_le_gap_lucas_convolution_shift_lower_normal_in_range + (S x) = S a) /\ (exists bcf_row_code_code_lucas_convolution_shift_lower_normal bcf_row_code_scale_lucas_convolution_shift_lower_normal bcf_row_scale_code_lucas_convolution_shift_lower_normal bcf_row_scale_scale_lucas_convolution_shift_lower_normal bcf_row_code_lucas_convolution_shift_lower_normal bcf_row_scale_lucas_convolution_shift_lower_normal. ((forall bcf_row_index_lucas_convolution_shift_lower_normal_table. (exists bcf_lt_gap_lucas_convolution_shift_lower_normal_table_row_bound. bcf_lt_gap_lucas_convolution_shift_lower_normal_table_row_bound + S (bcf_row_index_lucas_convolution_shift_lower_normal_table) = S (S a)) -> exists bcf_row_code_lucas_convolution_shift_lower_normal_table bcf_row_scale_lucas_convolution_shift_lower_normal_table. ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_decoded_row_code. bcf_height_lucas_convolution_shift_lower_normal_table_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_lower_normal_table) = S ((S (bcf_row_index_lucas_convolution_shift_lower_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_shift_lower_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal) + (bcf_row_code_lucas_convolution_shift_lower_normal_table))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_decoded_row_scale. bcf_height_lucas_convolution_shift_lower_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_lower_normal_table) = S ((S (bcf_row_index_lucas_convolution_shift_lower_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_shift_lower_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal) + (bcf_row_scale_lucas_convolution_shift_lower_normal_table))) /\ ((bcf_row_index_lucas_convolution_shift_lower_normal_table = 0 /\ (forall bcf_index_lucas_convolution_shift_lower_normal_table_zero_row. (exists bcf_lt_gap_lucas_convolution_shift_lower_normal_table_zero_row_bound. bcf_lt_gap_lucas_convolution_shift_lower_normal_table_zero_row_bound + S (bcf_index_lucas_convolution_shift_lower_normal_table_zero_row) = S (S a)) -> exists bcf_value_lucas_convolution_shift_lower_normal_table_zero_row. ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_zero_row_entry. bcf_height_lucas_convolution_shift_lower_normal_table_zero_row_entry + S (bcf_value_lucas_convolution_shift_lower_normal_table_zero_row) = S ((S (bcf_index_lucas_convolution_shift_lower_normal_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_lower_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_zero_row_entry. bcf_row_code_lucas_convolution_shift_lower_normal_table = bcf_quotient_lucas_convolution_shift_lower_normal_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_shift_lower_normal_table_zero_row)) * bcf_row_scale_lucas_convolution_shift_lower_normal_table) + (bcf_value_lucas_convolution_shift_lower_normal_table_zero_row))) /\ ((bcf_index_lucas_convolution_shift_lower_normal_table_zero_row = 0 /\ bcf_value_lucas_convolution_shift_lower_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_shift_lower_normal_table_zero_row. bcf_index_lucas_convolution_shift_lower_normal_table_zero_row = S bcf_predecessor_lucas_convolution_shift_lower_normal_table_zero_row /\ bcf_value_lucas_convolution_shift_lower_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_shift_lower_normal_table bcf_previous_code_lucas_convolution_shift_lower_normal_table bcf_previous_scale_lucas_convolution_shift_lower_normal_table. bcf_row_index_lucas_convolution_shift_lower_normal_table = S bcf_predecessor_lucas_convolution_shift_lower_normal_table /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_decoded_previous_code. bcf_height_lucas_convolution_shift_lower_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_shift_lower_normal_table) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal) + (bcf_previous_code_lucas_convolution_shift_lower_normal_table))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_decoded_previous_scale. bcf_height_lucas_convolution_shift_lower_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_shift_lower_normal_table) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal) + (bcf_previous_scale_lucas_convolution_shift_lower_normal_table))) /\ (forall bcf_index_lucas_convolution_shift_lower_normal_table_row_step. (exists bcf_lt_gap_lucas_convolution_shift_lower_normal_table_row_step_bound. bcf_lt_gap_lucas_convolution_shift_lower_normal_table_row_step_bound + S (bcf_index_lucas_convolution_shift_lower_normal_table_row_step) = S (S a)) -> exists bcf_value_lucas_convolution_shift_lower_normal_table_row_step. ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_row_step_entry. bcf_height_lucas_convolution_shift_lower_normal_table_row_step_entry + S (bcf_value_lucas_convolution_shift_lower_normal_table_row_step) = S ((S (bcf_index_lucas_convolution_shift_lower_normal_table_row_step)) * bcf_row_scale_lucas_convolution_shift_lower_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_entry. bcf_row_code_lucas_convolution_shift_lower_normal_table = bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_entry * S ((S (bcf_index_lucas_convolution_shift_lower_normal_table_row_step)) * bcf_row_scale_lucas_convolution_shift_lower_normal_table) + (bcf_value_lucas_convolution_shift_lower_normal_table_row_step))) /\ ((bcf_index_lucas_convolution_shift_lower_normal_table_row_step = 0 /\ bcf_value_lucas_convolution_shift_lower_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step bcf_left_lucas_convolution_shift_lower_normal_table_row_step bcf_right_lucas_convolution_shift_lower_normal_table_row_step. bcf_index_lucas_convolution_shift_lower_normal_table_row_step = S bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_row_step_previous_left. bcf_height_lucas_convolution_shift_lower_normal_table_row_step_previous_left + S (bcf_left_lucas_convolution_shift_lower_normal_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_lower_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_previous_left. bcf_previous_code_lucas_convolution_shift_lower_normal_table = bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step)) * bcf_previous_scale_lucas_convolution_shift_lower_normal_table) + (bcf_left_lucas_convolution_shift_lower_normal_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_table_row_step_previous_right. bcf_height_lucas_convolution_shift_lower_normal_table_row_step_previous_right + S (bcf_right_lucas_convolution_shift_lower_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_lower_normal_table)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_previous_right. bcf_previous_code_lucas_convolution_shift_lower_normal_table = bcf_quotient_lucas_convolution_shift_lower_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_shift_lower_normal_table_row_step))) * bcf_previous_scale_lucas_convolution_shift_lower_normal_table) + (bcf_right_lucas_convolution_shift_lower_normal_table_row_step))) /\ bcf_value_lucas_convolution_shift_lower_normal_table_row_step = bcf_left_lucas_convolution_shift_lower_normal_table_row_step + bcf_right_lucas_convolution_shift_lower_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_decoded_row_code. bcf_height_lucas_convolution_shift_lower_normal_decoded_row_code + S (bcf_row_code_lucas_convolution_shift_lower_normal) = S ((S (S a)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_decoded_row_code. bcf_row_code_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_decoded_row_code * S ((S (S a)) * bcf_row_code_scale_lucas_convolution_shift_lower_normal) + (bcf_row_code_lucas_convolution_shift_lower_normal))) /\ ((((exists bcf_height_lucas_convolution_shift_lower_normal_decoded_row_scale. bcf_height_lucas_convolution_shift_lower_normal_decoded_row_scale + S (bcf_row_scale_lucas_convolution_shift_lower_normal) = S ((S (S a)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_decoded_row_scale. bcf_row_scale_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_decoded_row_scale * S ((S (S a)) * bcf_row_scale_scale_lucas_convolution_shift_lower_normal) + (bcf_row_scale_lucas_convolution_shift_lower_normal))) /\ (((exists bcf_height_lucas_convolution_shift_lower_normal_decoded_value. bcf_height_lucas_convolution_shift_lower_normal_decoded_value + S (D) = S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_lower_normal)) /\ exists bcf_quotient_lucas_convolution_shift_lower_normal_decoded_value. bcf_row_code_lucas_convolution_shift_lower_normal = bcf_quotient_lucas_convolution_shift_lower_normal_decoded_value * S ((S (S x)) * bcf_row_scale_lucas_convolution_shift_lower_normal) + (D)))))))) - 0148
specialize lucas_choose_lower_eq_transport (S a) - 0149
specialize lucas_choose_lower_eq_transport b - 0150
specialize lucas_choose_lower_eq_transport (S x) - 0151
specialize lucas_choose_lower_eq_transport D - 0152
apply lucas_choose_lower_eq_transport - 0153
exact hsuccessor_witness - 0154
exact hlower - 0155
have hlower_sum : D = x3 + x4 - 0156
specialize choose_succ_succ a - 0157
specialize choose_succ_succ x - 0158
specialize choose_succ_succ x3 - 0159
specialize choose_succ_succ x4 - 0160
specialize choose_succ_succ D - 0161
apply choose_succ_succ - 0162
exact hleft_lower_witness - 0163
exact hright_lower_witness - 0164
exact hlower_normal - 0165
rewrite hlower_sum - 0166
specialize lucas_pascal_congruence_step p - 0167
specialize lucas_pascal_congruence_step (p + a) - 0168
specialize lucas_pascal_congruence_step x - 0169
specialize lucas_pascal_congruence_step x1 - 0170
specialize lucas_pascal_congruence_step x2 - 0171
specialize lucas_pascal_congruence_step C - 0172
specialize lucas_pascal_congruence_step x3 - 0173
specialize lucas_pascal_congruence_step x4 - 0174
apply lucas_pascal_congruence_step - 0175
exact hleft_upper_witness - 0176
exact hright_upper_witness - 0177
exact hupper_normal - 0178
exact hleft_mod - 0179
exact hright_mod