BT00VL

central_binom_recurrence_double_bundle

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

The recurrence and functional double-middle law share support.

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

Exact expanded PA statement

((forall n c d. (((exists bcf_lt_gap_bcbrdb_predecessor_out_of_range. bcf_lt_gap_bcbrdb_predecessor_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bcbrdb_predecessor_in_range. bcf_le_gap_bcbrdb_predecessor_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcbrdb_predecessor bcf_row_code_scale_bcbrdb_predecessor bcf_row_scale_code_bcbrdb_predecessor bcf_row_scale_scale_bcbrdb_predecessor bcf_row_code_bcbrdb_predecessor bcf_row_scale_bcbrdb_predecessor. ((forall bcf_row_index_bcbrdb_predecessor_table. (exists bcf_lt_gap_bcbrdb_predecessor_table_row_bound. bcf_lt_gap_bcbrdb_predecessor_table_row_bound + S (bcf_row_index_bcbrdb_predecessor_table) = S (n + n)) -> exists bcf_row_code_bcbrdb_predecessor_table bcf_row_scale_bcbrdb_predecessor_table. ((((exists bcf_height_bcbrdb_predecessor_table_decoded_row_code. bcf_height_bcbrdb_predecessor_table_decoded_row_code + S (bcf_row_code_bcbrdb_predecessor_table) = S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_row_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_row_code_bcbrdb_predecessor_table))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_row_scale. bcf_height_bcbrdb_predecessor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_predecessor_table) = S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_row_scale_bcbrdb_predecessor_table))) /\ ((bcf_row_index_bcbrdb_predecessor_table = 0 /\ (forall bcf_index_bcbrdb_predecessor_table_zero_row. (exists bcf_lt_gap_bcbrdb_predecessor_table_zero_row_bound. bcf_lt_gap_bcbrdb_predecessor_table_zero_row_bound + S (bcf_index_bcbrdb_predecessor_table_zero_row) = S (n + n)) -> exists bcf_value_bcbrdb_predecessor_table_zero_row. ((((exists bcf_height_bcbrdb_predecessor_table_zero_row_entry. bcf_height_bcbrdb_predecessor_table_zero_row_entry + S (bcf_value_bcbrdb_predecessor_table_zero_row) = S ((S (bcf_index_bcbrdb_predecessor_table_zero_row)) * bcf_row_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_zero_row_entry. bcf_row_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_predecessor_table_zero_row)) * bcf_row_scale_bcbrdb_predecessor_table) + (bcf_value_bcbrdb_predecessor_table_zero_row))) /\ ((bcf_index_bcbrdb_predecessor_table_zero_row = 0 /\ bcf_value_bcbrdb_predecessor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_predecessor_table_zero_row. bcf_index_bcbrdb_predecessor_table_zero_row = S bcf_predecessor_bcbrdb_predecessor_table_zero_row /\ bcf_value_bcbrdb_predecessor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_predecessor_table bcf_previous_code_bcbrdb_predecessor_table bcf_previous_scale_bcbrdb_predecessor_table. bcf_row_index_bcbrdb_predecessor_table = S bcf_predecessor_bcbrdb_predecessor_table /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_previous_code. bcf_height_bcbrdb_predecessor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_predecessor_table) = S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_previous_code_bcbrdb_predecessor_table))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_decoded_previous_scale. bcf_height_bcbrdb_predecessor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_predecessor_table) = S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_predecessor_table)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_previous_scale_bcbrdb_predecessor_table))) /\ (forall bcf_index_bcbrdb_predecessor_table_row_step. (exists bcf_lt_gap_bcbrdb_predecessor_table_row_step_bound. bcf_lt_gap_bcbrdb_predecessor_table_row_step_bound + S (bcf_index_bcbrdb_predecessor_table_row_step) = S (n + n)) -> exists bcf_value_bcbrdb_predecessor_table_row_step. ((((exists bcf_height_bcbrdb_predecessor_table_row_step_entry. bcf_height_bcbrdb_predecessor_table_row_step_entry + S (bcf_value_bcbrdb_predecessor_table_row_step) = S ((S (bcf_index_bcbrdb_predecessor_table_row_step)) * bcf_row_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_entry. bcf_row_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_entry * S ((S (bcf_index_bcbrdb_predecessor_table_row_step)) * bcf_row_scale_bcbrdb_predecessor_table) + (bcf_value_bcbrdb_predecessor_table_row_step))) /\ ((bcf_index_bcbrdb_predecessor_table_row_step = 0 /\ bcf_value_bcbrdb_predecessor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_predecessor_table_row_step bcf_left_bcbrdb_predecessor_table_row_step bcf_right_bcbrdb_predecessor_table_row_step. bcf_index_bcbrdb_predecessor_table_row_step = S bcf_predecessor_bcbrdb_predecessor_table_row_step /\ ((((exists bcf_height_bcbrdb_predecessor_table_row_step_previous_left. bcf_height_bcbrdb_predecessor_table_row_step_previous_left + S (bcf_left_bcbrdb_predecessor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_predecessor_table_row_step)) * bcf_previous_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_previous_left. bcf_previous_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_predecessor_table_row_step)) * bcf_previous_scale_bcbrdb_predecessor_table) + (bcf_left_bcbrdb_predecessor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_predecessor_table_row_step_previous_right. bcf_height_bcbrdb_predecessor_table_row_step_previous_right + S (bcf_right_bcbrdb_predecessor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_predecessor_table_row_step))) * bcf_previous_scale_bcbrdb_predecessor_table)) /\ exists bcf_quotient_bcbrdb_predecessor_table_row_step_previous_right. bcf_previous_code_bcbrdb_predecessor_table = bcf_quotient_bcbrdb_predecessor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_predecessor_table_row_step))) * bcf_previous_scale_bcbrdb_predecessor_table) + (bcf_right_bcbrdb_predecessor_table_row_step))) /\ bcf_value_bcbrdb_predecessor_table_row_step = bcf_left_bcbrdb_predecessor_table_row_step + bcf_right_bcbrdb_predecessor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_predecessor_decoded_row_code. bcf_height_bcbrdb_predecessor_decoded_row_code + S (bcf_row_code_bcbrdb_predecessor) = S ((S (n + n)) * bcf_row_code_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_row_code. bcf_row_code_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcbrdb_predecessor) + (bcf_row_code_bcbrdb_predecessor))) /\ ((((exists bcf_height_bcbrdb_predecessor_decoded_row_scale. bcf_height_bcbrdb_predecessor_decoded_row_scale + S (bcf_row_scale_bcbrdb_predecessor) = S ((S (n + n)) * bcf_row_scale_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_row_scale. bcf_row_scale_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcbrdb_predecessor) + (bcf_row_scale_bcbrdb_predecessor))) /\ (((exists bcf_height_bcbrdb_predecessor_decoded_value. bcf_height_bcbrdb_predecessor_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bcbrdb_predecessor)) /\ exists bcf_quotient_bcbrdb_predecessor_decoded_value. bcf_row_code_bcbrdb_predecessor = bcf_quotient_bcbrdb_predecessor_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_predecessor) + (c))))))))) -> (((exists bcf_lt_gap_bcbrdb_successor_out_of_range. bcf_lt_gap_bcbrdb_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbrdb_successor_in_range. bcf_le_gap_bcbrdb_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbrdb_successor bcf_row_code_scale_bcbrdb_successor bcf_row_scale_code_bcbrdb_successor bcf_row_scale_scale_bcbrdb_successor bcf_row_code_bcbrdb_successor bcf_row_scale_bcbrdb_successor. ((forall bcf_row_index_bcbrdb_successor_table. (exists bcf_lt_gap_bcbrdb_successor_table_row_bound. bcf_lt_gap_bcbrdb_successor_table_row_bound + S (bcf_row_index_bcbrdb_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbrdb_successor_table bcf_row_scale_bcbrdb_successor_table. ((((exists bcf_height_bcbrdb_successor_table_decoded_row_code. bcf_height_bcbrdb_successor_table_decoded_row_code + S (bcf_row_code_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_row_scale. bcf_height_bcbrdb_successor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor_table))) /\ ((bcf_row_index_bcbrdb_successor_table = 0 /\ (forall bcf_index_bcbrdb_successor_table_zero_row. (exists bcf_lt_gap_bcbrdb_successor_table_zero_row_bound. bcf_lt_gap_bcbrdb_successor_table_zero_row_bound + S (bcf_index_bcbrdb_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_zero_row. ((((exists bcf_height_bcbrdb_successor_table_zero_row_entry. bcf_height_bcbrdb_successor_table_zero_row_entry + S (bcf_value_bcbrdb_successor_table_zero_row) = S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_zero_row_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_zero_row))) /\ ((bcf_index_bcbrdb_successor_table_zero_row = 0 /\ bcf_value_bcbrdb_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_zero_row. bcf_index_bcbrdb_successor_table_zero_row = S bcf_predecessor_bcbrdb_successor_table_zero_row /\ bcf_value_bcbrdb_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_successor_table bcf_previous_code_bcbrdb_successor_table bcf_previous_scale_bcbrdb_successor_table. bcf_row_index_bcbrdb_successor_table = S bcf_predecessor_bcbrdb_successor_table /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_code. bcf_height_bcbrdb_successor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_previous_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_scale. bcf_height_bcbrdb_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_previous_scale_bcbrdb_successor_table))) /\ (forall bcf_index_bcbrdb_successor_table_row_step. (exists bcf_lt_gap_bcbrdb_successor_table_row_step_bound. bcf_lt_gap_bcbrdb_successor_table_row_step_bound + S (bcf_index_bcbrdb_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_row_step. ((((exists bcf_height_bcbrdb_successor_table_row_step_entry. bcf_height_bcbrdb_successor_table_row_step_entry + S (bcf_value_bcbrdb_successor_table_row_step) = S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_entry * S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_row_step))) /\ ((bcf_index_bcbrdb_successor_table_row_step = 0 /\ bcf_value_bcbrdb_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_row_step bcf_left_bcbrdb_successor_table_row_step bcf_right_bcbrdb_successor_table_row_step. bcf_index_bcbrdb_successor_table_row_step = S bcf_predecessor_bcbrdb_successor_table_row_step /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_left. bcf_height_bcbrdb_successor_table_row_step_previous_left + S (bcf_left_bcbrdb_successor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_left. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_left_bcbrdb_successor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_right. bcf_height_bcbrdb_successor_table_row_step_previous_right + S (bcf_right_bcbrdb_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_right. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_right_bcbrdb_successor_table_row_step))) /\ bcf_value_bcbrdb_successor_table_row_step = bcf_left_bcbrdb_successor_table_row_step + bcf_right_bcbrdb_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_code. bcf_height_bcbrdb_successor_decoded_row_code + S (bcf_row_code_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_scale. bcf_height_bcbrdb_successor_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor))) /\ (((exists bcf_height_bcbrdb_successor_decoded_value. bcf_height_bcbrdb_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_value. bcf_row_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbrdb_successor) + (d))))))))) -> S n * d = (2 * S (n + n)) * c) /\ (forall n d m. (((exists bcf_lt_gap_bcbrdb_successor_out_of_range. bcf_lt_gap_bcbrdb_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbrdb_successor_in_range. bcf_le_gap_bcbrdb_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbrdb_successor bcf_row_code_scale_bcbrdb_successor bcf_row_scale_code_bcbrdb_successor bcf_row_scale_scale_bcbrdb_successor bcf_row_code_bcbrdb_successor bcf_row_scale_bcbrdb_successor. ((forall bcf_row_index_bcbrdb_successor_table. (exists bcf_lt_gap_bcbrdb_successor_table_row_bound. bcf_lt_gap_bcbrdb_successor_table_row_bound + S (bcf_row_index_bcbrdb_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbrdb_successor_table bcf_row_scale_bcbrdb_successor_table. ((((exists bcf_height_bcbrdb_successor_table_decoded_row_code. bcf_height_bcbrdb_successor_table_decoded_row_code + S (bcf_row_code_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_row_scale. bcf_height_bcbrdb_successor_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor_table) = S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor_table))) /\ ((bcf_row_index_bcbrdb_successor_table = 0 /\ (forall bcf_index_bcbrdb_successor_table_zero_row. (exists bcf_lt_gap_bcbrdb_successor_table_zero_row_bound. bcf_lt_gap_bcbrdb_successor_table_zero_row_bound + S (bcf_index_bcbrdb_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_zero_row. ((((exists bcf_height_bcbrdb_successor_table_zero_row_entry. bcf_height_bcbrdb_successor_table_zero_row_entry + S (bcf_value_bcbrdb_successor_table_zero_row) = S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_zero_row_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_zero_row_entry * S ((S (bcf_index_bcbrdb_successor_table_zero_row)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_zero_row))) /\ ((bcf_index_bcbrdb_successor_table_zero_row = 0 /\ bcf_value_bcbrdb_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_zero_row. bcf_index_bcbrdb_successor_table_zero_row = S bcf_predecessor_bcbrdb_successor_table_zero_row /\ bcf_value_bcbrdb_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_successor_table bcf_previous_code_bcbrdb_successor_table bcf_previous_scale_bcbrdb_successor_table. bcf_row_index_bcbrdb_successor_table = S bcf_predecessor_bcbrdb_successor_table /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_code. bcf_height_bcbrdb_successor_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_previous_code_bcbrdb_successor_table))) /\ ((((exists bcf_height_bcbrdb_successor_table_decoded_previous_scale. bcf_height_bcbrdb_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_successor_table) = S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_successor_table)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_previous_scale_bcbrdb_successor_table))) /\ (forall bcf_index_bcbrdb_successor_table_row_step. (exists bcf_lt_gap_bcbrdb_successor_table_row_step_bound. bcf_lt_gap_bcbrdb_successor_table_row_step_bound + S (bcf_index_bcbrdb_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbrdb_successor_table_row_step. ((((exists bcf_height_bcbrdb_successor_table_row_step_entry. bcf_height_bcbrdb_successor_table_row_step_entry + S (bcf_value_bcbrdb_successor_table_row_step) = S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_entry. bcf_row_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_entry * S ((S (bcf_index_bcbrdb_successor_table_row_step)) * bcf_row_scale_bcbrdb_successor_table) + (bcf_value_bcbrdb_successor_table_row_step))) /\ ((bcf_index_bcbrdb_successor_table_row_step = 0 /\ bcf_value_bcbrdb_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_successor_table_row_step bcf_left_bcbrdb_successor_table_row_step bcf_right_bcbrdb_successor_table_row_step. bcf_index_bcbrdb_successor_table_row_step = S bcf_predecessor_bcbrdb_successor_table_row_step /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_left. bcf_height_bcbrdb_successor_table_row_step_previous_left + S (bcf_left_bcbrdb_successor_table_row_step) = S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_left. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_successor_table_row_step)) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_left_bcbrdb_successor_table_row_step))) /\ ((((exists bcf_height_bcbrdb_successor_table_row_step_previous_right. bcf_height_bcbrdb_successor_table_row_step_previous_right + S (bcf_right_bcbrdb_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table)) /\ exists bcf_quotient_bcbrdb_successor_table_row_step_previous_right. bcf_previous_code_bcbrdb_successor_table = bcf_quotient_bcbrdb_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_successor_table_row_step))) * bcf_previous_scale_bcbrdb_successor_table) + (bcf_right_bcbrdb_successor_table_row_step))) /\ bcf_value_bcbrdb_successor_table_row_step = bcf_left_bcbrdb_successor_table_row_step + bcf_right_bcbrdb_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_code. bcf_height_bcbrdb_successor_decoded_row_code + S (bcf_row_code_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_code. bcf_row_code_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbrdb_successor) + (bcf_row_code_bcbrdb_successor))) /\ ((((exists bcf_height_bcbrdb_successor_decoded_row_scale. bcf_height_bcbrdb_successor_decoded_row_scale + S (bcf_row_scale_bcbrdb_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_row_scale. bcf_row_scale_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbrdb_successor) + (bcf_row_scale_bcbrdb_successor))) /\ (((exists bcf_height_bcbrdb_successor_decoded_value. bcf_height_bcbrdb_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbrdb_successor)) /\ exists bcf_quotient_bcbrdb_successor_decoded_value. bcf_row_code_bcbrdb_successor = bcf_quotient_bcbrdb_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbrdb_successor) + (d))))))))) -> (((exists bcf_lt_gap_bcbrdb_middle_out_of_range. bcf_lt_gap_bcbrdb_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbrdb_middle_in_range. bcf_le_gap_bcbrdb_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbrdb_middle bcf_row_code_scale_bcbrdb_middle bcf_row_scale_code_bcbrdb_middle bcf_row_scale_scale_bcbrdb_middle bcf_row_code_bcbrdb_middle bcf_row_scale_bcbrdb_middle. ((forall bcf_row_index_bcbrdb_middle_table. (exists bcf_lt_gap_bcbrdb_middle_table_row_bound. bcf_lt_gap_bcbrdb_middle_table_row_bound + S (bcf_row_index_bcbrdb_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbrdb_middle_table bcf_row_scale_bcbrdb_middle_table. ((((exists bcf_height_bcbrdb_middle_table_decoded_row_code. bcf_height_bcbrdb_middle_table_decoded_row_code + S (bcf_row_code_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_row_scale. bcf_height_bcbrdb_middle_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle_table))) /\ ((bcf_row_index_bcbrdb_middle_table = 0 /\ (forall bcf_index_bcbrdb_middle_table_zero_row. (exists bcf_lt_gap_bcbrdb_middle_table_zero_row_bound. bcf_lt_gap_bcbrdb_middle_table_zero_row_bound + S (bcf_index_bcbrdb_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_zero_row. ((((exists bcf_height_bcbrdb_middle_table_zero_row_entry. bcf_height_bcbrdb_middle_table_zero_row_entry + S (bcf_value_bcbrdb_middle_table_zero_row) = S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_zero_row_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_zero_row_entry * S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_zero_row))) /\ ((bcf_index_bcbrdb_middle_table_zero_row = 0 /\ bcf_value_bcbrdb_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_zero_row. bcf_index_bcbrdb_middle_table_zero_row = S bcf_predecessor_bcbrdb_middle_table_zero_row /\ bcf_value_bcbrdb_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_middle_table bcf_previous_code_bcbrdb_middle_table bcf_previous_scale_bcbrdb_middle_table. bcf_row_index_bcbrdb_middle_table = S bcf_predecessor_bcbrdb_middle_table /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_code. bcf_height_bcbrdb_middle_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_previous_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_scale. bcf_height_bcbrdb_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_previous_scale_bcbrdb_middle_table))) /\ (forall bcf_index_bcbrdb_middle_table_row_step. (exists bcf_lt_gap_bcbrdb_middle_table_row_step_bound. bcf_lt_gap_bcbrdb_middle_table_row_step_bound + S (bcf_index_bcbrdb_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_row_step. ((((exists bcf_height_bcbrdb_middle_table_row_step_entry. bcf_height_bcbrdb_middle_table_row_step_entry + S (bcf_value_bcbrdb_middle_table_row_step) = S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_entry * S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_row_step))) /\ ((bcf_index_bcbrdb_middle_table_row_step = 0 /\ bcf_value_bcbrdb_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_row_step bcf_left_bcbrdb_middle_table_row_step bcf_right_bcbrdb_middle_table_row_step. bcf_index_bcbrdb_middle_table_row_step = S bcf_predecessor_bcbrdb_middle_table_row_step /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_left. bcf_height_bcbrdb_middle_table_row_step_previous_left + S (bcf_left_bcbrdb_middle_table_row_step) = S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_left. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_left_bcbrdb_middle_table_row_step))) /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_right. bcf_height_bcbrdb_middle_table_row_step_previous_right + S (bcf_right_bcbrdb_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_right. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_right_bcbrdb_middle_table_row_step))) /\ bcf_value_bcbrdb_middle_table_row_step = bcf_left_bcbrdb_middle_table_row_step + bcf_right_bcbrdb_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_code. bcf_height_bcbrdb_middle_decoded_row_code + S (bcf_row_code_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_scale. bcf_height_bcbrdb_middle_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle))) /\ (((exists bcf_height_bcbrdb_middle_decoded_value. bcf_height_bcbrdb_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_value. bcf_row_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_middle) + (m))))))))) -> d = m + m))

Structural proof guide

The recurrence and functional double-middle law share support.

Direct prerequisites: mul_add, mul_assoc, two_mul_eq_add_self, central_binom_succ_double_middle, choose_weighted_vertical, choose_functional. The authored body proceeds by case analysis (4), intermediate claims (4), equality transport (3).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0008 mul_assoc BT00QU two_mul_eq_add_self BT00TS central_binom_succ_double_middle BT00TT choose_weighted_vertical BT00TC choose_functional

Direct dependents

BT00VN central_binom_upper_support_package

Formal native tactic body

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

Read the argument

Proof checkpoints

62 script commands · 19 reading checkpoints · 4 local claims

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

Named ingredients (6)
mul addmul assoctwo mul eq add selfcentral binom succ double middlechoose weighted verticalchoose functional

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

01Separate the logical casesL1–1

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

  1. L1
    split
02Fix variables and assumptionsL2–6

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

  1. L2
    intro n
  2. L3
    intro c
  3. L4
    intro d
  4. L5
    intro hpredecessor
  5. L6
    intro hsuccessor
03Establish hmiddleL7–11

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

  1. L7
    have hmiddle : ∃ m. Choose(S (n + n),n,m) ∧ d = m + mDefinitions: Choose
  2. L8
    specialize central_binom_succ_double_middle n
  3. L9
    specialize central_binom_succ_double_middle d
  4. L10
    apply central_binom_succ_double_middle
  5. L11
    exact hsuccessor
04Separate the logical casesL12–13

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

  1. L12
    cases hmiddle
  2. L13
    cases hmiddle_witness
05Establish hweightedL14–23

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

  1. L14
    have hweighted : S n * x = S (n + n) * c
  2. L15
    specialize choose_weighted_vertical (n + n)
  3. L16
    specialize choose_weighted_vertical n
  4. L17
    specialize choose_weighted_vertical n
  5. L18
    specialize choose_weighted_vertical c
  6. L19
    specialize choose_weighted_vertical x
  7. L20
    apply choose_weighted_vertical
  8. L21
    refl
  9. L22
    exact hpredecessor
  10. L23
    exact hmiddle_witness_left
06Calculate and transport equalitiesL24–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    rewrite hmiddle_witness_right
  2. L25
    trans S n * x + S n * x
07Use earlier factsL26–26

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

  1. L26
    apply mul_add
08Calculate and transport equalitiesL27–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    rewrite hweighted
  2. L28
    rewrite hweighted
  3. L29
    trans 2 * (S (n + n) * c)
09Use earlier factsL30–30

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

  1. L30
    specialize two_mul_eq_add_self (S (n + n) * c)
10Calculate and transport equalitiesL31–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    symm
11Use earlier factsL32–35

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

  1. L32
    exact two_mul_eq_add_self
  2. L33
    specialize mul_assoc 2
  3. L34
    specialize mul_assoc (S (n + n))
  4. L35
    specialize mul_assoc c
12Calculate and transport equalitiesL36–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    symm
13Use earlier factsL37–37

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

  1. L37
    exact mul_assoc
14Fix variables and assumptionsL38–42

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

  1. L38
    intro n
  2. L39
    intro d
  3. L40
    intro m
  4. L41
    intro hsuccessor
  5. L42
    intro hmiddle_given
15Establish hmiddleL43–47

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

  1. L43
    have hmiddle : ∃ m. Choose(S (n + n),n,m) ∧ d = m + mDefinitions: Choose
  2. L44
    specialize central_binom_succ_double_middle n
  3. L45
    specialize central_binom_succ_double_middle d
  4. L46
    apply central_binom_succ_double_middle
  5. L47
    exact hsuccessor
16Separate the logical casesL48–49

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

  1. L48
    cases hmiddle
  2. L49
    cases hmiddle_witness
17Establish heqL50–59

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

  1. L50
    have heq : x = m
  2. L51
    specialize choose_functional (S (n + n))
  3. L52
    specialize choose_functional n
  4. L53
    specialize choose_functional x
  5. L54
    specialize choose_functional m
  6. L55
    apply choose_functional
  7. L56
    exact hmiddle_witness_left
  8. L57
    exact hmiddle_given
  9. L58
    trans x + x
  10. L59
    exact hmiddle_witness_right
18Calculate and transport equalitiesL60–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    congr
19Use earlier factsL61–62

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

  1. L61
    exact heq
  2. L62
    exact heq

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001split
  2. 0002intro n
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hpredecessor
  6. 0006intro hsuccessor
  7. 0007have hmiddle : exists m. ((((exists bcf_lt_gap_bcbrdb_middle_out_of_range. bcf_lt_gap_bcbrdb_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbrdb_middle_in_range. bcf_le_gap_bcbrdb_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbrdb_middle bcf_row_code_scale_bcbrdb_middle bcf_row_scale_code_bcbrdb_middle bcf_row_scale_scale_bcbrdb_middle bcf_row_code_bcbrdb_middle bcf_row_scale_bcbrdb_middle. ((forall bcf_row_index_bcbrdb_middle_table. (exists bcf_lt_gap_bcbrdb_middle_table_row_bound. bcf_lt_gap_bcbrdb_middle_table_row_bound + S (bcf_row_index_bcbrdb_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbrdb_middle_table bcf_row_scale_bcbrdb_middle_table. ((((exists bcf_height_bcbrdb_middle_table_decoded_row_code. bcf_height_bcbrdb_middle_table_decoded_row_code + S (bcf_row_code_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_row_scale. bcf_height_bcbrdb_middle_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle_table))) /\ ((bcf_row_index_bcbrdb_middle_table = 0 /\ (forall bcf_index_bcbrdb_middle_table_zero_row. (exists bcf_lt_gap_bcbrdb_middle_table_zero_row_bound. bcf_lt_gap_bcbrdb_middle_table_zero_row_bound + S (bcf_index_bcbrdb_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_zero_row. ((((exists bcf_height_bcbrdb_middle_table_zero_row_entry. bcf_height_bcbrdb_middle_table_zero_row_entry + S (bcf_value_bcbrdb_middle_table_zero_row) = S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_zero_row_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_zero_row_entry * S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_zero_row))) /\ ((bcf_index_bcbrdb_middle_table_zero_row = 0 /\ bcf_value_bcbrdb_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_zero_row. bcf_index_bcbrdb_middle_table_zero_row = S bcf_predecessor_bcbrdb_middle_table_zero_row /\ bcf_value_bcbrdb_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_middle_table bcf_previous_code_bcbrdb_middle_table bcf_previous_scale_bcbrdb_middle_table. bcf_row_index_bcbrdb_middle_table = S bcf_predecessor_bcbrdb_middle_table /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_code. bcf_height_bcbrdb_middle_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_previous_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_scale. bcf_height_bcbrdb_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_previous_scale_bcbrdb_middle_table))) /\ (forall bcf_index_bcbrdb_middle_table_row_step. (exists bcf_lt_gap_bcbrdb_middle_table_row_step_bound. bcf_lt_gap_bcbrdb_middle_table_row_step_bound + S (bcf_index_bcbrdb_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_row_step. ((((exists bcf_height_bcbrdb_middle_table_row_step_entry. bcf_height_bcbrdb_middle_table_row_step_entry + S (bcf_value_bcbrdb_middle_table_row_step) = S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_entry * S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_row_step))) /\ ((bcf_index_bcbrdb_middle_table_row_step = 0 /\ bcf_value_bcbrdb_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_row_step bcf_left_bcbrdb_middle_table_row_step bcf_right_bcbrdb_middle_table_row_step. bcf_index_bcbrdb_middle_table_row_step = S bcf_predecessor_bcbrdb_middle_table_row_step /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_left. bcf_height_bcbrdb_middle_table_row_step_previous_left + S (bcf_left_bcbrdb_middle_table_row_step) = S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_left. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_left_bcbrdb_middle_table_row_step))) /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_right. bcf_height_bcbrdb_middle_table_row_step_previous_right + S (bcf_right_bcbrdb_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_right. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_right_bcbrdb_middle_table_row_step))) /\ bcf_value_bcbrdb_middle_table_row_step = bcf_left_bcbrdb_middle_table_row_step + bcf_right_bcbrdb_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_code. bcf_height_bcbrdb_middle_decoded_row_code + S (bcf_row_code_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_scale. bcf_height_bcbrdb_middle_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle))) /\ (((exists bcf_height_bcbrdb_middle_decoded_value. bcf_height_bcbrdb_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_value. bcf_row_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_middle) + (m))))))))) /\ d = m + m)
  8. 0008specialize central_binom_succ_double_middle n
  9. 0009specialize central_binom_succ_double_middle d
  10. 0010apply central_binom_succ_double_middle
  11. 0011exact hsuccessor
  12. 0012cases hmiddle
  13. 0013cases hmiddle_witness
  14. 0014have hweighted : S n * x = S (n + n) * c
  15. 0015specialize choose_weighted_vertical (n + n)
  16. 0016specialize choose_weighted_vertical n
  17. 0017specialize choose_weighted_vertical n
  18. 0018specialize choose_weighted_vertical c
  19. 0019specialize choose_weighted_vertical x
  20. 0020apply choose_weighted_vertical
  21. 0021refl
  22. 0022exact hpredecessor
  23. 0023exact hmiddle_witness_left
  24. 0024rewrite hmiddle_witness_right
  25. 0025trans S n * x + S n * x
  26. 0026apply mul_add
  27. 0027rewrite hweighted
  28. 0028rewrite hweighted
  29. 0029trans 2 * (S (n + n) * c)
  30. 0030specialize two_mul_eq_add_self (S (n + n) * c)
  31. 0031symm
  32. 0032exact two_mul_eq_add_self
  33. 0033specialize mul_assoc 2
  34. 0034specialize mul_assoc (S (n + n))
  35. 0035specialize mul_assoc c
  36. 0036symm
  37. 0037exact mul_assoc
  38. 0038intro n
  39. 0039intro d
  40. 0040intro m
  41. 0041intro hsuccessor
  42. 0042intro hmiddle_given
  43. 0043have hmiddle : exists m. ((((exists bcf_lt_gap_bcbrdb_middle_out_of_range. bcf_lt_gap_bcbrdb_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbrdb_middle_in_range. bcf_le_gap_bcbrdb_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbrdb_middle bcf_row_code_scale_bcbrdb_middle bcf_row_scale_code_bcbrdb_middle bcf_row_scale_scale_bcbrdb_middle bcf_row_code_bcbrdb_middle bcf_row_scale_bcbrdb_middle. ((forall bcf_row_index_bcbrdb_middle_table. (exists bcf_lt_gap_bcbrdb_middle_table_row_bound. bcf_lt_gap_bcbrdb_middle_table_row_bound + S (bcf_row_index_bcbrdb_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbrdb_middle_table bcf_row_scale_bcbrdb_middle_table. ((((exists bcf_height_bcbrdb_middle_table_decoded_row_code. bcf_height_bcbrdb_middle_table_decoded_row_code + S (bcf_row_code_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_row_scale. bcf_height_bcbrdb_middle_table_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle_table) = S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle_table))) /\ ((bcf_row_index_bcbrdb_middle_table = 0 /\ (forall bcf_index_bcbrdb_middle_table_zero_row. (exists bcf_lt_gap_bcbrdb_middle_table_zero_row_bound. bcf_lt_gap_bcbrdb_middle_table_zero_row_bound + S (bcf_index_bcbrdb_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_zero_row. ((((exists bcf_height_bcbrdb_middle_table_zero_row_entry. bcf_height_bcbrdb_middle_table_zero_row_entry + S (bcf_value_bcbrdb_middle_table_zero_row) = S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_zero_row_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_zero_row_entry * S ((S (bcf_index_bcbrdb_middle_table_zero_row)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_zero_row))) /\ ((bcf_index_bcbrdb_middle_table_zero_row = 0 /\ bcf_value_bcbrdb_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_zero_row. bcf_index_bcbrdb_middle_table_zero_row = S bcf_predecessor_bcbrdb_middle_table_zero_row /\ bcf_value_bcbrdb_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbrdb_middle_table bcf_previous_code_bcbrdb_middle_table bcf_previous_scale_bcbrdb_middle_table. bcf_row_index_bcbrdb_middle_table = S bcf_predecessor_bcbrdb_middle_table /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_code. bcf_height_bcbrdb_middle_table_decoded_previous_code + S (bcf_previous_code_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_code_scale_bcbrdb_middle) + (bcf_previous_code_bcbrdb_middle_table))) /\ ((((exists bcf_height_bcbrdb_middle_table_decoded_previous_scale. bcf_height_bcbrdb_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbrdb_middle_table) = S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbrdb_middle_table)) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_previous_scale_bcbrdb_middle_table))) /\ (forall bcf_index_bcbrdb_middle_table_row_step. (exists bcf_lt_gap_bcbrdb_middle_table_row_step_bound. bcf_lt_gap_bcbrdb_middle_table_row_step_bound + S (bcf_index_bcbrdb_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbrdb_middle_table_row_step. ((((exists bcf_height_bcbrdb_middle_table_row_step_entry. bcf_height_bcbrdb_middle_table_row_step_entry + S (bcf_value_bcbrdb_middle_table_row_step) = S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_entry. bcf_row_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_entry * S ((S (bcf_index_bcbrdb_middle_table_row_step)) * bcf_row_scale_bcbrdb_middle_table) + (bcf_value_bcbrdb_middle_table_row_step))) /\ ((bcf_index_bcbrdb_middle_table_row_step = 0 /\ bcf_value_bcbrdb_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbrdb_middle_table_row_step bcf_left_bcbrdb_middle_table_row_step bcf_right_bcbrdb_middle_table_row_step. bcf_index_bcbrdb_middle_table_row_step = S bcf_predecessor_bcbrdb_middle_table_row_step /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_left. bcf_height_bcbrdb_middle_table_row_step_previous_left + S (bcf_left_bcbrdb_middle_table_row_step) = S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_left. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbrdb_middle_table_row_step)) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_left_bcbrdb_middle_table_row_step))) /\ ((((exists bcf_height_bcbrdb_middle_table_row_step_previous_right. bcf_height_bcbrdb_middle_table_row_step_previous_right + S (bcf_right_bcbrdb_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table)) /\ exists bcf_quotient_bcbrdb_middle_table_row_step_previous_right. bcf_previous_code_bcbrdb_middle_table = bcf_quotient_bcbrdb_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbrdb_middle_table_row_step))) * bcf_previous_scale_bcbrdb_middle_table) + (bcf_right_bcbrdb_middle_table_row_step))) /\ bcf_value_bcbrdb_middle_table_row_step = bcf_left_bcbrdb_middle_table_row_step + bcf_right_bcbrdb_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_code. bcf_height_bcbrdb_middle_decoded_row_code + S (bcf_row_code_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_code. bcf_row_code_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbrdb_middle) + (bcf_row_code_bcbrdb_middle))) /\ ((((exists bcf_height_bcbrdb_middle_decoded_row_scale. bcf_height_bcbrdb_middle_decoded_row_scale + S (bcf_row_scale_bcbrdb_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_row_scale. bcf_row_scale_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbrdb_middle) + (bcf_row_scale_bcbrdb_middle))) /\ (((exists bcf_height_bcbrdb_middle_decoded_value. bcf_height_bcbrdb_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbrdb_middle)) /\ exists bcf_quotient_bcbrdb_middle_decoded_value. bcf_row_code_bcbrdb_middle = bcf_quotient_bcbrdb_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbrdb_middle) + (m))))))))) /\ d = m + m)
  44. 0044specialize central_binom_succ_double_middle n
  45. 0045specialize central_binom_succ_double_middle d
  46. 0046apply central_binom_succ_double_middle
  47. 0047exact hsuccessor
  48. 0048cases hmiddle
  49. 0049cases hmiddle_witness
  50. 0050have heq : x = m
  51. 0051specialize choose_functional (S (n + n))
  52. 0052specialize choose_functional n
  53. 0053specialize choose_functional x
  54. 0054specialize choose_functional m
  55. 0055apply choose_functional
  56. 0056exact hmiddle_witness_left
  57. 0057exact hmiddle_given
  58. 0058trans x + x
  59. 0059exact hmiddle_witness_right
  60. 0060congr
  61. 0061exact heq
  62. 0062exact heq