BT00U2 · Bertrand theorem

central_binom_four_weighted_of_recurrence

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

The fourth central binomial satisfies the compact weighted value.

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

(∀ x. ∀ y. ∀ z. CentralBinom(x,y) → CentralBinom(S x,z) → S x · z = 2 · S (x + x) · y) → (∀ x. ∃ y. CentralBinom(x,y)) → ∀ x. CentralBinom(4,x) → 4 · x = 2 · S (3 + 3) · 20

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

PD0042 CentralBinom

4 occurrences

In local proof propositions

PD0042 CentralBinom

4 occurrences

Exact expanded native-PA statement
(forall n a b. (((exists bcf_lt_gap_bcb4we_recurrence_predecessor_out_of_range. bcf_lt_gap_bcb4we_recurrence_predecessor_out_of_range + S (n + n) = n) /\ a = 0) \/ ((exists bcf_le_gap_bcb4we_recurrence_predecessor_in_range. bcf_le_gap_bcb4we_recurrence_predecessor_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcb4we_recurrence_predecessor bcf_row_code_scale_bcb4we_recurrence_predecessor bcf_row_scale_code_bcb4we_recurrence_predecessor bcf_row_scale_scale_bcb4we_recurrence_predecessor bcf_row_code_bcb4we_recurrence_predecessor bcf_row_scale_bcb4we_recurrence_predecessor. ((forall bcf_row_index_bcb4we_recurrence_predecessor_table. (exists bcf_lt_gap_bcb4we_recurrence_predecessor_table_row_bound. bcf_lt_gap_bcb4we_recurrence_predecessor_table_row_bound + S (bcf_row_index_bcb4we_recurrence_predecessor_table) = S (n + n)) -> exists bcf_row_code_bcb4we_recurrence_predecessor_table bcf_row_scale_bcb4we_recurrence_predecessor_table. ((((exists bcf_height_bcb4we_recurrence_predecessor_table_decoded_row_code. bcf_height_bcb4we_recurrence_predecessor_table_decoded_row_code + S (bcf_row_code_bcb4we_recurrence_predecessor_table) = S ((S (bcf_row_index_bcb4we_recurrence_predecessor_table)) * bcf_row_code_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_row_code. bcf_row_code_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_recurrence_predecessor_table)) * bcf_row_code_scale_bcb4we_recurrence_predecessor) + (bcf_row_code_bcb4we_recurrence_predecessor_table))) /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_table_decoded_row_scale. bcf_height_bcb4we_recurrence_predecessor_table_decoded_row_scale + S (bcf_row_scale_bcb4we_recurrence_predecessor_table) = S ((S (bcf_row_index_bcb4we_recurrence_predecessor_table)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_row_scale. bcf_row_scale_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_recurrence_predecessor_table)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor) + (bcf_row_scale_bcb4we_recurrence_predecessor_table))) /\ ((bcf_row_index_bcb4we_recurrence_predecessor_table = 0 /\ (forall bcf_index_bcb4we_recurrence_predecessor_table_zero_row. (exists bcf_lt_gap_bcb4we_recurrence_predecessor_table_zero_row_bound. bcf_lt_gap_bcb4we_recurrence_predecessor_table_zero_row_bound + S (bcf_index_bcb4we_recurrence_predecessor_table_zero_row) = S (n + n)) -> exists bcf_value_bcb4we_recurrence_predecessor_table_zero_row. ((((exists bcf_height_bcb4we_recurrence_predecessor_table_zero_row_entry. bcf_height_bcb4we_recurrence_predecessor_table_zero_row_entry + S (bcf_value_bcb4we_recurrence_predecessor_table_zero_row) = S ((S (bcf_index_bcb4we_recurrence_predecessor_table_zero_row)) * bcf_row_scale_bcb4we_recurrence_predecessor_table)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_zero_row_entry. bcf_row_code_bcb4we_recurrence_predecessor_table = bcf_quotient_bcb4we_recurrence_predecessor_table_zero_row_entry * S ((S (bcf_index_bcb4we_recurrence_predecessor_table_zero_row)) * bcf_row_scale_bcb4we_recurrence_predecessor_table) + (bcf_value_bcb4we_recurrence_predecessor_table_zero_row))) /\ ((bcf_index_bcb4we_recurrence_predecessor_table_zero_row = 0 /\ bcf_value_bcb4we_recurrence_predecessor_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_recurrence_predecessor_table_zero_row. bcf_index_bcb4we_recurrence_predecessor_table_zero_row = S bcf_predecessor_bcb4we_recurrence_predecessor_table_zero_row /\ bcf_value_bcb4we_recurrence_predecessor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_recurrence_predecessor_table bcf_previous_code_bcb4we_recurrence_predecessor_table bcf_previous_scale_bcb4we_recurrence_predecessor_table. bcf_row_index_bcb4we_recurrence_predecessor_table = S bcf_predecessor_bcb4we_recurrence_predecessor_table /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_table_decoded_previous_code. bcf_height_bcb4we_recurrence_predecessor_table_decoded_previous_code + S (bcf_previous_code_bcb4we_recurrence_predecessor_table) = S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table)) * bcf_row_code_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_previous_code. bcf_row_code_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table)) * bcf_row_code_scale_bcb4we_recurrence_predecessor) + (bcf_previous_code_bcb4we_recurrence_predecessor_table))) /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_table_decoded_previous_scale. bcf_height_bcb4we_recurrence_predecessor_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_recurrence_predecessor_table) = S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor) + (bcf_previous_scale_bcb4we_recurrence_predecessor_table))) /\ (forall bcf_index_bcb4we_recurrence_predecessor_table_row_step. (exists bcf_lt_gap_bcb4we_recurrence_predecessor_table_row_step_bound. bcf_lt_gap_bcb4we_recurrence_predecessor_table_row_step_bound + S (bcf_index_bcb4we_recurrence_predecessor_table_row_step) = S (n + n)) -> exists bcf_value_bcb4we_recurrence_predecessor_table_row_step. ((((exists bcf_height_bcb4we_recurrence_predecessor_table_row_step_entry. bcf_height_bcb4we_recurrence_predecessor_table_row_step_entry + S (bcf_value_bcb4we_recurrence_predecessor_table_row_step) = S ((S (bcf_index_bcb4we_recurrence_predecessor_table_row_step)) * bcf_row_scale_bcb4we_recurrence_predecessor_table)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_entry. bcf_row_code_bcb4we_recurrence_predecessor_table = bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_entry * S ((S (bcf_index_bcb4we_recurrence_predecessor_table_row_step)) * bcf_row_scale_bcb4we_recurrence_predecessor_table) + (bcf_value_bcb4we_recurrence_predecessor_table_row_step))) /\ ((bcf_index_bcb4we_recurrence_predecessor_table_row_step = 0 /\ bcf_value_bcb4we_recurrence_predecessor_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step bcf_left_bcb4we_recurrence_predecessor_table_row_step bcf_right_bcb4we_recurrence_predecessor_table_row_step. bcf_index_bcb4we_recurrence_predecessor_table_row_step = S bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_table_row_step_previous_left. bcf_height_bcb4we_recurrence_predecessor_table_row_step_previous_left + S (bcf_left_bcb4we_recurrence_predecessor_table_row_step) = S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step)) * bcf_previous_scale_bcb4we_recurrence_predecessor_table)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_previous_left. bcf_previous_code_bcb4we_recurrence_predecessor_table = bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step)) * bcf_previous_scale_bcb4we_recurrence_predecessor_table) + (bcf_left_bcb4we_recurrence_predecessor_table_row_step))) /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_table_row_step_previous_right. bcf_height_bcb4we_recurrence_predecessor_table_row_step_previous_right + S (bcf_right_bcb4we_recurrence_predecessor_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step))) * bcf_previous_scale_bcb4we_recurrence_predecessor_table)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_previous_right. bcf_previous_code_bcb4we_recurrence_predecessor_table = bcf_quotient_bcb4we_recurrence_predecessor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_recurrence_predecessor_table_row_step))) * bcf_previous_scale_bcb4we_recurrence_predecessor_table) + (bcf_right_bcb4we_recurrence_predecessor_table_row_step))) /\ bcf_value_bcb4we_recurrence_predecessor_table_row_step = bcf_left_bcb4we_recurrence_predecessor_table_row_step + bcf_right_bcb4we_recurrence_predecessor_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_decoded_row_code. bcf_height_bcb4we_recurrence_predecessor_decoded_row_code + S (bcf_row_code_bcb4we_recurrence_predecessor) = S ((S (n + n)) * bcf_row_code_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_decoded_row_code. bcf_row_code_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcb4we_recurrence_predecessor) + (bcf_row_code_bcb4we_recurrence_predecessor))) /\ ((((exists bcf_height_bcb4we_recurrence_predecessor_decoded_row_scale. bcf_height_bcb4we_recurrence_predecessor_decoded_row_scale + S (bcf_row_scale_bcb4we_recurrence_predecessor) = S ((S (n + n)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_decoded_row_scale. bcf_row_scale_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcb4we_recurrence_predecessor) + (bcf_row_scale_bcb4we_recurrence_predecessor))) /\ (((exists bcf_height_bcb4we_recurrence_predecessor_decoded_value. bcf_height_bcb4we_recurrence_predecessor_decoded_value + S (a) = S ((S (n)) * bcf_row_scale_bcb4we_recurrence_predecessor)) /\ exists bcf_quotient_bcb4we_recurrence_predecessor_decoded_value. bcf_row_code_bcb4we_recurrence_predecessor = bcf_quotient_bcb4we_recurrence_predecessor_decoded_value * S ((S (n)) * bcf_row_scale_bcb4we_recurrence_predecessor) + (a))))))))) -> (((exists bcf_lt_gap_bcb4we_recurrence_successor_out_of_range. bcf_lt_gap_bcb4we_recurrence_successor_out_of_range + S (S n + S n) = S n) /\ b = 0) \/ ((exists bcf_le_gap_bcb4we_recurrence_successor_in_range. bcf_le_gap_bcb4we_recurrence_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcb4we_recurrence_successor bcf_row_code_scale_bcb4we_recurrence_successor bcf_row_scale_code_bcb4we_recurrence_successor bcf_row_scale_scale_bcb4we_recurrence_successor bcf_row_code_bcb4we_recurrence_successor bcf_row_scale_bcb4we_recurrence_successor. ((forall bcf_row_index_bcb4we_recurrence_successor_table. (exists bcf_lt_gap_bcb4we_recurrence_successor_table_row_bound. bcf_lt_gap_bcb4we_recurrence_successor_table_row_bound + S (bcf_row_index_bcb4we_recurrence_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcb4we_recurrence_successor_table bcf_row_scale_bcb4we_recurrence_successor_table. ((((exists bcf_height_bcb4we_recurrence_successor_table_decoded_row_code. bcf_height_bcb4we_recurrence_successor_table_decoded_row_code + S (bcf_row_code_bcb4we_recurrence_successor_table) = S ((S (bcf_row_index_bcb4we_recurrence_successor_table)) * bcf_row_code_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_decoded_row_code. bcf_row_code_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_recurrence_successor_table)) * bcf_row_code_scale_bcb4we_recurrence_successor) + (bcf_row_code_bcb4we_recurrence_successor_table))) /\ ((((exists bcf_height_bcb4we_recurrence_successor_table_decoded_row_scale. bcf_height_bcb4we_recurrence_successor_table_decoded_row_scale + S (bcf_row_scale_bcb4we_recurrence_successor_table) = S ((S (bcf_row_index_bcb4we_recurrence_successor_table)) * bcf_row_scale_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_decoded_row_scale. bcf_row_scale_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_recurrence_successor_table)) * bcf_row_scale_scale_bcb4we_recurrence_successor) + (bcf_row_scale_bcb4we_recurrence_successor_table))) /\ ((bcf_row_index_bcb4we_recurrence_successor_table = 0 /\ (forall bcf_index_bcb4we_recurrence_successor_table_zero_row. (exists bcf_lt_gap_bcb4we_recurrence_successor_table_zero_row_bound. bcf_lt_gap_bcb4we_recurrence_successor_table_zero_row_bound + S (bcf_index_bcb4we_recurrence_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcb4we_recurrence_successor_table_zero_row. ((((exists bcf_height_bcb4we_recurrence_successor_table_zero_row_entry. bcf_height_bcb4we_recurrence_successor_table_zero_row_entry + S (bcf_value_bcb4we_recurrence_successor_table_zero_row) = S ((S (bcf_index_bcb4we_recurrence_successor_table_zero_row)) * bcf_row_scale_bcb4we_recurrence_successor_table)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_zero_row_entry. bcf_row_code_bcb4we_recurrence_successor_table = bcf_quotient_bcb4we_recurrence_successor_table_zero_row_entry * S ((S (bcf_index_bcb4we_recurrence_successor_table_zero_row)) * bcf_row_scale_bcb4we_recurrence_successor_table) + (bcf_value_bcb4we_recurrence_successor_table_zero_row))) /\ ((bcf_index_bcb4we_recurrence_successor_table_zero_row = 0 /\ bcf_value_bcb4we_recurrence_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_recurrence_successor_table_zero_row. bcf_index_bcb4we_recurrence_successor_table_zero_row = S bcf_predecessor_bcb4we_recurrence_successor_table_zero_row /\ bcf_value_bcb4we_recurrence_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_recurrence_successor_table bcf_previous_code_bcb4we_recurrence_successor_table bcf_previous_scale_bcb4we_recurrence_successor_table. bcf_row_index_bcb4we_recurrence_successor_table = S bcf_predecessor_bcb4we_recurrence_successor_table /\ ((((exists bcf_height_bcb4we_recurrence_successor_table_decoded_previous_code. bcf_height_bcb4we_recurrence_successor_table_decoded_previous_code + S (bcf_previous_code_bcb4we_recurrence_successor_table) = S ((S (bcf_predecessor_bcb4we_recurrence_successor_table)) * bcf_row_code_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_decoded_previous_code. bcf_row_code_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_recurrence_successor_table)) * bcf_row_code_scale_bcb4we_recurrence_successor) + (bcf_previous_code_bcb4we_recurrence_successor_table))) /\ ((((exists bcf_height_bcb4we_recurrence_successor_table_decoded_previous_scale. bcf_height_bcb4we_recurrence_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_recurrence_successor_table) = S ((S (bcf_predecessor_bcb4we_recurrence_successor_table)) * bcf_row_scale_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_recurrence_successor_table)) * bcf_row_scale_scale_bcb4we_recurrence_successor) + (bcf_previous_scale_bcb4we_recurrence_successor_table))) /\ (forall bcf_index_bcb4we_recurrence_successor_table_row_step. (exists bcf_lt_gap_bcb4we_recurrence_successor_table_row_step_bound. bcf_lt_gap_bcb4we_recurrence_successor_table_row_step_bound + S (bcf_index_bcb4we_recurrence_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcb4we_recurrence_successor_table_row_step. ((((exists bcf_height_bcb4we_recurrence_successor_table_row_step_entry. bcf_height_bcb4we_recurrence_successor_table_row_step_entry + S (bcf_value_bcb4we_recurrence_successor_table_row_step) = S ((S (bcf_index_bcb4we_recurrence_successor_table_row_step)) * bcf_row_scale_bcb4we_recurrence_successor_table)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_row_step_entry. bcf_row_code_bcb4we_recurrence_successor_table = bcf_quotient_bcb4we_recurrence_successor_table_row_step_entry * S ((S (bcf_index_bcb4we_recurrence_successor_table_row_step)) * bcf_row_scale_bcb4we_recurrence_successor_table) + (bcf_value_bcb4we_recurrence_successor_table_row_step))) /\ ((bcf_index_bcb4we_recurrence_successor_table_row_step = 0 /\ bcf_value_bcb4we_recurrence_successor_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_recurrence_successor_table_row_step bcf_left_bcb4we_recurrence_successor_table_row_step bcf_right_bcb4we_recurrence_successor_table_row_step. bcf_index_bcb4we_recurrence_successor_table_row_step = S bcf_predecessor_bcb4we_recurrence_successor_table_row_step /\ ((((exists bcf_height_bcb4we_recurrence_successor_table_row_step_previous_left. bcf_height_bcb4we_recurrence_successor_table_row_step_previous_left + S (bcf_left_bcb4we_recurrence_successor_table_row_step) = S ((S (bcf_predecessor_bcb4we_recurrence_successor_table_row_step)) * bcf_previous_scale_bcb4we_recurrence_successor_table)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_row_step_previous_left. bcf_previous_code_bcb4we_recurrence_successor_table = bcf_quotient_bcb4we_recurrence_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_recurrence_successor_table_row_step)) * bcf_previous_scale_bcb4we_recurrence_successor_table) + (bcf_left_bcb4we_recurrence_successor_table_row_step))) /\ ((((exists bcf_height_bcb4we_recurrence_successor_table_row_step_previous_right. bcf_height_bcb4we_recurrence_successor_table_row_step_previous_right + S (bcf_right_bcb4we_recurrence_successor_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_recurrence_successor_table_row_step))) * bcf_previous_scale_bcb4we_recurrence_successor_table)) /\ exists bcf_quotient_bcb4we_recurrence_successor_table_row_step_previous_right. bcf_previous_code_bcb4we_recurrence_successor_table = bcf_quotient_bcb4we_recurrence_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_recurrence_successor_table_row_step))) * bcf_previous_scale_bcb4we_recurrence_successor_table) + (bcf_right_bcb4we_recurrence_successor_table_row_step))) /\ bcf_value_bcb4we_recurrence_successor_table_row_step = bcf_left_bcb4we_recurrence_successor_table_row_step + bcf_right_bcb4we_recurrence_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_recurrence_successor_decoded_row_code. bcf_height_bcb4we_recurrence_successor_decoded_row_code + S (bcf_row_code_bcb4we_recurrence_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_decoded_row_code. bcf_row_code_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcb4we_recurrence_successor) + (bcf_row_code_bcb4we_recurrence_successor))) /\ ((((exists bcf_height_bcb4we_recurrence_successor_decoded_row_scale. bcf_height_bcb4we_recurrence_successor_decoded_row_scale + S (bcf_row_scale_bcb4we_recurrence_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_decoded_row_scale. bcf_row_scale_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcb4we_recurrence_successor) + (bcf_row_scale_bcb4we_recurrence_successor))) /\ (((exists bcf_height_bcb4we_recurrence_successor_decoded_value. bcf_height_bcb4we_recurrence_successor_decoded_value + S (b) = S ((S (S n)) * bcf_row_scale_bcb4we_recurrence_successor)) /\ exists bcf_quotient_bcb4we_recurrence_successor_decoded_value. bcf_row_code_bcb4we_recurrence_successor = bcf_quotient_bcb4we_recurrence_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcb4we_recurrence_successor) + (b))))))))) -> S n * b = (2 * S (n + n)) * a) -> (forall n. exists z. (((exists bcf_lt_gap_bcb4we_exists_out_of_range. bcf_lt_gap_bcb4we_exists_out_of_range + S (n + n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bcb4we_exists_in_range. bcf_le_gap_bcb4we_exists_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcb4we_exists bcf_row_code_scale_bcb4we_exists bcf_row_scale_code_bcb4we_exists bcf_row_scale_scale_bcb4we_exists bcf_row_code_bcb4we_exists bcf_row_scale_bcb4we_exists. ((forall bcf_row_index_bcb4we_exists_table. (exists bcf_lt_gap_bcb4we_exists_table_row_bound. bcf_lt_gap_bcb4we_exists_table_row_bound + S (bcf_row_index_bcb4we_exists_table) = S (n + n)) -> exists bcf_row_code_bcb4we_exists_table bcf_row_scale_bcb4we_exists_table. ((((exists bcf_height_bcb4we_exists_table_decoded_row_code. bcf_height_bcb4we_exists_table_decoded_row_code + S (bcf_row_code_bcb4we_exists_table) = S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_row_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists) + (bcf_row_code_bcb4we_exists_table))) /\ ((((exists bcf_height_bcb4we_exists_table_decoded_row_scale. bcf_height_bcb4we_exists_table_decoded_row_scale + S (bcf_row_scale_bcb4we_exists_table) = S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_row_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_row_scale_bcb4we_exists_table))) /\ ((bcf_row_index_bcb4we_exists_table = 0 /\ (forall bcf_index_bcb4we_exists_table_zero_row. (exists bcf_lt_gap_bcb4we_exists_table_zero_row_bound. bcf_lt_gap_bcb4we_exists_table_zero_row_bound + S (bcf_index_bcb4we_exists_table_zero_row) = S (n + n)) -> exists bcf_value_bcb4we_exists_table_zero_row. ((((exists bcf_height_bcb4we_exists_table_zero_row_entry. bcf_height_bcb4we_exists_table_zero_row_entry + S (bcf_value_bcb4we_exists_table_zero_row) = S ((S (bcf_index_bcb4we_exists_table_zero_row)) * bcf_row_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_zero_row_entry. bcf_row_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_zero_row_entry * S ((S (bcf_index_bcb4we_exists_table_zero_row)) * bcf_row_scale_bcb4we_exists_table) + (bcf_value_bcb4we_exists_table_zero_row))) /\ ((bcf_index_bcb4we_exists_table_zero_row = 0 /\ bcf_value_bcb4we_exists_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_exists_table_zero_row. bcf_index_bcb4we_exists_table_zero_row = S bcf_predecessor_bcb4we_exists_table_zero_row /\ bcf_value_bcb4we_exists_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_exists_table bcf_previous_code_bcb4we_exists_table bcf_previous_scale_bcb4we_exists_table. bcf_row_index_bcb4we_exists_table = S bcf_predecessor_bcb4we_exists_table /\ ((((exists bcf_height_bcb4we_exists_table_decoded_previous_code. bcf_height_bcb4we_exists_table_decoded_previous_code + S (bcf_previous_code_bcb4we_exists_table) = S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_previous_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists) + (bcf_previous_code_bcb4we_exists_table))) /\ ((((exists bcf_height_bcb4we_exists_table_decoded_previous_scale. bcf_height_bcb4we_exists_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_exists_table) = S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_previous_scale_bcb4we_exists_table))) /\ (forall bcf_index_bcb4we_exists_table_row_step. (exists bcf_lt_gap_bcb4we_exists_table_row_step_bound. bcf_lt_gap_bcb4we_exists_table_row_step_bound + S (bcf_index_bcb4we_exists_table_row_step) = S (n + n)) -> exists bcf_value_bcb4we_exists_table_row_step. ((((exists bcf_height_bcb4we_exists_table_row_step_entry. bcf_height_bcb4we_exists_table_row_step_entry + S (bcf_value_bcb4we_exists_table_row_step) = S ((S (bcf_index_bcb4we_exists_table_row_step)) * bcf_row_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_entry. bcf_row_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_entry * S ((S (bcf_index_bcb4we_exists_table_row_step)) * bcf_row_scale_bcb4we_exists_table) + (bcf_value_bcb4we_exists_table_row_step))) /\ ((bcf_index_bcb4we_exists_table_row_step = 0 /\ bcf_value_bcb4we_exists_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_exists_table_row_step bcf_left_bcb4we_exists_table_row_step bcf_right_bcb4we_exists_table_row_step. bcf_index_bcb4we_exists_table_row_step = S bcf_predecessor_bcb4we_exists_table_row_step /\ ((((exists bcf_height_bcb4we_exists_table_row_step_previous_left. bcf_height_bcb4we_exists_table_row_step_previous_left + S (bcf_left_bcb4we_exists_table_row_step) = S ((S (bcf_predecessor_bcb4we_exists_table_row_step)) * bcf_previous_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_previous_left. bcf_previous_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_exists_table_row_step)) * bcf_previous_scale_bcb4we_exists_table) + (bcf_left_bcb4we_exists_table_row_step))) /\ ((((exists bcf_height_bcb4we_exists_table_row_step_previous_right. bcf_height_bcb4we_exists_table_row_step_previous_right + S (bcf_right_bcb4we_exists_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_exists_table_row_step))) * bcf_previous_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_previous_right. bcf_previous_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_exists_table_row_step))) * bcf_previous_scale_bcb4we_exists_table) + (bcf_right_bcb4we_exists_table_row_step))) /\ bcf_value_bcb4we_exists_table_row_step = bcf_left_bcb4we_exists_table_row_step + bcf_right_bcb4we_exists_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_exists_decoded_row_code. bcf_height_bcb4we_exists_decoded_row_code + S (bcf_row_code_bcb4we_exists) = S ((S (n + n)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_row_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcb4we_exists) + (bcf_row_code_bcb4we_exists))) /\ ((((exists bcf_height_bcb4we_exists_decoded_row_scale. bcf_height_bcb4we_exists_decoded_row_scale + S (bcf_row_scale_bcb4we_exists) = S ((S (n + n)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_row_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_row_scale_bcb4we_exists))) /\ (((exists bcf_height_bcb4we_exists_decoded_value. bcf_height_bcb4we_exists_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_value. bcf_row_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_value * S ((S (n)) * bcf_row_scale_bcb4we_exists) + (z)))))))))) -> forall c. (((exists bcf_lt_gap_bcb4we_source_out_of_range. bcf_lt_gap_bcb4we_source_out_of_range + S (4 + 4) = 4) /\ c = 0) \/ ((exists bcf_le_gap_bcb4we_source_in_range. bcf_le_gap_bcb4we_source_in_range + (4) = 4 + 4) /\ (exists bcf_row_code_code_bcb4we_source bcf_row_code_scale_bcb4we_source bcf_row_scale_code_bcb4we_source bcf_row_scale_scale_bcb4we_source bcf_row_code_bcb4we_source bcf_row_scale_bcb4we_source. ((forall bcf_row_index_bcb4we_source_table. (exists bcf_lt_gap_bcb4we_source_table_row_bound. bcf_lt_gap_bcb4we_source_table_row_bound + S (bcf_row_index_bcb4we_source_table) = S (4 + 4)) -> exists bcf_row_code_bcb4we_source_table bcf_row_scale_bcb4we_source_table. ((((exists bcf_height_bcb4we_source_table_decoded_row_code. bcf_height_bcb4we_source_table_decoded_row_code + S (bcf_row_code_bcb4we_source_table) = S ((S (bcf_row_index_bcb4we_source_table)) * bcf_row_code_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_table_decoded_row_code. bcf_row_code_code_bcb4we_source = bcf_quotient_bcb4we_source_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_source_table)) * bcf_row_code_scale_bcb4we_source) + (bcf_row_code_bcb4we_source_table))) /\ ((((exists bcf_height_bcb4we_source_table_decoded_row_scale. bcf_height_bcb4we_source_table_decoded_row_scale + S (bcf_row_scale_bcb4we_source_table) = S ((S (bcf_row_index_bcb4we_source_table)) * bcf_row_scale_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_table_decoded_row_scale. bcf_row_scale_code_bcb4we_source = bcf_quotient_bcb4we_source_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_source_table)) * bcf_row_scale_scale_bcb4we_source) + (bcf_row_scale_bcb4we_source_table))) /\ ((bcf_row_index_bcb4we_source_table = 0 /\ (forall bcf_index_bcb4we_source_table_zero_row. (exists bcf_lt_gap_bcb4we_source_table_zero_row_bound. bcf_lt_gap_bcb4we_source_table_zero_row_bound + S (bcf_index_bcb4we_source_table_zero_row) = S (4 + 4)) -> exists bcf_value_bcb4we_source_table_zero_row. ((((exists bcf_height_bcb4we_source_table_zero_row_entry. bcf_height_bcb4we_source_table_zero_row_entry + S (bcf_value_bcb4we_source_table_zero_row) = S ((S (bcf_index_bcb4we_source_table_zero_row)) * bcf_row_scale_bcb4we_source_table)) /\ exists bcf_quotient_bcb4we_source_table_zero_row_entry. bcf_row_code_bcb4we_source_table = bcf_quotient_bcb4we_source_table_zero_row_entry * S ((S (bcf_index_bcb4we_source_table_zero_row)) * bcf_row_scale_bcb4we_source_table) + (bcf_value_bcb4we_source_table_zero_row))) /\ ((bcf_index_bcb4we_source_table_zero_row = 0 /\ bcf_value_bcb4we_source_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_source_table_zero_row. bcf_index_bcb4we_source_table_zero_row = S bcf_predecessor_bcb4we_source_table_zero_row /\ bcf_value_bcb4we_source_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_source_table bcf_previous_code_bcb4we_source_table bcf_previous_scale_bcb4we_source_table. bcf_row_index_bcb4we_source_table = S bcf_predecessor_bcb4we_source_table /\ ((((exists bcf_height_bcb4we_source_table_decoded_previous_code. bcf_height_bcb4we_source_table_decoded_previous_code + S (bcf_previous_code_bcb4we_source_table) = S ((S (bcf_predecessor_bcb4we_source_table)) * bcf_row_code_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_table_decoded_previous_code. bcf_row_code_code_bcb4we_source = bcf_quotient_bcb4we_source_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_source_table)) * bcf_row_code_scale_bcb4we_source) + (bcf_previous_code_bcb4we_source_table))) /\ ((((exists bcf_height_bcb4we_source_table_decoded_previous_scale. bcf_height_bcb4we_source_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_source_table) = S ((S (bcf_predecessor_bcb4we_source_table)) * bcf_row_scale_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_source = bcf_quotient_bcb4we_source_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_source_table)) * bcf_row_scale_scale_bcb4we_source) + (bcf_previous_scale_bcb4we_source_table))) /\ (forall bcf_index_bcb4we_source_table_row_step. (exists bcf_lt_gap_bcb4we_source_table_row_step_bound. bcf_lt_gap_bcb4we_source_table_row_step_bound + S (bcf_index_bcb4we_source_table_row_step) = S (4 + 4)) -> exists bcf_value_bcb4we_source_table_row_step. ((((exists bcf_height_bcb4we_source_table_row_step_entry. bcf_height_bcb4we_source_table_row_step_entry + S (bcf_value_bcb4we_source_table_row_step) = S ((S (bcf_index_bcb4we_source_table_row_step)) * bcf_row_scale_bcb4we_source_table)) /\ exists bcf_quotient_bcb4we_source_table_row_step_entry. bcf_row_code_bcb4we_source_table = bcf_quotient_bcb4we_source_table_row_step_entry * S ((S (bcf_index_bcb4we_source_table_row_step)) * bcf_row_scale_bcb4we_source_table) + (bcf_value_bcb4we_source_table_row_step))) /\ ((bcf_index_bcb4we_source_table_row_step = 0 /\ bcf_value_bcb4we_source_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_source_table_row_step bcf_left_bcb4we_source_table_row_step bcf_right_bcb4we_source_table_row_step. bcf_index_bcb4we_source_table_row_step = S bcf_predecessor_bcb4we_source_table_row_step /\ ((((exists bcf_height_bcb4we_source_table_row_step_previous_left. bcf_height_bcb4we_source_table_row_step_previous_left + S (bcf_left_bcb4we_source_table_row_step) = S ((S (bcf_predecessor_bcb4we_source_table_row_step)) * bcf_previous_scale_bcb4we_source_table)) /\ exists bcf_quotient_bcb4we_source_table_row_step_previous_left. bcf_previous_code_bcb4we_source_table = bcf_quotient_bcb4we_source_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_source_table_row_step)) * bcf_previous_scale_bcb4we_source_table) + (bcf_left_bcb4we_source_table_row_step))) /\ ((((exists bcf_height_bcb4we_source_table_row_step_previous_right. bcf_height_bcb4we_source_table_row_step_previous_right + S (bcf_right_bcb4we_source_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_source_table_row_step))) * bcf_previous_scale_bcb4we_source_table)) /\ exists bcf_quotient_bcb4we_source_table_row_step_previous_right. bcf_previous_code_bcb4we_source_table = bcf_quotient_bcb4we_source_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_source_table_row_step))) * bcf_previous_scale_bcb4we_source_table) + (bcf_right_bcb4we_source_table_row_step))) /\ bcf_value_bcb4we_source_table_row_step = bcf_left_bcb4we_source_table_row_step + bcf_right_bcb4we_source_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_source_decoded_row_code. bcf_height_bcb4we_source_decoded_row_code + S (bcf_row_code_bcb4we_source) = S ((S (4 + 4)) * bcf_row_code_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_decoded_row_code. bcf_row_code_code_bcb4we_source = bcf_quotient_bcb4we_source_decoded_row_code * S ((S (4 + 4)) * bcf_row_code_scale_bcb4we_source) + (bcf_row_code_bcb4we_source))) /\ ((((exists bcf_height_bcb4we_source_decoded_row_scale. bcf_height_bcb4we_source_decoded_row_scale + S (bcf_row_scale_bcb4we_source) = S ((S (4 + 4)) * bcf_row_scale_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_decoded_row_scale. bcf_row_scale_code_bcb4we_source = bcf_quotient_bcb4we_source_decoded_row_scale * S ((S (4 + 4)) * bcf_row_scale_scale_bcb4we_source) + (bcf_row_scale_bcb4we_source))) /\ (((exists bcf_height_bcb4we_source_decoded_value. bcf_height_bcb4we_source_decoded_value + S (c) = S ((S (4)) * bcf_row_scale_bcb4we_source)) /\ exists bcf_quotient_bcb4we_source_decoded_value. bcf_row_code_bcb4we_source = bcf_quotient_bcb4we_source_decoded_value * S ((S (4)) * bcf_row_scale_bcb4we_source) + (c))))))))) -> 4 * c = (2 * S (3 + 3)) * 20

Proof neighborhood

Direct theorem prerequisites

BT0009 one_mul BT0022 mul_left_cancel_nonzero BT00TQ central_binom_zero

Direct theorem dependents

BT00U3 four_pow_central_seed_package

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

67 script commands · 20 reading checkpoints · 15 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
one mulmul left cancel nonzerocentral binom zero
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro hrecurrence
  2. L2
    intro hcentral_exists
  3. L3
    intro c
  4. L4
    intro hcentral
02Establish hzero_existsL5–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcentral exists.

  1. L5
    have hzero_exists : ∃ a. CentralBinom(0,a)Definitions: CentralBinom(0,a)Original native command in the exact edition
  2. L6
    apply hcentral_exists
03Separate the logical casesL7–7

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

  1. L7
    cases hzero_exists
04Establish hone_existsL8–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcentral exists.

  1. L8
    have hone_exists : ∃ a. CentralBinom(1,a)Definitions: CentralBinom(1,a)Original native command in the exact edition
  2. L9
    apply hcentral_exists
05Separate the logical casesL10–10

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

  1. L10
    cases hone_exists
06Establish htwo_existsL11–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcentral exists.

  1. L11
    have htwo_exists : ∃ a. CentralBinom(2,a)Definitions: CentralBinom(2,a)Original native command in the exact edition
  2. L12
    apply hcentral_exists
07Separate the logical casesL13–13

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

  1. L13
    cases htwo_exists
08Establish hthree_existsL14–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcentral exists.

  1. L14
    have hthree_exists : ∃ a. CentralBinom(3,a)Definitions: CentralBinom(3,a)Original native command in the exact edition
  2. L15
    apply hcentral_exists
09Separate the logical casesL16–16

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

  1. L16
    cases hthree_exists
10Establish hzero_valueL17–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom zero.

  1. L17
    have hzero_value : x = 1
  2. L18
    apply central_binom_zero
  3. L19
    exact hzero_exists_witness
11Establish hrecurrence_zeroL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrecurrence.

  1. L20
    have hrecurrence_zero : S 0 * x1 = (2 * S (0 + 0)) * x
  2. L21
    apply hrecurrence
  3. L22
    exact hzero_exists_witness
  4. L23
    exact hone_exists_witness
  5. L24
    rewrite hzero_value at hrecurrence_zero
  6. L25
    specialize one_mul x1
  7. L26
    rewrite one_mul at hrecurrence_zero
12Establish hzero_rhsL27–29

Establish this local claim before using it. It is not an additional assumption.

  1. L27
    have hzero_rhs : (2 * S (0 + 0)) * 1 = 2
  2. L28
    norm_num
  3. L29
    rewrite hzero_rhs at hrecurrence_zero
13Establish hone_valueL30–31

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hone_value : x1 = 2
  2. L31
    exact hrecurrence_zero
14Establish hrecurrence_oneL32–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrecurrence.

  1. L32
    have hrecurrence_one : S 1 * x2 = (2 * S (1 + 1)) * x1
  2. L33
    apply hrecurrence
  3. L34
    exact hone_exists_witness
  4. L35
    exact htwo_exists_witness
  5. L36
    rewrite hone_value at hrecurrence_one
15Establish hone_rhsL37–39

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hone_rhs : (2 * S (1 + 1)) * 2 = 2 * 6
  2. L38
    norm_num
  3. L39
    rewrite hone_rhs at hrecurrence_one
16Establish htwo_valueL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L40
    have htwo_value : x2 = 6
  2. L41
    specialize mul_left_cancel_nonzero 2
  3. L42
    apply mul_left_cancel_nonzero
  4. L43
    intro htwo_zero
  5. L44
    apply PA1
  6. L45
    exact htwo_zero
  7. L46
    exact hrecurrence_one
17Establish hrecurrence_twoL47–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrecurrence.

  1. L47
    have hrecurrence_two : S 2 * x3 = (2 * S (2 + 2)) * x2
  2. L48
    apply hrecurrence
  3. L49
    exact htwo_exists_witness
  4. L50
    exact hthree_exists_witness
  5. L51
    rewrite htwo_value at hrecurrence_two
18Establish htwo_rhsL52–54

Establish this local claim before using it. It is not an additional assumption.

  1. L52
    have htwo_rhs : (2 * S (2 + 2)) * 6 = 3 * 20
  2. L53
    norm_num
  3. L54
    rewrite htwo_rhs at hrecurrence_two
19Establish hthree_valueL55–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L55
    have hthree_value : x3 = 20
  2. L56
    specialize mul_left_cancel_nonzero 3
  3. L57
    apply mul_left_cancel_nonzero
  4. L58
    intro hthree_zero
  5. L59
    apply PA1
  6. L60
    exact hthree_zero
  7. L61
    exact hrecurrence_two
20Establish hrecurrence_threeL62–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrecurrence.

  1. L62
    have hrecurrence_three : S 3 * c = (2 * S (3 + 3)) * x3
  2. L63
    apply hrecurrence
  3. L64
    exact hthree_exists_witness
  4. L65
    exact hcentral
  5. L66
    rewrite hthree_value at hrecurrence_three
  6. L67
    exact hrecurrence_three

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro hrecurrence
  2. 0002intro hcentral_exists
  3. 0003intro c
  4. 0004intro hcentral
  5. 0005have hzero_exists : ∃ a. CentralBinom(0,a)
    Exact native replay linehave hzero_exists : exists a. (((exists bcf_lt_gap_bcb4we_zero_out_of_range. bcf_lt_gap_bcb4we_zero_out_of_range + S (0 + 0) = 0) /\ a = 0) \/ ((exists bcf_le_gap_bcb4we_zero_in_range. bcf_le_gap_bcb4we_zero_in_range + (0) = 0 + 0) /\ (exists bcf_row_code_code_bcb4we_zero bcf_row_code_scale_bcb4we_zero bcf_row_scale_code_bcb4we_zero bcf_row_scale_scale_bcb4we_zero bcf_row_code_bcb4we_zero bcf_row_scale_bcb4we_zero. ((forall bcf_row_index_bcb4we_zero_table. (exists bcf_lt_gap_bcb4we_zero_table_row_bound. bcf_lt_gap_bcb4we_zero_table_row_bound + S (bcf_row_index_bcb4we_zero_table) = S (0 + 0)) -> exists bcf_row_code_bcb4we_zero_table bcf_row_scale_bcb4we_zero_table. ((((exists bcf_height_bcb4we_zero_table_decoded_row_code. bcf_height_bcb4we_zero_table_decoded_row_code + S (bcf_row_code_bcb4we_zero_table) = S ((S (bcf_row_index_bcb4we_zero_table)) * bcf_row_code_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_table_decoded_row_code. bcf_row_code_code_bcb4we_zero = bcf_quotient_bcb4we_zero_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_zero_table)) * bcf_row_code_scale_bcb4we_zero) + (bcf_row_code_bcb4we_zero_table))) /\ ((((exists bcf_height_bcb4we_zero_table_decoded_row_scale. bcf_height_bcb4we_zero_table_decoded_row_scale + S (bcf_row_scale_bcb4we_zero_table) = S ((S (bcf_row_index_bcb4we_zero_table)) * bcf_row_scale_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_table_decoded_row_scale. bcf_row_scale_code_bcb4we_zero = bcf_quotient_bcb4we_zero_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_zero_table)) * bcf_row_scale_scale_bcb4we_zero) + (bcf_row_scale_bcb4we_zero_table))) /\ ((bcf_row_index_bcb4we_zero_table = 0 /\ (forall bcf_index_bcb4we_zero_table_zero_row. (exists bcf_lt_gap_bcb4we_zero_table_zero_row_bound. bcf_lt_gap_bcb4we_zero_table_zero_row_bound + S (bcf_index_bcb4we_zero_table_zero_row) = S (0 + 0)) -> exists bcf_value_bcb4we_zero_table_zero_row. ((((exists bcf_height_bcb4we_zero_table_zero_row_entry. bcf_height_bcb4we_zero_table_zero_row_entry + S (bcf_value_bcb4we_zero_table_zero_row) = S ((S (bcf_index_bcb4we_zero_table_zero_row)) * bcf_row_scale_bcb4we_zero_table)) /\ exists bcf_quotient_bcb4we_zero_table_zero_row_entry. bcf_row_code_bcb4we_zero_table = bcf_quotient_bcb4we_zero_table_zero_row_entry * S ((S (bcf_index_bcb4we_zero_table_zero_row)) * bcf_row_scale_bcb4we_zero_table) + (bcf_value_bcb4we_zero_table_zero_row))) /\ ((bcf_index_bcb4we_zero_table_zero_row = 0 /\ bcf_value_bcb4we_zero_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_zero_table_zero_row. bcf_index_bcb4we_zero_table_zero_row = S bcf_predecessor_bcb4we_zero_table_zero_row /\ bcf_value_bcb4we_zero_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_zero_table bcf_previous_code_bcb4we_zero_table bcf_previous_scale_bcb4we_zero_table. bcf_row_index_bcb4we_zero_table = S bcf_predecessor_bcb4we_zero_table /\ ((((exists bcf_height_bcb4we_zero_table_decoded_previous_code. bcf_height_bcb4we_zero_table_decoded_previous_code + S (bcf_previous_code_bcb4we_zero_table) = S ((S (bcf_predecessor_bcb4we_zero_table)) * bcf_row_code_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_table_decoded_previous_code. bcf_row_code_code_bcb4we_zero = bcf_quotient_bcb4we_zero_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_zero_table)) * bcf_row_code_scale_bcb4we_zero) + (bcf_previous_code_bcb4we_zero_table))) /\ ((((exists bcf_height_bcb4we_zero_table_decoded_previous_scale. bcf_height_bcb4we_zero_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_zero_table) = S ((S (bcf_predecessor_bcb4we_zero_table)) * bcf_row_scale_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_zero = bcf_quotient_bcb4we_zero_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_zero_table)) * bcf_row_scale_scale_bcb4we_zero) + (bcf_previous_scale_bcb4we_zero_table))) /\ (forall bcf_index_bcb4we_zero_table_row_step. (exists bcf_lt_gap_bcb4we_zero_table_row_step_bound. bcf_lt_gap_bcb4we_zero_table_row_step_bound + S (bcf_index_bcb4we_zero_table_row_step) = S (0 + 0)) -> exists bcf_value_bcb4we_zero_table_row_step. ((((exists bcf_height_bcb4we_zero_table_row_step_entry. bcf_height_bcb4we_zero_table_row_step_entry + S (bcf_value_bcb4we_zero_table_row_step) = S ((S (bcf_index_bcb4we_zero_table_row_step)) * bcf_row_scale_bcb4we_zero_table)) /\ exists bcf_quotient_bcb4we_zero_table_row_step_entry. bcf_row_code_bcb4we_zero_table = bcf_quotient_bcb4we_zero_table_row_step_entry * S ((S (bcf_index_bcb4we_zero_table_row_step)) * bcf_row_scale_bcb4we_zero_table) + (bcf_value_bcb4we_zero_table_row_step))) /\ ((bcf_index_bcb4we_zero_table_row_step = 0 /\ bcf_value_bcb4we_zero_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_zero_table_row_step bcf_left_bcb4we_zero_table_row_step bcf_right_bcb4we_zero_table_row_step. bcf_index_bcb4we_zero_table_row_step = S bcf_predecessor_bcb4we_zero_table_row_step /\ ((((exists bcf_height_bcb4we_zero_table_row_step_previous_left. bcf_height_bcb4we_zero_table_row_step_previous_left + S (bcf_left_bcb4we_zero_table_row_step) = S ((S (bcf_predecessor_bcb4we_zero_table_row_step)) * bcf_previous_scale_bcb4we_zero_table)) /\ exists bcf_quotient_bcb4we_zero_table_row_step_previous_left. bcf_previous_code_bcb4we_zero_table = bcf_quotient_bcb4we_zero_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_zero_table_row_step)) * bcf_previous_scale_bcb4we_zero_table) + (bcf_left_bcb4we_zero_table_row_step))) /\ ((((exists bcf_height_bcb4we_zero_table_row_step_previous_right. bcf_height_bcb4we_zero_table_row_step_previous_right + S (bcf_right_bcb4we_zero_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_zero_table_row_step))) * bcf_previous_scale_bcb4we_zero_table)) /\ exists bcf_quotient_bcb4we_zero_table_row_step_previous_right. bcf_previous_code_bcb4we_zero_table = bcf_quotient_bcb4we_zero_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_zero_table_row_step))) * bcf_previous_scale_bcb4we_zero_table) + (bcf_right_bcb4we_zero_table_row_step))) /\ bcf_value_bcb4we_zero_table_row_step = bcf_left_bcb4we_zero_table_row_step + bcf_right_bcb4we_zero_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_zero_decoded_row_code. bcf_height_bcb4we_zero_decoded_row_code + S (bcf_row_code_bcb4we_zero) = S ((S (0 + 0)) * bcf_row_code_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_decoded_row_code. bcf_row_code_code_bcb4we_zero = bcf_quotient_bcb4we_zero_decoded_row_code * S ((S (0 + 0)) * bcf_row_code_scale_bcb4we_zero) + (bcf_row_code_bcb4we_zero))) /\ ((((exists bcf_height_bcb4we_zero_decoded_row_scale. bcf_height_bcb4we_zero_decoded_row_scale + S (bcf_row_scale_bcb4we_zero) = S ((S (0 + 0)) * bcf_row_scale_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_decoded_row_scale. bcf_row_scale_code_bcb4we_zero = bcf_quotient_bcb4we_zero_decoded_row_scale * S ((S (0 + 0)) * bcf_row_scale_scale_bcb4we_zero) + (bcf_row_scale_bcb4we_zero))) /\ (((exists bcf_height_bcb4we_zero_decoded_value. bcf_height_bcb4we_zero_decoded_value + S (a) = S ((S (0)) * bcf_row_scale_bcb4we_zero)) /\ exists bcf_quotient_bcb4we_zero_decoded_value. bcf_row_code_bcb4we_zero = bcf_quotient_bcb4we_zero_decoded_value * S ((S (0)) * bcf_row_scale_bcb4we_zero) + (a)))))))))
  6. 0006apply hcentral_exists
  7. 0007cases hzero_exists
  8. 0008have hone_exists : ∃ a. CentralBinom(1,a)
    Exact native replay linehave hone_exists : exists a. (((exists bcf_lt_gap_bcb4we_one_out_of_range. bcf_lt_gap_bcb4we_one_out_of_range + S (1 + 1) = 1) /\ a = 0) \/ ((exists bcf_le_gap_bcb4we_one_in_range. bcf_le_gap_bcb4we_one_in_range + (1) = 1 + 1) /\ (exists bcf_row_code_code_bcb4we_one bcf_row_code_scale_bcb4we_one bcf_row_scale_code_bcb4we_one bcf_row_scale_scale_bcb4we_one bcf_row_code_bcb4we_one bcf_row_scale_bcb4we_one. ((forall bcf_row_index_bcb4we_one_table. (exists bcf_lt_gap_bcb4we_one_table_row_bound. bcf_lt_gap_bcb4we_one_table_row_bound + S (bcf_row_index_bcb4we_one_table) = S (1 + 1)) -> exists bcf_row_code_bcb4we_one_table bcf_row_scale_bcb4we_one_table. ((((exists bcf_height_bcb4we_one_table_decoded_row_code. bcf_height_bcb4we_one_table_decoded_row_code + S (bcf_row_code_bcb4we_one_table) = S ((S (bcf_row_index_bcb4we_one_table)) * bcf_row_code_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_table_decoded_row_code. bcf_row_code_code_bcb4we_one = bcf_quotient_bcb4we_one_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_one_table)) * bcf_row_code_scale_bcb4we_one) + (bcf_row_code_bcb4we_one_table))) /\ ((((exists bcf_height_bcb4we_one_table_decoded_row_scale. bcf_height_bcb4we_one_table_decoded_row_scale + S (bcf_row_scale_bcb4we_one_table) = S ((S (bcf_row_index_bcb4we_one_table)) * bcf_row_scale_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_table_decoded_row_scale. bcf_row_scale_code_bcb4we_one = bcf_quotient_bcb4we_one_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_one_table)) * bcf_row_scale_scale_bcb4we_one) + (bcf_row_scale_bcb4we_one_table))) /\ ((bcf_row_index_bcb4we_one_table = 0 /\ (forall bcf_index_bcb4we_one_table_zero_row. (exists bcf_lt_gap_bcb4we_one_table_zero_row_bound. bcf_lt_gap_bcb4we_one_table_zero_row_bound + S (bcf_index_bcb4we_one_table_zero_row) = S (1 + 1)) -> exists bcf_value_bcb4we_one_table_zero_row. ((((exists bcf_height_bcb4we_one_table_zero_row_entry. bcf_height_bcb4we_one_table_zero_row_entry + S (bcf_value_bcb4we_one_table_zero_row) = S ((S (bcf_index_bcb4we_one_table_zero_row)) * bcf_row_scale_bcb4we_one_table)) /\ exists bcf_quotient_bcb4we_one_table_zero_row_entry. bcf_row_code_bcb4we_one_table = bcf_quotient_bcb4we_one_table_zero_row_entry * S ((S (bcf_index_bcb4we_one_table_zero_row)) * bcf_row_scale_bcb4we_one_table) + (bcf_value_bcb4we_one_table_zero_row))) /\ ((bcf_index_bcb4we_one_table_zero_row = 0 /\ bcf_value_bcb4we_one_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_one_table_zero_row. bcf_index_bcb4we_one_table_zero_row = S bcf_predecessor_bcb4we_one_table_zero_row /\ bcf_value_bcb4we_one_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_one_table bcf_previous_code_bcb4we_one_table bcf_previous_scale_bcb4we_one_table. bcf_row_index_bcb4we_one_table = S bcf_predecessor_bcb4we_one_table /\ ((((exists bcf_height_bcb4we_one_table_decoded_previous_code. bcf_height_bcb4we_one_table_decoded_previous_code + S (bcf_previous_code_bcb4we_one_table) = S ((S (bcf_predecessor_bcb4we_one_table)) * bcf_row_code_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_table_decoded_previous_code. bcf_row_code_code_bcb4we_one = bcf_quotient_bcb4we_one_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_one_table)) * bcf_row_code_scale_bcb4we_one) + (bcf_previous_code_bcb4we_one_table))) /\ ((((exists bcf_height_bcb4we_one_table_decoded_previous_scale. bcf_height_bcb4we_one_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_one_table) = S ((S (bcf_predecessor_bcb4we_one_table)) * bcf_row_scale_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_one = bcf_quotient_bcb4we_one_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_one_table)) * bcf_row_scale_scale_bcb4we_one) + (bcf_previous_scale_bcb4we_one_table))) /\ (forall bcf_index_bcb4we_one_table_row_step. (exists bcf_lt_gap_bcb4we_one_table_row_step_bound. bcf_lt_gap_bcb4we_one_table_row_step_bound + S (bcf_index_bcb4we_one_table_row_step) = S (1 + 1)) -> exists bcf_value_bcb4we_one_table_row_step. ((((exists bcf_height_bcb4we_one_table_row_step_entry. bcf_height_bcb4we_one_table_row_step_entry + S (bcf_value_bcb4we_one_table_row_step) = S ((S (bcf_index_bcb4we_one_table_row_step)) * bcf_row_scale_bcb4we_one_table)) /\ exists bcf_quotient_bcb4we_one_table_row_step_entry. bcf_row_code_bcb4we_one_table = bcf_quotient_bcb4we_one_table_row_step_entry * S ((S (bcf_index_bcb4we_one_table_row_step)) * bcf_row_scale_bcb4we_one_table) + (bcf_value_bcb4we_one_table_row_step))) /\ ((bcf_index_bcb4we_one_table_row_step = 0 /\ bcf_value_bcb4we_one_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_one_table_row_step bcf_left_bcb4we_one_table_row_step bcf_right_bcb4we_one_table_row_step. bcf_index_bcb4we_one_table_row_step = S bcf_predecessor_bcb4we_one_table_row_step /\ ((((exists bcf_height_bcb4we_one_table_row_step_previous_left. bcf_height_bcb4we_one_table_row_step_previous_left + S (bcf_left_bcb4we_one_table_row_step) = S ((S (bcf_predecessor_bcb4we_one_table_row_step)) * bcf_previous_scale_bcb4we_one_table)) /\ exists bcf_quotient_bcb4we_one_table_row_step_previous_left. bcf_previous_code_bcb4we_one_table = bcf_quotient_bcb4we_one_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_one_table_row_step)) * bcf_previous_scale_bcb4we_one_table) + (bcf_left_bcb4we_one_table_row_step))) /\ ((((exists bcf_height_bcb4we_one_table_row_step_previous_right. bcf_height_bcb4we_one_table_row_step_previous_right + S (bcf_right_bcb4we_one_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_one_table_row_step))) * bcf_previous_scale_bcb4we_one_table)) /\ exists bcf_quotient_bcb4we_one_table_row_step_previous_right. bcf_previous_code_bcb4we_one_table = bcf_quotient_bcb4we_one_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_one_table_row_step))) * bcf_previous_scale_bcb4we_one_table) + (bcf_right_bcb4we_one_table_row_step))) /\ bcf_value_bcb4we_one_table_row_step = bcf_left_bcb4we_one_table_row_step + bcf_right_bcb4we_one_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_one_decoded_row_code. bcf_height_bcb4we_one_decoded_row_code + S (bcf_row_code_bcb4we_one) = S ((S (1 + 1)) * bcf_row_code_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_decoded_row_code. bcf_row_code_code_bcb4we_one = bcf_quotient_bcb4we_one_decoded_row_code * S ((S (1 + 1)) * bcf_row_code_scale_bcb4we_one) + (bcf_row_code_bcb4we_one))) /\ ((((exists bcf_height_bcb4we_one_decoded_row_scale. bcf_height_bcb4we_one_decoded_row_scale + S (bcf_row_scale_bcb4we_one) = S ((S (1 + 1)) * bcf_row_scale_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_decoded_row_scale. bcf_row_scale_code_bcb4we_one = bcf_quotient_bcb4we_one_decoded_row_scale * S ((S (1 + 1)) * bcf_row_scale_scale_bcb4we_one) + (bcf_row_scale_bcb4we_one))) /\ (((exists bcf_height_bcb4we_one_decoded_value. bcf_height_bcb4we_one_decoded_value + S (a) = S ((S (1)) * bcf_row_scale_bcb4we_one)) /\ exists bcf_quotient_bcb4we_one_decoded_value. bcf_row_code_bcb4we_one = bcf_quotient_bcb4we_one_decoded_value * S ((S (1)) * bcf_row_scale_bcb4we_one) + (a)))))))))
  9. 0009apply hcentral_exists
  10. 0010cases hone_exists
  11. 0011have htwo_exists : ∃ a. CentralBinom(2,a)
    Exact native replay linehave htwo_exists : exists a. (((exists bcf_lt_gap_bcb4we_two_out_of_range. bcf_lt_gap_bcb4we_two_out_of_range + S (2 + 2) = 2) /\ a = 0) \/ ((exists bcf_le_gap_bcb4we_two_in_range. bcf_le_gap_bcb4we_two_in_range + (2) = 2 + 2) /\ (exists bcf_row_code_code_bcb4we_two bcf_row_code_scale_bcb4we_two bcf_row_scale_code_bcb4we_two bcf_row_scale_scale_bcb4we_two bcf_row_code_bcb4we_two bcf_row_scale_bcb4we_two. ((forall bcf_row_index_bcb4we_two_table. (exists bcf_lt_gap_bcb4we_two_table_row_bound. bcf_lt_gap_bcb4we_two_table_row_bound + S (bcf_row_index_bcb4we_two_table) = S (2 + 2)) -> exists bcf_row_code_bcb4we_two_table bcf_row_scale_bcb4we_two_table. ((((exists bcf_height_bcb4we_two_table_decoded_row_code. bcf_height_bcb4we_two_table_decoded_row_code + S (bcf_row_code_bcb4we_two_table) = S ((S (bcf_row_index_bcb4we_two_table)) * bcf_row_code_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_table_decoded_row_code. bcf_row_code_code_bcb4we_two = bcf_quotient_bcb4we_two_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_two_table)) * bcf_row_code_scale_bcb4we_two) + (bcf_row_code_bcb4we_two_table))) /\ ((((exists bcf_height_bcb4we_two_table_decoded_row_scale. bcf_height_bcb4we_two_table_decoded_row_scale + S (bcf_row_scale_bcb4we_two_table) = S ((S (bcf_row_index_bcb4we_two_table)) * bcf_row_scale_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_table_decoded_row_scale. bcf_row_scale_code_bcb4we_two = bcf_quotient_bcb4we_two_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_two_table)) * bcf_row_scale_scale_bcb4we_two) + (bcf_row_scale_bcb4we_two_table))) /\ ((bcf_row_index_bcb4we_two_table = 0 /\ (forall bcf_index_bcb4we_two_table_zero_row. (exists bcf_lt_gap_bcb4we_two_table_zero_row_bound. bcf_lt_gap_bcb4we_two_table_zero_row_bound + S (bcf_index_bcb4we_two_table_zero_row) = S (2 + 2)) -> exists bcf_value_bcb4we_two_table_zero_row. ((((exists bcf_height_bcb4we_two_table_zero_row_entry. bcf_height_bcb4we_two_table_zero_row_entry + S (bcf_value_bcb4we_two_table_zero_row) = S ((S (bcf_index_bcb4we_two_table_zero_row)) * bcf_row_scale_bcb4we_two_table)) /\ exists bcf_quotient_bcb4we_two_table_zero_row_entry. bcf_row_code_bcb4we_two_table = bcf_quotient_bcb4we_two_table_zero_row_entry * S ((S (bcf_index_bcb4we_two_table_zero_row)) * bcf_row_scale_bcb4we_two_table) + (bcf_value_bcb4we_two_table_zero_row))) /\ ((bcf_index_bcb4we_two_table_zero_row = 0 /\ bcf_value_bcb4we_two_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_two_table_zero_row. bcf_index_bcb4we_two_table_zero_row = S bcf_predecessor_bcb4we_two_table_zero_row /\ bcf_value_bcb4we_two_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_two_table bcf_previous_code_bcb4we_two_table bcf_previous_scale_bcb4we_two_table. bcf_row_index_bcb4we_two_table = S bcf_predecessor_bcb4we_two_table /\ ((((exists bcf_height_bcb4we_two_table_decoded_previous_code. bcf_height_bcb4we_two_table_decoded_previous_code + S (bcf_previous_code_bcb4we_two_table) = S ((S (bcf_predecessor_bcb4we_two_table)) * bcf_row_code_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_table_decoded_previous_code. bcf_row_code_code_bcb4we_two = bcf_quotient_bcb4we_two_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_two_table)) * bcf_row_code_scale_bcb4we_two) + (bcf_previous_code_bcb4we_two_table))) /\ ((((exists bcf_height_bcb4we_two_table_decoded_previous_scale. bcf_height_bcb4we_two_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_two_table) = S ((S (bcf_predecessor_bcb4we_two_table)) * bcf_row_scale_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_two = bcf_quotient_bcb4we_two_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_two_table)) * bcf_row_scale_scale_bcb4we_two) + (bcf_previous_scale_bcb4we_two_table))) /\ (forall bcf_index_bcb4we_two_table_row_step. (exists bcf_lt_gap_bcb4we_two_table_row_step_bound. bcf_lt_gap_bcb4we_two_table_row_step_bound + S (bcf_index_bcb4we_two_table_row_step) = S (2 + 2)) -> exists bcf_value_bcb4we_two_table_row_step. ((((exists bcf_height_bcb4we_two_table_row_step_entry. bcf_height_bcb4we_two_table_row_step_entry + S (bcf_value_bcb4we_two_table_row_step) = S ((S (bcf_index_bcb4we_two_table_row_step)) * bcf_row_scale_bcb4we_two_table)) /\ exists bcf_quotient_bcb4we_two_table_row_step_entry. bcf_row_code_bcb4we_two_table = bcf_quotient_bcb4we_two_table_row_step_entry * S ((S (bcf_index_bcb4we_two_table_row_step)) * bcf_row_scale_bcb4we_two_table) + (bcf_value_bcb4we_two_table_row_step))) /\ ((bcf_index_bcb4we_two_table_row_step = 0 /\ bcf_value_bcb4we_two_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_two_table_row_step bcf_left_bcb4we_two_table_row_step bcf_right_bcb4we_two_table_row_step. bcf_index_bcb4we_two_table_row_step = S bcf_predecessor_bcb4we_two_table_row_step /\ ((((exists bcf_height_bcb4we_two_table_row_step_previous_left. bcf_height_bcb4we_two_table_row_step_previous_left + S (bcf_left_bcb4we_two_table_row_step) = S ((S (bcf_predecessor_bcb4we_two_table_row_step)) * bcf_previous_scale_bcb4we_two_table)) /\ exists bcf_quotient_bcb4we_two_table_row_step_previous_left. bcf_previous_code_bcb4we_two_table = bcf_quotient_bcb4we_two_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_two_table_row_step)) * bcf_previous_scale_bcb4we_two_table) + (bcf_left_bcb4we_two_table_row_step))) /\ ((((exists bcf_height_bcb4we_two_table_row_step_previous_right. bcf_height_bcb4we_two_table_row_step_previous_right + S (bcf_right_bcb4we_two_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_two_table_row_step))) * bcf_previous_scale_bcb4we_two_table)) /\ exists bcf_quotient_bcb4we_two_table_row_step_previous_right. bcf_previous_code_bcb4we_two_table = bcf_quotient_bcb4we_two_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_two_table_row_step))) * bcf_previous_scale_bcb4we_two_table) + (bcf_right_bcb4we_two_table_row_step))) /\ bcf_value_bcb4we_two_table_row_step = bcf_left_bcb4we_two_table_row_step + bcf_right_bcb4we_two_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_two_decoded_row_code. bcf_height_bcb4we_two_decoded_row_code + S (bcf_row_code_bcb4we_two) = S ((S (2 + 2)) * bcf_row_code_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_decoded_row_code. bcf_row_code_code_bcb4we_two = bcf_quotient_bcb4we_two_decoded_row_code * S ((S (2 + 2)) * bcf_row_code_scale_bcb4we_two) + (bcf_row_code_bcb4we_two))) /\ ((((exists bcf_height_bcb4we_two_decoded_row_scale. bcf_height_bcb4we_two_decoded_row_scale + S (bcf_row_scale_bcb4we_two) = S ((S (2 + 2)) * bcf_row_scale_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_decoded_row_scale. bcf_row_scale_code_bcb4we_two = bcf_quotient_bcb4we_two_decoded_row_scale * S ((S (2 + 2)) * bcf_row_scale_scale_bcb4we_two) + (bcf_row_scale_bcb4we_two))) /\ (((exists bcf_height_bcb4we_two_decoded_value. bcf_height_bcb4we_two_decoded_value + S (a) = S ((S (2)) * bcf_row_scale_bcb4we_two)) /\ exists bcf_quotient_bcb4we_two_decoded_value. bcf_row_code_bcb4we_two = bcf_quotient_bcb4we_two_decoded_value * S ((S (2)) * bcf_row_scale_bcb4we_two) + (a)))))))))
  12. 0012apply hcentral_exists
  13. 0013cases htwo_exists
  14. 0014have hthree_exists : ∃ a. CentralBinom(3,a)
    Exact native replay linehave hthree_exists : exists a. (((exists bcf_lt_gap_bcb4we_three_out_of_range. bcf_lt_gap_bcb4we_three_out_of_range + S (3 + 3) = 3) /\ a = 0) \/ ((exists bcf_le_gap_bcb4we_three_in_range. bcf_le_gap_bcb4we_three_in_range + (3) = 3 + 3) /\ (exists bcf_row_code_code_bcb4we_three bcf_row_code_scale_bcb4we_three bcf_row_scale_code_bcb4we_three bcf_row_scale_scale_bcb4we_three bcf_row_code_bcb4we_three bcf_row_scale_bcb4we_three. ((forall bcf_row_index_bcb4we_three_table. (exists bcf_lt_gap_bcb4we_three_table_row_bound. bcf_lt_gap_bcb4we_three_table_row_bound + S (bcf_row_index_bcb4we_three_table) = S (3 + 3)) -> exists bcf_row_code_bcb4we_three_table bcf_row_scale_bcb4we_three_table. ((((exists bcf_height_bcb4we_three_table_decoded_row_code. bcf_height_bcb4we_three_table_decoded_row_code + S (bcf_row_code_bcb4we_three_table) = S ((S (bcf_row_index_bcb4we_three_table)) * bcf_row_code_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_table_decoded_row_code. bcf_row_code_code_bcb4we_three = bcf_quotient_bcb4we_three_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_three_table)) * bcf_row_code_scale_bcb4we_three) + (bcf_row_code_bcb4we_three_table))) /\ ((((exists bcf_height_bcb4we_three_table_decoded_row_scale. bcf_height_bcb4we_three_table_decoded_row_scale + S (bcf_row_scale_bcb4we_three_table) = S ((S (bcf_row_index_bcb4we_three_table)) * bcf_row_scale_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_table_decoded_row_scale. bcf_row_scale_code_bcb4we_three = bcf_quotient_bcb4we_three_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_three_table)) * bcf_row_scale_scale_bcb4we_three) + (bcf_row_scale_bcb4we_three_table))) /\ ((bcf_row_index_bcb4we_three_table = 0 /\ (forall bcf_index_bcb4we_three_table_zero_row. (exists bcf_lt_gap_bcb4we_three_table_zero_row_bound. bcf_lt_gap_bcb4we_three_table_zero_row_bound + S (bcf_index_bcb4we_three_table_zero_row) = S (3 + 3)) -> exists bcf_value_bcb4we_three_table_zero_row. ((((exists bcf_height_bcb4we_three_table_zero_row_entry. bcf_height_bcb4we_three_table_zero_row_entry + S (bcf_value_bcb4we_three_table_zero_row) = S ((S (bcf_index_bcb4we_three_table_zero_row)) * bcf_row_scale_bcb4we_three_table)) /\ exists bcf_quotient_bcb4we_three_table_zero_row_entry. bcf_row_code_bcb4we_three_table = bcf_quotient_bcb4we_three_table_zero_row_entry * S ((S (bcf_index_bcb4we_three_table_zero_row)) * bcf_row_scale_bcb4we_three_table) + (bcf_value_bcb4we_three_table_zero_row))) /\ ((bcf_index_bcb4we_three_table_zero_row = 0 /\ bcf_value_bcb4we_three_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_three_table_zero_row. bcf_index_bcb4we_three_table_zero_row = S bcf_predecessor_bcb4we_three_table_zero_row /\ bcf_value_bcb4we_three_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_three_table bcf_previous_code_bcb4we_three_table bcf_previous_scale_bcb4we_three_table. bcf_row_index_bcb4we_three_table = S bcf_predecessor_bcb4we_three_table /\ ((((exists bcf_height_bcb4we_three_table_decoded_previous_code. bcf_height_bcb4we_three_table_decoded_previous_code + S (bcf_previous_code_bcb4we_three_table) = S ((S (bcf_predecessor_bcb4we_three_table)) * bcf_row_code_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_table_decoded_previous_code. bcf_row_code_code_bcb4we_three = bcf_quotient_bcb4we_three_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_three_table)) * bcf_row_code_scale_bcb4we_three) + (bcf_previous_code_bcb4we_three_table))) /\ ((((exists bcf_height_bcb4we_three_table_decoded_previous_scale. bcf_height_bcb4we_three_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_three_table) = S ((S (bcf_predecessor_bcb4we_three_table)) * bcf_row_scale_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_three = bcf_quotient_bcb4we_three_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_three_table)) * bcf_row_scale_scale_bcb4we_three) + (bcf_previous_scale_bcb4we_three_table))) /\ (forall bcf_index_bcb4we_three_table_row_step. (exists bcf_lt_gap_bcb4we_three_table_row_step_bound. bcf_lt_gap_bcb4we_three_table_row_step_bound + S (bcf_index_bcb4we_three_table_row_step) = S (3 + 3)) -> exists bcf_value_bcb4we_three_table_row_step. ((((exists bcf_height_bcb4we_three_table_row_step_entry. bcf_height_bcb4we_three_table_row_step_entry + S (bcf_value_bcb4we_three_table_row_step) = S ((S (bcf_index_bcb4we_three_table_row_step)) * bcf_row_scale_bcb4we_three_table)) /\ exists bcf_quotient_bcb4we_three_table_row_step_entry. bcf_row_code_bcb4we_three_table = bcf_quotient_bcb4we_three_table_row_step_entry * S ((S (bcf_index_bcb4we_three_table_row_step)) * bcf_row_scale_bcb4we_three_table) + (bcf_value_bcb4we_three_table_row_step))) /\ ((bcf_index_bcb4we_three_table_row_step = 0 /\ bcf_value_bcb4we_three_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_three_table_row_step bcf_left_bcb4we_three_table_row_step bcf_right_bcb4we_three_table_row_step. bcf_index_bcb4we_three_table_row_step = S bcf_predecessor_bcb4we_three_table_row_step /\ ((((exists bcf_height_bcb4we_three_table_row_step_previous_left. bcf_height_bcb4we_three_table_row_step_previous_left + S (bcf_left_bcb4we_three_table_row_step) = S ((S (bcf_predecessor_bcb4we_three_table_row_step)) * bcf_previous_scale_bcb4we_three_table)) /\ exists bcf_quotient_bcb4we_three_table_row_step_previous_left. bcf_previous_code_bcb4we_three_table = bcf_quotient_bcb4we_three_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_three_table_row_step)) * bcf_previous_scale_bcb4we_three_table) + (bcf_left_bcb4we_three_table_row_step))) /\ ((((exists bcf_height_bcb4we_three_table_row_step_previous_right. bcf_height_bcb4we_three_table_row_step_previous_right + S (bcf_right_bcb4we_three_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_three_table_row_step))) * bcf_previous_scale_bcb4we_three_table)) /\ exists bcf_quotient_bcb4we_three_table_row_step_previous_right. bcf_previous_code_bcb4we_three_table = bcf_quotient_bcb4we_three_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_three_table_row_step))) * bcf_previous_scale_bcb4we_three_table) + (bcf_right_bcb4we_three_table_row_step))) /\ bcf_value_bcb4we_three_table_row_step = bcf_left_bcb4we_three_table_row_step + bcf_right_bcb4we_three_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_three_decoded_row_code. bcf_height_bcb4we_three_decoded_row_code + S (bcf_row_code_bcb4we_three) = S ((S (3 + 3)) * bcf_row_code_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_decoded_row_code. bcf_row_code_code_bcb4we_three = bcf_quotient_bcb4we_three_decoded_row_code * S ((S (3 + 3)) * bcf_row_code_scale_bcb4we_three) + (bcf_row_code_bcb4we_three))) /\ ((((exists bcf_height_bcb4we_three_decoded_row_scale. bcf_height_bcb4we_three_decoded_row_scale + S (bcf_row_scale_bcb4we_three) = S ((S (3 + 3)) * bcf_row_scale_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_decoded_row_scale. bcf_row_scale_code_bcb4we_three = bcf_quotient_bcb4we_three_decoded_row_scale * S ((S (3 + 3)) * bcf_row_scale_scale_bcb4we_three) + (bcf_row_scale_bcb4we_three))) /\ (((exists bcf_height_bcb4we_three_decoded_value. bcf_height_bcb4we_three_decoded_value + S (a) = S ((S (3)) * bcf_row_scale_bcb4we_three)) /\ exists bcf_quotient_bcb4we_three_decoded_value. bcf_row_code_bcb4we_three = bcf_quotient_bcb4we_three_decoded_value * S ((S (3)) * bcf_row_scale_bcb4we_three) + (a)))))))))
  15. 0015apply hcentral_exists
  16. 0016cases hthree_exists
  17. 0017have hzero_value : x = 1
  18. 0018apply central_binom_zero
  19. 0019exact hzero_exists_witness
  20. 0020have hrecurrence_zero : S 0 * x1 = (2 * S (0 + 0)) * x
  21. 0021apply hrecurrence
  22. 0022exact hzero_exists_witness
  23. 0023exact hone_exists_witness
  24. 0024rewrite hzero_value at hrecurrence_zero
  25. 0025specialize one_mul x1
  26. 0026rewrite one_mul at hrecurrence_zero
  27. 0027have hzero_rhs : (2 * S (0 + 0)) * 1 = 2
  28. 0028norm_num
  29. 0029rewrite hzero_rhs at hrecurrence_zero
  30. 0030have hone_value : x1 = 2
  31. 0031exact hrecurrence_zero
  32. 0032have hrecurrence_one : S 1 * x2 = (2 * S (1 + 1)) * x1
  33. 0033apply hrecurrence
  34. 0034exact hone_exists_witness
  35. 0035exact htwo_exists_witness
  36. 0036rewrite hone_value at hrecurrence_one
  37. 0037have hone_rhs : (2 * S (1 + 1)) * 2 = 2 * 6
  38. 0038norm_num
  39. 0039rewrite hone_rhs at hrecurrence_one
  40. 0040have htwo_value : x2 = 6
  41. 0041specialize mul_left_cancel_nonzero 2
  42. 0042apply mul_left_cancel_nonzero
  43. 0043intro htwo_zero
  44. 0044apply PA1
  45. 0045exact htwo_zero
  46. 0046exact hrecurrence_one
  47. 0047have hrecurrence_two : S 2 * x3 = (2 * S (2 + 2)) * x2
  48. 0048apply hrecurrence
  49. 0049exact htwo_exists_witness
  50. 0050exact hthree_exists_witness
  51. 0051rewrite htwo_value at hrecurrence_two
  52. 0052have htwo_rhs : (2 * S (2 + 2)) * 6 = 3 * 20
  53. 0053norm_num
  54. 0054rewrite htwo_rhs at hrecurrence_two
  55. 0055have hthree_value : x3 = 20
  56. 0056specialize mul_left_cancel_nonzero 3
  57. 0057apply mul_left_cancel_nonzero
  58. 0058intro hthree_zero
  59. 0059apply PA1
  60. 0060exact hthree_zero
  61. 0061exact hrecurrence_two
  62. 0062have hrecurrence_three : S 3 * c = (2 * S (3 + 3)) * x3
  63. 0063apply hrecurrence
  64. 0064exact hthree_exists_witness
  65. 0065exact hcentral
  66. 0066rewrite hthree_value at hrecurrence_three
  67. 0067exact hrecurrence_three