MK000A

multinomial_binomial_prefix_extend

Append one actual binomial factor while preserving every previously coded factor.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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. ∀ a. ∀ u. ∀ C. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l) → BetaAt(b,c,l,a) → BetaAt(sb,sc,l,u) → Choose(u + a,u,C) → ∃ x. ∃ y. MultinomialBinomialPrefix(b,c,sb,sc,x,y,S l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l) · 2Lt(a,b) · 2BetaAt(b,c,i,x) · 8Choose(n,k,z) · 2

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c sb sc cb cc l a u C. (forall mkm_index_binextend_source. (exists mkm_lt_binextend_source_bound. mkm_lt_binextend_source_bound + S (mkm_index_binextend_source) = (l)) -> (exists mkm_value_binextend_source_point mkm_partial_binextend_source_point mkm_factor_binextend_source_point. (((exists fs_h_mkm_binextend_source_point_source. fs_h_mkm_binextend_source_point_source + S (mkm_value_binextend_source_point) = S ((S (mkm_index_binextend_source)) * c)) /\ exists fs_q_mkm_binextend_source_point_source. b = fs_q_mkm_binextend_source_point_source * S ((S (mkm_index_binextend_source)) * c) + (mkm_value_binextend_source_point))) /\ ((((exists fs_h_mkm_binextend_source_point_partial. fs_h_mkm_binextend_source_point_partial + S (mkm_partial_binextend_source_point) = S ((S (mkm_index_binextend_source)) * sc)) /\ exists fs_q_mkm_binextend_source_point_partial. sb = fs_q_mkm_binextend_source_point_partial * S ((S (mkm_index_binextend_source)) * sc) + (mkm_partial_binextend_source_point))) /\ ((((exists bcf_lt_gap_mkm_binextend_source_point_choose_out_of_range. bcf_lt_gap_mkm_binextend_source_point_choose_out_of_range + S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point) = mkm_partial_binextend_source_point) /\ mkm_factor_binextend_source_point = 0) \/ ((exists bcf_le_gap_mkm_binextend_source_point_choose_in_range. bcf_le_gap_mkm_binextend_source_point_choose_in_range + (mkm_partial_binextend_source_point) = mkm_partial_binextend_source_point + mkm_value_binextend_source_point) /\ (exists bcf_row_code_code_mkm_binextend_source_point_choose bcf_row_code_scale_mkm_binextend_source_point_choose bcf_row_scale_code_mkm_binextend_source_point_choose bcf_row_scale_scale_mkm_binextend_source_point_choose bcf_row_code_mkm_binextend_source_point_choose bcf_row_scale_mkm_binextend_source_point_choose. ((forall bcf_row_index_mkm_binextend_source_point_choose_table. (exists bcf_lt_gap_mkm_binextend_source_point_choose_table_row_bound. bcf_lt_gap_mkm_binextend_source_point_choose_table_row_bound + S (bcf_row_index_mkm_binextend_source_point_choose_table) = S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) -> exists bcf_row_code_mkm_binextend_source_point_choose_table bcf_row_scale_mkm_binextend_source_point_choose_table. ((((exists bcf_height_mkm_binextend_source_point_choose_table_decoded_row_code. bcf_height_mkm_binextend_source_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binextend_source_point_choose_table) = S ((S (bcf_row_index_mkm_binextend_source_point_choose_table)) * bcf_row_code_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binextend_source_point_choose_table)) * bcf_row_code_scale_mkm_binextend_source_point_choose) + (bcf_row_code_mkm_binextend_source_point_choose_table))) /\ ((((exists bcf_height_mkm_binextend_source_point_choose_table_decoded_row_scale. bcf_height_mkm_binextend_source_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binextend_source_point_choose_table) = S ((S (bcf_row_index_mkm_binextend_source_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binextend_source_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_source_point_choose) + (bcf_row_scale_mkm_binextend_source_point_choose_table))) /\ ((bcf_row_index_mkm_binextend_source_point_choose_table = 0 /\ (forall bcf_index_mkm_binextend_source_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binextend_source_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binextend_source_point_choose_table_zero_row_bound + S (bcf_index_mkm_binextend_source_point_choose_table_zero_row) = S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) -> exists bcf_value_mkm_binextend_source_point_choose_table_zero_row. ((((exists bcf_height_mkm_binextend_source_point_choose_table_zero_row_entry. bcf_height_mkm_binextend_source_point_choose_table_zero_row_entry + S (bcf_value_mkm_binextend_source_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binextend_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_source_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_zero_row_entry. bcf_row_code_mkm_binextend_source_point_choose_table = bcf_quotient_mkm_binextend_source_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binextend_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_source_point_choose_table) + (bcf_value_mkm_binextend_source_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binextend_source_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binextend_source_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binextend_source_point_choose_table_zero_row. bcf_index_mkm_binextend_source_point_choose_table_zero_row = S bcf_predecessor_mkm_binextend_source_point_choose_table_zero_row /\ bcf_value_mkm_binextend_source_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binextend_source_point_choose_table bcf_previous_code_mkm_binextend_source_point_choose_table bcf_previous_scale_mkm_binextend_source_point_choose_table. bcf_row_index_mkm_binextend_source_point_choose_table = S bcf_predecessor_mkm_binextend_source_point_choose_table /\ ((((exists bcf_height_mkm_binextend_source_point_choose_table_decoded_previous_code. bcf_height_mkm_binextend_source_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binextend_source_point_choose_table) = S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table)) * bcf_row_code_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table)) * bcf_row_code_scale_mkm_binextend_source_point_choose) + (bcf_previous_code_mkm_binextend_source_point_choose_table))) /\ ((((exists bcf_height_mkm_binextend_source_point_choose_table_decoded_previous_scale. bcf_height_mkm_binextend_source_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binextend_source_point_choose_table) = S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_source_point_choose) + (bcf_previous_scale_mkm_binextend_source_point_choose_table))) /\ (forall bcf_index_mkm_binextend_source_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binextend_source_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binextend_source_point_choose_table_row_step_bound + S (bcf_index_mkm_binextend_source_point_choose_table_row_step) = S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) -> exists bcf_value_mkm_binextend_source_point_choose_table_row_step. ((((exists bcf_height_mkm_binextend_source_point_choose_table_row_step_entry. bcf_height_mkm_binextend_source_point_choose_table_row_step_entry + S (bcf_value_mkm_binextend_source_point_choose_table_row_step) = S ((S (bcf_index_mkm_binextend_source_point_choose_table_row_step)) * bcf_row_scale_mkm_binextend_source_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_row_step_entry. bcf_row_code_mkm_binextend_source_point_choose_table = bcf_quotient_mkm_binextend_source_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binextend_source_point_choose_table_row_step)) * bcf_row_scale_mkm_binextend_source_point_choose_table) + (bcf_value_mkm_binextend_source_point_choose_table_row_step))) /\ ((bcf_index_mkm_binextend_source_point_choose_table_row_step = 0 /\ bcf_value_mkm_binextend_source_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binextend_source_point_choose_table_row_step bcf_left_mkm_binextend_source_point_choose_table_row_step bcf_right_mkm_binextend_source_point_choose_table_row_step. bcf_index_mkm_binextend_source_point_choose_table_row_step = S bcf_predecessor_mkm_binextend_source_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binextend_source_point_choose_table_row_step_previous_left. bcf_height_mkm_binextend_source_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binextend_source_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_source_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binextend_source_point_choose_table = bcf_quotient_mkm_binextend_source_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binextend_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_source_point_choose_table) + (bcf_left_mkm_binextend_source_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binextend_source_point_choose_table_row_step_previous_right. bcf_height_mkm_binextend_source_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binextend_source_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binextend_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_source_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binextend_source_point_choose_table = bcf_quotient_mkm_binextend_source_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binextend_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_source_point_choose_table) + (bcf_right_mkm_binextend_source_point_choose_table_row_step))) /\ bcf_value_mkm_binextend_source_point_choose_table_row_step = bcf_left_mkm_binextend_source_point_choose_table_row_step + bcf_right_mkm_binextend_source_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binextend_source_point_choose_decoded_row_code. bcf_height_mkm_binextend_source_point_choose_decoded_row_code + S (bcf_row_code_mkm_binextend_source_point_choose) = S ((S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) * bcf_row_code_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_decoded_row_code. bcf_row_code_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_decoded_row_code * S ((S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) * bcf_row_code_scale_mkm_binextend_source_point_choose) + (bcf_row_code_mkm_binextend_source_point_choose))) /\ ((((exists bcf_height_mkm_binextend_source_point_choose_decoded_row_scale. bcf_height_mkm_binextend_source_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binextend_source_point_choose) = S ((S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) * bcf_row_scale_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_decoded_row_scale * S ((S (mkm_partial_binextend_source_point + mkm_value_binextend_source_point)) * bcf_row_scale_scale_mkm_binextend_source_point_choose) + (bcf_row_scale_mkm_binextend_source_point_choose))) /\ (((exists bcf_height_mkm_binextend_source_point_choose_decoded_value. bcf_height_mkm_binextend_source_point_choose_decoded_value + S (mkm_factor_binextend_source_point) = S ((S (mkm_partial_binextend_source_point)) * bcf_row_scale_mkm_binextend_source_point_choose)) /\ exists bcf_quotient_mkm_binextend_source_point_choose_decoded_value. bcf_row_code_mkm_binextend_source_point_choose = bcf_quotient_mkm_binextend_source_point_choose_decoded_value * S ((S (mkm_partial_binextend_source_point)) * bcf_row_scale_mkm_binextend_source_point_choose) + (mkm_factor_binextend_source_point))))))))) /\ (((exists fs_h_mkm_binextend_source_point_factor. fs_h_mkm_binextend_source_point_factor + S (mkm_factor_binextend_source_point) = S ((S (mkm_index_binextend_source)) * cc)) /\ exists fs_q_mkm_binextend_source_point_factor. cb = fs_q_mkm_binextend_source_point_factor * S ((S (mkm_index_binextend_source)) * cc) + (mkm_factor_binextend_source_point))))))) -> (((exists fs_h_mkm_binextend_a. fs_h_mkm_binextend_a + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_binextend_a. b = fs_q_mkm_binextend_a * S ((S (l)) * c) + (a))) -> (((exists fs_h_mkm_binextend_u. fs_h_mkm_binextend_u + S (u) = S ((S (l)) * sc)) /\ exists fs_q_mkm_binextend_u. sb = fs_q_mkm_binextend_u * S ((S (l)) * sc) + (u))) -> (((exists bcf_lt_gap_mkm_binextend_choose_out_of_range. bcf_lt_gap_mkm_binextend_choose_out_of_range + S (u + a) = u) /\ C = 0) \/ ((exists bcf_le_gap_mkm_binextend_choose_in_range. bcf_le_gap_mkm_binextend_choose_in_range + (u) = u + a) /\ (exists bcf_row_code_code_mkm_binextend_choose bcf_row_code_scale_mkm_binextend_choose bcf_row_scale_code_mkm_binextend_choose bcf_row_scale_scale_mkm_binextend_choose bcf_row_code_mkm_binextend_choose bcf_row_scale_mkm_binextend_choose. ((forall bcf_row_index_mkm_binextend_choose_table. (exists bcf_lt_gap_mkm_binextend_choose_table_row_bound. bcf_lt_gap_mkm_binextend_choose_table_row_bound + S (bcf_row_index_mkm_binextend_choose_table) = S (u + a)) -> exists bcf_row_code_mkm_binextend_choose_table bcf_row_scale_mkm_binextend_choose_table. ((((exists bcf_height_mkm_binextend_choose_table_decoded_row_code. bcf_height_mkm_binextend_choose_table_decoded_row_code + S (bcf_row_code_mkm_binextend_choose_table) = S ((S (bcf_row_index_mkm_binextend_choose_table)) * bcf_row_code_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_table_decoded_row_code. bcf_row_code_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binextend_choose_table)) * bcf_row_code_scale_mkm_binextend_choose) + (bcf_row_code_mkm_binextend_choose_table))) /\ ((((exists bcf_height_mkm_binextend_choose_table_decoded_row_scale. bcf_height_mkm_binextend_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binextend_choose_table) = S ((S (bcf_row_index_mkm_binextend_choose_table)) * bcf_row_scale_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binextend_choose_table)) * bcf_row_scale_scale_mkm_binextend_choose) + (bcf_row_scale_mkm_binextend_choose_table))) /\ ((bcf_row_index_mkm_binextend_choose_table = 0 /\ (forall bcf_index_mkm_binextend_choose_table_zero_row. (exists bcf_lt_gap_mkm_binextend_choose_table_zero_row_bound. bcf_lt_gap_mkm_binextend_choose_table_zero_row_bound + S (bcf_index_mkm_binextend_choose_table_zero_row) = S (u + a)) -> exists bcf_value_mkm_binextend_choose_table_zero_row. ((((exists bcf_height_mkm_binextend_choose_table_zero_row_entry. bcf_height_mkm_binextend_choose_table_zero_row_entry + S (bcf_value_mkm_binextend_choose_table_zero_row) = S ((S (bcf_index_mkm_binextend_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_choose_table)) /\ exists bcf_quotient_mkm_binextend_choose_table_zero_row_entry. bcf_row_code_mkm_binextend_choose_table = bcf_quotient_mkm_binextend_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binextend_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_choose_table) + (bcf_value_mkm_binextend_choose_table_zero_row))) /\ ((bcf_index_mkm_binextend_choose_table_zero_row = 0 /\ bcf_value_mkm_binextend_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binextend_choose_table_zero_row. bcf_index_mkm_binextend_choose_table_zero_row = S bcf_predecessor_mkm_binextend_choose_table_zero_row /\ bcf_value_mkm_binextend_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binextend_choose_table bcf_previous_code_mkm_binextend_choose_table bcf_previous_scale_mkm_binextend_choose_table. bcf_row_index_mkm_binextend_choose_table = S bcf_predecessor_mkm_binextend_choose_table /\ ((((exists bcf_height_mkm_binextend_choose_table_decoded_previous_code. bcf_height_mkm_binextend_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binextend_choose_table) = S ((S (bcf_predecessor_mkm_binextend_choose_table)) * bcf_row_code_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binextend_choose_table)) * bcf_row_code_scale_mkm_binextend_choose) + (bcf_previous_code_mkm_binextend_choose_table))) /\ ((((exists bcf_height_mkm_binextend_choose_table_decoded_previous_scale. bcf_height_mkm_binextend_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binextend_choose_table) = S ((S (bcf_predecessor_mkm_binextend_choose_table)) * bcf_row_scale_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binextend_choose_table)) * bcf_row_scale_scale_mkm_binextend_choose) + (bcf_previous_scale_mkm_binextend_choose_table))) /\ (forall bcf_index_mkm_binextend_choose_table_row_step. (exists bcf_lt_gap_mkm_binextend_choose_table_row_step_bound. bcf_lt_gap_mkm_binextend_choose_table_row_step_bound + S (bcf_index_mkm_binextend_choose_table_row_step) = S (u + a)) -> exists bcf_value_mkm_binextend_choose_table_row_step. ((((exists bcf_height_mkm_binextend_choose_table_row_step_entry. bcf_height_mkm_binextend_choose_table_row_step_entry + S (bcf_value_mkm_binextend_choose_table_row_step) = S ((S (bcf_index_mkm_binextend_choose_table_row_step)) * bcf_row_scale_mkm_binextend_choose_table)) /\ exists bcf_quotient_mkm_binextend_choose_table_row_step_entry. bcf_row_code_mkm_binextend_choose_table = bcf_quotient_mkm_binextend_choose_table_row_step_entry * S ((S (bcf_index_mkm_binextend_choose_table_row_step)) * bcf_row_scale_mkm_binextend_choose_table) + (bcf_value_mkm_binextend_choose_table_row_step))) /\ ((bcf_index_mkm_binextend_choose_table_row_step = 0 /\ bcf_value_mkm_binextend_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binextend_choose_table_row_step bcf_left_mkm_binextend_choose_table_row_step bcf_right_mkm_binextend_choose_table_row_step. bcf_index_mkm_binextend_choose_table_row_step = S bcf_predecessor_mkm_binextend_choose_table_row_step /\ ((((exists bcf_height_mkm_binextend_choose_table_row_step_previous_left. bcf_height_mkm_binextend_choose_table_row_step_previous_left + S (bcf_left_mkm_binextend_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binextend_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_choose_table)) /\ exists bcf_quotient_mkm_binextend_choose_table_row_step_previous_left. bcf_previous_code_mkm_binextend_choose_table = bcf_quotient_mkm_binextend_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binextend_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_choose_table) + (bcf_left_mkm_binextend_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binextend_choose_table_row_step_previous_right. bcf_height_mkm_binextend_choose_table_row_step_previous_right + S (bcf_right_mkm_binextend_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binextend_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_choose_table)) /\ exists bcf_quotient_mkm_binextend_choose_table_row_step_previous_right. bcf_previous_code_mkm_binextend_choose_table = bcf_quotient_mkm_binextend_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binextend_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_choose_table) + (bcf_right_mkm_binextend_choose_table_row_step))) /\ bcf_value_mkm_binextend_choose_table_row_step = bcf_left_mkm_binextend_choose_table_row_step + bcf_right_mkm_binextend_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binextend_choose_decoded_row_code. bcf_height_mkm_binextend_choose_decoded_row_code + S (bcf_row_code_mkm_binextend_choose) = S ((S (u + a)) * bcf_row_code_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_decoded_row_code. bcf_row_code_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_decoded_row_code * S ((S (u + a)) * bcf_row_code_scale_mkm_binextend_choose) + (bcf_row_code_mkm_binextend_choose))) /\ ((((exists bcf_height_mkm_binextend_choose_decoded_row_scale. bcf_height_mkm_binextend_choose_decoded_row_scale + S (bcf_row_scale_mkm_binextend_choose) = S ((S (u + a)) * bcf_row_scale_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_decoded_row_scale. bcf_row_scale_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_decoded_row_scale * S ((S (u + a)) * bcf_row_scale_scale_mkm_binextend_choose) + (bcf_row_scale_mkm_binextend_choose))) /\ (((exists bcf_height_mkm_binextend_choose_decoded_value. bcf_height_mkm_binextend_choose_decoded_value + S (C) = S ((S (u)) * bcf_row_scale_mkm_binextend_choose)) /\ exists bcf_quotient_mkm_binextend_choose_decoded_value. bcf_row_code_mkm_binextend_choose = bcf_quotient_mkm_binextend_choose_decoded_value * S ((S (u)) * bcf_row_scale_mkm_binextend_choose) + (C))))))))) -> exists nb nc. (forall mkm_index_binextend_target. (exists mkm_lt_binextend_target_bound. mkm_lt_binextend_target_bound + S (mkm_index_binextend_target) = (S l)) -> (exists mkm_value_binextend_target_point mkm_partial_binextend_target_point mkm_factor_binextend_target_point. (((exists fs_h_mkm_binextend_target_point_source. fs_h_mkm_binextend_target_point_source + S (mkm_value_binextend_target_point) = S ((S (mkm_index_binextend_target)) * c)) /\ exists fs_q_mkm_binextend_target_point_source. b = fs_q_mkm_binextend_target_point_source * S ((S (mkm_index_binextend_target)) * c) + (mkm_value_binextend_target_point))) /\ ((((exists fs_h_mkm_binextend_target_point_partial. fs_h_mkm_binextend_target_point_partial + S (mkm_partial_binextend_target_point) = S ((S (mkm_index_binextend_target)) * sc)) /\ exists fs_q_mkm_binextend_target_point_partial. sb = fs_q_mkm_binextend_target_point_partial * S ((S (mkm_index_binextend_target)) * sc) + (mkm_partial_binextend_target_point))) /\ ((((exists bcf_lt_gap_mkm_binextend_target_point_choose_out_of_range. bcf_lt_gap_mkm_binextend_target_point_choose_out_of_range + S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point) = mkm_partial_binextend_target_point) /\ mkm_factor_binextend_target_point = 0) \/ ((exists bcf_le_gap_mkm_binextend_target_point_choose_in_range. bcf_le_gap_mkm_binextend_target_point_choose_in_range + (mkm_partial_binextend_target_point) = mkm_partial_binextend_target_point + mkm_value_binextend_target_point) /\ (exists bcf_row_code_code_mkm_binextend_target_point_choose bcf_row_code_scale_mkm_binextend_target_point_choose bcf_row_scale_code_mkm_binextend_target_point_choose bcf_row_scale_scale_mkm_binextend_target_point_choose bcf_row_code_mkm_binextend_target_point_choose bcf_row_scale_mkm_binextend_target_point_choose. ((forall bcf_row_index_mkm_binextend_target_point_choose_table. (exists bcf_lt_gap_mkm_binextend_target_point_choose_table_row_bound. bcf_lt_gap_mkm_binextend_target_point_choose_table_row_bound + S (bcf_row_index_mkm_binextend_target_point_choose_table) = S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) -> exists bcf_row_code_mkm_binextend_target_point_choose_table bcf_row_scale_mkm_binextend_target_point_choose_table. ((((exists bcf_height_mkm_binextend_target_point_choose_table_decoded_row_code. bcf_height_mkm_binextend_target_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binextend_target_point_choose_table) = S ((S (bcf_row_index_mkm_binextend_target_point_choose_table)) * bcf_row_code_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binextend_target_point_choose_table)) * bcf_row_code_scale_mkm_binextend_target_point_choose) + (bcf_row_code_mkm_binextend_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binextend_target_point_choose_table_decoded_row_scale. bcf_height_mkm_binextend_target_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binextend_target_point_choose_table) = S ((S (bcf_row_index_mkm_binextend_target_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binextend_target_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_target_point_choose) + (bcf_row_scale_mkm_binextend_target_point_choose_table))) /\ ((bcf_row_index_mkm_binextend_target_point_choose_table = 0 /\ (forall bcf_index_mkm_binextend_target_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binextend_target_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binextend_target_point_choose_table_zero_row_bound + S (bcf_index_mkm_binextend_target_point_choose_table_zero_row) = S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) -> exists bcf_value_mkm_binextend_target_point_choose_table_zero_row. ((((exists bcf_height_mkm_binextend_target_point_choose_table_zero_row_entry. bcf_height_mkm_binextend_target_point_choose_table_zero_row_entry + S (bcf_value_mkm_binextend_target_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binextend_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_target_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_zero_row_entry. bcf_row_code_mkm_binextend_target_point_choose_table = bcf_quotient_mkm_binextend_target_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binextend_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binextend_target_point_choose_table) + (bcf_value_mkm_binextend_target_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binextend_target_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binextend_target_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binextend_target_point_choose_table_zero_row. bcf_index_mkm_binextend_target_point_choose_table_zero_row = S bcf_predecessor_mkm_binextend_target_point_choose_table_zero_row /\ bcf_value_mkm_binextend_target_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binextend_target_point_choose_table bcf_previous_code_mkm_binextend_target_point_choose_table bcf_previous_scale_mkm_binextend_target_point_choose_table. bcf_row_index_mkm_binextend_target_point_choose_table = S bcf_predecessor_mkm_binextend_target_point_choose_table /\ ((((exists bcf_height_mkm_binextend_target_point_choose_table_decoded_previous_code. bcf_height_mkm_binextend_target_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binextend_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table)) * bcf_row_code_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table)) * bcf_row_code_scale_mkm_binextend_target_point_choose) + (bcf_previous_code_mkm_binextend_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binextend_target_point_choose_table_decoded_previous_scale. bcf_height_mkm_binextend_target_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binextend_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table)) * bcf_row_scale_scale_mkm_binextend_target_point_choose) + (bcf_previous_scale_mkm_binextend_target_point_choose_table))) /\ (forall bcf_index_mkm_binextend_target_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binextend_target_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binextend_target_point_choose_table_row_step_bound + S (bcf_index_mkm_binextend_target_point_choose_table_row_step) = S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) -> exists bcf_value_mkm_binextend_target_point_choose_table_row_step. ((((exists bcf_height_mkm_binextend_target_point_choose_table_row_step_entry. bcf_height_mkm_binextend_target_point_choose_table_row_step_entry + S (bcf_value_mkm_binextend_target_point_choose_table_row_step) = S ((S (bcf_index_mkm_binextend_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binextend_target_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_row_step_entry. bcf_row_code_mkm_binextend_target_point_choose_table = bcf_quotient_mkm_binextend_target_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binextend_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binextend_target_point_choose_table) + (bcf_value_mkm_binextend_target_point_choose_table_row_step))) /\ ((bcf_index_mkm_binextend_target_point_choose_table_row_step = 0 /\ bcf_value_mkm_binextend_target_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binextend_target_point_choose_table_row_step bcf_left_mkm_binextend_target_point_choose_table_row_step bcf_right_mkm_binextend_target_point_choose_table_row_step. bcf_index_mkm_binextend_target_point_choose_table_row_step = S bcf_predecessor_mkm_binextend_target_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binextend_target_point_choose_table_row_step_previous_left. bcf_height_mkm_binextend_target_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binextend_target_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_target_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binextend_target_point_choose_table = bcf_quotient_mkm_binextend_target_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binextend_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binextend_target_point_choose_table) + (bcf_left_mkm_binextend_target_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binextend_target_point_choose_table_row_step_previous_right. bcf_height_mkm_binextend_target_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binextend_target_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binextend_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_target_point_choose_table)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binextend_target_point_choose_table = bcf_quotient_mkm_binextend_target_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binextend_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binextend_target_point_choose_table) + (bcf_right_mkm_binextend_target_point_choose_table_row_step))) /\ bcf_value_mkm_binextend_target_point_choose_table_row_step = bcf_left_mkm_binextend_target_point_choose_table_row_step + bcf_right_mkm_binextend_target_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binextend_target_point_choose_decoded_row_code. bcf_height_mkm_binextend_target_point_choose_decoded_row_code + S (bcf_row_code_mkm_binextend_target_point_choose) = S ((S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) * bcf_row_code_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_decoded_row_code. bcf_row_code_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_decoded_row_code * S ((S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) * bcf_row_code_scale_mkm_binextend_target_point_choose) + (bcf_row_code_mkm_binextend_target_point_choose))) /\ ((((exists bcf_height_mkm_binextend_target_point_choose_decoded_row_scale. bcf_height_mkm_binextend_target_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binextend_target_point_choose) = S ((S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) * bcf_row_scale_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_decoded_row_scale * S ((S (mkm_partial_binextend_target_point + mkm_value_binextend_target_point)) * bcf_row_scale_scale_mkm_binextend_target_point_choose) + (bcf_row_scale_mkm_binextend_target_point_choose))) /\ (((exists bcf_height_mkm_binextend_target_point_choose_decoded_value. bcf_height_mkm_binextend_target_point_choose_decoded_value + S (mkm_factor_binextend_target_point) = S ((S (mkm_partial_binextend_target_point)) * bcf_row_scale_mkm_binextend_target_point_choose)) /\ exists bcf_quotient_mkm_binextend_target_point_choose_decoded_value. bcf_row_code_mkm_binextend_target_point_choose = bcf_quotient_mkm_binextend_target_point_choose_decoded_value * S ((S (mkm_partial_binextend_target_point)) * bcf_row_scale_mkm_binextend_target_point_choose) + (mkm_factor_binextend_target_point))))))))) /\ (((exists fs_h_mkm_binextend_target_point_factor. fs_h_mkm_binextend_target_point_factor + S (mkm_factor_binextend_target_point) = S ((S (mkm_index_binextend_target)) * nc)) /\ exists fs_q_mkm_binextend_target_point_factor. nb = fs_q_mkm_binextend_target_point_factor * S ((S (mkm_index_binextend_target)) * nc) + (mkm_factor_binextend_target_point)))))))

Complete tactic proof in conservative notation

All 76 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

76 script commands · 28 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro cb
  6. L6
    intro cc
  7. L7
    intro l
  8. L8
    intro a
  9. L9
    intro u
  10. L10
    intro C
02Fix variables and assumptionsL11–14

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

  1. L11
    intro h
  2. L12
    intro ha
  3. L13
    intro hu
  4. L14
    intro hC
03Establish hextL15–20

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

  1. L15
    have hext : ∃ nb. ∃ nc. BetaAt(nb,nc,l,C) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(cb,cc,x,y) → BetaAt(nb,nc,x,y))Definitions: BetaAt(nb,nc,l,C)Lt(x,l)BetaAt(cb,cc,x,y)BetaAt(nb,nc,x,y)Original native command in the exact edition
  2. L16
    specialize beta_prefix_extend l
  3. L17
    specialize beta_prefix_extend cb
  4. L18
    specialize beta_prefix_extend cc
  5. L19
    specialize beta_prefix_extend C
  6. L20
    apply beta_prefix_extend
04Separate the logical casesL21–23

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

  1. L21
    cases hext
  2. L22
    cases hext_witness
  3. L23
    cases hext_witness_witness
05Construct an explicit witnessL24–25

Supply the displayed value, then prove that it has the required property.

  1. L24
    exists x
  2. L25
    exists x1
06Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
07Establish hsplitL28–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L28
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L29
    specialize le_eq_or_lt i
  3. L30
    specialize le_eq_or_lt l
  4. L31
    apply le_eq_or_lt
  5. L32
    specialize le_of_succ_le_succ i
  6. L33
    specialize le_of_succ_le_succ l
  7. L34
    apply le_of_succ_le_succ
  8. L35
    exact hi
08Separate the logical casesL36–36

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

  1. L36
    cases hsplit
09Construct an explicit witnessL37–39

Supply the displayed value, then prove that it has the required property.

  1. L37
    exists a
  2. L38
    exists u
  3. L39
    exists C
10Separate the logical casesL40–40

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

  1. L40
    split
11Calculate and transport equalitiesL41–42

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

  1. L41
    rewrite hsplit_left
  2. L42
    rewrite hsplit_left
12Use earlier factsL43–43

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

  1. L43
    exact ha
13Separate the logical casesL44–44

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

  1. L44
    split
14Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite hsplit_left
  2. L46
    rewrite hsplit_left
15Use earlier factsL47–47

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

  1. L47
    exact hu
16Separate the logical casesL48–48

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

  1. L48
    split
17Use earlier factsL49–49

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

  1. L49
    exact hC
18Calculate and transport equalitiesL50–51

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

  1. L50
    rewrite hsplit_left
  2. L51
    rewrite hsplit_left
19Use earlier factsL52–52

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

  1. L52
    exact hext_witness_witness_left
20Establish hpointL53–56

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

  1. L53
    have hpoint : ∃ mkm_value_binextend_point. ∃ mkm_partial_binextend_point. ∃ mkm_factor_binextend_point. BetaAt(b,c,i,mkm_value_binextend_point) ∧ (BetaAt(sb,sc,i,mkm_partial_binextend_point) ∧ (Choose(mkm_partial_binextend_point + mkm_value_binextend_point,mkm_partial_binextend_point,mkm_factor_binextend_point) ∧ BetaAt(cb,cc,i,mkm_factor_binextend_point)))Definitions: BetaAt(b,c,i,mkm_value_binextend_point)BetaAt(sb,sc,i,mkm_partial_binextend_point)Choose(mkm_partial_binextend_point + mkm_value_binextend_point,mkm_partial_binextend_point,mkm_factor_binextend_point)BetaAt(cb,cc,i,mkm_factor_binextend_point)Original native command in the exact edition
  2. L54
    specialize h i
  3. L55
    apply h
  4. L56
    exact hsplit_right
21Separate the logical casesL57–62

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

  1. L57
    cases hpoint
  2. L58
    cases hpoint_witness
  3. L59
    cases hpoint_witness_witness
  4. L60
    cases hpoint_witness_witness_witness
  5. L61
    cases hpoint_witness_witness_witness_right
  6. L62
    cases hpoint_witness_witness_witness_right_right
22Construct an explicit witnessL63–65

Supply the displayed value, then prove that it has the required property.

  1. L63
    exists x2
  2. L64
    exists x3
  3. L65
    exists x4
23Separate the logical casesL66–66

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

  1. L66
    split
24Use earlier factsL67–67

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

  1. L67
    exact hpoint_witness_witness_witness_left
25Separate the logical casesL68–68

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

  1. L68
    split
26Use earlier factsL69–69

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

  1. L69
    exact hpoint_witness_witness_witness_right_left
27Separate the logical casesL70–70

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

  1. L70
    split
28Use earlier factsL71–76

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

  1. L71
    exact hpoint_witness_witness_witness_right_right_left
  2. L72
    specialize hext_witness_witness_right i
  3. L73
    specialize hext_witness_witness_right x4
  4. L74
    apply hext_witness_witness_right
  5. L75
    exact hsplit_right
  6. L76
    exact hpoint_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro cb
  6. 0006intro cc
  7. 0007intro l
  8. 0008intro a
  9. 0009intro u
  10. 0010intro C
  11. 0011intro h
  12. 0012intro ha
  13. 0013intro hu
  14. 0014intro hC
  15. 0015have hext : ∃ nb. ∃ nc. BetaAt(nb,nc,l,C) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(cb,cc,x,y) → BetaAt(nb,nc,x,y))
  16. 0016specialize beta_prefix_extend l
  17. 0017specialize beta_prefix_extend cb
  18. 0018specialize beta_prefix_extend cc
  19. 0019specialize beta_prefix_extend C
  20. 0020apply beta_prefix_extend
  21. 0021cases hext
  22. 0022cases hext_witness
  23. 0023cases hext_witness_witness
  24. 0024exists x
  25. 0025exists x1
  26. 0026intro i
  27. 0027intro hi
  28. 0028have hsplit : i = l ∨ Lt(i,l)
  29. 0029specialize le_eq_or_lt i
  30. 0030specialize le_eq_or_lt l
  31. 0031apply le_eq_or_lt
  32. 0032specialize le_of_succ_le_succ i
  33. 0033specialize le_of_succ_le_succ l
  34. 0034apply le_of_succ_le_succ
  35. 0035exact hi
  36. 0036cases hsplit
  37. 0037exists a
  38. 0038exists u
  39. 0039exists C
  40. 0040split
  41. 0041rewrite hsplit_left
  42. 0042rewrite hsplit_left
  43. 0043exact ha
  44. 0044split
  45. 0045rewrite hsplit_left
  46. 0046rewrite hsplit_left
  47. 0047exact hu
  48. 0048split
  49. 0049exact hC
  50. 0050rewrite hsplit_left
  51. 0051rewrite hsplit_left
  52. 0052exact hext_witness_witness_left
  53. 0053have hpoint : ∃ mkm_value_binextend_point. ∃ mkm_partial_binextend_point. ∃ mkm_factor_binextend_point. BetaAt(b,c,i,mkm_value_binextend_point) ∧ (BetaAt(sb,sc,i,mkm_partial_binextend_point) ∧ (Choose(mkm_partial_binextend_point + mkm_value_binextend_point,mkm_partial_binextend_point,mkm_factor_binextend_point) ∧ BetaAt(cb,cc,i,mkm_factor_binextend_point)))
  54. 0054specialize h i
  55. 0055apply h
  56. 0056exact hsplit_right
  57. 0057cases hpoint
  58. 0058cases hpoint_witness
  59. 0059cases hpoint_witness_witness
  60. 0060cases hpoint_witness_witness_witness
  61. 0061cases hpoint_witness_witness_witness_right
  62. 0062cases hpoint_witness_witness_witness_right_right
  63. 0063exists x2
  64. 0064exists x3
  65. 0065exists x4
  66. 0066split
  67. 0067exact hpoint_witness_witness_witness_left
  68. 0068split
  69. 0069exact hpoint_witness_witness_witness_right_left
  70. 0070split
  71. 0071exact hpoint_witness_witness_witness_right_right_left
  72. 0072specialize hext_witness_witness_right i
  73. 0073specialize hext_witness_witness_right x4
  74. 0074apply hext_witness_witness_right
  75. 0075exact hsplit_right
  76. 0076exact hpoint_witness_witness_witness_right_right_right