BT00TI · Bertrand theorem

choose_succ_succ_of_lt

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

Interior Choose values satisfy Pascal's successor recurrence.

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. Lt(k,n) → 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

PD0002 Lt PD0041 Choose

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

21 occurrences

Exact expanded native-PA statement
forall n k x y z. (exists bcf_lt_gap_bcssol_bound. bcf_lt_gap_bcssol_bound + S (k) = n) -> (((exists bcf_lt_gap_bcssol_left_out_of_range. bcf_lt_gap_bcssol_left_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bcssol_left_in_range. bcf_le_gap_bcssol_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcssol_left bcf_row_code_scale_bcssol_left bcf_row_scale_code_bcssol_left bcf_row_scale_scale_bcssol_left bcf_row_code_bcssol_left bcf_row_scale_bcssol_left. ((forall bcf_row_index_bcssol_left_table. (exists bcf_lt_gap_bcssol_left_table_row_bound. bcf_lt_gap_bcssol_left_table_row_bound + S (bcf_row_index_bcssol_left_table) = S (n)) -> exists bcf_row_code_bcssol_left_table bcf_row_scale_bcssol_left_table. ((((exists bcf_height_bcssol_left_table_decoded_row_code. bcf_height_bcssol_left_table_decoded_row_code + S (bcf_row_code_bcssol_left_table) = S ((S (bcf_row_index_bcssol_left_table)) * bcf_row_code_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_table_decoded_row_code. bcf_row_code_code_bcssol_left = bcf_quotient_bcssol_left_table_decoded_row_code * S ((S (bcf_row_index_bcssol_left_table)) * bcf_row_code_scale_bcssol_left) + (bcf_row_code_bcssol_left_table))) /\ ((((exists bcf_height_bcssol_left_table_decoded_row_scale. bcf_height_bcssol_left_table_decoded_row_scale + S (bcf_row_scale_bcssol_left_table) = S ((S (bcf_row_index_bcssol_left_table)) * bcf_row_scale_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_table_decoded_row_scale. bcf_row_scale_code_bcssol_left = bcf_quotient_bcssol_left_table_decoded_row_scale * S ((S (bcf_row_index_bcssol_left_table)) * bcf_row_scale_scale_bcssol_left) + (bcf_row_scale_bcssol_left_table))) /\ ((bcf_row_index_bcssol_left_table = 0 /\ (forall bcf_index_bcssol_left_table_zero_row. (exists bcf_lt_gap_bcssol_left_table_zero_row_bound. bcf_lt_gap_bcssol_left_table_zero_row_bound + S (bcf_index_bcssol_left_table_zero_row) = S (n)) -> exists bcf_value_bcssol_left_table_zero_row. ((((exists bcf_height_bcssol_left_table_zero_row_entry. bcf_height_bcssol_left_table_zero_row_entry + S (bcf_value_bcssol_left_table_zero_row) = S ((S (bcf_index_bcssol_left_table_zero_row)) * bcf_row_scale_bcssol_left_table)) /\ exists bcf_quotient_bcssol_left_table_zero_row_entry. bcf_row_code_bcssol_left_table = bcf_quotient_bcssol_left_table_zero_row_entry * S ((S (bcf_index_bcssol_left_table_zero_row)) * bcf_row_scale_bcssol_left_table) + (bcf_value_bcssol_left_table_zero_row))) /\ ((bcf_index_bcssol_left_table_zero_row = 0 /\ bcf_value_bcssol_left_table_zero_row = 1) \/ exists bcf_predecessor_bcssol_left_table_zero_row. bcf_index_bcssol_left_table_zero_row = S bcf_predecessor_bcssol_left_table_zero_row /\ bcf_value_bcssol_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcssol_left_table bcf_previous_code_bcssol_left_table bcf_previous_scale_bcssol_left_table. bcf_row_index_bcssol_left_table = S bcf_predecessor_bcssol_left_table /\ ((((exists bcf_height_bcssol_left_table_decoded_previous_code. bcf_height_bcssol_left_table_decoded_previous_code + S (bcf_previous_code_bcssol_left_table) = S ((S (bcf_predecessor_bcssol_left_table)) * bcf_row_code_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_table_decoded_previous_code. bcf_row_code_code_bcssol_left = bcf_quotient_bcssol_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcssol_left_table)) * bcf_row_code_scale_bcssol_left) + (bcf_previous_code_bcssol_left_table))) /\ ((((exists bcf_height_bcssol_left_table_decoded_previous_scale. bcf_height_bcssol_left_table_decoded_previous_scale + S (bcf_previous_scale_bcssol_left_table) = S ((S (bcf_predecessor_bcssol_left_table)) * bcf_row_scale_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_table_decoded_previous_scale. bcf_row_scale_code_bcssol_left = bcf_quotient_bcssol_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcssol_left_table)) * bcf_row_scale_scale_bcssol_left) + (bcf_previous_scale_bcssol_left_table))) /\ (forall bcf_index_bcssol_left_table_row_step. (exists bcf_lt_gap_bcssol_left_table_row_step_bound. bcf_lt_gap_bcssol_left_table_row_step_bound + S (bcf_index_bcssol_left_table_row_step) = S (n)) -> exists bcf_value_bcssol_left_table_row_step. ((((exists bcf_height_bcssol_left_table_row_step_entry. bcf_height_bcssol_left_table_row_step_entry + S (bcf_value_bcssol_left_table_row_step) = S ((S (bcf_index_bcssol_left_table_row_step)) * bcf_row_scale_bcssol_left_table)) /\ exists bcf_quotient_bcssol_left_table_row_step_entry. bcf_row_code_bcssol_left_table = bcf_quotient_bcssol_left_table_row_step_entry * S ((S (bcf_index_bcssol_left_table_row_step)) * bcf_row_scale_bcssol_left_table) + (bcf_value_bcssol_left_table_row_step))) /\ ((bcf_index_bcssol_left_table_row_step = 0 /\ bcf_value_bcssol_left_table_row_step = 1) \/ exists bcf_predecessor_bcssol_left_table_row_step bcf_left_bcssol_left_table_row_step bcf_right_bcssol_left_table_row_step. bcf_index_bcssol_left_table_row_step = S bcf_predecessor_bcssol_left_table_row_step /\ ((((exists bcf_height_bcssol_left_table_row_step_previous_left. bcf_height_bcssol_left_table_row_step_previous_left + S (bcf_left_bcssol_left_table_row_step) = S ((S (bcf_predecessor_bcssol_left_table_row_step)) * bcf_previous_scale_bcssol_left_table)) /\ exists bcf_quotient_bcssol_left_table_row_step_previous_left. bcf_previous_code_bcssol_left_table = bcf_quotient_bcssol_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcssol_left_table_row_step)) * bcf_previous_scale_bcssol_left_table) + (bcf_left_bcssol_left_table_row_step))) /\ ((((exists bcf_height_bcssol_left_table_row_step_previous_right. bcf_height_bcssol_left_table_row_step_previous_right + S (bcf_right_bcssol_left_table_row_step) = S ((S (S (bcf_predecessor_bcssol_left_table_row_step))) * bcf_previous_scale_bcssol_left_table)) /\ exists bcf_quotient_bcssol_left_table_row_step_previous_right. bcf_previous_code_bcssol_left_table = bcf_quotient_bcssol_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcssol_left_table_row_step))) * bcf_previous_scale_bcssol_left_table) + (bcf_right_bcssol_left_table_row_step))) /\ bcf_value_bcssol_left_table_row_step = bcf_left_bcssol_left_table_row_step + bcf_right_bcssol_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcssol_left_decoded_row_code. bcf_height_bcssol_left_decoded_row_code + S (bcf_row_code_bcssol_left) = S ((S (n)) * bcf_row_code_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_decoded_row_code. bcf_row_code_code_bcssol_left = bcf_quotient_bcssol_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcssol_left) + (bcf_row_code_bcssol_left))) /\ ((((exists bcf_height_bcssol_left_decoded_row_scale. bcf_height_bcssol_left_decoded_row_scale + S (bcf_row_scale_bcssol_left) = S ((S (n)) * bcf_row_scale_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_decoded_row_scale. bcf_row_scale_code_bcssol_left = bcf_quotient_bcssol_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcssol_left) + (bcf_row_scale_bcssol_left))) /\ (((exists bcf_height_bcssol_left_decoded_value. bcf_height_bcssol_left_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bcssol_left)) /\ exists bcf_quotient_bcssol_left_decoded_value. bcf_row_code_bcssol_left = bcf_quotient_bcssol_left_decoded_value * S ((S (k)) * bcf_row_scale_bcssol_left) + (x))))))))) -> (((exists bcf_lt_gap_bcssol_right_out_of_range. bcf_lt_gap_bcssol_right_out_of_range + S (n) = S k) /\ y = 0) \/ ((exists bcf_le_gap_bcssol_right_in_range. bcf_le_gap_bcssol_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcssol_right bcf_row_code_scale_bcssol_right bcf_row_scale_code_bcssol_right bcf_row_scale_scale_bcssol_right bcf_row_code_bcssol_right bcf_row_scale_bcssol_right. ((forall bcf_row_index_bcssol_right_table. (exists bcf_lt_gap_bcssol_right_table_row_bound. bcf_lt_gap_bcssol_right_table_row_bound + S (bcf_row_index_bcssol_right_table) = S (n)) -> exists bcf_row_code_bcssol_right_table bcf_row_scale_bcssol_right_table. ((((exists bcf_height_bcssol_right_table_decoded_row_code. bcf_height_bcssol_right_table_decoded_row_code + S (bcf_row_code_bcssol_right_table) = S ((S (bcf_row_index_bcssol_right_table)) * bcf_row_code_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_table_decoded_row_code. bcf_row_code_code_bcssol_right = bcf_quotient_bcssol_right_table_decoded_row_code * S ((S (bcf_row_index_bcssol_right_table)) * bcf_row_code_scale_bcssol_right) + (bcf_row_code_bcssol_right_table))) /\ ((((exists bcf_height_bcssol_right_table_decoded_row_scale. bcf_height_bcssol_right_table_decoded_row_scale + S (bcf_row_scale_bcssol_right_table) = S ((S (bcf_row_index_bcssol_right_table)) * bcf_row_scale_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_table_decoded_row_scale. bcf_row_scale_code_bcssol_right = bcf_quotient_bcssol_right_table_decoded_row_scale * S ((S (bcf_row_index_bcssol_right_table)) * bcf_row_scale_scale_bcssol_right) + (bcf_row_scale_bcssol_right_table))) /\ ((bcf_row_index_bcssol_right_table = 0 /\ (forall bcf_index_bcssol_right_table_zero_row. (exists bcf_lt_gap_bcssol_right_table_zero_row_bound. bcf_lt_gap_bcssol_right_table_zero_row_bound + S (bcf_index_bcssol_right_table_zero_row) = S (n)) -> exists bcf_value_bcssol_right_table_zero_row. ((((exists bcf_height_bcssol_right_table_zero_row_entry. bcf_height_bcssol_right_table_zero_row_entry + S (bcf_value_bcssol_right_table_zero_row) = S ((S (bcf_index_bcssol_right_table_zero_row)) * bcf_row_scale_bcssol_right_table)) /\ exists bcf_quotient_bcssol_right_table_zero_row_entry. bcf_row_code_bcssol_right_table = bcf_quotient_bcssol_right_table_zero_row_entry * S ((S (bcf_index_bcssol_right_table_zero_row)) * bcf_row_scale_bcssol_right_table) + (bcf_value_bcssol_right_table_zero_row))) /\ ((bcf_index_bcssol_right_table_zero_row = 0 /\ bcf_value_bcssol_right_table_zero_row = 1) \/ exists bcf_predecessor_bcssol_right_table_zero_row. bcf_index_bcssol_right_table_zero_row = S bcf_predecessor_bcssol_right_table_zero_row /\ bcf_value_bcssol_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcssol_right_table bcf_previous_code_bcssol_right_table bcf_previous_scale_bcssol_right_table. bcf_row_index_bcssol_right_table = S bcf_predecessor_bcssol_right_table /\ ((((exists bcf_height_bcssol_right_table_decoded_previous_code. bcf_height_bcssol_right_table_decoded_previous_code + S (bcf_previous_code_bcssol_right_table) = S ((S (bcf_predecessor_bcssol_right_table)) * bcf_row_code_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_table_decoded_previous_code. bcf_row_code_code_bcssol_right = bcf_quotient_bcssol_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcssol_right_table)) * bcf_row_code_scale_bcssol_right) + (bcf_previous_code_bcssol_right_table))) /\ ((((exists bcf_height_bcssol_right_table_decoded_previous_scale. bcf_height_bcssol_right_table_decoded_previous_scale + S (bcf_previous_scale_bcssol_right_table) = S ((S (bcf_predecessor_bcssol_right_table)) * bcf_row_scale_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_table_decoded_previous_scale. bcf_row_scale_code_bcssol_right = bcf_quotient_bcssol_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcssol_right_table)) * bcf_row_scale_scale_bcssol_right) + (bcf_previous_scale_bcssol_right_table))) /\ (forall bcf_index_bcssol_right_table_row_step. (exists bcf_lt_gap_bcssol_right_table_row_step_bound. bcf_lt_gap_bcssol_right_table_row_step_bound + S (bcf_index_bcssol_right_table_row_step) = S (n)) -> exists bcf_value_bcssol_right_table_row_step. ((((exists bcf_height_bcssol_right_table_row_step_entry. bcf_height_bcssol_right_table_row_step_entry + S (bcf_value_bcssol_right_table_row_step) = S ((S (bcf_index_bcssol_right_table_row_step)) * bcf_row_scale_bcssol_right_table)) /\ exists bcf_quotient_bcssol_right_table_row_step_entry. bcf_row_code_bcssol_right_table = bcf_quotient_bcssol_right_table_row_step_entry * S ((S (bcf_index_bcssol_right_table_row_step)) * bcf_row_scale_bcssol_right_table) + (bcf_value_bcssol_right_table_row_step))) /\ ((bcf_index_bcssol_right_table_row_step = 0 /\ bcf_value_bcssol_right_table_row_step = 1) \/ exists bcf_predecessor_bcssol_right_table_row_step bcf_left_bcssol_right_table_row_step bcf_right_bcssol_right_table_row_step. bcf_index_bcssol_right_table_row_step = S bcf_predecessor_bcssol_right_table_row_step /\ ((((exists bcf_height_bcssol_right_table_row_step_previous_left. bcf_height_bcssol_right_table_row_step_previous_left + S (bcf_left_bcssol_right_table_row_step) = S ((S (bcf_predecessor_bcssol_right_table_row_step)) * bcf_previous_scale_bcssol_right_table)) /\ exists bcf_quotient_bcssol_right_table_row_step_previous_left. bcf_previous_code_bcssol_right_table = bcf_quotient_bcssol_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcssol_right_table_row_step)) * bcf_previous_scale_bcssol_right_table) + (bcf_left_bcssol_right_table_row_step))) /\ ((((exists bcf_height_bcssol_right_table_row_step_previous_right. bcf_height_bcssol_right_table_row_step_previous_right + S (bcf_right_bcssol_right_table_row_step) = S ((S (S (bcf_predecessor_bcssol_right_table_row_step))) * bcf_previous_scale_bcssol_right_table)) /\ exists bcf_quotient_bcssol_right_table_row_step_previous_right. bcf_previous_code_bcssol_right_table = bcf_quotient_bcssol_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcssol_right_table_row_step))) * bcf_previous_scale_bcssol_right_table) + (bcf_right_bcssol_right_table_row_step))) /\ bcf_value_bcssol_right_table_row_step = bcf_left_bcssol_right_table_row_step + bcf_right_bcssol_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcssol_right_decoded_row_code. bcf_height_bcssol_right_decoded_row_code + S (bcf_row_code_bcssol_right) = S ((S (n)) * bcf_row_code_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_decoded_row_code. bcf_row_code_code_bcssol_right = bcf_quotient_bcssol_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcssol_right) + (bcf_row_code_bcssol_right))) /\ ((((exists bcf_height_bcssol_right_decoded_row_scale. bcf_height_bcssol_right_decoded_row_scale + S (bcf_row_scale_bcssol_right) = S ((S (n)) * bcf_row_scale_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_decoded_row_scale. bcf_row_scale_code_bcssol_right = bcf_quotient_bcssol_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcssol_right) + (bcf_row_scale_bcssol_right))) /\ (((exists bcf_height_bcssol_right_decoded_value. bcf_height_bcssol_right_decoded_value + S (y) = S ((S (S k)) * bcf_row_scale_bcssol_right)) /\ exists bcf_quotient_bcssol_right_decoded_value. bcf_row_code_bcssol_right = bcf_quotient_bcssol_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcssol_right) + (y))))))))) -> (((exists bcf_lt_gap_bcssol_result_out_of_range. bcf_lt_gap_bcssol_result_out_of_range + S (S n) = S k) /\ z = 0) \/ ((exists bcf_le_gap_bcssol_result_in_range. bcf_le_gap_bcssol_result_in_range + (S k) = S n) /\ (exists bcf_row_code_code_bcssol_result bcf_row_code_scale_bcssol_result bcf_row_scale_code_bcssol_result bcf_row_scale_scale_bcssol_result bcf_row_code_bcssol_result bcf_row_scale_bcssol_result. ((forall bcf_row_index_bcssol_result_table. (exists bcf_lt_gap_bcssol_result_table_row_bound. bcf_lt_gap_bcssol_result_table_row_bound + S (bcf_row_index_bcssol_result_table) = S (S n)) -> exists bcf_row_code_bcssol_result_table bcf_row_scale_bcssol_result_table. ((((exists bcf_height_bcssol_result_table_decoded_row_code. bcf_height_bcssol_result_table_decoded_row_code + S (bcf_row_code_bcssol_result_table) = S ((S (bcf_row_index_bcssol_result_table)) * bcf_row_code_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_table_decoded_row_code. bcf_row_code_code_bcssol_result = bcf_quotient_bcssol_result_table_decoded_row_code * S ((S (bcf_row_index_bcssol_result_table)) * bcf_row_code_scale_bcssol_result) + (bcf_row_code_bcssol_result_table))) /\ ((((exists bcf_height_bcssol_result_table_decoded_row_scale. bcf_height_bcssol_result_table_decoded_row_scale + S (bcf_row_scale_bcssol_result_table) = S ((S (bcf_row_index_bcssol_result_table)) * bcf_row_scale_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_table_decoded_row_scale. bcf_row_scale_code_bcssol_result = bcf_quotient_bcssol_result_table_decoded_row_scale * S ((S (bcf_row_index_bcssol_result_table)) * bcf_row_scale_scale_bcssol_result) + (bcf_row_scale_bcssol_result_table))) /\ ((bcf_row_index_bcssol_result_table = 0 /\ (forall bcf_index_bcssol_result_table_zero_row. (exists bcf_lt_gap_bcssol_result_table_zero_row_bound. bcf_lt_gap_bcssol_result_table_zero_row_bound + S (bcf_index_bcssol_result_table_zero_row) = S (S n)) -> exists bcf_value_bcssol_result_table_zero_row. ((((exists bcf_height_bcssol_result_table_zero_row_entry. bcf_height_bcssol_result_table_zero_row_entry + S (bcf_value_bcssol_result_table_zero_row) = S ((S (bcf_index_bcssol_result_table_zero_row)) * bcf_row_scale_bcssol_result_table)) /\ exists bcf_quotient_bcssol_result_table_zero_row_entry. bcf_row_code_bcssol_result_table = bcf_quotient_bcssol_result_table_zero_row_entry * S ((S (bcf_index_bcssol_result_table_zero_row)) * bcf_row_scale_bcssol_result_table) + (bcf_value_bcssol_result_table_zero_row))) /\ ((bcf_index_bcssol_result_table_zero_row = 0 /\ bcf_value_bcssol_result_table_zero_row = 1) \/ exists bcf_predecessor_bcssol_result_table_zero_row. bcf_index_bcssol_result_table_zero_row = S bcf_predecessor_bcssol_result_table_zero_row /\ bcf_value_bcssol_result_table_zero_row = 0)))) \/ exists bcf_predecessor_bcssol_result_table bcf_previous_code_bcssol_result_table bcf_previous_scale_bcssol_result_table. bcf_row_index_bcssol_result_table = S bcf_predecessor_bcssol_result_table /\ ((((exists bcf_height_bcssol_result_table_decoded_previous_code. bcf_height_bcssol_result_table_decoded_previous_code + S (bcf_previous_code_bcssol_result_table) = S ((S (bcf_predecessor_bcssol_result_table)) * bcf_row_code_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_table_decoded_previous_code. bcf_row_code_code_bcssol_result = bcf_quotient_bcssol_result_table_decoded_previous_code * S ((S (bcf_predecessor_bcssol_result_table)) * bcf_row_code_scale_bcssol_result) + (bcf_previous_code_bcssol_result_table))) /\ ((((exists bcf_height_bcssol_result_table_decoded_previous_scale. bcf_height_bcssol_result_table_decoded_previous_scale + S (bcf_previous_scale_bcssol_result_table) = S ((S (bcf_predecessor_bcssol_result_table)) * bcf_row_scale_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_table_decoded_previous_scale. bcf_row_scale_code_bcssol_result = bcf_quotient_bcssol_result_table_decoded_previous_scale * S ((S (bcf_predecessor_bcssol_result_table)) * bcf_row_scale_scale_bcssol_result) + (bcf_previous_scale_bcssol_result_table))) /\ (forall bcf_index_bcssol_result_table_row_step. (exists bcf_lt_gap_bcssol_result_table_row_step_bound. bcf_lt_gap_bcssol_result_table_row_step_bound + S (bcf_index_bcssol_result_table_row_step) = S (S n)) -> exists bcf_value_bcssol_result_table_row_step. ((((exists bcf_height_bcssol_result_table_row_step_entry. bcf_height_bcssol_result_table_row_step_entry + S (bcf_value_bcssol_result_table_row_step) = S ((S (bcf_index_bcssol_result_table_row_step)) * bcf_row_scale_bcssol_result_table)) /\ exists bcf_quotient_bcssol_result_table_row_step_entry. bcf_row_code_bcssol_result_table = bcf_quotient_bcssol_result_table_row_step_entry * S ((S (bcf_index_bcssol_result_table_row_step)) * bcf_row_scale_bcssol_result_table) + (bcf_value_bcssol_result_table_row_step))) /\ ((bcf_index_bcssol_result_table_row_step = 0 /\ bcf_value_bcssol_result_table_row_step = 1) \/ exists bcf_predecessor_bcssol_result_table_row_step bcf_left_bcssol_result_table_row_step bcf_right_bcssol_result_table_row_step. bcf_index_bcssol_result_table_row_step = S bcf_predecessor_bcssol_result_table_row_step /\ ((((exists bcf_height_bcssol_result_table_row_step_previous_left. bcf_height_bcssol_result_table_row_step_previous_left + S (bcf_left_bcssol_result_table_row_step) = S ((S (bcf_predecessor_bcssol_result_table_row_step)) * bcf_previous_scale_bcssol_result_table)) /\ exists bcf_quotient_bcssol_result_table_row_step_previous_left. bcf_previous_code_bcssol_result_table = bcf_quotient_bcssol_result_table_row_step_previous_left * S ((S (bcf_predecessor_bcssol_result_table_row_step)) * bcf_previous_scale_bcssol_result_table) + (bcf_left_bcssol_result_table_row_step))) /\ ((((exists bcf_height_bcssol_result_table_row_step_previous_right. bcf_height_bcssol_result_table_row_step_previous_right + S (bcf_right_bcssol_result_table_row_step) = S ((S (S (bcf_predecessor_bcssol_result_table_row_step))) * bcf_previous_scale_bcssol_result_table)) /\ exists bcf_quotient_bcssol_result_table_row_step_previous_right. bcf_previous_code_bcssol_result_table = bcf_quotient_bcssol_result_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcssol_result_table_row_step))) * bcf_previous_scale_bcssol_result_table) + (bcf_right_bcssol_result_table_row_step))) /\ bcf_value_bcssol_result_table_row_step = bcf_left_bcssol_result_table_row_step + bcf_right_bcssol_result_table_row_step))))))))))) /\ ((((exists bcf_height_bcssol_result_decoded_row_code. bcf_height_bcssol_result_decoded_row_code + S (bcf_row_code_bcssol_result) = S ((S (S n)) * bcf_row_code_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_decoded_row_code. bcf_row_code_code_bcssol_result = bcf_quotient_bcssol_result_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcssol_result) + (bcf_row_code_bcssol_result))) /\ ((((exists bcf_height_bcssol_result_decoded_row_scale. bcf_height_bcssol_result_decoded_row_scale + S (bcf_row_scale_bcssol_result) = S ((S (S n)) * bcf_row_scale_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_decoded_row_scale. bcf_row_scale_code_bcssol_result = bcf_quotient_bcssol_result_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcssol_result) + (bcf_row_scale_bcssol_result))) /\ (((exists bcf_height_bcssol_result_decoded_value. bcf_height_bcssol_result_decoded_value + S (z) = S ((S (S k)) * bcf_row_scale_bcssol_result)) /\ exists bcf_quotient_bcssol_result_decoded_value. bcf_row_code_bcssol_result = bcf_quotient_bcssol_result_decoded_value * S ((S (S k)) * bcf_row_scale_bcssol_result) + (z))))))))) -> z = x + y

Proof neighborhood

Direct theorem prerequisites

BT001I lt_not_le BT0019 lt_to_le BT000E le_refl BT0018 le_succ BT0016 succ_le_succ BT00TB beta_pascal_table_row_pointwise_functional BT00TH beta_pascal_table_successor_cell_recurrence

Direct theorem dependents

BT00TJ choose_succ_succ

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

206 script commands · 32 reading checkpoints · 14 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 not lelt to lele reflle succsucc le succbeta pascal table row pointwise functionalbeta pascal table successor cell recurrence
01Fix variables and assumptionsL1–9

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 hbound
  7. L7
    intro hleft
  8. L8
    intro hright
  9. L9
    intro htarget
02Separate the logical casesL10–12

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

  1. L10
    cases hleft
  2. L11
    cases hleft_left
  3. L12
    exfalso
03Establish hleft_leL13–22

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

  1. L13
    have hleft_le : Le(k,n)Definitions: Le(k,n)Original native command in the exact edition
  2. L14
    specialize lt_to_le k
  3. L15
    specialize lt_to_le n
  4. L16
    apply lt_to_le
  5. L17
    exact hbound
  6. L18
    specialize lt_not_le n
  7. L19
    specialize lt_not_le k
  8. L20
    apply lt_not_le
  9. L21
    exact hleft_left_left
  10. L22
    exact hleft_le
04Separate the logical casesL23–32

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

  1. L23
    cases hleft_right
  2. L24
    cases hleft_right_right
  3. L25
    cases hleft_right_right_witness
  4. L26
    cases hleft_right_right_witness_witness
  5. L27
    cases hleft_right_right_witness_witness_witness
  6. L28
    cases hleft_right_right_witness_witness_witness_witness
  7. L29
    cases hleft_right_right_witness_witness_witness_witness_witness
  8. L30
    cases hleft_right_right_witness_witness_witness_witness_witness_witness
  9. L31
    cases hleft_right_right_witness_witness_witness_witness_witness_witness_right
  10. L32
    cases hleft_right_right_witness_witness_witness_witness_witness_witness_right_right
05Separate the logical casesL33–35

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

  1. L33
    cases hright
  2. L34
    cases hright_left
  3. L35
    exfalso
06Use earlier factsL36–40

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

  1. L36
    specialize lt_not_le n
  2. L37
    specialize lt_not_le (S k)
  3. L38
    apply lt_not_le
  4. L39
    exact hright_left_left
  5. L40
    exact hbound
07Separate the logical casesL41–50

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

  1. L41
    cases hright_right
  2. L42
    cases hright_right_right
  3. L43
    cases hright_right_right_witness
  4. L44
    cases hright_right_right_witness_witness
  5. L45
    cases hright_right_right_witness_witness_witness
  6. L46
    cases hright_right_right_witness_witness_witness_witness
  7. L47
    cases hright_right_right_witness_witness_witness_witness_witness
  8. L48
    cases hright_right_right_witness_witness_witness_witness_witness_witness
  9. L49
    cases hright_right_right_witness_witness_witness_witness_witness_witness_right
  10. L50
    cases hright_right_right_witness_witness_witness_witness_witness_witness_right_right
08Establish htarget_rangeL51–55

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

  1. L51
    have htarget_range : Lt(k,S n)Definitions: Lt(k,S n)Original native command in the exact edition
  2. L52
    specialize le_succ (S k)
  3. L53
    specialize le_succ n
  4. L54
    apply le_succ
  5. L55
    exact hbound
09Separate the logical casesL56–58

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

  1. L56
    cases htarget
  2. L57
    cases htarget_left
  3. L58
    exfalso
10Use earlier factsL59–63

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

  1. L59
    specialize lt_not_le (S n)
  2. L60
    specialize lt_not_le (S k)
  3. L61
    apply lt_not_le
  4. L62
    exact htarget_left_left
  5. L63
    exact htarget_range
11Separate the logical casesL64–73

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

  1. L64
    cases htarget_right
  2. L65
    cases htarget_right_right
  3. L66
    cases htarget_right_right_witness
  4. L67
    cases htarget_right_right_witness_witness
  5. L68
    cases htarget_right_right_witness_witness_witness
  6. L69
    cases htarget_right_right_witness_witness_witness_witness
  7. L70
    cases htarget_right_right_witness_witness_witness_witness_witness
  8. L71
    cases htarget_right_right_witness_witness_witness_witness_witness_witness
  9. L72
    cases htarget_right_right_witness_witness_witness_witness_witness_witness_right
  10. L73
    cases htarget_right_right_witness_witness_witness_witness_witness_witness_right_right
12Establish hcurrent_row_boundL74–76

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

  1. L74
    have hcurrent_row_bound : Lt(S n,S S n)Definitions: Lt(S n,S S n)Original native command in the exact edition
  2. L75
    specialize le_refl (S (S n))
  3. L76
    exact le_refl
13Establish hcurrent_cell_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 hcurrent_cell_bound : Lt(S k,S S n)Definitions: Lt(S k,S S n)Original native command in the exact edition
  2. L78
    specialize succ_le_succ (S k)
  3. L79
    specialize succ_le_succ (S n)
  4. L80
    apply succ_le_succ
  5. L81
    exact htarget_range
14Establish hrecurrenceL82–91

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

  1. L82
    have hrecurrence · expand full local formula (699 characters)have hrecurrence : ∃ bcf_previous_code_bcssol_recurrence_result. ∃ bcf_previous_scale_bcssol_recurrence_result. ∃ bcf_left_value_bcssol_recurrence_result. ∃ bcf_right_value_bcssol_recurrence_result. BetaAt(x13,x14,n,bcf_previous_code_bcssol_recurrence_result) ∧ (BetaAt(x15,x16,n,bcf_previous_scale_bcssol_recurrence_result) ∧ (BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,k,bcf_left_value_bcssol_recurrence_result) ∧ (BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,S k,bcf_right_value_bcssol_recurrence_result) ∧ z = bcf_left_value_bcssol_recurrence_result + bcf_right_value_bcssol_recurrence_result)))
    Definitions: BetaAt(x13,x14,n,bcf_previous_code_bcssol_recurrence_result)BetaAt(x15,x16,n,bcf_previous_scale_bcssol_recurrence_result)BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,k,bcf_left_value_bcssol_recurrence_result)BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,S k,bcf_right_value_bcssol_recurrence_result)Original native command in the exact edition
  2. L83
    specialize beta_pascal_table_successor_cell_recurrence x13
  3. L84
    specialize beta_pascal_table_successor_cell_recurrence x14
  4. L85
    specialize beta_pascal_table_successor_cell_recurrence x15
  5. L86
    specialize beta_pascal_table_successor_cell_recurrence x16
  6. L87
    specialize beta_pascal_table_successor_cell_recurrence (S (S n))
  7. L88
    specialize beta_pascal_table_successor_cell_recurrence (S (S n))
  8. L89
    specialize beta_pascal_table_successor_cell_recurrence n
  9. L90
    specialize beta_pascal_table_successor_cell_recurrence k
  10. L91
    specialize beta_pascal_table_successor_cell_recurrence x17
15Use earlier factsL92–100

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

  1. L92
    specialize beta_pascal_table_successor_cell_recurrence x18
  2. L93
    specialize beta_pascal_table_successor_cell_recurrence z
  3. L94
    apply beta_pascal_table_successor_cell_recurrence
  4. L95
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
  5. L96
    exact hcurrent_row_bound
  6. L97
    exact hcurrent_cell_bound
  7. L98
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_left
  8. L99
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  9. L100
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_right_right
16Separate the logical casesL101–108

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

  1. L101
    cases hrecurrence
  2. L102
    cases hrecurrence_witness
  3. L103
    cases hrecurrence_witness_witness
  4. L104
    cases hrecurrence_witness_witness_witness
  5. L105
    cases hrecurrence_witness_witness_witness_witness
  6. L106
    cases hrecurrence_witness_witness_witness_witness_right
  7. L107
    cases hrecurrence_witness_witness_witness_witness_right_right
  8. L108
    cases hrecurrence_witness_witness_witness_witness_right_right_right
17Establish hpredecessor_row_boundL109–114

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

  1. L109
    have hpredecessor_row_bound : Lt(n,S S n)Definitions: Lt(n,S S n)Original native command in the exact edition
  2. L110
    specialize le_succ (S n)
  3. L111
    specialize le_succ (S n)
  4. L112
    apply le_succ
  5. L113
    specialize le_refl (S n)
  6. L114
    exact le_refl
18Establish hsource_row_boundL115–117

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

  1. L115
    have hsource_row_bound : Lt(n,S n)Definitions: Lt(n,S n)Original native command in the exact edition
  2. L116
    specialize le_refl (S n)
  3. L117
    exact le_refl
19Establish hresult_left_boundL118–122

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

  1. L118
    have hresult_left_bound : Lt(k,S S n)Definitions: Lt(k,S S n)Original native command in the exact edition
  2. L119
    specialize le_succ (S k)
  3. L120
    specialize le_succ (S n)
  4. L121
    apply le_succ
  5. L122
    exact htarget_range
20Establish hsource_left_boundL123–124

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

  1. L123
    have hsource_left_bound : Lt(k,S n)Definitions: Lt(k,S n)Original native command in the exact edition
  2. L124
    exact htarget_range
21Establish hsource_right_boundL125–129

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

  1. L125
    have hsource_right_bound : Lt(S k,S n)Definitions: Lt(S k,S n)Original native command in the exact edition
  2. L126
    specialize succ_le_succ (S k)
  3. L127
    specialize succ_le_succ n
  4. L128
    apply succ_le_succ
  5. L129
    exact hbound
22Establish hleft_agreementL130–139

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

  1. L130
    have hleft_agreement : ∀ bcf_index_bcssol_left_agreement. ∀ bcf_left_value_bcssol_left_agreement. ∀ bcf_right_value_bcssol_left_agreement. Lt(bcf_index_bcssol_left_agreement,S S n) → Lt(bcf_index_bcssol_left_agreement,S n) → BetaAt(x19,x20,bcf_index_bcssol_left_agreement,bcf_left_value_bcssol_left_agreement) → BetaAt(x5,x6,bcf_index_bcssol_left_agreement,bcf_right_value_bcssol_left_agreement) → bcf_left_value_bcssol_left_agreement = bcf_right_value_bcssol_left_agreementDefinitions: Lt(bcf_index_bcssol_left_agreement,S S n)Lt(bcf_index_bcssol_left_agreement,S n)BetaAt(x19,x20,bcf_index_bcssol_left_agreement,bcf_left_value_bcssol_left_agreement)BetaAt(x5,x6,bcf_index_bcssol_left_agreement,bcf_right_value_bcssol_left_agreement)Original native command in the exact edition
  2. L131
    specialize beta_pascal_table_row_pointwise_functional x13
  3. L132
    specialize beta_pascal_table_row_pointwise_functional x14
  4. L133
    specialize beta_pascal_table_row_pointwise_functional x15
  5. L134
    specialize beta_pascal_table_row_pointwise_functional x16
  6. L135
    specialize beta_pascal_table_row_pointwise_functional (S (S n))
  7. L136
    specialize beta_pascal_table_row_pointwise_functional (S (S n))
  8. L137
    specialize beta_pascal_table_row_pointwise_functional x1
  9. L138
    specialize beta_pascal_table_row_pointwise_functional x2
  10. L139
    specialize beta_pascal_table_row_pointwise_functional x3
23Use earlier factsL140–149

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

  1. L140
    specialize beta_pascal_table_row_pointwise_functional x4
  2. L141
    specialize beta_pascal_table_row_pointwise_functional (S n)
  3. L142
    specialize beta_pascal_table_row_pointwise_functional (S n)
  4. L143
    specialize beta_pascal_table_row_pointwise_functional n
  5. L144
    specialize beta_pascal_table_row_pointwise_functional x19
  6. L145
    specialize beta_pascal_table_row_pointwise_functional x20
  7. L146
    specialize beta_pascal_table_row_pointwise_functional x5
  8. L147
    specialize beta_pascal_table_row_pointwise_functional x6
  9. L148
    apply beta_pascal_table_row_pointwise_functional
  10. L149
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
24Use earlier factsL150–156

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

  1. L150
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_left
  2. L151
    exact hpredecessor_row_bound
  3. L152
    exact hsource_row_bound
  4. L153
    exact hrecurrence_witness_witness_witness_witness_left
  5. L154
    exact hrecurrence_witness_witness_witness_witness_right_left
  6. L155
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_left
  7. L156
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_left
25Establish hleft_valueL157–165

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

  1. L157
    have hleft_value : x21 = x
  2. L158
    specialize hleft_agreement k
  3. L159
    specialize hleft_agreement x21
  4. L160
    specialize hleft_agreement x
  5. L161
    apply hleft_agreement
  6. L162
    exact hresult_left_bound
  7. L163
    exact hsource_left_bound
  8. L164
    exact hrecurrence_witness_witness_witness_witness_right_right_left
  9. L165
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_right
26Establish hright_agreementL166–175

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

  1. L166
    have hright_agreement : ∀ bcf_index_bcssol_right_agreement. ∀ bcf_left_value_bcssol_right_agreement. ∀ bcf_right_value_bcssol_right_agreement. Lt(bcf_index_bcssol_right_agreement,S S n) → Lt(bcf_index_bcssol_right_agreement,S n) → BetaAt(x19,x20,bcf_index_bcssol_right_agreement,bcf_left_value_bcssol_right_agreement) → BetaAt(x11,x12,bcf_index_bcssol_right_agreement,bcf_right_value_bcssol_right_agreement) → bcf_left_value_bcssol_right_agreement = bcf_right_value_bcssol_right_agreementDefinitions: Lt(bcf_index_bcssol_right_agreement,S S n)Lt(bcf_index_bcssol_right_agreement,S n)BetaAt(x19,x20,bcf_index_bcssol_right_agreement,bcf_left_value_bcssol_right_agreement)BetaAt(x11,x12,bcf_index_bcssol_right_agreement,bcf_right_value_bcssol_right_agreement)Original native command in the exact edition
  2. L167
    specialize beta_pascal_table_row_pointwise_functional x13
  3. L168
    specialize beta_pascal_table_row_pointwise_functional x14
  4. L169
    specialize beta_pascal_table_row_pointwise_functional x15
  5. L170
    specialize beta_pascal_table_row_pointwise_functional x16
  6. L171
    specialize beta_pascal_table_row_pointwise_functional (S (S n))
  7. L172
    specialize beta_pascal_table_row_pointwise_functional (S (S n))
  8. L173
    specialize beta_pascal_table_row_pointwise_functional x7
  9. L174
    specialize beta_pascal_table_row_pointwise_functional x8
  10. L175
    specialize beta_pascal_table_row_pointwise_functional x9
27Use earlier factsL176–185

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

  1. L176
    specialize beta_pascal_table_row_pointwise_functional x10
  2. L177
    specialize beta_pascal_table_row_pointwise_functional (S n)
  3. L178
    specialize beta_pascal_table_row_pointwise_functional (S n)
  4. L179
    specialize beta_pascal_table_row_pointwise_functional n
  5. L180
    specialize beta_pascal_table_row_pointwise_functional x19
  6. L181
    specialize beta_pascal_table_row_pointwise_functional x20
  7. L182
    specialize beta_pascal_table_row_pointwise_functional x11
  8. L183
    specialize beta_pascal_table_row_pointwise_functional x12
  9. L184
    apply beta_pascal_table_row_pointwise_functional
  10. L185
    exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
28Use earlier factsL186–192

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

  1. L186
    exact hright_right_right_witness_witness_witness_witness_witness_witness_left
  2. L187
    exact hpredecessor_row_bound
  3. L188
    exact hsource_row_bound
  4. L189
    exact hrecurrence_witness_witness_witness_witness_left
  5. L190
    exact hrecurrence_witness_witness_witness_witness_right_left
  6. L191
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_left
  7. L192
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_left
29Establish hright_valueL193–202

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

  1. L193
    have hright_value : x22 = y
  2. L194
    specialize hright_agreement (S k)
  3. L195
    specialize hright_agreement x22
  4. L196
    specialize hright_agreement y
  5. L197
    apply hright_agreement
  6. L198
    exact hcurrent_cell_bound
  7. L199
    exact hsource_right_bound
  8. L200
    exact hrecurrence_witness_witness_witness_witness_right_right_right_left
  9. L201
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  10. L202
    trans x21 + x22
30Use earlier factsL203–203

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

  1. L203
    exact hrecurrence_witness_witness_witness_witness_right_right_right_right
31Calculate and transport equalitiesL204–204

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

  1. L204
    congr
32Use earlier factsL205–206

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

  1. L205
    exact hleft_value
  2. L206
    exact hright_value

Library-wide reading audit

Original defined command ledger · 206 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hbound
  7. 0007intro hleft
  8. 0008intro hright
  9. 0009intro htarget
  10. 0010cases hleft
  11. 0011cases hleft_left
  12. 0012exfalso
  13. 0013have hleft_le : Le(k,n)
    Exact native replay linehave hleft_le : exists bcf_le_gap_bcssol_left_le. bcf_le_gap_bcssol_left_le + (k) = n
  14. 0014specialize lt_to_le k
  15. 0015specialize lt_to_le n
  16. 0016apply lt_to_le
  17. 0017exact hbound
  18. 0018specialize lt_not_le n
  19. 0019specialize lt_not_le k
  20. 0020apply lt_not_le
  21. 0021exact hleft_left_left
  22. 0022exact hleft_le
  23. 0023cases hleft_right
  24. 0024cases hleft_right_right
  25. 0025cases hleft_right_right_witness
  26. 0026cases hleft_right_right_witness_witness
  27. 0027cases hleft_right_right_witness_witness_witness
  28. 0028cases hleft_right_right_witness_witness_witness_witness
  29. 0029cases hleft_right_right_witness_witness_witness_witness_witness
  30. 0030cases hleft_right_right_witness_witness_witness_witness_witness_witness
  31. 0031cases hleft_right_right_witness_witness_witness_witness_witness_witness_right
  32. 0032cases hleft_right_right_witness_witness_witness_witness_witness_witness_right_right
  33. 0033cases hright
  34. 0034cases hright_left
  35. 0035exfalso
  36. 0036specialize lt_not_le n
  37. 0037specialize lt_not_le (S k)
  38. 0038apply lt_not_le
  39. 0039exact hright_left_left
  40. 0040exact hbound
  41. 0041cases hright_right
  42. 0042cases hright_right_right
  43. 0043cases hright_right_right_witness
  44. 0044cases hright_right_right_witness_witness
  45. 0045cases hright_right_right_witness_witness_witness
  46. 0046cases hright_right_right_witness_witness_witness_witness
  47. 0047cases hright_right_right_witness_witness_witness_witness_witness
  48. 0048cases hright_right_right_witness_witness_witness_witness_witness_witness
  49. 0049cases hright_right_right_witness_witness_witness_witness_witness_witness_right
  50. 0050cases hright_right_right_witness_witness_witness_witness_witness_witness_right_right
  51. 0051have htarget_range : Lt(k,S n)
    Exact native replay linehave htarget_range : exists bcf_le_gap_bcssol_target_range. bcf_le_gap_bcssol_target_range + (S k) = S n
  52. 0052specialize le_succ (S k)
  53. 0053specialize le_succ n
  54. 0054apply le_succ
  55. 0055exact hbound
  56. 0056cases htarget
  57. 0057cases htarget_left
  58. 0058exfalso
  59. 0059specialize lt_not_le (S n)
  60. 0060specialize lt_not_le (S k)
  61. 0061apply lt_not_le
  62. 0062exact htarget_left_left
  63. 0063exact htarget_range
  64. 0064cases htarget_right
  65. 0065cases htarget_right_right
  66. 0066cases htarget_right_right_witness
  67. 0067cases htarget_right_right_witness_witness
  68. 0068cases htarget_right_right_witness_witness_witness
  69. 0069cases htarget_right_right_witness_witness_witness_witness
  70. 0070cases htarget_right_right_witness_witness_witness_witness_witness
  71. 0071cases htarget_right_right_witness_witness_witness_witness_witness_witness
  72. 0072cases htarget_right_right_witness_witness_witness_witness_witness_witness_right
  73. 0073cases htarget_right_right_witness_witness_witness_witness_witness_witness_right_right
  74. 0074have hcurrent_row_bound : Lt(S n,S S n)
    Exact native replay linehave hcurrent_row_bound : exists bcf_lt_gap_bcssol_current_row_bound. bcf_lt_gap_bcssol_current_row_bound + S (S n) = S (S n)
  75. 0075specialize le_refl (S (S n))
  76. 0076exact le_refl
  77. 0077have hcurrent_cell_bound : Lt(S k,S S n)
    Exact native replay linehave hcurrent_cell_bound : exists bcf_lt_gap_bcssol_current_cell_bound. bcf_lt_gap_bcssol_current_cell_bound + S (S k) = S (S n)
  78. 0078specialize succ_le_succ (S k)
  79. 0079specialize succ_le_succ (S n)
  80. 0080apply succ_le_succ
  81. 0081exact htarget_range
  82. 0082have hrecurrence : ∃ bcf_previous_code_bcssol_recurrence_result. ∃ bcf_previous_scale_bcssol_recurrence_result. ∃ bcf_left_value_bcssol_recurrence_result. ∃ bcf_right_value_bcssol_recurrence_result. BetaAt(x13,x14,n,bcf_previous_code_bcssol_recurrence_result) ∧ (BetaAt(x15,x16,n,bcf_previous_scale_bcssol_recurrence_result) ∧ (BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,k,bcf_left_value_bcssol_recurrence_result) ∧ (BetaAt(bcf_previous_code_bcssol_recurrence_result,bcf_previous_scale_bcssol_recurrence_result,S k,bcf_right_value_bcssol_recurrence_result) ∧ z = bcf_left_value_bcssol_recurrence_result + bcf_right_value_bcssol_recurrence_result)))
    Exact native replay linehave hrecurrence : exists bcf_previous_code_bcssol_recurrence_result bcf_previous_scale_bcssol_recurrence_result bcf_left_value_bcssol_recurrence_result bcf_right_value_bcssol_recurrence_result. (((exists bcf_height_bcssol_recurrence_result_previous_code_at. bcf_height_bcssol_recurrence_result_previous_code_at + S (bcf_previous_code_bcssol_recurrence_result) = S ((S (n)) * x14)) /\ exists bcf_quotient_bcssol_recurrence_result_previous_code_at. x13 = bcf_quotient_bcssol_recurrence_result_previous_code_at * S ((S (n)) * x14) + (bcf_previous_code_bcssol_recurrence_result))) /\ ((((exists bcf_height_bcssol_recurrence_result_previous_scale_at. bcf_height_bcssol_recurrence_result_previous_scale_at + S (bcf_previous_scale_bcssol_recurrence_result) = S ((S (n)) * x16)) /\ exists bcf_quotient_bcssol_recurrence_result_previous_scale_at. x15 = bcf_quotient_bcssol_recurrence_result_previous_scale_at * S ((S (n)) * x16) + (bcf_previous_scale_bcssol_recurrence_result))) /\ ((((exists bcf_height_bcssol_recurrence_result_left_at. bcf_height_bcssol_recurrence_result_left_at + S (bcf_left_value_bcssol_recurrence_result) = S ((S (k)) * bcf_previous_scale_bcssol_recurrence_result)) /\ exists bcf_quotient_bcssol_recurrence_result_left_at. bcf_previous_code_bcssol_recurrence_result = bcf_quotient_bcssol_recurrence_result_left_at * S ((S (k)) * bcf_previous_scale_bcssol_recurrence_result) + (bcf_left_value_bcssol_recurrence_result))) /\ ((((exists bcf_height_bcssol_recurrence_result_right_at. bcf_height_bcssol_recurrence_result_right_at + S (bcf_right_value_bcssol_recurrence_result) = S ((S (S (k))) * bcf_previous_scale_bcssol_recurrence_result)) /\ exists bcf_quotient_bcssol_recurrence_result_right_at. bcf_previous_code_bcssol_recurrence_result = bcf_quotient_bcssol_recurrence_result_right_at * S ((S (S (k))) * bcf_previous_scale_bcssol_recurrence_result) + (bcf_right_value_bcssol_recurrence_result))) /\ z = bcf_left_value_bcssol_recurrence_result + bcf_right_value_bcssol_recurrence_result)))
  83. 0083specialize beta_pascal_table_successor_cell_recurrence x13
  84. 0084specialize beta_pascal_table_successor_cell_recurrence x14
  85. 0085specialize beta_pascal_table_successor_cell_recurrence x15
  86. 0086specialize beta_pascal_table_successor_cell_recurrence x16
  87. 0087specialize beta_pascal_table_successor_cell_recurrence (S (S n))
  88. 0088specialize beta_pascal_table_successor_cell_recurrence (S (S n))
  89. 0089specialize beta_pascal_table_successor_cell_recurrence n
  90. 0090specialize beta_pascal_table_successor_cell_recurrence k
  91. 0091specialize beta_pascal_table_successor_cell_recurrence x17
  92. 0092specialize beta_pascal_table_successor_cell_recurrence x18
  93. 0093specialize beta_pascal_table_successor_cell_recurrence z
  94. 0094apply beta_pascal_table_successor_cell_recurrence
  95. 0095exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
  96. 0096exact hcurrent_row_bound
  97. 0097exact hcurrent_cell_bound
  98. 0098exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_left
  99. 0099exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  100. 0100exact htarget_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  101. 0101cases hrecurrence
  102. 0102cases hrecurrence_witness
  103. 0103cases hrecurrence_witness_witness
  104. 0104cases hrecurrence_witness_witness_witness
  105. 0105cases hrecurrence_witness_witness_witness_witness
  106. 0106cases hrecurrence_witness_witness_witness_witness_right
  107. 0107cases hrecurrence_witness_witness_witness_witness_right_right
  108. 0108cases hrecurrence_witness_witness_witness_witness_right_right_right
  109. 0109have hpredecessor_row_bound : Lt(n,S S n)
    Exact native replay linehave hpredecessor_row_bound : exists bcf_lt_gap_bcssol_predecessor_row_bound. bcf_lt_gap_bcssol_predecessor_row_bound + S (n) = S (S n)
  110. 0110specialize le_succ (S n)
  111. 0111specialize le_succ (S n)
  112. 0112apply le_succ
  113. 0113specialize le_refl (S n)
  114. 0114exact le_refl
  115. 0115have hsource_row_bound : Lt(n,S n)
    Exact native replay linehave hsource_row_bound : exists bcf_lt_gap_bcssol_source_row_bound. bcf_lt_gap_bcssol_source_row_bound + S (n) = S n
  116. 0116specialize le_refl (S n)
  117. 0117exact le_refl
  118. 0118have hresult_left_bound : Lt(k,S S n)
    Exact native replay linehave hresult_left_bound : exists bcf_lt_gap_bcssol_result_left_bound. bcf_lt_gap_bcssol_result_left_bound + S (k) = S (S n)
  119. 0119specialize le_succ (S k)
  120. 0120specialize le_succ (S n)
  121. 0121apply le_succ
  122. 0122exact htarget_range
  123. 0123have hsource_left_bound : Lt(k,S n)
    Exact native replay linehave hsource_left_bound : exists bcf_lt_gap_bcssol_source_left_bound. bcf_lt_gap_bcssol_source_left_bound + S (k) = S n
  124. 0124exact htarget_range
  125. 0125have hsource_right_bound : Lt(S k,S n)
    Exact native replay linehave hsource_right_bound : exists bcf_lt_gap_bcssol_source_right_bound. bcf_lt_gap_bcssol_source_right_bound + S (S k) = S n
  126. 0126specialize succ_le_succ (S k)
  127. 0127specialize succ_le_succ n
  128. 0128apply succ_le_succ
  129. 0129exact hbound
  130. 0130have hleft_agreement : ∀ bcf_index_bcssol_left_agreement. ∀ bcf_left_value_bcssol_left_agreement. ∀ bcf_right_value_bcssol_left_agreement. Lt(bcf_index_bcssol_left_agreement,S S n) → Lt(bcf_index_bcssol_left_agreement,S n) → BetaAt(x19,x20,bcf_index_bcssol_left_agreement,bcf_left_value_bcssol_left_agreement) → BetaAt(x5,x6,bcf_index_bcssol_left_agreement,bcf_right_value_bcssol_left_agreement) → bcf_left_value_bcssol_left_agreement = bcf_right_value_bcssol_left_agreement
    Exact native replay linehave hleft_agreement : forall bcf_index_bcssol_left_agreement bcf_left_value_bcssol_left_agreement bcf_right_value_bcssol_left_agreement. (exists bcf_lt_gap_bcssol_left_agreement_left_bound. bcf_lt_gap_bcssol_left_agreement_left_bound + S (bcf_index_bcssol_left_agreement) = S (S n)) -> (exists bcf_lt_gap_bcssol_left_agreement_right_bound. bcf_lt_gap_bcssol_left_agreement_right_bound + S (bcf_index_bcssol_left_agreement) = S n) -> (((exists bcf_height_bcssol_left_agreement_left_at. bcf_height_bcssol_left_agreement_left_at + S (bcf_left_value_bcssol_left_agreement) = S ((S (bcf_index_bcssol_left_agreement)) * x20)) /\ exists bcf_quotient_bcssol_left_agreement_left_at. x19 = bcf_quotient_bcssol_left_agreement_left_at * S ((S (bcf_index_bcssol_left_agreement)) * x20) + (bcf_left_value_bcssol_left_agreement))) -> (((exists bcf_height_bcssol_left_agreement_right_at. bcf_height_bcssol_left_agreement_right_at + S (bcf_right_value_bcssol_left_agreement) = S ((S (bcf_index_bcssol_left_agreement)) * x6)) /\ exists bcf_quotient_bcssol_left_agreement_right_at. x5 = bcf_quotient_bcssol_left_agreement_right_at * S ((S (bcf_index_bcssol_left_agreement)) * x6) + (bcf_right_value_bcssol_left_agreement))) -> bcf_left_value_bcssol_left_agreement = bcf_right_value_bcssol_left_agreement
  131. 0131specialize beta_pascal_table_row_pointwise_functional x13
  132. 0132specialize beta_pascal_table_row_pointwise_functional x14
  133. 0133specialize beta_pascal_table_row_pointwise_functional x15
  134. 0134specialize beta_pascal_table_row_pointwise_functional x16
  135. 0135specialize beta_pascal_table_row_pointwise_functional (S (S n))
  136. 0136specialize beta_pascal_table_row_pointwise_functional (S (S n))
  137. 0137specialize beta_pascal_table_row_pointwise_functional x1
  138. 0138specialize beta_pascal_table_row_pointwise_functional x2
  139. 0139specialize beta_pascal_table_row_pointwise_functional x3
  140. 0140specialize beta_pascal_table_row_pointwise_functional x4
  141. 0141specialize beta_pascal_table_row_pointwise_functional (S n)
  142. 0142specialize beta_pascal_table_row_pointwise_functional (S n)
  143. 0143specialize beta_pascal_table_row_pointwise_functional n
  144. 0144specialize beta_pascal_table_row_pointwise_functional x19
  145. 0145specialize beta_pascal_table_row_pointwise_functional x20
  146. 0146specialize beta_pascal_table_row_pointwise_functional x5
  147. 0147specialize beta_pascal_table_row_pointwise_functional x6
  148. 0148apply beta_pascal_table_row_pointwise_functional
  149. 0149exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
  150. 0150exact hleft_right_right_witness_witness_witness_witness_witness_witness_left
  151. 0151exact hpredecessor_row_bound
  152. 0152exact hsource_row_bound
  153. 0153exact hrecurrence_witness_witness_witness_witness_left
  154. 0154exact hrecurrence_witness_witness_witness_witness_right_left
  155. 0155exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_left
  156. 0156exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  157. 0157have hleft_value : x21 = x
  158. 0158specialize hleft_agreement k
  159. 0159specialize hleft_agreement x21
  160. 0160specialize hleft_agreement x
  161. 0161apply hleft_agreement
  162. 0162exact hresult_left_bound
  163. 0163exact hsource_left_bound
  164. 0164exact hrecurrence_witness_witness_witness_witness_right_right_left
  165. 0165exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  166. 0166have hright_agreement : ∀ bcf_index_bcssol_right_agreement. ∀ bcf_left_value_bcssol_right_agreement. ∀ bcf_right_value_bcssol_right_agreement. Lt(bcf_index_bcssol_right_agreement,S S n) → Lt(bcf_index_bcssol_right_agreement,S n) → BetaAt(x19,x20,bcf_index_bcssol_right_agreement,bcf_left_value_bcssol_right_agreement) → BetaAt(x11,x12,bcf_index_bcssol_right_agreement,bcf_right_value_bcssol_right_agreement) → bcf_left_value_bcssol_right_agreement = bcf_right_value_bcssol_right_agreement
    Exact native replay linehave hright_agreement : forall bcf_index_bcssol_right_agreement bcf_left_value_bcssol_right_agreement bcf_right_value_bcssol_right_agreement. (exists bcf_lt_gap_bcssol_right_agreement_left_bound. bcf_lt_gap_bcssol_right_agreement_left_bound + S (bcf_index_bcssol_right_agreement) = S (S n)) -> (exists bcf_lt_gap_bcssol_right_agreement_right_bound. bcf_lt_gap_bcssol_right_agreement_right_bound + S (bcf_index_bcssol_right_agreement) = S n) -> (((exists bcf_height_bcssol_right_agreement_left_at. bcf_height_bcssol_right_agreement_left_at + S (bcf_left_value_bcssol_right_agreement) = S ((S (bcf_index_bcssol_right_agreement)) * x20)) /\ exists bcf_quotient_bcssol_right_agreement_left_at. x19 = bcf_quotient_bcssol_right_agreement_left_at * S ((S (bcf_index_bcssol_right_agreement)) * x20) + (bcf_left_value_bcssol_right_agreement))) -> (((exists bcf_height_bcssol_right_agreement_right_at. bcf_height_bcssol_right_agreement_right_at + S (bcf_right_value_bcssol_right_agreement) = S ((S (bcf_index_bcssol_right_agreement)) * x12)) /\ exists bcf_quotient_bcssol_right_agreement_right_at. x11 = bcf_quotient_bcssol_right_agreement_right_at * S ((S (bcf_index_bcssol_right_agreement)) * x12) + (bcf_right_value_bcssol_right_agreement))) -> bcf_left_value_bcssol_right_agreement = bcf_right_value_bcssol_right_agreement
  167. 0167specialize beta_pascal_table_row_pointwise_functional x13
  168. 0168specialize beta_pascal_table_row_pointwise_functional x14
  169. 0169specialize beta_pascal_table_row_pointwise_functional x15
  170. 0170specialize beta_pascal_table_row_pointwise_functional x16
  171. 0171specialize beta_pascal_table_row_pointwise_functional (S (S n))
  172. 0172specialize beta_pascal_table_row_pointwise_functional (S (S n))
  173. 0173specialize beta_pascal_table_row_pointwise_functional x7
  174. 0174specialize beta_pascal_table_row_pointwise_functional x8
  175. 0175specialize beta_pascal_table_row_pointwise_functional x9
  176. 0176specialize beta_pascal_table_row_pointwise_functional x10
  177. 0177specialize beta_pascal_table_row_pointwise_functional (S n)
  178. 0178specialize beta_pascal_table_row_pointwise_functional (S n)
  179. 0179specialize beta_pascal_table_row_pointwise_functional n
  180. 0180specialize beta_pascal_table_row_pointwise_functional x19
  181. 0181specialize beta_pascal_table_row_pointwise_functional x20
  182. 0182specialize beta_pascal_table_row_pointwise_functional x11
  183. 0183specialize beta_pascal_table_row_pointwise_functional x12
  184. 0184apply beta_pascal_table_row_pointwise_functional
  185. 0185exact htarget_right_right_witness_witness_witness_witness_witness_witness_left
  186. 0186exact hright_right_right_witness_witness_witness_witness_witness_witness_left
  187. 0187exact hpredecessor_row_bound
  188. 0188exact hsource_row_bound
  189. 0189exact hrecurrence_witness_witness_witness_witness_left
  190. 0190exact hrecurrence_witness_witness_witness_witness_right_left
  191. 0191exact hright_right_right_witness_witness_witness_witness_witness_witness_right_left
  192. 0192exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  193. 0193have hright_value : x22 = y
  194. 0194specialize hright_agreement (S k)
  195. 0195specialize hright_agreement x22
  196. 0196specialize hright_agreement y
  197. 0197apply hright_agreement
  198. 0198exact hcurrent_cell_bound
  199. 0199exact hsource_right_bound
  200. 0200exact hrecurrence_witness_witness_witness_witness_right_right_right_left
  201. 0201exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  202. 0202trans x21 + x22
  203. 0203exact hrecurrence_witness_witness_witness_witness_right_right_right_right
  204. 0204congr
  205. 0205exact hleft_value
  206. 0206exact hright_value