BT00VO — central_binom_strong

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded 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)

Structural proof guide

Twice a positive-index central binomial is at most four-power.

Direct prerequisites: central_binom_upper_support_package, central_binom_strong_upper_of_laws. The authored body proceeds by case analysis (2), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT00VN central_binom_upper_support_package BT00VM central_binom_strong_upper_of_laws

Direct dependents

BT00VT central_binom_nonzero_strong_upper

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

7 script commands · 3 reading checkpoints · 1 local claims

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

Named ingredients (2)

central binom upper support package central binom strong upper of laws

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: Choose CentralBinom
L2
exact central_binom_upper_support_package

02Separate the logical casesL3–4

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

L3
cases hpackage
L4
cases hpackage_left

03Use earlier factsL5–7

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

L5
apply central_binom_strong_upper_of_laws
L6
exact hpackage_left_left
L7
exact hpackage_right

Library-wide reading audit

Original exact command ledger · 7 lines

0001have 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)))))))))))
0002exact central_binom_upper_support_package
0003cases hpackage
0004cases hpackage_left
0005apply central_binom_strong_upper_of_laws
0006exact hpackage_left_left
0007exact hpackage_right