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. ∀ m. ∀ q. Choose(S (n + n),n,m) → Pow(4,n,q) → Le(m,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
11 occurrences
Exact expanded native-PA statement
forall n m q. (((exists bcf_lt_gap_bcomlfp_middle_out_of_range. bcf_lt_gap_bcomlfp_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcomlfp_middle_in_range. bcf_le_gap_bcomlfp_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcomlfp_middle bcf_row_code_scale_bcomlfp_middle bcf_row_scale_code_bcomlfp_middle bcf_row_scale_scale_bcomlfp_middle bcf_row_code_bcomlfp_middle bcf_row_scale_bcomlfp_middle. ((forall bcf_row_index_bcomlfp_middle_table. (exists bcf_lt_gap_bcomlfp_middle_table_row_bound. bcf_lt_gap_bcomlfp_middle_table_row_bound + S (bcf_row_index_bcomlfp_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcomlfp_middle_table bcf_row_scale_bcomlfp_middle_table. ((((exists bcf_height_bcomlfp_middle_table_decoded_row_code. bcf_height_bcomlfp_middle_table_decoded_row_code + S (bcf_row_code_bcomlfp_middle_table) = S ((S (bcf_row_index_bcomlfp_middle_table)) * bcf_row_code_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_table_decoded_row_code. bcf_row_code_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_table_decoded_row_code * S ((S (bcf_row_index_bcomlfp_middle_table)) * bcf_row_code_scale_bcomlfp_middle) + (bcf_row_code_bcomlfp_middle_table))) /\ ((((exists bcf_height_bcomlfp_middle_table_decoded_row_scale. bcf_height_bcomlfp_middle_table_decoded_row_scale + S (bcf_row_scale_bcomlfp_middle_table) = S ((S (bcf_row_index_bcomlfp_middle_table)) * bcf_row_scale_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_table_decoded_row_scale. bcf_row_scale_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcomlfp_middle_table)) * bcf_row_scale_scale_bcomlfp_middle) + (bcf_row_scale_bcomlfp_middle_table))) /\ ((bcf_row_index_bcomlfp_middle_table = 0 /\ (forall bcf_index_bcomlfp_middle_table_zero_row. (exists bcf_lt_gap_bcomlfp_middle_table_zero_row_bound. bcf_lt_gap_bcomlfp_middle_table_zero_row_bound + S (bcf_index_bcomlfp_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcomlfp_middle_table_zero_row. ((((exists bcf_height_bcomlfp_middle_table_zero_row_entry. bcf_height_bcomlfp_middle_table_zero_row_entry + S (bcf_value_bcomlfp_middle_table_zero_row) = S ((S (bcf_index_bcomlfp_middle_table_zero_row)) * bcf_row_scale_bcomlfp_middle_table)) /\ exists bcf_quotient_bcomlfp_middle_table_zero_row_entry. bcf_row_code_bcomlfp_middle_table = bcf_quotient_bcomlfp_middle_table_zero_row_entry * S ((S (bcf_index_bcomlfp_middle_table_zero_row)) * bcf_row_scale_bcomlfp_middle_table) + (bcf_value_bcomlfp_middle_table_zero_row))) /\ ((bcf_index_bcomlfp_middle_table_zero_row = 0 /\ bcf_value_bcomlfp_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcomlfp_middle_table_zero_row. bcf_index_bcomlfp_middle_table_zero_row = S bcf_predecessor_bcomlfp_middle_table_zero_row /\ bcf_value_bcomlfp_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcomlfp_middle_table bcf_previous_code_bcomlfp_middle_table bcf_previous_scale_bcomlfp_middle_table. bcf_row_index_bcomlfp_middle_table = S bcf_predecessor_bcomlfp_middle_table /\ ((((exists bcf_height_bcomlfp_middle_table_decoded_previous_code. bcf_height_bcomlfp_middle_table_decoded_previous_code + S (bcf_previous_code_bcomlfp_middle_table) = S ((S (bcf_predecessor_bcomlfp_middle_table)) * bcf_row_code_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_table_decoded_previous_code. bcf_row_code_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcomlfp_middle_table)) * bcf_row_code_scale_bcomlfp_middle) + (bcf_previous_code_bcomlfp_middle_table))) /\ ((((exists bcf_height_bcomlfp_middle_table_decoded_previous_scale. bcf_height_bcomlfp_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcomlfp_middle_table) = S ((S (bcf_predecessor_bcomlfp_middle_table)) * bcf_row_scale_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_table_decoded_previous_scale. bcf_row_scale_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcomlfp_middle_table)) * bcf_row_scale_scale_bcomlfp_middle) + (bcf_previous_scale_bcomlfp_middle_table))) /\ (forall bcf_index_bcomlfp_middle_table_row_step. (exists bcf_lt_gap_bcomlfp_middle_table_row_step_bound. bcf_lt_gap_bcomlfp_middle_table_row_step_bound + S (bcf_index_bcomlfp_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcomlfp_middle_table_row_step. ((((exists bcf_height_bcomlfp_middle_table_row_step_entry. bcf_height_bcomlfp_middle_table_row_step_entry + S (bcf_value_bcomlfp_middle_table_row_step) = S ((S (bcf_index_bcomlfp_middle_table_row_step)) * bcf_row_scale_bcomlfp_middle_table)) /\ exists bcf_quotient_bcomlfp_middle_table_row_step_entry. bcf_row_code_bcomlfp_middle_table = bcf_quotient_bcomlfp_middle_table_row_step_entry * S ((S (bcf_index_bcomlfp_middle_table_row_step)) * bcf_row_scale_bcomlfp_middle_table) + (bcf_value_bcomlfp_middle_table_row_step))) /\ ((bcf_index_bcomlfp_middle_table_row_step = 0 /\ bcf_value_bcomlfp_middle_table_row_step = 1) \/ exists bcf_predecessor_bcomlfp_middle_table_row_step bcf_left_bcomlfp_middle_table_row_step bcf_right_bcomlfp_middle_table_row_step. bcf_index_bcomlfp_middle_table_row_step = S bcf_predecessor_bcomlfp_middle_table_row_step /\ ((((exists bcf_height_bcomlfp_middle_table_row_step_previous_left. bcf_height_bcomlfp_middle_table_row_step_previous_left + S (bcf_left_bcomlfp_middle_table_row_step) = S ((S (bcf_predecessor_bcomlfp_middle_table_row_step)) * bcf_previous_scale_bcomlfp_middle_table)) /\ exists bcf_quotient_bcomlfp_middle_table_row_step_previous_left. bcf_previous_code_bcomlfp_middle_table = bcf_quotient_bcomlfp_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcomlfp_middle_table_row_step)) * bcf_previous_scale_bcomlfp_middle_table) + (bcf_left_bcomlfp_middle_table_row_step))) /\ ((((exists bcf_height_bcomlfp_middle_table_row_step_previous_right. bcf_height_bcomlfp_middle_table_row_step_previous_right + S (bcf_right_bcomlfp_middle_table_row_step) = S ((S (S (bcf_predecessor_bcomlfp_middle_table_row_step))) * bcf_previous_scale_bcomlfp_middle_table)) /\ exists bcf_quotient_bcomlfp_middle_table_row_step_previous_right. bcf_previous_code_bcomlfp_middle_table = bcf_quotient_bcomlfp_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcomlfp_middle_table_row_step))) * bcf_previous_scale_bcomlfp_middle_table) + (bcf_right_bcomlfp_middle_table_row_step))) /\ bcf_value_bcomlfp_middle_table_row_step = bcf_left_bcomlfp_middle_table_row_step + bcf_right_bcomlfp_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcomlfp_middle_decoded_row_code. bcf_height_bcomlfp_middle_decoded_row_code + S (bcf_row_code_bcomlfp_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_decoded_row_code. bcf_row_code_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcomlfp_middle) + (bcf_row_code_bcomlfp_middle))) /\ ((((exists bcf_height_bcomlfp_middle_decoded_row_scale. bcf_height_bcomlfp_middle_decoded_row_scale + S (bcf_row_scale_bcomlfp_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_decoded_row_scale. bcf_row_scale_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcomlfp_middle) + (bcf_row_scale_bcomlfp_middle))) /\ (((exists bcf_height_bcomlfp_middle_decoded_value. bcf_height_bcomlfp_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcomlfp_middle)) /\ exists bcf_quotient_bcomlfp_middle_decoded_value. bcf_row_code_bcomlfp_middle = bcf_quotient_bcomlfp_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcomlfp_middle) + (m))))))))) -> (exists pa_b_bcomlfp_power pa_c_bcomlfp_power. ((forall pa_i_bcomlfp_power_repeat. (exists pa_lt_bcomlfp_power_repeat_bound. pa_lt_bcomlfp_power_repeat_bound + S pa_i_bcomlfp_power_repeat = n) -> (((exists pa_h_bcomlfp_power_repeat_decoded. pa_h_bcomlfp_power_repeat_decoded + S (4) = S ((S (pa_i_bcomlfp_power_repeat)) * pa_c_bcomlfp_power)) /\ exists pa_q_bcomlfp_power_repeat_decoded. pa_b_bcomlfp_power = pa_q_bcomlfp_power_repeat_decoded * S ((S (pa_i_bcomlfp_power_repeat)) * pa_c_bcomlfp_power) + (4)))) /\ (exists pa_u_bcomlfp_power_product pa_v_bcomlfp_power_product. ((((exists pa_h_bcomlfp_power_product_start. pa_h_bcomlfp_power_product_start + S (1) = S ((S (0)) * pa_v_bcomlfp_power_product)) /\ exists pa_q_bcomlfp_power_product_start. pa_u_bcomlfp_power_product = pa_q_bcomlfp_power_product_start * S ((S (0)) * pa_v_bcomlfp_power_product) + (1))) /\ ((((exists pa_h_bcomlfp_power_product_terminal. pa_h_bcomlfp_power_product_terminal + S (q) = S ((S (n)) * pa_v_bcomlfp_power_product)) /\ exists pa_q_bcomlfp_power_product_terminal. pa_u_bcomlfp_power_product = pa_q_bcomlfp_power_product_terminal * S ((S (n)) * pa_v_bcomlfp_power_product) + (q))) /\ forall pa_i_bcomlfp_power_product. (exists pa_lt_bcomlfp_power_product_bound. pa_lt_bcomlfp_power_product_bound + S pa_i_bcomlfp_power_product = n) -> exists pa_p_bcomlfp_power_product pa_r_bcomlfp_power_product pa_s_bcomlfp_power_product. ((((exists pa_h_bcomlfp_power_product_factor. pa_h_bcomlfp_power_product_factor + S (pa_p_bcomlfp_power_product) = S ((S (pa_i_bcomlfp_power_product)) * pa_c_bcomlfp_power)) /\ exists pa_q_bcomlfp_power_product_factor. pa_b_bcomlfp_power = pa_q_bcomlfp_power_product_factor * S ((S (pa_i_bcomlfp_power_product)) * pa_c_bcomlfp_power) + (pa_p_bcomlfp_power_product))) /\ ((((exists pa_h_bcomlfp_power_product_partial. pa_h_bcomlfp_power_product_partial + S (pa_r_bcomlfp_power_product) = S ((S (pa_i_bcomlfp_power_product)) * pa_v_bcomlfp_power_product)) /\ exists pa_q_bcomlfp_power_product_partial. pa_u_bcomlfp_power_product = pa_q_bcomlfp_power_product_partial * S ((S (pa_i_bcomlfp_power_product)) * pa_v_bcomlfp_power_product) + (pa_r_bcomlfp_power_product))) /\ ((((exists pa_h_bcomlfp_power_product_successor. pa_h_bcomlfp_power_product_successor + S (pa_s_bcomlfp_power_product) = S ((S (S pa_i_bcomlfp_power_product)) * pa_v_bcomlfp_power_product)) /\ exists pa_q_bcomlfp_power_product_successor. pa_u_bcomlfp_power_product = pa_q_bcomlfp_power_product_successor * S ((S (S pa_i_bcomlfp_power_product)) * pa_v_bcomlfp_power_product) + (pa_s_bcomlfp_power_product))) /\ pa_s_bcomlfp_power_product = pa_r_bcomlfp_power_product * pa_p_bcomlfp_power_product)))))))) -> (exists bcf_le_gap_bcomlfp_result. bcf_le_gap_bcomlfp_result + (m) = q)Proof neighborhood
Direct theorem prerequisites
BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT00QU two_mul_eq_add_self BT00RD mul_le_cancel_left_nonzero BT00S5 pow_successor_compose BT00VN central_binom_upper_support_package BT00VM central_binom_strong_upper_of_lawsDirect 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 (8)
01Fix variables and assumptionsL1–5
02Establish hpackageL6–7
Establish this local claim before using it. It is not an additional assumption.
- L6
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 - L7
exact central_binom_upper_support_package
03Separate the logical casesL8–9
04Establish hcentral_existsL10–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpackage right.
- L10
have hcentral_exists : ∃ d. CentralBinom(S n,d)Definitions: CentralBinom(S n,d)Original native command in the exact edition - L11
apply hpackage_right
05Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
cases hcentral_exists
06Establish hdoubleL13–16
07Establish hsuccessor_powerL17–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose.
- L17
have hsuccessor_power : Pow(4,S n,q · 4)Definitions: Pow(4,S n,q · 4)Original native command in the exact edition - L18
specialize pow_successor_compose 4 - L19
specialize pow_successor_compose n - L20
specialize pow_successor_compose q - L21
specialize pow_successor_compose (q * 4) - L22
apply pow_successor_compose - L23
exact hpower - L24
refl
08Establish hstrong_allL25–28
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom strong upper of laws.
- L25
have hstrong_all : ∀ n. ∀ c. ∀ q. CentralBinom(S n,c) → Pow(4,S n,q) → Le(2 · c,q)Definitions: CentralBinom(S n,c)Pow(4,S n,q)Le(2 · c,q)Original native command in the exact edition - L26
apply central_binom_strong_upper_of_laws - L27
exact hpackage_left_left - L28
exact hpackage_right
09Establish hstrongL29–35
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hstrong all.
- L29
have hstrong : Le(2 · x,q · 4)Definitions: Le(2 · x,q · 4)Original native command in the exact edition - L30
specialize hstrong_all n - L31
specialize hstrong_all x - L32
specialize hstrong_all (q * 4) - L33
apply hstrong_all - L34
exact hcentral_exists_witness - L35
exact hsuccessor_power
10Establish hleftL36–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul add.
11Establish htwo_twoL46–49
12Establish hrightL50–59
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.
- L50
have hright : q * 4 = 4 * q - L51
apply mul_comm - L52
rewrite hdouble at hstrong - L53
rewrite hleft at hstrong - L54
rewrite hright at hstrong - L55
specialize mul_le_cancel_left_nonzero 4 - L56
specialize mul_le_cancel_left_nonzero m - L57
specialize mul_le_cancel_left_nonzero q - L58
apply mul_le_cancel_left_nonzero - L59
intro hfour_zero
Original defined command ledger · 62 lines
- 0001
intro n - 0002
intro m - 0003
intro q - 0004
intro hmiddle - 0005
intro hpower - 0006
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))))))))))) - 0007
exact central_binom_upper_support_package - 0008
cases hpackage - 0009
cases hpackage_left - 0010
have hcentral_exists : ∃ d. CentralBinom(S n,d)Exact native replay line
have hcentral_exists : exists d. (((exists bcf_lt_gap_bcomlfp_central_out_of_range. bcf_lt_gap_bcomlfp_central_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcomlfp_central_in_range. bcf_le_gap_bcomlfp_central_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcomlfp_central bcf_row_code_scale_bcomlfp_central bcf_row_scale_code_bcomlfp_central bcf_row_scale_scale_bcomlfp_central bcf_row_code_bcomlfp_central bcf_row_scale_bcomlfp_central. ((forall bcf_row_index_bcomlfp_central_table. (exists bcf_lt_gap_bcomlfp_central_table_row_bound. bcf_lt_gap_bcomlfp_central_table_row_bound + S (bcf_row_index_bcomlfp_central_table) = S (S n + S n)) -> exists bcf_row_code_bcomlfp_central_table bcf_row_scale_bcomlfp_central_table. ((((exists bcf_height_bcomlfp_central_table_decoded_row_code. bcf_height_bcomlfp_central_table_decoded_row_code + S (bcf_row_code_bcomlfp_central_table) = S ((S (bcf_row_index_bcomlfp_central_table)) * bcf_row_code_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_table_decoded_row_code. bcf_row_code_code_bcomlfp_central = bcf_quotient_bcomlfp_central_table_decoded_row_code * S ((S (bcf_row_index_bcomlfp_central_table)) * bcf_row_code_scale_bcomlfp_central) + (bcf_row_code_bcomlfp_central_table))) /\ ((((exists bcf_height_bcomlfp_central_table_decoded_row_scale. bcf_height_bcomlfp_central_table_decoded_row_scale + S (bcf_row_scale_bcomlfp_central_table) = S ((S (bcf_row_index_bcomlfp_central_table)) * bcf_row_scale_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_table_decoded_row_scale. bcf_row_scale_code_bcomlfp_central = bcf_quotient_bcomlfp_central_table_decoded_row_scale * S ((S (bcf_row_index_bcomlfp_central_table)) * bcf_row_scale_scale_bcomlfp_central) + (bcf_row_scale_bcomlfp_central_table))) /\ ((bcf_row_index_bcomlfp_central_table = 0 /\ (forall bcf_index_bcomlfp_central_table_zero_row. (exists bcf_lt_gap_bcomlfp_central_table_zero_row_bound. bcf_lt_gap_bcomlfp_central_table_zero_row_bound + S (bcf_index_bcomlfp_central_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcomlfp_central_table_zero_row. ((((exists bcf_height_bcomlfp_central_table_zero_row_entry. bcf_height_bcomlfp_central_table_zero_row_entry + S (bcf_value_bcomlfp_central_table_zero_row) = S ((S (bcf_index_bcomlfp_central_table_zero_row)) * bcf_row_scale_bcomlfp_central_table)) /\ exists bcf_quotient_bcomlfp_central_table_zero_row_entry. bcf_row_code_bcomlfp_central_table = bcf_quotient_bcomlfp_central_table_zero_row_entry * S ((S (bcf_index_bcomlfp_central_table_zero_row)) * bcf_row_scale_bcomlfp_central_table) + (bcf_value_bcomlfp_central_table_zero_row))) /\ ((bcf_index_bcomlfp_central_table_zero_row = 0 /\ bcf_value_bcomlfp_central_table_zero_row = 1) \/ exists bcf_predecessor_bcomlfp_central_table_zero_row. bcf_index_bcomlfp_central_table_zero_row = S bcf_predecessor_bcomlfp_central_table_zero_row /\ bcf_value_bcomlfp_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bcomlfp_central_table bcf_previous_code_bcomlfp_central_table bcf_previous_scale_bcomlfp_central_table. bcf_row_index_bcomlfp_central_table = S bcf_predecessor_bcomlfp_central_table /\ ((((exists bcf_height_bcomlfp_central_table_decoded_previous_code. bcf_height_bcomlfp_central_table_decoded_previous_code + S (bcf_previous_code_bcomlfp_central_table) = S ((S (bcf_predecessor_bcomlfp_central_table)) * bcf_row_code_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_table_decoded_previous_code. bcf_row_code_code_bcomlfp_central = bcf_quotient_bcomlfp_central_table_decoded_previous_code * S ((S (bcf_predecessor_bcomlfp_central_table)) * bcf_row_code_scale_bcomlfp_central) + (bcf_previous_code_bcomlfp_central_table))) /\ ((((exists bcf_height_bcomlfp_central_table_decoded_previous_scale. bcf_height_bcomlfp_central_table_decoded_previous_scale + S (bcf_previous_scale_bcomlfp_central_table) = S ((S (bcf_predecessor_bcomlfp_central_table)) * bcf_row_scale_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_table_decoded_previous_scale. bcf_row_scale_code_bcomlfp_central = bcf_quotient_bcomlfp_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bcomlfp_central_table)) * bcf_row_scale_scale_bcomlfp_central) + (bcf_previous_scale_bcomlfp_central_table))) /\ (forall bcf_index_bcomlfp_central_table_row_step. (exists bcf_lt_gap_bcomlfp_central_table_row_step_bound. bcf_lt_gap_bcomlfp_central_table_row_step_bound + S (bcf_index_bcomlfp_central_table_row_step) = S (S n + S n)) -> exists bcf_value_bcomlfp_central_table_row_step. ((((exists bcf_height_bcomlfp_central_table_row_step_entry. bcf_height_bcomlfp_central_table_row_step_entry + S (bcf_value_bcomlfp_central_table_row_step) = S ((S (bcf_index_bcomlfp_central_table_row_step)) * bcf_row_scale_bcomlfp_central_table)) /\ exists bcf_quotient_bcomlfp_central_table_row_step_entry. bcf_row_code_bcomlfp_central_table = bcf_quotient_bcomlfp_central_table_row_step_entry * S ((S (bcf_index_bcomlfp_central_table_row_step)) * bcf_row_scale_bcomlfp_central_table) + (bcf_value_bcomlfp_central_table_row_step))) /\ ((bcf_index_bcomlfp_central_table_row_step = 0 /\ bcf_value_bcomlfp_central_table_row_step = 1) \/ exists bcf_predecessor_bcomlfp_central_table_row_step bcf_left_bcomlfp_central_table_row_step bcf_right_bcomlfp_central_table_row_step. bcf_index_bcomlfp_central_table_row_step = S bcf_predecessor_bcomlfp_central_table_row_step /\ ((((exists bcf_height_bcomlfp_central_table_row_step_previous_left. bcf_height_bcomlfp_central_table_row_step_previous_left + S (bcf_left_bcomlfp_central_table_row_step) = S ((S (bcf_predecessor_bcomlfp_central_table_row_step)) * bcf_previous_scale_bcomlfp_central_table)) /\ exists bcf_quotient_bcomlfp_central_table_row_step_previous_left. bcf_previous_code_bcomlfp_central_table = bcf_quotient_bcomlfp_central_table_row_step_previous_left * S ((S (bcf_predecessor_bcomlfp_central_table_row_step)) * bcf_previous_scale_bcomlfp_central_table) + (bcf_left_bcomlfp_central_table_row_step))) /\ ((((exists bcf_height_bcomlfp_central_table_row_step_previous_right. bcf_height_bcomlfp_central_table_row_step_previous_right + S (bcf_right_bcomlfp_central_table_row_step) = S ((S (S (bcf_predecessor_bcomlfp_central_table_row_step))) * bcf_previous_scale_bcomlfp_central_table)) /\ exists bcf_quotient_bcomlfp_central_table_row_step_previous_right. bcf_previous_code_bcomlfp_central_table = bcf_quotient_bcomlfp_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcomlfp_central_table_row_step))) * bcf_previous_scale_bcomlfp_central_table) + (bcf_right_bcomlfp_central_table_row_step))) /\ bcf_value_bcomlfp_central_table_row_step = bcf_left_bcomlfp_central_table_row_step + bcf_right_bcomlfp_central_table_row_step))))))))))) /\ ((((exists bcf_height_bcomlfp_central_decoded_row_code. bcf_height_bcomlfp_central_decoded_row_code + S (bcf_row_code_bcomlfp_central) = S ((S (S n + S n)) * bcf_row_code_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_decoded_row_code. bcf_row_code_code_bcomlfp_central = bcf_quotient_bcomlfp_central_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcomlfp_central) + (bcf_row_code_bcomlfp_central))) /\ ((((exists bcf_height_bcomlfp_central_decoded_row_scale. bcf_height_bcomlfp_central_decoded_row_scale + S (bcf_row_scale_bcomlfp_central) = S ((S (S n + S n)) * bcf_row_scale_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_decoded_row_scale. bcf_row_scale_code_bcomlfp_central = bcf_quotient_bcomlfp_central_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcomlfp_central) + (bcf_row_scale_bcomlfp_central))) /\ (((exists bcf_height_bcomlfp_central_decoded_value. bcf_height_bcomlfp_central_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcomlfp_central)) /\ exists bcf_quotient_bcomlfp_central_decoded_value. bcf_row_code_bcomlfp_central = bcf_quotient_bcomlfp_central_decoded_value * S ((S (S n)) * bcf_row_scale_bcomlfp_central) + (d))))))))) - 0011
apply hpackage_right - 0012
cases hcentral_exists - 0013
have hdouble : x = m + m - 0014
apply hpackage_left_right - 0015
exact hcentral_exists_witness - 0016
exact hmiddle - 0017
have hsuccessor_power : Pow(4,S n,q · 4)Exact native replay line
have hsuccessor_power : exists pa_b_bcomlfp_successor_power pa_c_bcomlfp_successor_power. ((forall pa_i_bcomlfp_successor_power_repeat. (exists pa_lt_bcomlfp_successor_power_repeat_bound. pa_lt_bcomlfp_successor_power_repeat_bound + S pa_i_bcomlfp_successor_power_repeat = S n) -> (((exists pa_h_bcomlfp_successor_power_repeat_decoded. pa_h_bcomlfp_successor_power_repeat_decoded + S (4) = S ((S (pa_i_bcomlfp_successor_power_repeat)) * pa_c_bcomlfp_successor_power)) /\ exists pa_q_bcomlfp_successor_power_repeat_decoded. pa_b_bcomlfp_successor_power = pa_q_bcomlfp_successor_power_repeat_decoded * S ((S (pa_i_bcomlfp_successor_power_repeat)) * pa_c_bcomlfp_successor_power) + (4)))) /\ (exists pa_u_bcomlfp_successor_power_product pa_v_bcomlfp_successor_power_product. ((((exists pa_h_bcomlfp_successor_power_product_start. pa_h_bcomlfp_successor_power_product_start + S (1) = S ((S (0)) * pa_v_bcomlfp_successor_power_product)) /\ exists pa_q_bcomlfp_successor_power_product_start. pa_u_bcomlfp_successor_power_product = pa_q_bcomlfp_successor_power_product_start * S ((S (0)) * pa_v_bcomlfp_successor_power_product) + (1))) /\ ((((exists pa_h_bcomlfp_successor_power_product_terminal. pa_h_bcomlfp_successor_power_product_terminal + S (q * 4) = S ((S (S n)) * pa_v_bcomlfp_successor_power_product)) /\ exists pa_q_bcomlfp_successor_power_product_terminal. pa_u_bcomlfp_successor_power_product = pa_q_bcomlfp_successor_power_product_terminal * S ((S (S n)) * pa_v_bcomlfp_successor_power_product) + (q * 4))) /\ forall pa_i_bcomlfp_successor_power_product. (exists pa_lt_bcomlfp_successor_power_product_bound. pa_lt_bcomlfp_successor_power_product_bound + S pa_i_bcomlfp_successor_power_product = S n) -> exists pa_p_bcomlfp_successor_power_product pa_r_bcomlfp_successor_power_product pa_s_bcomlfp_successor_power_product. ((((exists pa_h_bcomlfp_successor_power_product_factor. pa_h_bcomlfp_successor_power_product_factor + S (pa_p_bcomlfp_successor_power_product) = S ((S (pa_i_bcomlfp_successor_power_product)) * pa_c_bcomlfp_successor_power)) /\ exists pa_q_bcomlfp_successor_power_product_factor. pa_b_bcomlfp_successor_power = pa_q_bcomlfp_successor_power_product_factor * S ((S (pa_i_bcomlfp_successor_power_product)) * pa_c_bcomlfp_successor_power) + (pa_p_bcomlfp_successor_power_product))) /\ ((((exists pa_h_bcomlfp_successor_power_product_partial. pa_h_bcomlfp_successor_power_product_partial + S (pa_r_bcomlfp_successor_power_product) = S ((S (pa_i_bcomlfp_successor_power_product)) * pa_v_bcomlfp_successor_power_product)) /\ exists pa_q_bcomlfp_successor_power_product_partial. pa_u_bcomlfp_successor_power_product = pa_q_bcomlfp_successor_power_product_partial * S ((S (pa_i_bcomlfp_successor_power_product)) * pa_v_bcomlfp_successor_power_product) + (pa_r_bcomlfp_successor_power_product))) /\ ((((exists pa_h_bcomlfp_successor_power_product_successor. pa_h_bcomlfp_successor_power_product_successor + S (pa_s_bcomlfp_successor_power_product) = S ((S (S pa_i_bcomlfp_successor_power_product)) * pa_v_bcomlfp_successor_power_product)) /\ exists pa_q_bcomlfp_successor_power_product_successor. pa_u_bcomlfp_successor_power_product = pa_q_bcomlfp_successor_power_product_successor * S ((S (S pa_i_bcomlfp_successor_power_product)) * pa_v_bcomlfp_successor_power_product) + (pa_s_bcomlfp_successor_power_product))) /\ pa_s_bcomlfp_successor_power_product = pa_r_bcomlfp_successor_power_product * pa_p_bcomlfp_successor_power_product))))))) - 0018
specialize pow_successor_compose 4 - 0019
specialize pow_successor_compose n - 0020
specialize pow_successor_compose q - 0021
specialize pow_successor_compose (q * 4) - 0022
apply pow_successor_compose - 0023
exact hpower - 0024
refl - 0025
have hstrong_all : ∀ n. ∀ c. ∀ q. CentralBinom(S n,c) → Pow(4,S n,q) → Le(2 · c,q)Exact native replay line
have hstrong_all : 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) - 0026
apply central_binom_strong_upper_of_laws - 0027
exact hpackage_left_left - 0028
exact hpackage_right - 0029
have hstrong : Le(2 · x,q · 4)Exact native replay line
have hstrong : exists bcf_le_gap_bcomlfp_strong. bcf_le_gap_bcomlfp_strong + (2 * x) = q * 4 - 0030
specialize hstrong_all n - 0031
specialize hstrong_all x - 0032
specialize hstrong_all (q * 4) - 0033
apply hstrong_all - 0034
exact hcentral_exists_witness - 0035
exact hsuccessor_power - 0036
have hleft : 2 * (m + m) = 4 * m - 0037
trans 2 * m + 2 * m - 0038
apply mul_add - 0039
trans 2 * (2 * m) - 0040
specialize two_mul_eq_add_self (2 * m) - 0041
symm - 0042
exact two_mul_eq_add_self - 0043
trans (2 * 2) * m - 0044
symm - 0045
apply mul_assoc - 0046
have htwo_two : 2 * 2 = 4 - 0047
norm_num - 0048
rewrite htwo_two - 0049
refl - 0050
have hright : q * 4 = 4 * q - 0051
apply mul_comm - 0052
rewrite hdouble at hstrong - 0053
rewrite hleft at hstrong - 0054
rewrite hright at hstrong - 0055
specialize mul_le_cancel_left_nonzero 4 - 0056
specialize mul_le_cancel_left_nonzero m - 0057
specialize mul_le_cancel_left_nonzero q - 0058
apply mul_le_cancel_left_nonzero - 0059
intro hfour_zero - 0060
apply PA1 - 0061
exact hfour_zero - 0062
exact hstrong