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.
The carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.
Exact theorem in conservative defined notation
∀ b. ∀ c. ∀ sb. ∀ sc. ∀ cb. ∀ cc. ∀ l. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,S l) → MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
le_succ · checked external prerequisite
Original expanded first-order statement
forall b c sb sc cb cc l. (forall mkm_index_bindrop_source. (exists mkm_lt_bindrop_source_bound. mkm_lt_bindrop_source_bound + S (mkm_index_bindrop_source) = (S l)) -> (exists mkm_value_bindrop_source_point mkm_partial_bindrop_source_point mkm_factor_bindrop_source_point. (((exists fs_h_mkm_bindrop_source_point_source. fs_h_mkm_bindrop_source_point_source + S (mkm_value_bindrop_source_point) = S ((S (mkm_index_bindrop_source)) * c)) /\ exists fs_q_mkm_bindrop_source_point_source. b = fs_q_mkm_bindrop_source_point_source * S ((S (mkm_index_bindrop_source)) * c) + (mkm_value_bindrop_source_point))) /\ ((((exists fs_h_mkm_bindrop_source_point_partial. fs_h_mkm_bindrop_source_point_partial + S (mkm_partial_bindrop_source_point) = S ((S (mkm_index_bindrop_source)) * sc)) /\ exists fs_q_mkm_bindrop_source_point_partial. sb = fs_q_mkm_bindrop_source_point_partial * S ((S (mkm_index_bindrop_source)) * sc) + (mkm_partial_bindrop_source_point))) /\ ((((exists bcf_lt_gap_mkm_bindrop_source_point_choose_out_of_range. bcf_lt_gap_mkm_bindrop_source_point_choose_out_of_range + S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point) = mkm_partial_bindrop_source_point) /\ mkm_factor_bindrop_source_point = 0) \/ ((exists bcf_le_gap_mkm_bindrop_source_point_choose_in_range. bcf_le_gap_mkm_bindrop_source_point_choose_in_range + (mkm_partial_bindrop_source_point) = mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point) /\ (exists bcf_row_code_code_mkm_bindrop_source_point_choose bcf_row_code_scale_mkm_bindrop_source_point_choose bcf_row_scale_code_mkm_bindrop_source_point_choose bcf_row_scale_scale_mkm_bindrop_source_point_choose bcf_row_code_mkm_bindrop_source_point_choose bcf_row_scale_mkm_bindrop_source_point_choose. ((forall bcf_row_index_mkm_bindrop_source_point_choose_table. (exists bcf_lt_gap_mkm_bindrop_source_point_choose_table_row_bound. bcf_lt_gap_mkm_bindrop_source_point_choose_table_row_bound + S (bcf_row_index_mkm_bindrop_source_point_choose_table) = S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) -> exists bcf_row_code_mkm_bindrop_source_point_choose_table bcf_row_scale_mkm_bindrop_source_point_choose_table. ((((exists bcf_height_mkm_bindrop_source_point_choose_table_decoded_row_code. bcf_height_mkm_bindrop_source_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_bindrop_source_point_choose_table) = S ((S (bcf_row_index_mkm_bindrop_source_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_bindrop_source_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_source_point_choose) + (bcf_row_code_mkm_bindrop_source_point_choose_table))) /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_table_decoded_row_scale. bcf_height_mkm_bindrop_source_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_bindrop_source_point_choose_table) = S ((S (bcf_row_index_mkm_bindrop_source_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_bindrop_source_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose) + (bcf_row_scale_mkm_bindrop_source_point_choose_table))) /\ ((bcf_row_index_mkm_bindrop_source_point_choose_table = 0 /\ (forall bcf_index_mkm_bindrop_source_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_bindrop_source_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_bindrop_source_point_choose_table_zero_row_bound + S (bcf_index_mkm_bindrop_source_point_choose_table_zero_row) = S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) -> exists bcf_value_mkm_bindrop_source_point_choose_table_zero_row. ((((exists bcf_height_mkm_bindrop_source_point_choose_table_zero_row_entry. bcf_height_mkm_bindrop_source_point_choose_table_zero_row_entry + S (bcf_value_mkm_bindrop_source_point_choose_table_zero_row) = S ((S (bcf_index_mkm_bindrop_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_bindrop_source_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_zero_row_entry. bcf_row_code_mkm_bindrop_source_point_choose_table = bcf_quotient_mkm_bindrop_source_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_bindrop_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_bindrop_source_point_choose_table) + (bcf_value_mkm_bindrop_source_point_choose_table_zero_row))) /\ ((bcf_index_mkm_bindrop_source_point_choose_table_zero_row = 0 /\ bcf_value_mkm_bindrop_source_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_bindrop_source_point_choose_table_zero_row. bcf_index_mkm_bindrop_source_point_choose_table_zero_row = S bcf_predecessor_mkm_bindrop_source_point_choose_table_zero_row /\ bcf_value_mkm_bindrop_source_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_bindrop_source_point_choose_table bcf_previous_code_mkm_bindrop_source_point_choose_table bcf_previous_scale_mkm_bindrop_source_point_choose_table. bcf_row_index_mkm_bindrop_source_point_choose_table = S bcf_predecessor_mkm_bindrop_source_point_choose_table /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_table_decoded_previous_code. bcf_height_mkm_bindrop_source_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_bindrop_source_point_choose_table) = S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_source_point_choose) + (bcf_previous_code_mkm_bindrop_source_point_choose_table))) /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_table_decoded_previous_scale. bcf_height_mkm_bindrop_source_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_bindrop_source_point_choose_table) = S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose) + (bcf_previous_scale_mkm_bindrop_source_point_choose_table))) /\ (forall bcf_index_mkm_bindrop_source_point_choose_table_row_step. (exists bcf_lt_gap_mkm_bindrop_source_point_choose_table_row_step_bound. bcf_lt_gap_mkm_bindrop_source_point_choose_table_row_step_bound + S (bcf_index_mkm_bindrop_source_point_choose_table_row_step) = S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) -> exists bcf_value_mkm_bindrop_source_point_choose_table_row_step. ((((exists bcf_height_mkm_bindrop_source_point_choose_table_row_step_entry. bcf_height_mkm_bindrop_source_point_choose_table_row_step_entry + S (bcf_value_mkm_bindrop_source_point_choose_table_row_step) = S ((S (bcf_index_mkm_bindrop_source_point_choose_table_row_step)) * bcf_row_scale_mkm_bindrop_source_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_entry. bcf_row_code_mkm_bindrop_source_point_choose_table = bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_bindrop_source_point_choose_table_row_step)) * bcf_row_scale_mkm_bindrop_source_point_choose_table) + (bcf_value_mkm_bindrop_source_point_choose_table_row_step))) /\ ((bcf_index_mkm_bindrop_source_point_choose_table_row_step = 0 /\ bcf_value_mkm_bindrop_source_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step bcf_left_mkm_bindrop_source_point_choose_table_row_step bcf_right_mkm_bindrop_source_point_choose_table_row_step. bcf_index_mkm_bindrop_source_point_choose_table_row_step = S bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_table_row_step_previous_left. bcf_height_mkm_bindrop_source_point_choose_table_row_step_previous_left + S (bcf_left_mkm_bindrop_source_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_bindrop_source_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_bindrop_source_point_choose_table = bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_bindrop_source_point_choose_table) + (bcf_left_mkm_bindrop_source_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_table_row_step_previous_right. bcf_height_mkm_bindrop_source_point_choose_table_row_step_previous_right + S (bcf_right_mkm_bindrop_source_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_bindrop_source_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_bindrop_source_point_choose_table = bcf_quotient_mkm_bindrop_source_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_bindrop_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_bindrop_source_point_choose_table) + (bcf_right_mkm_bindrop_source_point_choose_table_row_step))) /\ bcf_value_mkm_bindrop_source_point_choose_table_row_step = bcf_left_mkm_bindrop_source_point_choose_table_row_step + bcf_right_mkm_bindrop_source_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_decoded_row_code. bcf_height_mkm_bindrop_source_point_choose_decoded_row_code + S (bcf_row_code_mkm_bindrop_source_point_choose) = S ((S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) * bcf_row_code_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_decoded_row_code. bcf_row_code_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_decoded_row_code * S ((S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) * bcf_row_code_scale_mkm_bindrop_source_point_choose) + (bcf_row_code_mkm_bindrop_source_point_choose))) /\ ((((exists bcf_height_mkm_bindrop_source_point_choose_decoded_row_scale. bcf_height_mkm_bindrop_source_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_bindrop_source_point_choose) = S ((S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_decoded_row_scale * S ((S (mkm_partial_bindrop_source_point + mkm_value_bindrop_source_point)) * bcf_row_scale_scale_mkm_bindrop_source_point_choose) + (bcf_row_scale_mkm_bindrop_source_point_choose))) /\ (((exists bcf_height_mkm_bindrop_source_point_choose_decoded_value. bcf_height_mkm_bindrop_source_point_choose_decoded_value + S (mkm_factor_bindrop_source_point) = S ((S (mkm_partial_bindrop_source_point)) * bcf_row_scale_mkm_bindrop_source_point_choose)) /\ exists bcf_quotient_mkm_bindrop_source_point_choose_decoded_value. bcf_row_code_mkm_bindrop_source_point_choose = bcf_quotient_mkm_bindrop_source_point_choose_decoded_value * S ((S (mkm_partial_bindrop_source_point)) * bcf_row_scale_mkm_bindrop_source_point_choose) + (mkm_factor_bindrop_source_point))))))))) /\ (((exists fs_h_mkm_bindrop_source_point_factor. fs_h_mkm_bindrop_source_point_factor + S (mkm_factor_bindrop_source_point) = S ((S (mkm_index_bindrop_source)) * cc)) /\ exists fs_q_mkm_bindrop_source_point_factor. cb = fs_q_mkm_bindrop_source_point_factor * S ((S (mkm_index_bindrop_source)) * cc) + (mkm_factor_bindrop_source_point))))))) -> (forall mkm_index_bindrop_target. (exists mkm_lt_bindrop_target_bound. mkm_lt_bindrop_target_bound + S (mkm_index_bindrop_target) = (l)) -> (exists mkm_value_bindrop_target_point mkm_partial_bindrop_target_point mkm_factor_bindrop_target_point. (((exists fs_h_mkm_bindrop_target_point_source. fs_h_mkm_bindrop_target_point_source + S (mkm_value_bindrop_target_point) = S ((S (mkm_index_bindrop_target)) * c)) /\ exists fs_q_mkm_bindrop_target_point_source. b = fs_q_mkm_bindrop_target_point_source * S ((S (mkm_index_bindrop_target)) * c) + (mkm_value_bindrop_target_point))) /\ ((((exists fs_h_mkm_bindrop_target_point_partial. fs_h_mkm_bindrop_target_point_partial + S (mkm_partial_bindrop_target_point) = S ((S (mkm_index_bindrop_target)) * sc)) /\ exists fs_q_mkm_bindrop_target_point_partial. sb = fs_q_mkm_bindrop_target_point_partial * S ((S (mkm_index_bindrop_target)) * sc) + (mkm_partial_bindrop_target_point))) /\ ((((exists bcf_lt_gap_mkm_bindrop_target_point_choose_out_of_range. bcf_lt_gap_mkm_bindrop_target_point_choose_out_of_range + S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point) = mkm_partial_bindrop_target_point) /\ mkm_factor_bindrop_target_point = 0) \/ ((exists bcf_le_gap_mkm_bindrop_target_point_choose_in_range. bcf_le_gap_mkm_bindrop_target_point_choose_in_range + (mkm_partial_bindrop_target_point) = mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point) /\ (exists bcf_row_code_code_mkm_bindrop_target_point_choose bcf_row_code_scale_mkm_bindrop_target_point_choose bcf_row_scale_code_mkm_bindrop_target_point_choose bcf_row_scale_scale_mkm_bindrop_target_point_choose bcf_row_code_mkm_bindrop_target_point_choose bcf_row_scale_mkm_bindrop_target_point_choose. ((forall bcf_row_index_mkm_bindrop_target_point_choose_table. (exists bcf_lt_gap_mkm_bindrop_target_point_choose_table_row_bound. bcf_lt_gap_mkm_bindrop_target_point_choose_table_row_bound + S (bcf_row_index_mkm_bindrop_target_point_choose_table) = S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) -> exists bcf_row_code_mkm_bindrop_target_point_choose_table bcf_row_scale_mkm_bindrop_target_point_choose_table. ((((exists bcf_height_mkm_bindrop_target_point_choose_table_decoded_row_code. bcf_height_mkm_bindrop_target_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_bindrop_target_point_choose_table) = S ((S (bcf_row_index_mkm_bindrop_target_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_bindrop_target_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_target_point_choose) + (bcf_row_code_mkm_bindrop_target_point_choose_table))) /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_table_decoded_row_scale. bcf_height_mkm_bindrop_target_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_bindrop_target_point_choose_table) = S ((S (bcf_row_index_mkm_bindrop_target_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_bindrop_target_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose) + (bcf_row_scale_mkm_bindrop_target_point_choose_table))) /\ ((bcf_row_index_mkm_bindrop_target_point_choose_table = 0 /\ (forall bcf_index_mkm_bindrop_target_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_bindrop_target_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_bindrop_target_point_choose_table_zero_row_bound + S (bcf_index_mkm_bindrop_target_point_choose_table_zero_row) = S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) -> exists bcf_value_mkm_bindrop_target_point_choose_table_zero_row. ((((exists bcf_height_mkm_bindrop_target_point_choose_table_zero_row_entry. bcf_height_mkm_bindrop_target_point_choose_table_zero_row_entry + S (bcf_value_mkm_bindrop_target_point_choose_table_zero_row) = S ((S (bcf_index_mkm_bindrop_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_bindrop_target_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_zero_row_entry. bcf_row_code_mkm_bindrop_target_point_choose_table = bcf_quotient_mkm_bindrop_target_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_bindrop_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_bindrop_target_point_choose_table) + (bcf_value_mkm_bindrop_target_point_choose_table_zero_row))) /\ ((bcf_index_mkm_bindrop_target_point_choose_table_zero_row = 0 /\ bcf_value_mkm_bindrop_target_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_bindrop_target_point_choose_table_zero_row. bcf_index_mkm_bindrop_target_point_choose_table_zero_row = S bcf_predecessor_mkm_bindrop_target_point_choose_table_zero_row /\ bcf_value_mkm_bindrop_target_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_bindrop_target_point_choose_table bcf_previous_code_mkm_bindrop_target_point_choose_table bcf_previous_scale_mkm_bindrop_target_point_choose_table. bcf_row_index_mkm_bindrop_target_point_choose_table = S bcf_predecessor_mkm_bindrop_target_point_choose_table /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_table_decoded_previous_code. bcf_height_mkm_bindrop_target_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_bindrop_target_point_choose_table) = S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table)) * bcf_row_code_scale_mkm_bindrop_target_point_choose) + (bcf_previous_code_mkm_bindrop_target_point_choose_table))) /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_table_decoded_previous_scale. bcf_height_mkm_bindrop_target_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_bindrop_target_point_choose_table) = S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose) + (bcf_previous_scale_mkm_bindrop_target_point_choose_table))) /\ (forall bcf_index_mkm_bindrop_target_point_choose_table_row_step. (exists bcf_lt_gap_mkm_bindrop_target_point_choose_table_row_step_bound. bcf_lt_gap_mkm_bindrop_target_point_choose_table_row_step_bound + S (bcf_index_mkm_bindrop_target_point_choose_table_row_step) = S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) -> exists bcf_value_mkm_bindrop_target_point_choose_table_row_step. ((((exists bcf_height_mkm_bindrop_target_point_choose_table_row_step_entry. bcf_height_mkm_bindrop_target_point_choose_table_row_step_entry + S (bcf_value_mkm_bindrop_target_point_choose_table_row_step) = S ((S (bcf_index_mkm_bindrop_target_point_choose_table_row_step)) * bcf_row_scale_mkm_bindrop_target_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_entry. bcf_row_code_mkm_bindrop_target_point_choose_table = bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_bindrop_target_point_choose_table_row_step)) * bcf_row_scale_mkm_bindrop_target_point_choose_table) + (bcf_value_mkm_bindrop_target_point_choose_table_row_step))) /\ ((bcf_index_mkm_bindrop_target_point_choose_table_row_step = 0 /\ bcf_value_mkm_bindrop_target_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step bcf_left_mkm_bindrop_target_point_choose_table_row_step bcf_right_mkm_bindrop_target_point_choose_table_row_step. bcf_index_mkm_bindrop_target_point_choose_table_row_step = S bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_table_row_step_previous_left. bcf_height_mkm_bindrop_target_point_choose_table_row_step_previous_left + S (bcf_left_mkm_bindrop_target_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_bindrop_target_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_bindrop_target_point_choose_table = bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_bindrop_target_point_choose_table) + (bcf_left_mkm_bindrop_target_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_table_row_step_previous_right. bcf_height_mkm_bindrop_target_point_choose_table_row_step_previous_right + S (bcf_right_mkm_bindrop_target_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_bindrop_target_point_choose_table)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_bindrop_target_point_choose_table = bcf_quotient_mkm_bindrop_target_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_bindrop_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_bindrop_target_point_choose_table) + (bcf_right_mkm_bindrop_target_point_choose_table_row_step))) /\ bcf_value_mkm_bindrop_target_point_choose_table_row_step = bcf_left_mkm_bindrop_target_point_choose_table_row_step + bcf_right_mkm_bindrop_target_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_decoded_row_code. bcf_height_mkm_bindrop_target_point_choose_decoded_row_code + S (bcf_row_code_mkm_bindrop_target_point_choose) = S ((S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) * bcf_row_code_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_decoded_row_code. bcf_row_code_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_decoded_row_code * S ((S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) * bcf_row_code_scale_mkm_bindrop_target_point_choose) + (bcf_row_code_mkm_bindrop_target_point_choose))) /\ ((((exists bcf_height_mkm_bindrop_target_point_choose_decoded_row_scale. bcf_height_mkm_bindrop_target_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_bindrop_target_point_choose) = S ((S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_decoded_row_scale * S ((S (mkm_partial_bindrop_target_point + mkm_value_bindrop_target_point)) * bcf_row_scale_scale_mkm_bindrop_target_point_choose) + (bcf_row_scale_mkm_bindrop_target_point_choose))) /\ (((exists bcf_height_mkm_bindrop_target_point_choose_decoded_value. bcf_height_mkm_bindrop_target_point_choose_decoded_value + S (mkm_factor_bindrop_target_point) = S ((S (mkm_partial_bindrop_target_point)) * bcf_row_scale_mkm_bindrop_target_point_choose)) /\ exists bcf_quotient_mkm_bindrop_target_point_choose_decoded_value. bcf_row_code_mkm_bindrop_target_point_choose = bcf_quotient_mkm_bindrop_target_point_choose_decoded_value * S ((S (mkm_partial_bindrop_target_point)) * bcf_row_scale_mkm_bindrop_target_point_choose) + (mkm_factor_bindrop_target_point))))))))) /\ (((exists fs_h_mkm_bindrop_target_point_factor. fs_h_mkm_bindrop_target_point_factor + S (mkm_factor_bindrop_target_point) = S ((S (mkm_index_bindrop_target)) * cc)) /\ exists fs_q_mkm_bindrop_target_point_factor. cb = fs_q_mkm_bindrop_target_point_factor * S ((S (mkm_index_bindrop_target)) * cc) + (mkm_factor_bindrop_target_point)))))))Complete tactic proof in conservative notation
All 16 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
16 script commands · 2 reading checkpoints · 0 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.