Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ c. ∀ d. CentralBinom(n,c) → CentralBinom(S n,d) → S n · d = 2 · S (n + n) · cEvery 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
2 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall n c d. (((exists bcf_lt_gap_bcbsr_predecessor_out_of_range. bcf_lt_gap_bcbsr_predecessor_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bcbsr_predecessor_in_range. bcf_le_gap_bcbsr_predecessor_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcbsr_predecessor bcf_row_code_scale_bcbsr_predecessor bcf_row_scale_code_bcbsr_predecessor bcf_row_scale_scale_bcbsr_predecessor bcf_row_code_bcbsr_predecessor bcf_row_scale_bcbsr_predecessor. ((forall bcf_row_index_bcbsr_predecessor_table. (exists bcf_lt_gap_bcbsr_predecessor_table_row_bound. bcf_lt_gap_bcbsr_predecessor_table_row_bound + S (bcf_row_index_bcbsr_predecessor_table) = S (n + n)) -> exists bcf_row_code_bcbsr_predecessor_table bcf_row_scale_bcbsr_predecessor_table. ((((exists bcf_height_bcbsr_predecessor_table_decoded_row_code. bcf_height_bcbsr_predecessor_table_decoded_row_code + S (bcf_row_code_bcbsr_predecessor_table) = S ((S (bcf_row_index_bcbsr_predecessor_table)) * bcf_row_code_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_table_decoded_row_code. bcf_row_code_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_table_decoded_row_code * S ((S (bcf_row_index_bcbsr_predecessor_table)) * bcf_row_code_scale_bcbsr_predecessor) + (bcf_row_code_bcbsr_predecessor_table))) /\ ((((exists bcf_height_bcbsr_predecessor_table_decoded_row_scale. bcf_height_bcbsr_predecessor_table_decoded_row_scale + S (bcf_row_scale_bcbsr_predecessor_table) = S ((S (bcf_row_index_bcbsr_predecessor_table)) * bcf_row_scale_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_table_decoded_row_scale. bcf_row_scale_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_table_decoded_row_scale * S ((S (bcf_row_index_bcbsr_predecessor_table)) * bcf_row_scale_scale_bcbsr_predecessor) + (bcf_row_scale_bcbsr_predecessor_table))) /\ ((bcf_row_index_bcbsr_predecessor_table = 0 /\ (forall bcf_index_bcbsr_predecessor_table_zero_row. (exists bcf_lt_gap_bcbsr_predecessor_table_zero_row_bound. bcf_lt_gap_bcbsr_predecessor_table_zero_row_bound + S (bcf_index_bcbsr_predecessor_table_zero_row) = S (n + n)) -> exists bcf_value_bcbsr_predecessor_table_zero_row. ((((exists bcf_height_bcbsr_predecessor_table_zero_row_entry. bcf_height_bcbsr_predecessor_table_zero_row_entry + S (bcf_value_bcbsr_predecessor_table_zero_row) = S ((S (bcf_index_bcbsr_predecessor_table_zero_row)) * bcf_row_scale_bcbsr_predecessor_table)) /\ exists bcf_quotient_bcbsr_predecessor_table_zero_row_entry. bcf_row_code_bcbsr_predecessor_table = bcf_quotient_bcbsr_predecessor_table_zero_row_entry * S ((S (bcf_index_bcbsr_predecessor_table_zero_row)) * bcf_row_scale_bcbsr_predecessor_table) + (bcf_value_bcbsr_predecessor_table_zero_row))) /\ ((bcf_index_bcbsr_predecessor_table_zero_row = 0 /\ bcf_value_bcbsr_predecessor_table_zero_row = 1) \/ exists bcf_predecessor_bcbsr_predecessor_table_zero_row. bcf_index_bcbsr_predecessor_table_zero_row = S bcf_predecessor_bcbsr_predecessor_table_zero_row /\ bcf_value_bcbsr_predecessor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsr_predecessor_table bcf_previous_code_bcbsr_predecessor_table bcf_previous_scale_bcbsr_predecessor_table. bcf_row_index_bcbsr_predecessor_table = S bcf_predecessor_bcbsr_predecessor_table /\ ((((exists bcf_height_bcbsr_predecessor_table_decoded_previous_code. bcf_height_bcbsr_predecessor_table_decoded_previous_code + S (bcf_previous_code_bcbsr_predecessor_table) = S ((S (bcf_predecessor_bcbsr_predecessor_table)) * bcf_row_code_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_table_decoded_previous_code. bcf_row_code_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsr_predecessor_table)) * bcf_row_code_scale_bcbsr_predecessor) + (bcf_previous_code_bcbsr_predecessor_table))) /\ ((((exists bcf_height_bcbsr_predecessor_table_decoded_previous_scale. bcf_height_bcbsr_predecessor_table_decoded_previous_scale + S (bcf_previous_scale_bcbsr_predecessor_table) = S ((S (bcf_predecessor_bcbsr_predecessor_table)) * bcf_row_scale_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_table_decoded_previous_scale. bcf_row_scale_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsr_predecessor_table)) * bcf_row_scale_scale_bcbsr_predecessor) + (bcf_previous_scale_bcbsr_predecessor_table))) /\ (forall bcf_index_bcbsr_predecessor_table_row_step. (exists bcf_lt_gap_bcbsr_predecessor_table_row_step_bound. bcf_lt_gap_bcbsr_predecessor_table_row_step_bound + S (bcf_index_bcbsr_predecessor_table_row_step) = S (n + n)) -> exists bcf_value_bcbsr_predecessor_table_row_step. ((((exists bcf_height_bcbsr_predecessor_table_row_step_entry. bcf_height_bcbsr_predecessor_table_row_step_entry + S (bcf_value_bcbsr_predecessor_table_row_step) = S ((S (bcf_index_bcbsr_predecessor_table_row_step)) * bcf_row_scale_bcbsr_predecessor_table)) /\ exists bcf_quotient_bcbsr_predecessor_table_row_step_entry. bcf_row_code_bcbsr_predecessor_table = bcf_quotient_bcbsr_predecessor_table_row_step_entry * S ((S (bcf_index_bcbsr_predecessor_table_row_step)) * bcf_row_scale_bcbsr_predecessor_table) + (bcf_value_bcbsr_predecessor_table_row_step))) /\ ((bcf_index_bcbsr_predecessor_table_row_step = 0 /\ bcf_value_bcbsr_predecessor_table_row_step = 1) \/ exists bcf_predecessor_bcbsr_predecessor_table_row_step bcf_left_bcbsr_predecessor_table_row_step bcf_right_bcbsr_predecessor_table_row_step. bcf_index_bcbsr_predecessor_table_row_step = S bcf_predecessor_bcbsr_predecessor_table_row_step /\ ((((exists bcf_height_bcbsr_predecessor_table_row_step_previous_left. bcf_height_bcbsr_predecessor_table_row_step_previous_left + S (bcf_left_bcbsr_predecessor_table_row_step) = S ((S (bcf_predecessor_bcbsr_predecessor_table_row_step)) * bcf_previous_scale_bcbsr_predecessor_table)) /\ exists bcf_quotient_bcbsr_predecessor_table_row_step_previous_left. bcf_previous_code_bcbsr_predecessor_table = bcf_quotient_bcbsr_predecessor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsr_predecessor_table_row_step)) * bcf_previous_scale_bcbsr_predecessor_table) + (bcf_left_bcbsr_predecessor_table_row_step))) /\ ((((exists bcf_height_bcbsr_predecessor_table_row_step_previous_right. bcf_height_bcbsr_predecessor_table_row_step_previous_right + S (bcf_right_bcbsr_predecessor_table_row_step) = S ((S (S (bcf_predecessor_bcbsr_predecessor_table_row_step))) * bcf_previous_scale_bcbsr_predecessor_table)) /\ exists bcf_quotient_bcbsr_predecessor_table_row_step_previous_right. bcf_previous_code_bcbsr_predecessor_table = bcf_quotient_bcbsr_predecessor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsr_predecessor_table_row_step))) * bcf_previous_scale_bcbsr_predecessor_table) + (bcf_right_bcbsr_predecessor_table_row_step))) /\ bcf_value_bcbsr_predecessor_table_row_step = bcf_left_bcbsr_predecessor_table_row_step + bcf_right_bcbsr_predecessor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsr_predecessor_decoded_row_code. bcf_height_bcbsr_predecessor_decoded_row_code + S (bcf_row_code_bcbsr_predecessor) = S ((S (n + n)) * bcf_row_code_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_decoded_row_code. bcf_row_code_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcbsr_predecessor) + (bcf_row_code_bcbsr_predecessor))) /\ ((((exists bcf_height_bcbsr_predecessor_decoded_row_scale. bcf_height_bcbsr_predecessor_decoded_row_scale + S (bcf_row_scale_bcbsr_predecessor) = S ((S (n + n)) * bcf_row_scale_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_decoded_row_scale. bcf_row_scale_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcbsr_predecessor) + (bcf_row_scale_bcbsr_predecessor))) /\ (((exists bcf_height_bcbsr_predecessor_decoded_value. bcf_height_bcbsr_predecessor_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bcbsr_predecessor)) /\ exists bcf_quotient_bcbsr_predecessor_decoded_value. bcf_row_code_bcbsr_predecessor = bcf_quotient_bcbsr_predecessor_decoded_value * S ((S (n)) * bcf_row_scale_bcbsr_predecessor) + (c))))))))) -> (((exists bcf_lt_gap_bcbsr_successor_out_of_range. bcf_lt_gap_bcbsr_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbsr_successor_in_range. bcf_le_gap_bcbsr_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbsr_successor bcf_row_code_scale_bcbsr_successor bcf_row_scale_code_bcbsr_successor bcf_row_scale_scale_bcbsr_successor bcf_row_code_bcbsr_successor bcf_row_scale_bcbsr_successor. ((forall bcf_row_index_bcbsr_successor_table. (exists bcf_lt_gap_bcbsr_successor_table_row_bound. bcf_lt_gap_bcbsr_successor_table_row_bound + S (bcf_row_index_bcbsr_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbsr_successor_table bcf_row_scale_bcbsr_successor_table. ((((exists bcf_height_bcbsr_successor_table_decoded_row_code. bcf_height_bcbsr_successor_table_decoded_row_code + S (bcf_row_code_bcbsr_successor_table) = S ((S (bcf_row_index_bcbsr_successor_table)) * bcf_row_code_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_table_decoded_row_code. bcf_row_code_code_bcbsr_successor = bcf_quotient_bcbsr_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbsr_successor_table)) * bcf_row_code_scale_bcbsr_successor) + (bcf_row_code_bcbsr_successor_table))) /\ ((((exists bcf_height_bcbsr_successor_table_decoded_row_scale. bcf_height_bcbsr_successor_table_decoded_row_scale + S (bcf_row_scale_bcbsr_successor_table) = S ((S (bcf_row_index_bcbsr_successor_table)) * bcf_row_scale_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_table_decoded_row_scale. bcf_row_scale_code_bcbsr_successor = bcf_quotient_bcbsr_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbsr_successor_table)) * bcf_row_scale_scale_bcbsr_successor) + (bcf_row_scale_bcbsr_successor_table))) /\ ((bcf_row_index_bcbsr_successor_table = 0 /\ (forall bcf_index_bcbsr_successor_table_zero_row. (exists bcf_lt_gap_bcbsr_successor_table_zero_row_bound. bcf_lt_gap_bcbsr_successor_table_zero_row_bound + S (bcf_index_bcbsr_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbsr_successor_table_zero_row. ((((exists bcf_height_bcbsr_successor_table_zero_row_entry. bcf_height_bcbsr_successor_table_zero_row_entry + S (bcf_value_bcbsr_successor_table_zero_row) = S ((S (bcf_index_bcbsr_successor_table_zero_row)) * bcf_row_scale_bcbsr_successor_table)) /\ exists bcf_quotient_bcbsr_successor_table_zero_row_entry. bcf_row_code_bcbsr_successor_table = bcf_quotient_bcbsr_successor_table_zero_row_entry * S ((S (bcf_index_bcbsr_successor_table_zero_row)) * bcf_row_scale_bcbsr_successor_table) + (bcf_value_bcbsr_successor_table_zero_row))) /\ ((bcf_index_bcbsr_successor_table_zero_row = 0 /\ bcf_value_bcbsr_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbsr_successor_table_zero_row. bcf_index_bcbsr_successor_table_zero_row = S bcf_predecessor_bcbsr_successor_table_zero_row /\ bcf_value_bcbsr_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsr_successor_table bcf_previous_code_bcbsr_successor_table bcf_previous_scale_bcbsr_successor_table. bcf_row_index_bcbsr_successor_table = S bcf_predecessor_bcbsr_successor_table /\ ((((exists bcf_height_bcbsr_successor_table_decoded_previous_code. bcf_height_bcbsr_successor_table_decoded_previous_code + S (bcf_previous_code_bcbsr_successor_table) = S ((S (bcf_predecessor_bcbsr_successor_table)) * bcf_row_code_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_table_decoded_previous_code. bcf_row_code_code_bcbsr_successor = bcf_quotient_bcbsr_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsr_successor_table)) * bcf_row_code_scale_bcbsr_successor) + (bcf_previous_code_bcbsr_successor_table))) /\ ((((exists bcf_height_bcbsr_successor_table_decoded_previous_scale. bcf_height_bcbsr_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbsr_successor_table) = S ((S (bcf_predecessor_bcbsr_successor_table)) * bcf_row_scale_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbsr_successor = bcf_quotient_bcbsr_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsr_successor_table)) * bcf_row_scale_scale_bcbsr_successor) + (bcf_previous_scale_bcbsr_successor_table))) /\ (forall bcf_index_bcbsr_successor_table_row_step. (exists bcf_lt_gap_bcbsr_successor_table_row_step_bound. bcf_lt_gap_bcbsr_successor_table_row_step_bound + S (bcf_index_bcbsr_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbsr_successor_table_row_step. ((((exists bcf_height_bcbsr_successor_table_row_step_entry. bcf_height_bcbsr_successor_table_row_step_entry + S (bcf_value_bcbsr_successor_table_row_step) = S ((S (bcf_index_bcbsr_successor_table_row_step)) * bcf_row_scale_bcbsr_successor_table)) /\ exists bcf_quotient_bcbsr_successor_table_row_step_entry. bcf_row_code_bcbsr_successor_table = bcf_quotient_bcbsr_successor_table_row_step_entry * S ((S (bcf_index_bcbsr_successor_table_row_step)) * bcf_row_scale_bcbsr_successor_table) + (bcf_value_bcbsr_successor_table_row_step))) /\ ((bcf_index_bcbsr_successor_table_row_step = 0 /\ bcf_value_bcbsr_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbsr_successor_table_row_step bcf_left_bcbsr_successor_table_row_step bcf_right_bcbsr_successor_table_row_step. bcf_index_bcbsr_successor_table_row_step = S bcf_predecessor_bcbsr_successor_table_row_step /\ ((((exists bcf_height_bcbsr_successor_table_row_step_previous_left. bcf_height_bcbsr_successor_table_row_step_previous_left + S (bcf_left_bcbsr_successor_table_row_step) = S ((S (bcf_predecessor_bcbsr_successor_table_row_step)) * bcf_previous_scale_bcbsr_successor_table)) /\ exists bcf_quotient_bcbsr_successor_table_row_step_previous_left. bcf_previous_code_bcbsr_successor_table = bcf_quotient_bcbsr_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsr_successor_table_row_step)) * bcf_previous_scale_bcbsr_successor_table) + (bcf_left_bcbsr_successor_table_row_step))) /\ ((((exists bcf_height_bcbsr_successor_table_row_step_previous_right. bcf_height_bcbsr_successor_table_row_step_previous_right + S (bcf_right_bcbsr_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbsr_successor_table_row_step))) * bcf_previous_scale_bcbsr_successor_table)) /\ exists bcf_quotient_bcbsr_successor_table_row_step_previous_right. bcf_previous_code_bcbsr_successor_table = bcf_quotient_bcbsr_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsr_successor_table_row_step))) * bcf_previous_scale_bcbsr_successor_table) + (bcf_right_bcbsr_successor_table_row_step))) /\ bcf_value_bcbsr_successor_table_row_step = bcf_left_bcbsr_successor_table_row_step + bcf_right_bcbsr_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsr_successor_decoded_row_code. bcf_height_bcbsr_successor_decoded_row_code + S (bcf_row_code_bcbsr_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_decoded_row_code. bcf_row_code_code_bcbsr_successor = bcf_quotient_bcbsr_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbsr_successor) + (bcf_row_code_bcbsr_successor))) /\ ((((exists bcf_height_bcbsr_successor_decoded_row_scale. bcf_height_bcbsr_successor_decoded_row_scale + S (bcf_row_scale_bcbsr_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_decoded_row_scale. bcf_row_scale_code_bcbsr_successor = bcf_quotient_bcbsr_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbsr_successor) + (bcf_row_scale_bcbsr_successor))) /\ (((exists bcf_height_bcbsr_successor_decoded_value. bcf_height_bcbsr_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbsr_successor)) /\ exists bcf_quotient_bcbsr_successor_decoded_value. bcf_row_code_bcbsr_successor = bcf_quotient_bcbsr_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbsr_successor) + (d))))))))) -> S n * d = (2 * S (n + n)) * cProof neighborhood
Direct theorem prerequisites
BT0007 mul_add BT0008 mul_assoc BT00QU two_mul_eq_add_self BT00TS central_binom_succ_double_middle BT00TT choose_weighted_verticalDirect 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 (5)
01Fix variables and assumptionsL1–5
02Establish hmiddleL6–10
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom succ double middle.
- L6
have hmiddle : ∃ m. Choose(S (n + n),n,m) ∧ d = m + mDefinitions: Choose(S (n + n),n,m)Original native command in the exact edition - L7
specialize central_binom_succ_double_middle n - L8
specialize central_binom_succ_double_middle d - L9
apply central_binom_succ_double_middle - L10
exact hsuccessor
03Separate the logical casesL11–12
04Establish hweightedL13–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose weighted vertical.
- L13
have hweighted : S n * x = S (n + n) * c - L14
specialize choose_weighted_vertical (n + n) - L15
specialize choose_weighted_vertical n - L16
specialize choose_weighted_vertical n - L17
specialize choose_weighted_vertical c - L18
specialize choose_weighted_vertical x - L19
apply choose_weighted_vertical - L20
refl - L21
exact hpredecessor - L22
exact hmiddle_witness_left
05Calculate and transport equalitiesL23–24
06Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
apply mul_add
07Calculate and transport equalitiesL26–28
08Use earlier factsL29–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L29
specialize two_mul_eq_add_self (S (n + n) * c)
09Calculate and transport equalitiesL30–30
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L30
symm
10Use earlier factsL31–34
11Calculate and transport equalitiesL35–35
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L35
symm
12Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact mul_assoc
Original defined command ledger · 36 lines
- 0001
intro n - 0002
intro c - 0003
intro d - 0004
intro hpredecessor - 0005
intro hsuccessor - 0006
have hmiddle : ∃ m. Choose(S (n + n),n,m) ∧ d = m + mExact native replay line
have hmiddle : exists m. ((((exists bcf_lt_gap_bcbsr_middle_out_of_range. bcf_lt_gap_bcbsr_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbsr_middle_in_range. bcf_le_gap_bcbsr_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbsr_middle bcf_row_code_scale_bcbsr_middle bcf_row_scale_code_bcbsr_middle bcf_row_scale_scale_bcbsr_middle bcf_row_code_bcbsr_middle bcf_row_scale_bcbsr_middle. ((forall bcf_row_index_bcbsr_middle_table. (exists bcf_lt_gap_bcbsr_middle_table_row_bound. bcf_lt_gap_bcbsr_middle_table_row_bound + S (bcf_row_index_bcbsr_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbsr_middle_table bcf_row_scale_bcbsr_middle_table. ((((exists bcf_height_bcbsr_middle_table_decoded_row_code. bcf_height_bcbsr_middle_table_decoded_row_code + S (bcf_row_code_bcbsr_middle_table) = S ((S (bcf_row_index_bcbsr_middle_table)) * bcf_row_code_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_table_decoded_row_code. bcf_row_code_code_bcbsr_middle = bcf_quotient_bcbsr_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbsr_middle_table)) * bcf_row_code_scale_bcbsr_middle) + (bcf_row_code_bcbsr_middle_table))) /\ ((((exists bcf_height_bcbsr_middle_table_decoded_row_scale. bcf_height_bcbsr_middle_table_decoded_row_scale + S (bcf_row_scale_bcbsr_middle_table) = S ((S (bcf_row_index_bcbsr_middle_table)) * bcf_row_scale_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_table_decoded_row_scale. bcf_row_scale_code_bcbsr_middle = bcf_quotient_bcbsr_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbsr_middle_table)) * bcf_row_scale_scale_bcbsr_middle) + (bcf_row_scale_bcbsr_middle_table))) /\ ((bcf_row_index_bcbsr_middle_table = 0 /\ (forall bcf_index_bcbsr_middle_table_zero_row. (exists bcf_lt_gap_bcbsr_middle_table_zero_row_bound. bcf_lt_gap_bcbsr_middle_table_zero_row_bound + S (bcf_index_bcbsr_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbsr_middle_table_zero_row. ((((exists bcf_height_bcbsr_middle_table_zero_row_entry. bcf_height_bcbsr_middle_table_zero_row_entry + S (bcf_value_bcbsr_middle_table_zero_row) = S ((S (bcf_index_bcbsr_middle_table_zero_row)) * bcf_row_scale_bcbsr_middle_table)) /\ exists bcf_quotient_bcbsr_middle_table_zero_row_entry. bcf_row_code_bcbsr_middle_table = bcf_quotient_bcbsr_middle_table_zero_row_entry * S ((S (bcf_index_bcbsr_middle_table_zero_row)) * bcf_row_scale_bcbsr_middle_table) + (bcf_value_bcbsr_middle_table_zero_row))) /\ ((bcf_index_bcbsr_middle_table_zero_row = 0 /\ bcf_value_bcbsr_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbsr_middle_table_zero_row. bcf_index_bcbsr_middle_table_zero_row = S bcf_predecessor_bcbsr_middle_table_zero_row /\ bcf_value_bcbsr_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsr_middle_table bcf_previous_code_bcbsr_middle_table bcf_previous_scale_bcbsr_middle_table. bcf_row_index_bcbsr_middle_table = S bcf_predecessor_bcbsr_middle_table /\ ((((exists bcf_height_bcbsr_middle_table_decoded_previous_code. bcf_height_bcbsr_middle_table_decoded_previous_code + S (bcf_previous_code_bcbsr_middle_table) = S ((S (bcf_predecessor_bcbsr_middle_table)) * bcf_row_code_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_table_decoded_previous_code. bcf_row_code_code_bcbsr_middle = bcf_quotient_bcbsr_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsr_middle_table)) * bcf_row_code_scale_bcbsr_middle) + (bcf_previous_code_bcbsr_middle_table))) /\ ((((exists bcf_height_bcbsr_middle_table_decoded_previous_scale. bcf_height_bcbsr_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbsr_middle_table) = S ((S (bcf_predecessor_bcbsr_middle_table)) * bcf_row_scale_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbsr_middle = bcf_quotient_bcbsr_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsr_middle_table)) * bcf_row_scale_scale_bcbsr_middle) + (bcf_previous_scale_bcbsr_middle_table))) /\ (forall bcf_index_bcbsr_middle_table_row_step. (exists bcf_lt_gap_bcbsr_middle_table_row_step_bound. bcf_lt_gap_bcbsr_middle_table_row_step_bound + S (bcf_index_bcbsr_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbsr_middle_table_row_step. ((((exists bcf_height_bcbsr_middle_table_row_step_entry. bcf_height_bcbsr_middle_table_row_step_entry + S (bcf_value_bcbsr_middle_table_row_step) = S ((S (bcf_index_bcbsr_middle_table_row_step)) * bcf_row_scale_bcbsr_middle_table)) /\ exists bcf_quotient_bcbsr_middle_table_row_step_entry. bcf_row_code_bcbsr_middle_table = bcf_quotient_bcbsr_middle_table_row_step_entry * S ((S (bcf_index_bcbsr_middle_table_row_step)) * bcf_row_scale_bcbsr_middle_table) + (bcf_value_bcbsr_middle_table_row_step))) /\ ((bcf_index_bcbsr_middle_table_row_step = 0 /\ bcf_value_bcbsr_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbsr_middle_table_row_step bcf_left_bcbsr_middle_table_row_step bcf_right_bcbsr_middle_table_row_step. bcf_index_bcbsr_middle_table_row_step = S bcf_predecessor_bcbsr_middle_table_row_step /\ ((((exists bcf_height_bcbsr_middle_table_row_step_previous_left. bcf_height_bcbsr_middle_table_row_step_previous_left + S (bcf_left_bcbsr_middle_table_row_step) = S ((S (bcf_predecessor_bcbsr_middle_table_row_step)) * bcf_previous_scale_bcbsr_middle_table)) /\ exists bcf_quotient_bcbsr_middle_table_row_step_previous_left. bcf_previous_code_bcbsr_middle_table = bcf_quotient_bcbsr_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsr_middle_table_row_step)) * bcf_previous_scale_bcbsr_middle_table) + (bcf_left_bcbsr_middle_table_row_step))) /\ ((((exists bcf_height_bcbsr_middle_table_row_step_previous_right. bcf_height_bcbsr_middle_table_row_step_previous_right + S (bcf_right_bcbsr_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbsr_middle_table_row_step))) * bcf_previous_scale_bcbsr_middle_table)) /\ exists bcf_quotient_bcbsr_middle_table_row_step_previous_right. bcf_previous_code_bcbsr_middle_table = bcf_quotient_bcbsr_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsr_middle_table_row_step))) * bcf_previous_scale_bcbsr_middle_table) + (bcf_right_bcbsr_middle_table_row_step))) /\ bcf_value_bcbsr_middle_table_row_step = bcf_left_bcbsr_middle_table_row_step + bcf_right_bcbsr_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsr_middle_decoded_row_code. bcf_height_bcbsr_middle_decoded_row_code + S (bcf_row_code_bcbsr_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_decoded_row_code. bcf_row_code_code_bcbsr_middle = bcf_quotient_bcbsr_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbsr_middle) + (bcf_row_code_bcbsr_middle))) /\ ((((exists bcf_height_bcbsr_middle_decoded_row_scale. bcf_height_bcbsr_middle_decoded_row_scale + S (bcf_row_scale_bcbsr_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_decoded_row_scale. bcf_row_scale_code_bcbsr_middle = bcf_quotient_bcbsr_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbsr_middle) + (bcf_row_scale_bcbsr_middle))) /\ (((exists bcf_height_bcbsr_middle_decoded_value. bcf_height_bcbsr_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbsr_middle)) /\ exists bcf_quotient_bcbsr_middle_decoded_value. bcf_row_code_bcbsr_middle = bcf_quotient_bcbsr_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbsr_middle) + (m))))))))) /\ d = m + m) - 0007
specialize central_binom_succ_double_middle n - 0008
specialize central_binom_succ_double_middle d - 0009
apply central_binom_succ_double_middle - 0010
exact hsuccessor - 0011
cases hmiddle - 0012
cases hmiddle_witness - 0013
have hweighted : S n * x = S (n + n) * c - 0014
specialize choose_weighted_vertical (n + n) - 0015
specialize choose_weighted_vertical n - 0016
specialize choose_weighted_vertical n - 0017
specialize choose_weighted_vertical c - 0018
specialize choose_weighted_vertical x - 0019
apply choose_weighted_vertical - 0020
refl - 0021
exact hpredecessor - 0022
exact hmiddle_witness_left - 0023
rewrite hmiddle_witness_right - 0024
trans S n * x + S n * x - 0025
apply mul_add - 0026
rewrite hweighted - 0027
rewrite hweighted - 0028
trans 2 * (S (n + n) * c) - 0029
specialize two_mul_eq_add_self (S (n + n) * c) - 0030
symm - 0031
exact two_mul_eq_add_self - 0032
specialize mul_assoc 2 - 0033
specialize mul_assoc (S (n + n)) - 0034
specialize mul_assoc c - 0035
symm - 0036
exact mul_assoc