BT00T5 — beta_pascal_row_step

Exact expanded PA statement

forall pb pc w. exists b c. (forall bcf_index_bpsrx_result. (exists bcf_lt_gap_bpsrx_result_bound. bcf_lt_gap_bpsrx_result_bound + S (bcf_index_bpsrx_result) = w) -> exists bcf_value_bpsrx_result. ((((exists bcf_height_bpsrx_result_entry. bcf_height_bpsrx_result_entry + S (bcf_value_bpsrx_result) = S ((S (bcf_index_bpsrx_result)) * c)) /\ exists bcf_quotient_bpsrx_result_entry. b = bcf_quotient_bpsrx_result_entry * S ((S (bcf_index_bpsrx_result)) * c) + (bcf_value_bpsrx_result))) /\ ((bcf_index_bpsrx_result = 0 /\ bcf_value_bpsrx_result = 1) \/ exists bcf_predecessor_bpsrx_result bcf_left_bpsrx_result bcf_right_bpsrx_result. bcf_index_bpsrx_result = S bcf_predecessor_bpsrx_result /\ ((((exists bcf_height_bpsrx_result_previous_left. bcf_height_bpsrx_result_previous_left + S (bcf_left_bpsrx_result) = S ((S (bcf_predecessor_bpsrx_result)) * pc)) /\ exists bcf_quotient_bpsrx_result_previous_left. pb = bcf_quotient_bpsrx_result_previous_left * S ((S (bcf_predecessor_bpsrx_result)) * pc) + (bcf_left_bpsrx_result))) /\ ((((exists bcf_height_bpsrx_result_previous_right. bcf_height_bpsrx_result_previous_right + S (bcf_right_bpsrx_result) = S ((S (S (bcf_predecessor_bpsrx_result))) * pc)) /\ exists bcf_quotient_bpsrx_result_previous_right. pb = bcf_quotient_bpsrx_result_previous_right * S ((S (S (bcf_predecessor_bpsrx_result))) * pc) + (bcf_right_bpsrx_result))) /\ bcf_value_bpsrx_result = bcf_left_bpsrx_result + bcf_right_bpsrx_result)))))

Structural proof guide

Every previous beta row has a finite Pascal successor row.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, beta_pascal_row_step_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00T4 beta_pascal_row_step_extend

Direct dependents

BT00T6 beta_pascal_table_prefix_extend

Formal native tactic body

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

0001intro pb
0002intro pc
0003induction w
0004exists 0
0005exists 0
0006intro i
0007intro hi
0008exfalso
0009cases hi
0010have hsi : S i = 0
0011specialize add_eq_zero_right x
0012specialize add_eq_zero_right (S i)
0013apply add_eq_zero_right
0014exact hi_witness
0015specialize succ_ne_zero i
0016apply succ_ne_zero
0017exact hsi
0018have hprevious : exists b c. (forall bcf_index_bpsrx_previous. (exists bcf_lt_gap_bpsrx_previous_bound. bcf_lt_gap_bpsrx_previous_bound + S (bcf_index_bpsrx_previous) = w) -> exists bcf_value_bpsrx_previous. ((((exists bcf_height_bpsrx_previous_entry. bcf_height_bpsrx_previous_entry + S (bcf_value_bpsrx_previous) = S ((S (bcf_index_bpsrx_previous)) * c)) /\ exists bcf_quotient_bpsrx_previous_entry. b = bcf_quotient_bpsrx_previous_entry * S ((S (bcf_index_bpsrx_previous)) * c) + (bcf_value_bpsrx_previous))) /\ ((bcf_index_bpsrx_previous = 0 /\ bcf_value_bpsrx_previous = 1) \/ exists bcf_predecessor_bpsrx_previous bcf_left_bpsrx_previous bcf_right_bpsrx_previous. bcf_index_bpsrx_previous = S bcf_predecessor_bpsrx_previous /\ ((((exists bcf_height_bpsrx_previous_previous_left. bcf_height_bpsrx_previous_previous_left + S (bcf_left_bpsrx_previous) = S ((S (bcf_predecessor_bpsrx_previous)) * pc)) /\ exists bcf_quotient_bpsrx_previous_previous_left. pb = bcf_quotient_bpsrx_previous_previous_left * S ((S (bcf_predecessor_bpsrx_previous)) * pc) + (bcf_left_bpsrx_previous))) /\ ((((exists bcf_height_bpsrx_previous_previous_right. bcf_height_bpsrx_previous_previous_right + S (bcf_right_bpsrx_previous) = S ((S (S (bcf_predecessor_bpsrx_previous))) * pc)) /\ exists bcf_quotient_bpsrx_previous_previous_right. pb = bcf_quotient_bpsrx_previous_previous_right * S ((S (S (bcf_predecessor_bpsrx_previous))) * pc) + (bcf_right_bpsrx_previous))) /\ bcf_value_bpsrx_previous = bcf_left_bpsrx_previous + bcf_right_bpsrx_previous)))))
0019exact IH
0020cases hprevious
0021cases hprevious_witness
0022have hnext : exists b c. (forall bcf_index_bpsrx_successor. (exists bcf_lt_gap_bpsrx_successor_bound. bcf_lt_gap_bpsrx_successor_bound + S (bcf_index_bpsrx_successor) = S (w)) -> exists bcf_value_bpsrx_successor. ((((exists bcf_height_bpsrx_successor_entry. bcf_height_bpsrx_successor_entry + S (bcf_value_bpsrx_successor) = S ((S (bcf_index_bpsrx_successor)) * c)) /\ exists bcf_quotient_bpsrx_successor_entry. b = bcf_quotient_bpsrx_successor_entry * S ((S (bcf_index_bpsrx_successor)) * c) + (bcf_value_bpsrx_successor))) /\ ((bcf_index_bpsrx_successor = 0 /\ bcf_value_bpsrx_successor = 1) \/ exists bcf_predecessor_bpsrx_successor bcf_left_bpsrx_successor bcf_right_bpsrx_successor. bcf_index_bpsrx_successor = S bcf_predecessor_bpsrx_successor /\ ((((exists bcf_height_bpsrx_successor_previous_left. bcf_height_bpsrx_successor_previous_left + S (bcf_left_bpsrx_successor) = S ((S (bcf_predecessor_bpsrx_successor)) * pc)) /\ exists bcf_quotient_bpsrx_successor_previous_left. pb = bcf_quotient_bpsrx_successor_previous_left * S ((S (bcf_predecessor_bpsrx_successor)) * pc) + (bcf_left_bpsrx_successor))) /\ ((((exists bcf_height_bpsrx_successor_previous_right. bcf_height_bpsrx_successor_previous_right + S (bcf_right_bpsrx_successor) = S ((S (S (bcf_predecessor_bpsrx_successor))) * pc)) /\ exists bcf_quotient_bpsrx_successor_previous_right. pb = bcf_quotient_bpsrx_successor_previous_right * S ((S (S (bcf_predecessor_bpsrx_successor))) * pc) + (bcf_right_bpsrx_successor))) /\ bcf_value_bpsrx_successor = bcf_left_bpsrx_successor + bcf_right_bpsrx_successor)))))
0023specialize beta_pascal_row_step_extend pb
0024specialize beta_pascal_row_step_extend pc
0025specialize beta_pascal_row_step_extend x
0026specialize beta_pascal_row_step_extend x1
0027specialize beta_pascal_row_step_extend w
0028apply beta_pascal_row_step_extend
0029exact hprevious_witness_witness
0030exact hnext