BT00TI

choose_succ_succ_of_lt

Alpha body-checked · checked-use disabled

Interior Choose values satisfy Pascal's successor recurrence.

Exact expanded 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

Structural proof guide

Interior Choose values satisfy Pascal's successor recurrence.

Direct prerequisites: lt_not_le, lt_to_le, le_refl, le_succ, succ_le_succ, beta_pascal_table_row_pointwise_functional, beta_pascal_table_successor_cell_recurrence. The authored body proceeds by case analysis (44), intermediate claims (14).

Proof neighborhood

Direct dependencies

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 dependents

BT00TJ choose_succ_succ

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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