BT00TJ · Bertrand theorem

choose_succ_succ

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

Relational Choose values satisfy Pascal recurrence everywhere.

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

Statement with defined notation

∀ n. ∀ k. ∀ x. ∀ y. ∀ z. Choose(n,k,x) → Choose(n,S k,y) → Choose(S n,S k,z) → z = x + y

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0041 Choose

3 occurrences

In local proof propositions

PD0002 Lt

3 occurrences

Exact expanded native-PA statement
forall n k x y z. (((exists bcf_lt_gap_bcss_left_out_of_range. bcf_lt_gap_bcss_left_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bcss_left_in_range. bcf_le_gap_bcss_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcss_left bcf_row_code_scale_bcss_left bcf_row_scale_code_bcss_left bcf_row_scale_scale_bcss_left bcf_row_code_bcss_left bcf_row_scale_bcss_left. ((forall bcf_row_index_bcss_left_table. (exists bcf_lt_gap_bcss_left_table_row_bound. bcf_lt_gap_bcss_left_table_row_bound + S (bcf_row_index_bcss_left_table) = S (n)) -> exists bcf_row_code_bcss_left_table bcf_row_scale_bcss_left_table. ((((exists bcf_height_bcss_left_table_decoded_row_code. bcf_height_bcss_left_table_decoded_row_code + S (bcf_row_code_bcss_left_table) = S ((S (bcf_row_index_bcss_left_table)) * bcf_row_code_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_table_decoded_row_code. bcf_row_code_code_bcss_left = bcf_quotient_bcss_left_table_decoded_row_code * S ((S (bcf_row_index_bcss_left_table)) * bcf_row_code_scale_bcss_left) + (bcf_row_code_bcss_left_table))) /\ ((((exists bcf_height_bcss_left_table_decoded_row_scale. bcf_height_bcss_left_table_decoded_row_scale + S (bcf_row_scale_bcss_left_table) = S ((S (bcf_row_index_bcss_left_table)) * bcf_row_scale_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_table_decoded_row_scale. bcf_row_scale_code_bcss_left = bcf_quotient_bcss_left_table_decoded_row_scale * S ((S (bcf_row_index_bcss_left_table)) * bcf_row_scale_scale_bcss_left) + (bcf_row_scale_bcss_left_table))) /\ ((bcf_row_index_bcss_left_table = 0 /\ (forall bcf_index_bcss_left_table_zero_row. (exists bcf_lt_gap_bcss_left_table_zero_row_bound. bcf_lt_gap_bcss_left_table_zero_row_bound + S (bcf_index_bcss_left_table_zero_row) = S (n)) -> exists bcf_value_bcss_left_table_zero_row. ((((exists bcf_height_bcss_left_table_zero_row_entry. bcf_height_bcss_left_table_zero_row_entry + S (bcf_value_bcss_left_table_zero_row) = S ((S (bcf_index_bcss_left_table_zero_row)) * bcf_row_scale_bcss_left_table)) /\ exists bcf_quotient_bcss_left_table_zero_row_entry. bcf_row_code_bcss_left_table = bcf_quotient_bcss_left_table_zero_row_entry * S ((S (bcf_index_bcss_left_table_zero_row)) * bcf_row_scale_bcss_left_table) + (bcf_value_bcss_left_table_zero_row))) /\ ((bcf_index_bcss_left_table_zero_row = 0 /\ bcf_value_bcss_left_table_zero_row = 1) \/ exists bcf_predecessor_bcss_left_table_zero_row. bcf_index_bcss_left_table_zero_row = S bcf_predecessor_bcss_left_table_zero_row /\ bcf_value_bcss_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcss_left_table bcf_previous_code_bcss_left_table bcf_previous_scale_bcss_left_table. bcf_row_index_bcss_left_table = S bcf_predecessor_bcss_left_table /\ ((((exists bcf_height_bcss_left_table_decoded_previous_code. bcf_height_bcss_left_table_decoded_previous_code + S (bcf_previous_code_bcss_left_table) = S ((S (bcf_predecessor_bcss_left_table)) * bcf_row_code_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_table_decoded_previous_code. bcf_row_code_code_bcss_left = bcf_quotient_bcss_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcss_left_table)) * bcf_row_code_scale_bcss_left) + (bcf_previous_code_bcss_left_table))) /\ ((((exists bcf_height_bcss_left_table_decoded_previous_scale. bcf_height_bcss_left_table_decoded_previous_scale + S (bcf_previous_scale_bcss_left_table) = S ((S (bcf_predecessor_bcss_left_table)) * bcf_row_scale_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_table_decoded_previous_scale. bcf_row_scale_code_bcss_left = bcf_quotient_bcss_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcss_left_table)) * bcf_row_scale_scale_bcss_left) + (bcf_previous_scale_bcss_left_table))) /\ (forall bcf_index_bcss_left_table_row_step. (exists bcf_lt_gap_bcss_left_table_row_step_bound. bcf_lt_gap_bcss_left_table_row_step_bound + S (bcf_index_bcss_left_table_row_step) = S (n)) -> exists bcf_value_bcss_left_table_row_step. ((((exists bcf_height_bcss_left_table_row_step_entry. bcf_height_bcss_left_table_row_step_entry + S (bcf_value_bcss_left_table_row_step) = S ((S (bcf_index_bcss_left_table_row_step)) * bcf_row_scale_bcss_left_table)) /\ exists bcf_quotient_bcss_left_table_row_step_entry. bcf_row_code_bcss_left_table = bcf_quotient_bcss_left_table_row_step_entry * S ((S (bcf_index_bcss_left_table_row_step)) * bcf_row_scale_bcss_left_table) + (bcf_value_bcss_left_table_row_step))) /\ ((bcf_index_bcss_left_table_row_step = 0 /\ bcf_value_bcss_left_table_row_step = 1) \/ exists bcf_predecessor_bcss_left_table_row_step bcf_left_bcss_left_table_row_step bcf_right_bcss_left_table_row_step. bcf_index_bcss_left_table_row_step = S bcf_predecessor_bcss_left_table_row_step /\ ((((exists bcf_height_bcss_left_table_row_step_previous_left. bcf_height_bcss_left_table_row_step_previous_left + S (bcf_left_bcss_left_table_row_step) = S ((S (bcf_predecessor_bcss_left_table_row_step)) * bcf_previous_scale_bcss_left_table)) /\ exists bcf_quotient_bcss_left_table_row_step_previous_left. bcf_previous_code_bcss_left_table = bcf_quotient_bcss_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcss_left_table_row_step)) * bcf_previous_scale_bcss_left_table) + (bcf_left_bcss_left_table_row_step))) /\ ((((exists bcf_height_bcss_left_table_row_step_previous_right. bcf_height_bcss_left_table_row_step_previous_right + S (bcf_right_bcss_left_table_row_step) = S ((S (S (bcf_predecessor_bcss_left_table_row_step))) * bcf_previous_scale_bcss_left_table)) /\ exists bcf_quotient_bcss_left_table_row_step_previous_right. bcf_previous_code_bcss_left_table = bcf_quotient_bcss_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcss_left_table_row_step))) * bcf_previous_scale_bcss_left_table) + (bcf_right_bcss_left_table_row_step))) /\ bcf_value_bcss_left_table_row_step = bcf_left_bcss_left_table_row_step + bcf_right_bcss_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcss_left_decoded_row_code. bcf_height_bcss_left_decoded_row_code + S (bcf_row_code_bcss_left) = S ((S (n)) * bcf_row_code_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_decoded_row_code. bcf_row_code_code_bcss_left = bcf_quotient_bcss_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcss_left) + (bcf_row_code_bcss_left))) /\ ((((exists bcf_height_bcss_left_decoded_row_scale. bcf_height_bcss_left_decoded_row_scale + S (bcf_row_scale_bcss_left) = S ((S (n)) * bcf_row_scale_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_decoded_row_scale. bcf_row_scale_code_bcss_left = bcf_quotient_bcss_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcss_left) + (bcf_row_scale_bcss_left))) /\ (((exists bcf_height_bcss_left_decoded_value. bcf_height_bcss_left_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bcss_left)) /\ exists bcf_quotient_bcss_left_decoded_value. bcf_row_code_bcss_left = bcf_quotient_bcss_left_decoded_value * S ((S (k)) * bcf_row_scale_bcss_left) + (x))))))))) -> (((exists bcf_lt_gap_bcss_right_out_of_range. bcf_lt_gap_bcss_right_out_of_range + S (n) = S k) /\ y = 0) \/ ((exists bcf_le_gap_bcss_right_in_range. bcf_le_gap_bcss_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcss_right bcf_row_code_scale_bcss_right bcf_row_scale_code_bcss_right bcf_row_scale_scale_bcss_right bcf_row_code_bcss_right bcf_row_scale_bcss_right. ((forall bcf_row_index_bcss_right_table. (exists bcf_lt_gap_bcss_right_table_row_bound. bcf_lt_gap_bcss_right_table_row_bound + S (bcf_row_index_bcss_right_table) = S (n)) -> exists bcf_row_code_bcss_right_table bcf_row_scale_bcss_right_table. ((((exists bcf_height_bcss_right_table_decoded_row_code. bcf_height_bcss_right_table_decoded_row_code + S (bcf_row_code_bcss_right_table) = S ((S (bcf_row_index_bcss_right_table)) * bcf_row_code_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_table_decoded_row_code. bcf_row_code_code_bcss_right = bcf_quotient_bcss_right_table_decoded_row_code * S ((S (bcf_row_index_bcss_right_table)) * bcf_row_code_scale_bcss_right) + (bcf_row_code_bcss_right_table))) /\ ((((exists bcf_height_bcss_right_table_decoded_row_scale. bcf_height_bcss_right_table_decoded_row_scale + S (bcf_row_scale_bcss_right_table) = S ((S (bcf_row_index_bcss_right_table)) * bcf_row_scale_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_table_decoded_row_scale. bcf_row_scale_code_bcss_right = bcf_quotient_bcss_right_table_decoded_row_scale * S ((S (bcf_row_index_bcss_right_table)) * bcf_row_scale_scale_bcss_right) + (bcf_row_scale_bcss_right_table))) /\ ((bcf_row_index_bcss_right_table = 0 /\ (forall bcf_index_bcss_right_table_zero_row. (exists bcf_lt_gap_bcss_right_table_zero_row_bound. bcf_lt_gap_bcss_right_table_zero_row_bound + S (bcf_index_bcss_right_table_zero_row) = S (n)) -> exists bcf_value_bcss_right_table_zero_row. ((((exists bcf_height_bcss_right_table_zero_row_entry. bcf_height_bcss_right_table_zero_row_entry + S (bcf_value_bcss_right_table_zero_row) = S ((S (bcf_index_bcss_right_table_zero_row)) * bcf_row_scale_bcss_right_table)) /\ exists bcf_quotient_bcss_right_table_zero_row_entry. bcf_row_code_bcss_right_table = bcf_quotient_bcss_right_table_zero_row_entry * S ((S (bcf_index_bcss_right_table_zero_row)) * bcf_row_scale_bcss_right_table) + (bcf_value_bcss_right_table_zero_row))) /\ ((bcf_index_bcss_right_table_zero_row = 0 /\ bcf_value_bcss_right_table_zero_row = 1) \/ exists bcf_predecessor_bcss_right_table_zero_row. bcf_index_bcss_right_table_zero_row = S bcf_predecessor_bcss_right_table_zero_row /\ bcf_value_bcss_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcss_right_table bcf_previous_code_bcss_right_table bcf_previous_scale_bcss_right_table. bcf_row_index_bcss_right_table = S bcf_predecessor_bcss_right_table /\ ((((exists bcf_height_bcss_right_table_decoded_previous_code. bcf_height_bcss_right_table_decoded_previous_code + S (bcf_previous_code_bcss_right_table) = S ((S (bcf_predecessor_bcss_right_table)) * bcf_row_code_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_table_decoded_previous_code. bcf_row_code_code_bcss_right = bcf_quotient_bcss_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcss_right_table)) * bcf_row_code_scale_bcss_right) + (bcf_previous_code_bcss_right_table))) /\ ((((exists bcf_height_bcss_right_table_decoded_previous_scale. bcf_height_bcss_right_table_decoded_previous_scale + S (bcf_previous_scale_bcss_right_table) = S ((S (bcf_predecessor_bcss_right_table)) * bcf_row_scale_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_table_decoded_previous_scale. bcf_row_scale_code_bcss_right = bcf_quotient_bcss_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcss_right_table)) * bcf_row_scale_scale_bcss_right) + (bcf_previous_scale_bcss_right_table))) /\ (forall bcf_index_bcss_right_table_row_step. (exists bcf_lt_gap_bcss_right_table_row_step_bound. bcf_lt_gap_bcss_right_table_row_step_bound + S (bcf_index_bcss_right_table_row_step) = S (n)) -> exists bcf_value_bcss_right_table_row_step. ((((exists bcf_height_bcss_right_table_row_step_entry. bcf_height_bcss_right_table_row_step_entry + S (bcf_value_bcss_right_table_row_step) = S ((S (bcf_index_bcss_right_table_row_step)) * bcf_row_scale_bcss_right_table)) /\ exists bcf_quotient_bcss_right_table_row_step_entry. bcf_row_code_bcss_right_table = bcf_quotient_bcss_right_table_row_step_entry * S ((S (bcf_index_bcss_right_table_row_step)) * bcf_row_scale_bcss_right_table) + (bcf_value_bcss_right_table_row_step))) /\ ((bcf_index_bcss_right_table_row_step = 0 /\ bcf_value_bcss_right_table_row_step = 1) \/ exists bcf_predecessor_bcss_right_table_row_step bcf_left_bcss_right_table_row_step bcf_right_bcss_right_table_row_step. bcf_index_bcss_right_table_row_step = S bcf_predecessor_bcss_right_table_row_step /\ ((((exists bcf_height_bcss_right_table_row_step_previous_left. bcf_height_bcss_right_table_row_step_previous_left + S (bcf_left_bcss_right_table_row_step) = S ((S (bcf_predecessor_bcss_right_table_row_step)) * bcf_previous_scale_bcss_right_table)) /\ exists bcf_quotient_bcss_right_table_row_step_previous_left. bcf_previous_code_bcss_right_table = bcf_quotient_bcss_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcss_right_table_row_step)) * bcf_previous_scale_bcss_right_table) + (bcf_left_bcss_right_table_row_step))) /\ ((((exists bcf_height_bcss_right_table_row_step_previous_right. bcf_height_bcss_right_table_row_step_previous_right + S (bcf_right_bcss_right_table_row_step) = S ((S (S (bcf_predecessor_bcss_right_table_row_step))) * bcf_previous_scale_bcss_right_table)) /\ exists bcf_quotient_bcss_right_table_row_step_previous_right. bcf_previous_code_bcss_right_table = bcf_quotient_bcss_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcss_right_table_row_step))) * bcf_previous_scale_bcss_right_table) + (bcf_right_bcss_right_table_row_step))) /\ bcf_value_bcss_right_table_row_step = bcf_left_bcss_right_table_row_step + bcf_right_bcss_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcss_right_decoded_row_code. bcf_height_bcss_right_decoded_row_code + S (bcf_row_code_bcss_right) = S ((S (n)) * bcf_row_code_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_decoded_row_code. bcf_row_code_code_bcss_right = bcf_quotient_bcss_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcss_right) + (bcf_row_code_bcss_right))) /\ ((((exists bcf_height_bcss_right_decoded_row_scale. bcf_height_bcss_right_decoded_row_scale + S (bcf_row_scale_bcss_right) = S ((S (n)) * bcf_row_scale_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_decoded_row_scale. bcf_row_scale_code_bcss_right = bcf_quotient_bcss_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcss_right) + (bcf_row_scale_bcss_right))) /\ (((exists bcf_height_bcss_right_decoded_value. bcf_height_bcss_right_decoded_value + S (y) = S ((S (S k)) * bcf_row_scale_bcss_right)) /\ exists bcf_quotient_bcss_right_decoded_value. bcf_row_code_bcss_right = bcf_quotient_bcss_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcss_right) + (y))))))))) -> (((exists bcf_lt_gap_bcss_result_out_of_range. bcf_lt_gap_bcss_result_out_of_range + S (S n) = S k) /\ z = 0) \/ ((exists bcf_le_gap_bcss_result_in_range. bcf_le_gap_bcss_result_in_range + (S k) = S n) /\ (exists bcf_row_code_code_bcss_result bcf_row_code_scale_bcss_result bcf_row_scale_code_bcss_result bcf_row_scale_scale_bcss_result bcf_row_code_bcss_result bcf_row_scale_bcss_result. ((forall bcf_row_index_bcss_result_table. (exists bcf_lt_gap_bcss_result_table_row_bound. bcf_lt_gap_bcss_result_table_row_bound + S (bcf_row_index_bcss_result_table) = S (S n)) -> exists bcf_row_code_bcss_result_table bcf_row_scale_bcss_result_table. ((((exists bcf_height_bcss_result_table_decoded_row_code. bcf_height_bcss_result_table_decoded_row_code + S (bcf_row_code_bcss_result_table) = S ((S (bcf_row_index_bcss_result_table)) * bcf_row_code_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_table_decoded_row_code. bcf_row_code_code_bcss_result = bcf_quotient_bcss_result_table_decoded_row_code * S ((S (bcf_row_index_bcss_result_table)) * bcf_row_code_scale_bcss_result) + (bcf_row_code_bcss_result_table))) /\ ((((exists bcf_height_bcss_result_table_decoded_row_scale. bcf_height_bcss_result_table_decoded_row_scale + S (bcf_row_scale_bcss_result_table) = S ((S (bcf_row_index_bcss_result_table)) * bcf_row_scale_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_table_decoded_row_scale. bcf_row_scale_code_bcss_result = bcf_quotient_bcss_result_table_decoded_row_scale * S ((S (bcf_row_index_bcss_result_table)) * bcf_row_scale_scale_bcss_result) + (bcf_row_scale_bcss_result_table))) /\ ((bcf_row_index_bcss_result_table = 0 /\ (forall bcf_index_bcss_result_table_zero_row. (exists bcf_lt_gap_bcss_result_table_zero_row_bound. bcf_lt_gap_bcss_result_table_zero_row_bound + S (bcf_index_bcss_result_table_zero_row) = S (S n)) -> exists bcf_value_bcss_result_table_zero_row. ((((exists bcf_height_bcss_result_table_zero_row_entry. bcf_height_bcss_result_table_zero_row_entry + S (bcf_value_bcss_result_table_zero_row) = S ((S (bcf_index_bcss_result_table_zero_row)) * bcf_row_scale_bcss_result_table)) /\ exists bcf_quotient_bcss_result_table_zero_row_entry. bcf_row_code_bcss_result_table = bcf_quotient_bcss_result_table_zero_row_entry * S ((S (bcf_index_bcss_result_table_zero_row)) * bcf_row_scale_bcss_result_table) + (bcf_value_bcss_result_table_zero_row))) /\ ((bcf_index_bcss_result_table_zero_row = 0 /\ bcf_value_bcss_result_table_zero_row = 1) \/ exists bcf_predecessor_bcss_result_table_zero_row. bcf_index_bcss_result_table_zero_row = S bcf_predecessor_bcss_result_table_zero_row /\ bcf_value_bcss_result_table_zero_row = 0)))) \/ exists bcf_predecessor_bcss_result_table bcf_previous_code_bcss_result_table bcf_previous_scale_bcss_result_table. bcf_row_index_bcss_result_table = S bcf_predecessor_bcss_result_table /\ ((((exists bcf_height_bcss_result_table_decoded_previous_code. bcf_height_bcss_result_table_decoded_previous_code + S (bcf_previous_code_bcss_result_table) = S ((S (bcf_predecessor_bcss_result_table)) * bcf_row_code_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_table_decoded_previous_code. bcf_row_code_code_bcss_result = bcf_quotient_bcss_result_table_decoded_previous_code * S ((S (bcf_predecessor_bcss_result_table)) * bcf_row_code_scale_bcss_result) + (bcf_previous_code_bcss_result_table))) /\ ((((exists bcf_height_bcss_result_table_decoded_previous_scale. bcf_height_bcss_result_table_decoded_previous_scale + S (bcf_previous_scale_bcss_result_table) = S ((S (bcf_predecessor_bcss_result_table)) * bcf_row_scale_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_table_decoded_previous_scale. bcf_row_scale_code_bcss_result = bcf_quotient_bcss_result_table_decoded_previous_scale * S ((S (bcf_predecessor_bcss_result_table)) * bcf_row_scale_scale_bcss_result) + (bcf_previous_scale_bcss_result_table))) /\ (forall bcf_index_bcss_result_table_row_step. (exists bcf_lt_gap_bcss_result_table_row_step_bound. bcf_lt_gap_bcss_result_table_row_step_bound + S (bcf_index_bcss_result_table_row_step) = S (S n)) -> exists bcf_value_bcss_result_table_row_step. ((((exists bcf_height_bcss_result_table_row_step_entry. bcf_height_bcss_result_table_row_step_entry + S (bcf_value_bcss_result_table_row_step) = S ((S (bcf_index_bcss_result_table_row_step)) * bcf_row_scale_bcss_result_table)) /\ exists bcf_quotient_bcss_result_table_row_step_entry. bcf_row_code_bcss_result_table = bcf_quotient_bcss_result_table_row_step_entry * S ((S (bcf_index_bcss_result_table_row_step)) * bcf_row_scale_bcss_result_table) + (bcf_value_bcss_result_table_row_step))) /\ ((bcf_index_bcss_result_table_row_step = 0 /\ bcf_value_bcss_result_table_row_step = 1) \/ exists bcf_predecessor_bcss_result_table_row_step bcf_left_bcss_result_table_row_step bcf_right_bcss_result_table_row_step. bcf_index_bcss_result_table_row_step = S bcf_predecessor_bcss_result_table_row_step /\ ((((exists bcf_height_bcss_result_table_row_step_previous_left. bcf_height_bcss_result_table_row_step_previous_left + S (bcf_left_bcss_result_table_row_step) = S ((S (bcf_predecessor_bcss_result_table_row_step)) * bcf_previous_scale_bcss_result_table)) /\ exists bcf_quotient_bcss_result_table_row_step_previous_left. bcf_previous_code_bcss_result_table = bcf_quotient_bcss_result_table_row_step_previous_left * S ((S (bcf_predecessor_bcss_result_table_row_step)) * bcf_previous_scale_bcss_result_table) + (bcf_left_bcss_result_table_row_step))) /\ ((((exists bcf_height_bcss_result_table_row_step_previous_right. bcf_height_bcss_result_table_row_step_previous_right + S (bcf_right_bcss_result_table_row_step) = S ((S (S (bcf_predecessor_bcss_result_table_row_step))) * bcf_previous_scale_bcss_result_table)) /\ exists bcf_quotient_bcss_result_table_row_step_previous_right. bcf_previous_code_bcss_result_table = bcf_quotient_bcss_result_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcss_result_table_row_step))) * bcf_previous_scale_bcss_result_table) + (bcf_right_bcss_result_table_row_step))) /\ bcf_value_bcss_result_table_row_step = bcf_left_bcss_result_table_row_step + bcf_right_bcss_result_table_row_step))))))))))) /\ ((((exists bcf_height_bcss_result_decoded_row_code. bcf_height_bcss_result_decoded_row_code + S (bcf_row_code_bcss_result) = S ((S (S n)) * bcf_row_code_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_decoded_row_code. bcf_row_code_code_bcss_result = bcf_quotient_bcss_result_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcss_result) + (bcf_row_code_bcss_result))) /\ ((((exists bcf_height_bcss_result_decoded_row_scale. bcf_height_bcss_result_decoded_row_scale + S (bcf_row_scale_bcss_result) = S ((S (S n)) * bcf_row_scale_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_decoded_row_scale. bcf_row_scale_code_bcss_result = bcf_quotient_bcss_result_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcss_result) + (bcf_row_scale_bcss_result))) /\ (((exists bcf_height_bcss_result_decoded_value. bcf_height_bcss_result_decoded_value + S (z) = S ((S (S k)) * bcf_row_scale_bcss_result)) /\ exists bcf_quotient_bcss_result_decoded_value. bcf_row_code_bcss_result = bcf_quotient_bcss_result_decoded_value * S ((S (S k)) * bcf_row_scale_bcss_result) + (z))))))))) -> z = x + y

Proof neighborhood

Direct theorem prerequisites

BT001H lt_trichotomy BT000E le_refl BT0018 le_succ BT0016 succ_le_succ BT00TD choose_out_of_range_zero BT00TG choose_self BT00TI choose_succ_succ_of_lt

Direct theorem dependents

BT00TL choose_symmetry BT00TM choose_positive BT00TS central_binom_succ_double_middle BT00TT choose_weighted_vertical

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

94 script commands · 20 reading checkpoints · 9 local claims

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

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

Named ingredients (7)
lt trichotomyle reflle succsucc le succchoose out of range zerochoose selfchoose succ succ of lt
01Fix variables and assumptionsL1–8

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro z
  6. L6
    intro hleft
  7. L7
    intro hright
  8. L8
    intro hresult
02Use earlier factsL9–10

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

  1. L9
    specialize lt_trichotomy k
  2. L10
    specialize lt_trichotomy n
03Separate the logical casesL11–11

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

  1. L11
    cases lt_trichotomy
04Establish hxL12–20

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

  1. L12
    have hx : x = 1
  2. L13
    specialize choose_self n
  3. L14
    specialize choose_self x
  4. L15
    apply choose_self
  5. L16
    rewrite lt_trichotomy_left at hleft
  6. L17
    rewrite lt_trichotomy_left at hleft
  7. L18
    rewrite lt_trichotomy_left at hleft
  8. L19
    rewrite lt_trichotomy_left at hleft
  9. L20
    exact hleft
05Establish hzL21–29

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

  1. L21
    have hz : z = 1
  2. L22
    specialize choose_self (S n)
  3. L23
    specialize choose_self z
  4. L24
    apply choose_self
  5. L25
    rewrite lt_trichotomy_left at hresult
  6. L26
    rewrite lt_trichotomy_left at hresult
  7. L27
    rewrite lt_trichotomy_left at hresult
  8. L28
    rewrite lt_trichotomy_left at hresult
  9. L29
    exact hresult
06Establish hequality_right_boundL30–33

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

  1. L30
    have hequality_right_bound : Lt(n,S k)Definitions: Lt(n,S k)Original native command in the exact edition
  2. L31
    rewrite lt_trichotomy_left
  3. L32
    specialize le_refl (S n)
  4. L33
    exact le_refl
07Establish hyL34–43

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

  1. L34
    have hy : y = 0
  2. L35
    specialize choose_out_of_range_zero n
  3. L36
    specialize choose_out_of_range_zero (S k)
  4. L37
    specialize choose_out_of_range_zero y
  5. L38
    apply choose_out_of_range_zero
  6. L39
    exact hequality_right_bound
  7. L40
    exact hright
  8. L41
    rewrite hx
  9. L42
    rewrite hy
  10. L43
    trans 1
08Use earlier factsL44–44

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

  1. L44
    exact hz
09Calculate and transport equalitiesL45–45

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

  1. L45
    symm
10Use earlier factsL46–46

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

  1. L46
    apply PA3
11Separate the logical casesL47–47

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

  1. L47
    cases lt_trichotomy_right
12Use earlier factsL48–57

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

  1. L48
    specialize choose_succ_succ_of_lt n
  2. L49
    specialize choose_succ_succ_of_lt k
  3. L50
    specialize choose_succ_succ_of_lt x
  4. L51
    specialize choose_succ_succ_of_lt y
  5. L52
    specialize choose_succ_succ_of_lt z
  6. L53
    apply choose_succ_succ_of_lt
  7. L54
    exact lt_trichotomy_right_left
  8. L55
    exact hleft
  9. L56
    exact hright
  10. L57
    exact hresult
13Establish hxL58–64

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

  1. L58
    have hx : x = 0
  2. L59
    specialize choose_out_of_range_zero n
  3. L60
    specialize choose_out_of_range_zero k
  4. L61
    specialize choose_out_of_range_zero x
  5. L62
    apply choose_out_of_range_zero
  6. L63
    exact lt_trichotomy_right_right
  7. L64
    exact hleft
14Establish habove_right_boundL65–69

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

  1. L65
    have habove_right_bound : Lt(n,S k)Definitions: Lt(n,S k)Original native command in the exact edition
  2. L66
    specialize le_succ (S n)
  3. L67
    specialize le_succ k
  4. L68
    apply le_succ
  5. L69
    exact lt_trichotomy_right_right
15Establish hyL70–76

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

  1. L70
    have hy : y = 0
  2. L71
    specialize choose_out_of_range_zero n
  3. L72
    specialize choose_out_of_range_zero (S k)
  4. L73
    specialize choose_out_of_range_zero y
  5. L74
    apply choose_out_of_range_zero
  6. L75
    exact habove_right_bound
  7. L76
    exact hright
16Establish habove_result_boundL77–81

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

  1. L77
    have habove_result_bound : Lt(S n,S k)Definitions: Lt(S n,S k)Original native command in the exact edition
  2. L78
    specialize succ_le_succ (S n)
  3. L79
    specialize succ_le_succ k
  4. L80
    apply succ_le_succ
  5. L81
    exact lt_trichotomy_right_right
17Establish hzL82–91

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

  1. L82
    have hz : z = 0
  2. L83
    specialize choose_out_of_range_zero (S n)
  3. L84
    specialize choose_out_of_range_zero (S k)
  4. L85
    specialize choose_out_of_range_zero z
  5. L86
    apply choose_out_of_range_zero
  6. L87
    exact habove_result_bound
  7. L88
    exact hresult
  8. L89
    rewrite hx
  9. L90
    rewrite hy
  10. L91
    trans 0
18Use earlier factsL92–92

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

  1. L92
    exact hz
19Calculate and transport equalitiesL93–93

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

  1. L93
    symm
20Use earlier factsL94–94

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

  1. L94
    apply PA3

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hleft
  7. 0007intro hright
  8. 0008intro hresult
  9. 0009specialize lt_trichotomy k
  10. 0010specialize lt_trichotomy n
  11. 0011cases lt_trichotomy
  12. 0012have hx : x = 1
  13. 0013specialize choose_self n
  14. 0014specialize choose_self x
  15. 0015apply choose_self
  16. 0016rewrite lt_trichotomy_left at hleft
  17. 0017rewrite lt_trichotomy_left at hleft
  18. 0018rewrite lt_trichotomy_left at hleft
  19. 0019rewrite lt_trichotomy_left at hleft
  20. 0020exact hleft
  21. 0021have hz : z = 1
  22. 0022specialize choose_self (S n)
  23. 0023specialize choose_self z
  24. 0024apply choose_self
  25. 0025rewrite lt_trichotomy_left at hresult
  26. 0026rewrite lt_trichotomy_left at hresult
  27. 0027rewrite lt_trichotomy_left at hresult
  28. 0028rewrite lt_trichotomy_left at hresult
  29. 0029exact hresult
  30. 0030have hequality_right_bound : Lt(n,S k)
    Exact native replay linehave hequality_right_bound : exists bcf_lt_gap_bcss_equality_right_bound. bcf_lt_gap_bcss_equality_right_bound + S (n) = S k
  31. 0031rewrite lt_trichotomy_left
  32. 0032specialize le_refl (S n)
  33. 0033exact le_refl
  34. 0034have hy : y = 0
  35. 0035specialize choose_out_of_range_zero n
  36. 0036specialize choose_out_of_range_zero (S k)
  37. 0037specialize choose_out_of_range_zero y
  38. 0038apply choose_out_of_range_zero
  39. 0039exact hequality_right_bound
  40. 0040exact hright
  41. 0041rewrite hx
  42. 0042rewrite hy
  43. 0043trans 1
  44. 0044exact hz
  45. 0045symm
  46. 0046apply PA3
  47. 0047cases lt_trichotomy_right
  48. 0048specialize choose_succ_succ_of_lt n
  49. 0049specialize choose_succ_succ_of_lt k
  50. 0050specialize choose_succ_succ_of_lt x
  51. 0051specialize choose_succ_succ_of_lt y
  52. 0052specialize choose_succ_succ_of_lt z
  53. 0053apply choose_succ_succ_of_lt
  54. 0054exact lt_trichotomy_right_left
  55. 0055exact hleft
  56. 0056exact hright
  57. 0057exact hresult
  58. 0058have hx : x = 0
  59. 0059specialize choose_out_of_range_zero n
  60. 0060specialize choose_out_of_range_zero k
  61. 0061specialize choose_out_of_range_zero x
  62. 0062apply choose_out_of_range_zero
  63. 0063exact lt_trichotomy_right_right
  64. 0064exact hleft
  65. 0065have habove_right_bound : Lt(n,S k)
    Exact native replay linehave habove_right_bound : exists bcf_lt_gap_bcss_above_right_bound. bcf_lt_gap_bcss_above_right_bound + S (n) = S k
  66. 0066specialize le_succ (S n)
  67. 0067specialize le_succ k
  68. 0068apply le_succ
  69. 0069exact lt_trichotomy_right_right
  70. 0070have hy : y = 0
  71. 0071specialize choose_out_of_range_zero n
  72. 0072specialize choose_out_of_range_zero (S k)
  73. 0073specialize choose_out_of_range_zero y
  74. 0074apply choose_out_of_range_zero
  75. 0075exact habove_right_bound
  76. 0076exact hright
  77. 0077have habove_result_bound : Lt(S n,S k)
    Exact native replay linehave habove_result_bound : exists bcf_lt_gap_bcss_above_result_bound. bcf_lt_gap_bcss_above_result_bound + S (S n) = S k
  78. 0078specialize succ_le_succ (S n)
  79. 0079specialize succ_le_succ k
  80. 0080apply succ_le_succ
  81. 0081exact lt_trichotomy_right_right
  82. 0082have hz : z = 0
  83. 0083specialize choose_out_of_range_zero (S n)
  84. 0084specialize choose_out_of_range_zero (S k)
  85. 0085specialize choose_out_of_range_zero z
  86. 0086apply choose_out_of_range_zero
  87. 0087exact habove_result_bound
  88. 0088exact hresult
  89. 0089rewrite hx
  90. 0090rewrite hy
  91. 0091trans 0
  92. 0092exact hz
  93. 0093symm
  94. 0094apply PA3