BT00T3

beta_pascal_zero_row_exists

Alpha body-checked · checked-use disabled

Every finite width has a beta-coded Pascal zero row.

Exact expanded PA statement

forall w. exists b c. (forall bcf_index_bpzrx_result. (exists bcf_lt_gap_bpzrx_result_bound. bcf_lt_gap_bpzrx_result_bound + S (bcf_index_bpzrx_result) = w) -> exists bcf_value_bpzrx_result. ((((exists bcf_height_bpzrx_result_entry. bcf_height_bpzrx_result_entry + S (bcf_value_bpzrx_result) = S ((S (bcf_index_bpzrx_result)) * c)) /\ exists bcf_quotient_bpzrx_result_entry. b = bcf_quotient_bpzrx_result_entry * S ((S (bcf_index_bpzrx_result)) * c) + (bcf_value_bpzrx_result))) /\ ((bcf_index_bpzrx_result = 0 /\ bcf_value_bpzrx_result = 1) \/ exists bcf_predecessor_bpzrx_result. bcf_index_bpzrx_result = S bcf_predecessor_bpzrx_result /\ bcf_value_bpzrx_result = 0)))

Structural proof guide

Every finite width has a beta-coded Pascal zero row.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, beta_pascal_zero_row_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 BT00T2 beta_pascal_zero_row_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.

  1. 0001induction w
  2. 0002exists 0
  3. 0003exists 0
  4. 0004intro i
  5. 0005intro hi
  6. 0006exfalso
  7. 0007cases hi
  8. 0008have hsi : S i = 0
  9. 0009specialize add_eq_zero_right x
  10. 0010specialize add_eq_zero_right (S i)
  11. 0011apply add_eq_zero_right
  12. 0012exact hi_witness
  13. 0013specialize succ_ne_zero i
  14. 0014apply succ_ne_zero
  15. 0015exact hsi
  16. 0016have hprevious : exists b c. (forall bcf_index_bpzrx_previous. (exists bcf_lt_gap_bpzrx_previous_bound. bcf_lt_gap_bpzrx_previous_bound + S (bcf_index_bpzrx_previous) = w) -> exists bcf_value_bpzrx_previous. ((((exists bcf_height_bpzrx_previous_entry. bcf_height_bpzrx_previous_entry + S (bcf_value_bpzrx_previous) = S ((S (bcf_index_bpzrx_previous)) * c)) /\ exists bcf_quotient_bpzrx_previous_entry. b = bcf_quotient_bpzrx_previous_entry * S ((S (bcf_index_bpzrx_previous)) * c) + (bcf_value_bpzrx_previous))) /\ ((bcf_index_bpzrx_previous = 0 /\ bcf_value_bpzrx_previous = 1) \/ exists bcf_predecessor_bpzrx_previous. bcf_index_bpzrx_previous = S bcf_predecessor_bpzrx_previous /\ bcf_value_bpzrx_previous = 0)))
  17. 0017exact IH
  18. 0018cases hprevious
  19. 0019cases hprevious_witness
  20. 0020have hnext : exists b c. (forall bcf_index_bpzrx_successor. (exists bcf_lt_gap_bpzrx_successor_bound. bcf_lt_gap_bpzrx_successor_bound + S (bcf_index_bpzrx_successor) = S (w)) -> exists bcf_value_bpzrx_successor. ((((exists bcf_height_bpzrx_successor_entry. bcf_height_bpzrx_successor_entry + S (bcf_value_bpzrx_successor) = S ((S (bcf_index_bpzrx_successor)) * c)) /\ exists bcf_quotient_bpzrx_successor_entry. b = bcf_quotient_bpzrx_successor_entry * S ((S (bcf_index_bpzrx_successor)) * c) + (bcf_value_bpzrx_successor))) /\ ((bcf_index_bpzrx_successor = 0 /\ bcf_value_bpzrx_successor = 1) \/ exists bcf_predecessor_bpzrx_successor. bcf_index_bpzrx_successor = S bcf_predecessor_bpzrx_successor /\ bcf_value_bpzrx_successor = 0)))
  21. 0021specialize beta_pascal_zero_row_extend x
  22. 0022specialize beta_pascal_zero_row_extend x1
  23. 0023specialize beta_pascal_zero_row_extend w
  24. 0024apply beta_pascal_zero_row_extend
  25. 0025exact hprevious_witness_witness
  26. 0026exact hnext