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
∀ n. ∀ c. ∀ q. CentralBinom(S n,c) → Pow(4,S n,q) → Le(2 · c,q)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
5 occurrences
Exact expanded native-PA statement
forall n c q. (((exists bcf_lt_gap_bcbsuo_central_out_of_range. bcf_lt_gap_bcbsuo_central_out_of_range + S (S n + S n) = S n) /\ c = 0) \/ ((exists bcf_le_gap_bcbsuo_central_in_range. bcf_le_gap_bcbsuo_central_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbsuo_central bcf_row_code_scale_bcbsuo_central bcf_row_scale_code_bcbsuo_central bcf_row_scale_scale_bcbsuo_central bcf_row_code_bcbsuo_central bcf_row_scale_bcbsuo_central. ((forall bcf_row_index_bcbsuo_central_table. (exists bcf_lt_gap_bcbsuo_central_table_row_bound. bcf_lt_gap_bcbsuo_central_table_row_bound + S (bcf_row_index_bcbsuo_central_table) = S (S n + S n)) -> exists bcf_row_code_bcbsuo_central_table bcf_row_scale_bcbsuo_central_table. ((((exists bcf_height_bcbsuo_central_table_decoded_row_code. bcf_height_bcbsuo_central_table_decoded_row_code + S (bcf_row_code_bcbsuo_central_table) = S ((S (bcf_row_index_bcbsuo_central_table)) * bcf_row_code_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_table_decoded_row_code. bcf_row_code_code_bcbsuo_central = bcf_quotient_bcbsuo_central_table_decoded_row_code * S ((S (bcf_row_index_bcbsuo_central_table)) * bcf_row_code_scale_bcbsuo_central) + (bcf_row_code_bcbsuo_central_table))) /\ ((((exists bcf_height_bcbsuo_central_table_decoded_row_scale. bcf_height_bcbsuo_central_table_decoded_row_scale + S (bcf_row_scale_bcbsuo_central_table) = S ((S (bcf_row_index_bcbsuo_central_table)) * bcf_row_scale_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_table_decoded_row_scale. bcf_row_scale_code_bcbsuo_central = bcf_quotient_bcbsuo_central_table_decoded_row_scale * S ((S (bcf_row_index_bcbsuo_central_table)) * bcf_row_scale_scale_bcbsuo_central) + (bcf_row_scale_bcbsuo_central_table))) /\ ((bcf_row_index_bcbsuo_central_table = 0 /\ (forall bcf_index_bcbsuo_central_table_zero_row. (exists bcf_lt_gap_bcbsuo_central_table_zero_row_bound. bcf_lt_gap_bcbsuo_central_table_zero_row_bound + S (bcf_index_bcbsuo_central_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbsuo_central_table_zero_row. ((((exists bcf_height_bcbsuo_central_table_zero_row_entry. bcf_height_bcbsuo_central_table_zero_row_entry + S (bcf_value_bcbsuo_central_table_zero_row) = S ((S (bcf_index_bcbsuo_central_table_zero_row)) * bcf_row_scale_bcbsuo_central_table)) /\ exists bcf_quotient_bcbsuo_central_table_zero_row_entry. bcf_row_code_bcbsuo_central_table = bcf_quotient_bcbsuo_central_table_zero_row_entry * S ((S (bcf_index_bcbsuo_central_table_zero_row)) * bcf_row_scale_bcbsuo_central_table) + (bcf_value_bcbsuo_central_table_zero_row))) /\ ((bcf_index_bcbsuo_central_table_zero_row = 0 /\ bcf_value_bcbsuo_central_table_zero_row = 1) \/ exists bcf_predecessor_bcbsuo_central_table_zero_row. bcf_index_bcbsuo_central_table_zero_row = S bcf_predecessor_bcbsuo_central_table_zero_row /\ bcf_value_bcbsuo_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsuo_central_table bcf_previous_code_bcbsuo_central_table bcf_previous_scale_bcbsuo_central_table. bcf_row_index_bcbsuo_central_table = S bcf_predecessor_bcbsuo_central_table /\ ((((exists bcf_height_bcbsuo_central_table_decoded_previous_code. bcf_height_bcbsuo_central_table_decoded_previous_code + S (bcf_previous_code_bcbsuo_central_table) = S ((S (bcf_predecessor_bcbsuo_central_table)) * bcf_row_code_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_table_decoded_previous_code. bcf_row_code_code_bcbsuo_central = bcf_quotient_bcbsuo_central_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsuo_central_table)) * bcf_row_code_scale_bcbsuo_central) + (bcf_previous_code_bcbsuo_central_table))) /\ ((((exists bcf_height_bcbsuo_central_table_decoded_previous_scale. bcf_height_bcbsuo_central_table_decoded_previous_scale + S (bcf_previous_scale_bcbsuo_central_table) = S ((S (bcf_predecessor_bcbsuo_central_table)) * bcf_row_scale_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_table_decoded_previous_scale. bcf_row_scale_code_bcbsuo_central = bcf_quotient_bcbsuo_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsuo_central_table)) * bcf_row_scale_scale_bcbsuo_central) + (bcf_previous_scale_bcbsuo_central_table))) /\ (forall bcf_index_bcbsuo_central_table_row_step. (exists bcf_lt_gap_bcbsuo_central_table_row_step_bound. bcf_lt_gap_bcbsuo_central_table_row_step_bound + S (bcf_index_bcbsuo_central_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbsuo_central_table_row_step. ((((exists bcf_height_bcbsuo_central_table_row_step_entry. bcf_height_bcbsuo_central_table_row_step_entry + S (bcf_value_bcbsuo_central_table_row_step) = S ((S (bcf_index_bcbsuo_central_table_row_step)) * bcf_row_scale_bcbsuo_central_table)) /\ exists bcf_quotient_bcbsuo_central_table_row_step_entry. bcf_row_code_bcbsuo_central_table = bcf_quotient_bcbsuo_central_table_row_step_entry * S ((S (bcf_index_bcbsuo_central_table_row_step)) * bcf_row_scale_bcbsuo_central_table) + (bcf_value_bcbsuo_central_table_row_step))) /\ ((bcf_index_bcbsuo_central_table_row_step = 0 /\ bcf_value_bcbsuo_central_table_row_step = 1) \/ exists bcf_predecessor_bcbsuo_central_table_row_step bcf_left_bcbsuo_central_table_row_step bcf_right_bcbsuo_central_table_row_step. bcf_index_bcbsuo_central_table_row_step = S bcf_predecessor_bcbsuo_central_table_row_step /\ ((((exists bcf_height_bcbsuo_central_table_row_step_previous_left. bcf_height_bcbsuo_central_table_row_step_previous_left + S (bcf_left_bcbsuo_central_table_row_step) = S ((S (bcf_predecessor_bcbsuo_central_table_row_step)) * bcf_previous_scale_bcbsuo_central_table)) /\ exists bcf_quotient_bcbsuo_central_table_row_step_previous_left. bcf_previous_code_bcbsuo_central_table = bcf_quotient_bcbsuo_central_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsuo_central_table_row_step)) * bcf_previous_scale_bcbsuo_central_table) + (bcf_left_bcbsuo_central_table_row_step))) /\ ((((exists bcf_height_bcbsuo_central_table_row_step_previous_right. bcf_height_bcbsuo_central_table_row_step_previous_right + S (bcf_right_bcbsuo_central_table_row_step) = S ((S (S (bcf_predecessor_bcbsuo_central_table_row_step))) * bcf_previous_scale_bcbsuo_central_table)) /\ exists bcf_quotient_bcbsuo_central_table_row_step_previous_right. bcf_previous_code_bcbsuo_central_table = bcf_quotient_bcbsuo_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsuo_central_table_row_step))) * bcf_previous_scale_bcbsuo_central_table) + (bcf_right_bcbsuo_central_table_row_step))) /\ bcf_value_bcbsuo_central_table_row_step = bcf_left_bcbsuo_central_table_row_step + bcf_right_bcbsuo_central_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsuo_central_decoded_row_code. bcf_height_bcbsuo_central_decoded_row_code + S (bcf_row_code_bcbsuo_central) = S ((S (S n + S n)) * bcf_row_code_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_decoded_row_code. bcf_row_code_code_bcbsuo_central = bcf_quotient_bcbsuo_central_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbsuo_central) + (bcf_row_code_bcbsuo_central))) /\ ((((exists bcf_height_bcbsuo_central_decoded_row_scale. bcf_height_bcbsuo_central_decoded_row_scale + S (bcf_row_scale_bcbsuo_central) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_decoded_row_scale. bcf_row_scale_code_bcbsuo_central = bcf_quotient_bcbsuo_central_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbsuo_central) + (bcf_row_scale_bcbsuo_central))) /\ (((exists bcf_height_bcbsuo_central_decoded_value. bcf_height_bcbsuo_central_decoded_value + S (c) = S ((S (S n)) * bcf_row_scale_bcbsuo_central)) /\ exists bcf_quotient_bcbsuo_central_decoded_value. bcf_row_code_bcbsuo_central = bcf_quotient_bcbsuo_central_decoded_value * S ((S (S n)) * bcf_row_scale_bcbsuo_central) + (c))))))))) -> (exists pa_b_bcbsuo_power pa_c_bcbsuo_power. ((forall pa_i_bcbsuo_power_repeat. (exists pa_lt_bcbsuo_power_repeat_bound. pa_lt_bcbsuo_power_repeat_bound + S pa_i_bcbsuo_power_repeat = S n) -> (((exists pa_h_bcbsuo_power_repeat_decoded. pa_h_bcbsuo_power_repeat_decoded + S (4) = S ((S (pa_i_bcbsuo_power_repeat)) * pa_c_bcbsuo_power)) /\ exists pa_q_bcbsuo_power_repeat_decoded. pa_b_bcbsuo_power = pa_q_bcbsuo_power_repeat_decoded * S ((S (pa_i_bcbsuo_power_repeat)) * pa_c_bcbsuo_power) + (4)))) /\ (exists pa_u_bcbsuo_power_product pa_v_bcbsuo_power_product. ((((exists pa_h_bcbsuo_power_product_start. pa_h_bcbsuo_power_product_start + S (1) = S ((S (0)) * pa_v_bcbsuo_power_product)) /\ exists pa_q_bcbsuo_power_product_start. pa_u_bcbsuo_power_product = pa_q_bcbsuo_power_product_start * S ((S (0)) * pa_v_bcbsuo_power_product) + (1))) /\ ((((exists pa_h_bcbsuo_power_product_terminal. pa_h_bcbsuo_power_product_terminal + S (q) = S ((S (S n)) * pa_v_bcbsuo_power_product)) /\ exists pa_q_bcbsuo_power_product_terminal. pa_u_bcbsuo_power_product = pa_q_bcbsuo_power_product_terminal * S ((S (S n)) * pa_v_bcbsuo_power_product) + (q))) /\ forall pa_i_bcbsuo_power_product. (exists pa_lt_bcbsuo_power_product_bound. pa_lt_bcbsuo_power_product_bound + S pa_i_bcbsuo_power_product = S n) -> exists pa_p_bcbsuo_power_product pa_r_bcbsuo_power_product pa_s_bcbsuo_power_product. ((((exists pa_h_bcbsuo_power_product_factor. pa_h_bcbsuo_power_product_factor + S (pa_p_bcbsuo_power_product) = S ((S (pa_i_bcbsuo_power_product)) * pa_c_bcbsuo_power)) /\ exists pa_q_bcbsuo_power_product_factor. pa_b_bcbsuo_power = pa_q_bcbsuo_power_product_factor * S ((S (pa_i_bcbsuo_power_product)) * pa_c_bcbsuo_power) + (pa_p_bcbsuo_power_product))) /\ ((((exists pa_h_bcbsuo_power_product_partial. pa_h_bcbsuo_power_product_partial + S (pa_r_bcbsuo_power_product) = S ((S (pa_i_bcbsuo_power_product)) * pa_v_bcbsuo_power_product)) /\ exists pa_q_bcbsuo_power_product_partial. pa_u_bcbsuo_power_product = pa_q_bcbsuo_power_product_partial * S ((S (pa_i_bcbsuo_power_product)) * pa_v_bcbsuo_power_product) + (pa_r_bcbsuo_power_product))) /\ ((((exists pa_h_bcbsuo_power_product_successor. pa_h_bcbsuo_power_product_successor + S (pa_s_bcbsuo_power_product) = S ((S (S pa_i_bcbsuo_power_product)) * pa_v_bcbsuo_power_product)) /\ exists pa_q_bcbsuo_power_product_successor. pa_u_bcbsuo_power_product = pa_q_bcbsuo_power_product_successor * S ((S (S pa_i_bcbsuo_power_product)) * pa_v_bcbsuo_power_product) + (pa_s_bcbsuo_power_product))) /\ pa_s_bcbsuo_power_product = pa_r_bcbsuo_power_product * pa_p_bcbsuo_power_product)))))))) -> (exists bcf_le_gap_bcbsuo_result. bcf_le_gap_bcbsuo_result + (2 * c) = q)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Establish hpackageL1–2
Establish this local claim before using it. It is not an additional assumption.
- L1
have hpackage : (∀ x. ∀ y. ∀ z. CentralBinom(x,y) → CentralBinom(S x,z) → S x · z = 2 · S (x + x) · y) ∧ (∀ x. ∀ y. ∀ z. CentralBinom(S x,y) → Choose(S (x + x),x,z) → y = z + z) ∧ (∀ x. ∃ y. CentralBinom(x,y))Definitions: CentralBinom(x,y)CentralBinom(S x,z)CentralBinom(S x,y)Choose(S (x + x),x,z)Original native command in the exact edition - L2
exact central_binom_upper_support_package
02Separate the logical casesL3–4
Original defined command ledger · 7 lines
- 0001
have hpackage : (∀ x. ∀ y. ∀ z. CentralBinom(x,y) → CentralBinom(S x,z) → S x · z = 2 · S (x + x) · y) ∧ (∀ x. ∀ y. ∀ z. CentralBinom(S x,y) → Choose(S (x + x),x,z) → y = z + z) ∧ (∀ x. ∃ y. CentralBinom(x,y))Exact native replay line
have hpackage : ((((forall n c d. (((exists bcf_lt_gap_bcbrdb_predecessor_out_of_range. bcf_lt_gap_bcbrdb_predecessor_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bcbrdb_predecessor_in_range. bcf_le_gap_bcbrdb_predecessor_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcbrdb_predecessor bcf_row_code_scale_bcbrdb_predecessor bcf_row_scale_code_bcbrdb_predecessor bcf_row_scale_scale_bcbrdb_predecessor bcf_row_code_bcbrdb_predecessor bcf_row_scale_bcbrdb_predecessor. ((forall bcf_row_index_bcbrdb_predecessor_table. (exists bcf_lt_gap_bcbrdb_predecessor_table_row_bound. bcf_lt_gap_bcbrdb_predecessor_table_row_bound + S (bcf_row_index_bcbrdb_predecessor_table) = S (n + n)) -> exists bcf_row_code_bcbrdb_predecessor_table bcf_row_scale_bcbrdb_predecessor_table. ((((exists bcf_height_bcbrdb_predecessor_table_decoded_row_code. bcf_height_bcbrdb_predecessor_table_decoded_row_code + S (bcf_row_code_bcbrdb_predecessor_table) = S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_row_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_row_code_bcbrdb_predecessor_table))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_row_scale. bcf_height_bcbrdb_predecessor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_predecessor_table) = S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_row_scale_bcbrdb_predecessor_table))) /\ ((bcf_row_index_bcbrdb_predecessor_table = 0 /\ (forall bcf_index_bcbrdb_predecessor_table_zero_row. (exists bcf_lt_gap_bcbrdb_predecessor_table_zero_row_bound. bcf_lt_gap_bcbrdb_predecessor_table_zero_row_bound + S (bcf_index_bcbrdb_predecessor_table_zero_row) = S (n + n)) -> exists bcf_value_bcbrdb_predecessor_table_zero_row. ((((exists bcf_height_bcbrdb_predecessor_table_zero_row_entry. bcf_height_bcbrdb_predecessor_table_zero_row_entry + S (bcf_value_bcbrdb_predecessor_table_zero_row) = S ((S (bcf_index_bcbrdb_predecessor_table_zero_row)) * bcf_row_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_zero_row_entry. bcf_row_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_predecessor_table_zero_row)) * bcf_row_scale_bcbrdb_predecessor_table) + (bcf_value_bcbrdb_predecessor_table_zero_row))) /\ ((bcf_index_bcbrdb_predecessor_table_zero_row = 0 /\ bcf_value_bcbrdb_predecessor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_predecessor_table_zero_row. bcf_index_bcbrdb_predecessor_table_zero_row = S bcf_predecessor_bcbrdb_predecessor_table_zero_row /\ bcf_value_bcbrdb_predecessor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_predecessor_table bcf_previous_code_bcbrdb_predecessor_table bcf_previous_scale_bcbrdb_predecessor_table. bcf_row_index_bcbrdb_predecessor_table = S bcf_predecessor_bcbrdb_predecessor_table /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_previous_code. bcf_height_bcbrdb_predecessor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_predecessor_table) = S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_previous_code_bcbrdb_predecessor_table))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_previous_scale. bcf_height_bcbrdb_predecessor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_predecessor_table) = S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_previous_scale_bcbrdb_predecessor_table))) /\ (forall bcf_index_bcbrdb_predecessor_table_row_step. (exists bcf_lt_gap_bcbrdb_predecessor_table_row_step_bound. bcf_lt_gap_bcbrdb_predecessor_table_row_step_bound + S (bcf_index_bcbrdb_predecessor_table_row_step) = S (n + n)) -> exists bcf_value_bcbrdb_predecessor_table_row_step. ((((exists bcf_height_bcbrdb_predecessor_table_row_step_entry. bcf_height_bcbrdb_predecessor_table_row_step_entry + S (bcf_value_bcbrdb_predecessor_table_row_step) = S ((S (bcf_index_bcbrdb_predecessor_table_row_step)) * bcf_row_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_entry. bcf_row_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_entry * S ((S (bcf_index_bcbrdb_predecessor_table_row_step)) * bcf_row_scale_bcbrdb_predecessor_table) + (bcf_value_bcbrdb_predecessor_table_row_step))) /\ ((bcf_index_bcbrdb_predecessor_table_row_step = 0 /\ bcf_value_bcbrdb_predecessor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_predecessor_table_row_step bcf_left_bcbrdb_predecessor_table_row_step bcf_right_bcbrdb_predecessor_table_row_step. bcf_index_bcbrdb_predecessor_table_row_step = S bcf_predecessor_bcbrdb_predecessor_table_row_step /\ ((((exists bcf_height_bcbrdb_predecessor_table_row_step_previous_left. bcf_height_bcbrdb_predecessor_table_row_step_previous_left + S (bcf_left_bcbrdb_predecessor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_predecessor_table_row_step)) * bcf_previous_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_previous_left. bcf_previous_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_predecessor_table_row_step)) * bcf_previous_scale_bcbrdb_predecessor_table) + (bcf_left_bcbrdb_predecessor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_row_step_previous_right. bcf_height_bcbrdb_predecessor_table_row_step_previous_right + S (bcf_right_bcbrdb_predecessor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_predecessor_table_row_step))) * bcf_previous_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_previous_right. bcf_previous_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_predecessor_table_row_step))) * bcf_previous_scale_bcbrdb_predecessor_table) + (bcf_right_bcbrdb_predecessor_table_row_step))) /\ bcf_value_bcbrdb_predecessor_table_row_step = bcf_left_bcbrdb_predecessor_table_row_step + bcf_right_bcbrdb_predecessor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_predecessor_decoded_row_code. bcf_height_bcbrdb_predecessor_decoded_row_code + S (bcf_row_code_bcbrdb_predecessor) = S ((S (n + n)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_row_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_row_code_bcbrdb_predecessor))) /\ ((((exists bcf_height_bcbrdb_predecessor_decoded_row_scale. bcf_height_bcbrdb_predecessor_decoded_row_scale + S (bcf_row_scale_bcbrdb_predecessor) = S ((S (n + n)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_row_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_row_scale_bcbrdb_predecessor))) /\ (((exists bcf_height_bcbrdb_predecessor_decoded_value. bcf_height_bcbrdb_predecessor_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_value. bcf_row_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_predecessor) + (c))))))))) -> (((exists bcf_lt_gap_bcbrdb_successor_out_of_range. bcf_lt_gap_bcbrdb_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbrdb_successor_in_range. bcf_le_gap_bcbrdb_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbrdb_successor bcf_row_code_scale_bcbrdb_successor bcf_row_scale_code_bcbrdb_successor bcf_row_scale_scale_bcbrdb_successor bcf_row_code_bcbrdb_successor bcf_row_scale_bcbrdb_successor. ((forall bcf_row_index_bcbrdb_successor_table. (exists bcf_lt_gap_bcbrdb_successor_table_row_bound. bcf_lt_gap_bcbrdb_successor_table_row_bound + S (bcf_row_index_bcbrdb_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbrdb_successor_table bcf_row_scale_bcbrdb_successor_table. ((((exists bcf_height_bcbrdb_successor_table_decoded_row_code. bcf_height_bcbrdb_successor_table_decoded_row_code + S (bcf_row_code_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_row_scale. bcf_height_bcbrdb_successor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor_table))) /\ ((bcf_row_index_bcbrdb_successor_table = 0 /\ (forall bcf_index_bcbrdb_successor_table_zero_row. (exists bcf_lt_gap_bcbrdb_successor_table_zero_row_bound. bcf_lt_gap_bcbrdb_successor_table_zero_row_bound + S (bcf_index_bcbrdb_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_zero_row. ((((exists bcf_height_bcbrdb_successor_table_zero_row_entry. bcf_height_bcbrdb_successor_table_zero_row_entry + S (bcf_value_bcbrdb_successor_table_zero_row) = S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_zero_row_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_zero_row))) /\ ((bcf_index_bcbrdb_successor_table_zero_row = 0 /\ bcf_value_bcbrdb_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_zero_row. bcf_index_bcbrdb_successor_table_zero_row = S bcf_predecessor_bcbrdb_successor_table_zero_row /\ bcf_value_bcbrdb_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_successor_table bcf_previous_code_bcbrdb_successor_table bcf_previous_scale_bcbrdb_successor_table. bcf_row_index_bcbrdb_successor_table = S bcf_predecessor_bcbrdb_successor_table /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_code. bcf_height_bcbrdb_successor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_previous_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_scale. bcf_height_bcbrdb_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_previous_scale_bcbrdb_successor_table))) /\ (forall bcf_index_bcbrdb_successor_table_row_step. (exists bcf_lt_gap_bcbrdb_successor_table_row_step_bound. bcf_lt_gap_bcbrdb_successor_table_row_step_bound + S (bcf_index_bcbrdb_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_row_step. ((((exists bcf_height_bcbrdb_successor_table_row_step_entry. bcf_height_bcbrdb_successor_table_row_step_entry + S (bcf_value_bcbrdb_successor_table_row_step) = S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_entry * S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_row_step))) /\ ((bcf_index_bcbrdb_successor_table_row_step = 0 /\ bcf_value_bcbrdb_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_row_step bcf_left_bcbrdb_successor_table_row_step bcf_right_bcbrdb_successor_table_row_step. bcf_index_bcbrdb_successor_table_row_step = S bcf_predecessor_bcbrdb_successor_table_row_step /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_left. bcf_height_bcbrdb_successor_table_row_step_previous_left + S (bcf_left_bcbrdb_successor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_left. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_left_bcbrdb_successor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_right. bcf_height_bcbrdb_successor_table_row_step_previous_right + S (bcf_right_bcbrdb_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_right. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_right_bcbrdb_successor_table_row_step))) /\ bcf_value_bcbrdb_successor_table_row_step = bcf_left_bcbrdb_successor_table_row_step + bcf_right_bcbrdb_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_code. bcf_height_bcbrdb_successor_decoded_row_code + S (bcf_row_code_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_scale. bcf_height_bcbrdb_successor_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor))) /\ (((exists bcf_height_bcbrdb_successor_decoded_value. bcf_height_bcbrdb_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_value. bcf_row_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbrdb_successor) + (d))))))))) -> S n * d = (2 * S (n + n)) * c) /\ (forall n d m. (((exists bcf_lt_gap_bcbrdb_successor_out_of_range. bcf_lt_gap_bcbrdb_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbrdb_successor_in_range. bcf_le_gap_bcbrdb_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbrdb_successor bcf_row_code_scale_bcbrdb_successor bcf_row_scale_code_bcbrdb_successor bcf_row_scale_scale_bcbrdb_successor bcf_row_code_bcbrdb_successor bcf_row_scale_bcbrdb_successor. ((forall bcf_row_index_bcbrdb_successor_table. (exists bcf_lt_gap_bcbrdb_successor_table_row_bound. bcf_lt_gap_bcbrdb_successor_table_row_bound + S (bcf_row_index_bcbrdb_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbrdb_successor_table bcf_row_scale_bcbrdb_successor_table. ((((exists bcf_height_bcbrdb_successor_table_decoded_row_code. bcf_height_bcbrdb_successor_table_decoded_row_code + S (bcf_row_code_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_row_scale. bcf_height_bcbrdb_successor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor_table))) /\ ((bcf_row_index_bcbrdb_successor_table = 0 /\ (forall bcf_index_bcbrdb_successor_table_zero_row. (exists bcf_lt_gap_bcbrdb_successor_table_zero_row_bound. bcf_lt_gap_bcbrdb_successor_table_zero_row_bound + S (bcf_index_bcbrdb_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_zero_row. ((((exists bcf_height_bcbrdb_successor_table_zero_row_entry. bcf_height_bcbrdb_successor_table_zero_row_entry + S (bcf_value_bcbrdb_successor_table_zero_row) = S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_zero_row_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_zero_row))) /\ ((bcf_index_bcbrdb_successor_table_zero_row = 0 /\ bcf_value_bcbrdb_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_zero_row. bcf_index_bcbrdb_successor_table_zero_row = S bcf_predecessor_bcbrdb_successor_table_zero_row /\ bcf_value_bcbrdb_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_successor_table bcf_previous_code_bcbrdb_successor_table bcf_previous_scale_bcbrdb_successor_table. bcf_row_index_bcbrdb_successor_table = S bcf_predecessor_bcbrdb_successor_table /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_code. bcf_height_bcbrdb_successor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_previous_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_scale. bcf_height_bcbrdb_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_previous_scale_bcbrdb_successor_table))) /\ (forall bcf_index_bcbrdb_successor_table_row_step. (exists bcf_lt_gap_bcbrdb_successor_table_row_step_bound. bcf_lt_gap_bcbrdb_successor_table_row_step_bound + S (bcf_index_bcbrdb_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_row_step. ((((exists bcf_height_bcbrdb_successor_table_row_step_entry. bcf_height_bcbrdb_successor_table_row_step_entry + S (bcf_value_bcbrdb_successor_table_row_step) = S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_entry * S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_row_step))) /\ ((bcf_index_bcbrdb_successor_table_row_step = 0 /\ bcf_value_bcbrdb_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_row_step bcf_left_bcbrdb_successor_table_row_step bcf_right_bcbrdb_successor_table_row_step. bcf_index_bcbrdb_successor_table_row_step = S bcf_predecessor_bcbrdb_successor_table_row_step /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_left. bcf_height_bcbrdb_successor_table_row_step_previous_left + S (bcf_left_bcbrdb_successor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_left. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_left_bcbrdb_successor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_right. bcf_height_bcbrdb_successor_table_row_step_previous_right + S (bcf_right_bcbrdb_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_right. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_right_bcbrdb_successor_table_row_step))) /\ bcf_value_bcbrdb_successor_table_row_step = bcf_left_bcbrdb_successor_table_row_step + bcf_right_bcbrdb_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_code. bcf_height_bcbrdb_successor_decoded_row_code + S (bcf_row_code_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_scale. bcf_height_bcbrdb_successor_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor))) /\ (((exists bcf_height_bcbrdb_successor_decoded_value. bcf_height_bcbrdb_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_value. bcf_row_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbrdb_successor) + (d))))))))) -> (((exists bcf_lt_gap_bcbrdb_middle_out_of_range. bcf_lt_gap_bcbrdb_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbrdb_middle_in_range. bcf_le_gap_bcbrdb_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbrdb_middle bcf_row_code_scale_bcbrdb_middle bcf_row_scale_code_bcbrdb_middle bcf_row_scale_scale_bcbrdb_middle bcf_row_code_bcbrdb_middle bcf_row_scale_bcbrdb_middle. ((forall bcf_row_index_bcbrdb_middle_table. (exists bcf_lt_gap_bcbrdb_middle_table_row_bound. bcf_lt_gap_bcbrdb_middle_table_row_bound + S (bcf_row_index_bcbrdb_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbrdb_middle_table bcf_row_scale_bcbrdb_middle_table. ((((exists bcf_height_bcbrdb_middle_table_decoded_row_code. bcf_height_bcbrdb_middle_table_decoded_row_code + S (bcf_row_code_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_row_scale. bcf_height_bcbrdb_middle_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle_table))) /\ ((bcf_row_index_bcbrdb_middle_table = 0 /\ (forall bcf_index_bcbrdb_middle_table_zero_row. (exists bcf_lt_gap_bcbrdb_middle_table_zero_row_bound. bcf_lt_gap_bcbrdb_middle_table_zero_row_bound + S (bcf_index_bcbrdb_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_zero_row. ((((exists bcf_height_bcbrdb_middle_table_zero_row_entry. bcf_height_bcbrdb_middle_table_zero_row_entry + S (bcf_value_bcbrdb_middle_table_zero_row) = S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_zero_row_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_zero_row_entry * S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_zero_row))) /\ ((bcf_index_bcbrdb_middle_table_zero_row = 0 /\ bcf_value_bcbrdb_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_zero_row. bcf_index_bcbrdb_middle_table_zero_row = S bcf_predecessor_bcbrdb_middle_table_zero_row /\ bcf_value_bcbrdb_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_middle_table bcf_previous_code_bcbrdb_middle_table bcf_previous_scale_bcbrdb_middle_table. bcf_row_index_bcbrdb_middle_table = S bcf_predecessor_bcbrdb_middle_table /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_code. bcf_height_bcbrdb_middle_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_previous_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_scale. bcf_height_bcbrdb_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_previous_scale_bcbrdb_middle_table))) /\ (forall bcf_index_bcbrdb_middle_table_row_step. (exists bcf_lt_gap_bcbrdb_middle_table_row_step_bound. bcf_lt_gap_bcbrdb_middle_table_row_step_bound + S (bcf_index_bcbrdb_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_row_step. ((((exists bcf_height_bcbrdb_middle_table_row_step_entry. bcf_height_bcbrdb_middle_table_row_step_entry + S (bcf_value_bcbrdb_middle_table_row_step) = S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_entry * S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_row_step))) /\ ((bcf_index_bcbrdb_middle_table_row_step = 0 /\ bcf_value_bcbrdb_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_row_step bcf_left_bcbrdb_middle_table_row_step bcf_right_bcbrdb_middle_table_row_step. bcf_index_bcbrdb_middle_table_row_step = S bcf_predecessor_bcbrdb_middle_table_row_step /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_left. bcf_height_bcbrdb_middle_table_row_step_previous_left + S (bcf_left_bcbrdb_middle_table_row_step) = S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_left. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_left_bcbrdb_middle_table_row_step))) /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_right. bcf_height_bcbrdb_middle_table_row_step_previous_right + S (bcf_right_bcbrdb_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_right. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_right_bcbrdb_middle_table_row_step))) /\ bcf_value_bcbrdb_middle_table_row_step = bcf_left_bcbrdb_middle_table_row_step + bcf_right_bcbrdb_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_code. bcf_height_bcbrdb_middle_decoded_row_code + S (bcf_row_code_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_scale. bcf_height_bcbrdb_middle_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle))) /\ (((exists bcf_height_bcbrdb_middle_decoded_value. bcf_height_bcbrdb_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_value. bcf_row_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_middle) + (m))))))))) -> d = m + m))) /\ (forall n. exists z. (((exists bcf_lt_gap_bcbsuo_exists_out_of_range. bcf_lt_gap_bcbsuo_exists_out_of_range + S (n + n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bcbsuo_exists_in_range. bcf_le_gap_bcbsuo_exists_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcbsuo_exists bcf_row_code_scale_bcbsuo_exists bcf_row_scale_code_bcbsuo_exists bcf_row_scale_scale_bcbsuo_exists bcf_row_code_bcbsuo_exists bcf_row_scale_bcbsuo_exists. ((forall bcf_row_index_bcbsuo_exists_table. (exists bcf_lt_gap_bcbsuo_exists_table_row_bound. bcf_lt_gap_bcbsuo_exists_table_row_bound + S (bcf_row_index_bcbsuo_exists_table) = S (n + n)) -> exists bcf_row_code_bcbsuo_exists_table bcf_row_scale_bcbsuo_exists_table. ((((exists bcf_height_bcbsuo_exists_table_decoded_row_code. bcf_height_bcbsuo_exists_table_decoded_row_code + S (bcf_row_code_bcbsuo_exists_table) = S ((S (bcf_row_index_bcbsuo_exists_table)) * bcf_row_code_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_table_decoded_row_code. bcf_row_code_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_table_decoded_row_code * S ((S (bcf_row_index_bcbsuo_exists_table)) * bcf_row_code_scale_bcbsuo_exists) + (bcf_row_code_bcbsuo_exists_table))) /\ ((((exists bcf_height_bcbsuo_exists_table_decoded_row_scale. bcf_height_bcbsuo_exists_table_decoded_row_scale + S (bcf_row_scale_bcbsuo_exists_table) = S ((S (bcf_row_index_bcbsuo_exists_table)) * bcf_row_scale_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_table_decoded_row_scale. bcf_row_scale_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_table_decoded_row_scale * S ((S (bcf_row_index_bcbsuo_exists_table)) * bcf_row_scale_scale_bcbsuo_exists) + (bcf_row_scale_bcbsuo_exists_table))) /\ ((bcf_row_index_bcbsuo_exists_table = 0 /\ (forall bcf_index_bcbsuo_exists_table_zero_row. (exists bcf_lt_gap_bcbsuo_exists_table_zero_row_bound. bcf_lt_gap_bcbsuo_exists_table_zero_row_bound + S (bcf_index_bcbsuo_exists_table_zero_row) = S (n + n)) -> exists bcf_value_bcbsuo_exists_table_zero_row. ((((exists bcf_height_bcbsuo_exists_table_zero_row_entry. bcf_height_bcbsuo_exists_table_zero_row_entry + S (bcf_value_bcbsuo_exists_table_zero_row) = S ((S (bcf_index_bcbsuo_exists_table_zero_row)) * bcf_row_scale_bcbsuo_exists_table)) /\ exists bcf_quotient_bcbsuo_exists_table_zero_row_entry. bcf_row_code_bcbsuo_exists_table = bcf_quotient_bcbsuo_exists_table_zero_row_entry * S ((S (bcf_index_bcbsuo_exists_table_zero_row)) * bcf_row_scale_bcbsuo_exists_table) + (bcf_value_bcbsuo_exists_table_zero_row))) /\ ((bcf_index_bcbsuo_exists_table_zero_row = 0 /\ bcf_value_bcbsuo_exists_table_zero_row = 1) \/ exists bcf_predecessor_bcbsuo_exists_table_zero_row. bcf_index_bcbsuo_exists_table_zero_row = S bcf_predecessor_bcbsuo_exists_table_zero_row /\ bcf_value_bcbsuo_exists_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsuo_exists_table bcf_previous_code_bcbsuo_exists_table bcf_previous_scale_bcbsuo_exists_table. bcf_row_index_bcbsuo_exists_table = S bcf_predecessor_bcbsuo_exists_table /\ ((((exists bcf_height_bcbsuo_exists_table_decoded_previous_code. bcf_height_bcbsuo_exists_table_decoded_previous_code + S (bcf_previous_code_bcbsuo_exists_table) = S ((S (bcf_predecessor_bcbsuo_exists_table)) * bcf_row_code_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_table_decoded_previous_code. bcf_row_code_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsuo_exists_table)) * bcf_row_code_scale_bcbsuo_exists) + (bcf_previous_code_bcbsuo_exists_table))) /\ ((((exists bcf_height_bcbsuo_exists_table_decoded_previous_scale. bcf_height_bcbsuo_exists_table_decoded_previous_scale + S (bcf_previous_scale_bcbsuo_exists_table) = S ((S (bcf_predecessor_bcbsuo_exists_table)) * bcf_row_scale_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_table_decoded_previous_scale. bcf_row_scale_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsuo_exists_table)) * bcf_row_scale_scale_bcbsuo_exists) + (bcf_previous_scale_bcbsuo_exists_table))) /\ (forall bcf_index_bcbsuo_exists_table_row_step. (exists bcf_lt_gap_bcbsuo_exists_table_row_step_bound. bcf_lt_gap_bcbsuo_exists_table_row_step_bound + S (bcf_index_bcbsuo_exists_table_row_step) = S (n + n)) -> exists bcf_value_bcbsuo_exists_table_row_step. ((((exists bcf_height_bcbsuo_exists_table_row_step_entry. bcf_height_bcbsuo_exists_table_row_step_entry + S (bcf_value_bcbsuo_exists_table_row_step) = S ((S (bcf_index_bcbsuo_exists_table_row_step)) * bcf_row_scale_bcbsuo_exists_table)) /\ exists bcf_quotient_bcbsuo_exists_table_row_step_entry. bcf_row_code_bcbsuo_exists_table = bcf_quotient_bcbsuo_exists_table_row_step_entry * S ((S (bcf_index_bcbsuo_exists_table_row_step)) * bcf_row_scale_bcbsuo_exists_table) + (bcf_value_bcbsuo_exists_table_row_step))) /\ ((bcf_index_bcbsuo_exists_table_row_step = 0 /\ bcf_value_bcbsuo_exists_table_row_step = 1) \/ exists bcf_predecessor_bcbsuo_exists_table_row_step bcf_left_bcbsuo_exists_table_row_step bcf_right_bcbsuo_exists_table_row_step. bcf_index_bcbsuo_exists_table_row_step = S bcf_predecessor_bcbsuo_exists_table_row_step /\ ((((exists bcf_height_bcbsuo_exists_table_row_step_previous_left. bcf_height_bcbsuo_exists_table_row_step_previous_left + S (bcf_left_bcbsuo_exists_table_row_step) = S ((S (bcf_predecessor_bcbsuo_exists_table_row_step)) * bcf_previous_scale_bcbsuo_exists_table)) /\ exists bcf_quotient_bcbsuo_exists_table_row_step_previous_left. bcf_previous_code_bcbsuo_exists_table = bcf_quotient_bcbsuo_exists_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsuo_exists_table_row_step)) * bcf_previous_scale_bcbsuo_exists_table) + (bcf_left_bcbsuo_exists_table_row_step))) /\ ((((exists bcf_height_bcbsuo_exists_table_row_step_previous_right. bcf_height_bcbsuo_exists_table_row_step_previous_right + S (bcf_right_bcbsuo_exists_table_row_step) = S ((S (S (bcf_predecessor_bcbsuo_exists_table_row_step))) * bcf_previous_scale_bcbsuo_exists_table)) /\ exists bcf_quotient_bcbsuo_exists_table_row_step_previous_right. bcf_previous_code_bcbsuo_exists_table = bcf_quotient_bcbsuo_exists_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsuo_exists_table_row_step))) * bcf_previous_scale_bcbsuo_exists_table) + (bcf_right_bcbsuo_exists_table_row_step))) /\ bcf_value_bcbsuo_exists_table_row_step = bcf_left_bcbsuo_exists_table_row_step + bcf_right_bcbsuo_exists_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsuo_exists_decoded_row_code. bcf_height_bcbsuo_exists_decoded_row_code + S (bcf_row_code_bcbsuo_exists) = S ((S (n + n)) * bcf_row_code_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_decoded_row_code. bcf_row_code_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcbsuo_exists) + (bcf_row_code_bcbsuo_exists))) /\ ((((exists bcf_height_bcbsuo_exists_decoded_row_scale. bcf_height_bcbsuo_exists_decoded_row_scale + S (bcf_row_scale_bcbsuo_exists) = S ((S (n + n)) * bcf_row_scale_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_decoded_row_scale. bcf_row_scale_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcbsuo_exists) + (bcf_row_scale_bcbsuo_exists))) /\ (((exists bcf_height_bcbsuo_exists_decoded_value. bcf_height_bcbsuo_exists_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bcbsuo_exists)) /\ exists bcf_quotient_bcbsuo_exists_decoded_value. bcf_row_code_bcbsuo_exists = bcf_quotient_bcbsuo_exists_decoded_value * S ((S (n)) * bcf_row_scale_bcbsuo_exists) + (z))))))))))) - 0002
exact central_binom_upper_support_package - 0003
cases hpackage - 0004
cases hpackage_left - 0005
apply central_binom_strong_upper_of_laws - 0006
exact hpackage_left_left - 0007
exact hpackage_right