BT00T7

beta_pascal_table_prefix_exists

Alpha body-checked · checked-use disabled

Every finite width and height has a nested beta Pascal table.

Exact expanded PA statement

forall w r. exists bb bc sb sc. (forall bcf_row_index_bptpx_result. (exists bcf_lt_gap_bptpx_result_row_bound. bcf_lt_gap_bptpx_result_row_bound + S (bcf_row_index_bptpx_result) = r) -> exists bcf_row_code_bptpx_result bcf_row_scale_bptpx_result. ((((exists bcf_height_bptpx_result_decoded_row_code. bcf_height_bptpx_result_decoded_row_code + S (bcf_row_code_bptpx_result) = S ((S (bcf_row_index_bptpx_result)) * bc)) /\ exists bcf_quotient_bptpx_result_decoded_row_code. bb = bcf_quotient_bptpx_result_decoded_row_code * S ((S (bcf_row_index_bptpx_result)) * bc) + (bcf_row_code_bptpx_result))) /\ ((((exists bcf_height_bptpx_result_decoded_row_scale. bcf_height_bptpx_result_decoded_row_scale + S (bcf_row_scale_bptpx_result) = S ((S (bcf_row_index_bptpx_result)) * sc)) /\ exists bcf_quotient_bptpx_result_decoded_row_scale. sb = bcf_quotient_bptpx_result_decoded_row_scale * S ((S (bcf_row_index_bptpx_result)) * sc) + (bcf_row_scale_bptpx_result))) /\ ((bcf_row_index_bptpx_result = 0 /\ (forall bcf_index_bptpx_result_zero_row. (exists bcf_lt_gap_bptpx_result_zero_row_bound. bcf_lt_gap_bptpx_result_zero_row_bound + S (bcf_index_bptpx_result_zero_row) = w) -> exists bcf_value_bptpx_result_zero_row. ((((exists bcf_height_bptpx_result_zero_row_entry. bcf_height_bptpx_result_zero_row_entry + S (bcf_value_bptpx_result_zero_row) = S ((S (bcf_index_bptpx_result_zero_row)) * bcf_row_scale_bptpx_result)) /\ exists bcf_quotient_bptpx_result_zero_row_entry. bcf_row_code_bptpx_result = bcf_quotient_bptpx_result_zero_row_entry * S ((S (bcf_index_bptpx_result_zero_row)) * bcf_row_scale_bptpx_result) + (bcf_value_bptpx_result_zero_row))) /\ ((bcf_index_bptpx_result_zero_row = 0 /\ bcf_value_bptpx_result_zero_row = 1) \/ exists bcf_predecessor_bptpx_result_zero_row. bcf_index_bptpx_result_zero_row = S bcf_predecessor_bptpx_result_zero_row /\ bcf_value_bptpx_result_zero_row = 0)))) \/ exists bcf_predecessor_bptpx_result bcf_previous_code_bptpx_result bcf_previous_scale_bptpx_result. bcf_row_index_bptpx_result = S bcf_predecessor_bptpx_result /\ ((((exists bcf_height_bptpx_result_decoded_previous_code. bcf_height_bptpx_result_decoded_previous_code + S (bcf_previous_code_bptpx_result) = S ((S (bcf_predecessor_bptpx_result)) * bc)) /\ exists bcf_quotient_bptpx_result_decoded_previous_code. bb = bcf_quotient_bptpx_result_decoded_previous_code * S ((S (bcf_predecessor_bptpx_result)) * bc) + (bcf_previous_code_bptpx_result))) /\ ((((exists bcf_height_bptpx_result_decoded_previous_scale. bcf_height_bptpx_result_decoded_previous_scale + S (bcf_previous_scale_bptpx_result) = S ((S (bcf_predecessor_bptpx_result)) * sc)) /\ exists bcf_quotient_bptpx_result_decoded_previous_scale. sb = bcf_quotient_bptpx_result_decoded_previous_scale * S ((S (bcf_predecessor_bptpx_result)) * sc) + (bcf_previous_scale_bptpx_result))) /\ (forall bcf_index_bptpx_result_row_step. (exists bcf_lt_gap_bptpx_result_row_step_bound. bcf_lt_gap_bptpx_result_row_step_bound + S (bcf_index_bptpx_result_row_step) = w) -> exists bcf_value_bptpx_result_row_step. ((((exists bcf_height_bptpx_result_row_step_entry. bcf_height_bptpx_result_row_step_entry + S (bcf_value_bptpx_result_row_step) = S ((S (bcf_index_bptpx_result_row_step)) * bcf_row_scale_bptpx_result)) /\ exists bcf_quotient_bptpx_result_row_step_entry. bcf_row_code_bptpx_result = bcf_quotient_bptpx_result_row_step_entry * S ((S (bcf_index_bptpx_result_row_step)) * bcf_row_scale_bptpx_result) + (bcf_value_bptpx_result_row_step))) /\ ((bcf_index_bptpx_result_row_step = 0 /\ bcf_value_bptpx_result_row_step = 1) \/ exists bcf_predecessor_bptpx_result_row_step bcf_left_bptpx_result_row_step bcf_right_bptpx_result_row_step. bcf_index_bptpx_result_row_step = S bcf_predecessor_bptpx_result_row_step /\ ((((exists bcf_height_bptpx_result_row_step_previous_left. bcf_height_bptpx_result_row_step_previous_left + S (bcf_left_bptpx_result_row_step) = S ((S (bcf_predecessor_bptpx_result_row_step)) * bcf_previous_scale_bptpx_result)) /\ exists bcf_quotient_bptpx_result_row_step_previous_left. bcf_previous_code_bptpx_result = bcf_quotient_bptpx_result_row_step_previous_left * S ((S (bcf_predecessor_bptpx_result_row_step)) * bcf_previous_scale_bptpx_result) + (bcf_left_bptpx_result_row_step))) /\ ((((exists bcf_height_bptpx_result_row_step_previous_right. bcf_height_bptpx_result_row_step_previous_right + S (bcf_right_bptpx_result_row_step) = S ((S (S (bcf_predecessor_bptpx_result_row_step))) * bcf_previous_scale_bptpx_result)) /\ exists bcf_quotient_bptpx_result_row_step_previous_right. bcf_previous_code_bptpx_result = bcf_quotient_bptpx_result_row_step_previous_right * S ((S (S (bcf_predecessor_bptpx_result_row_step))) * bcf_previous_scale_bptpx_result) + (bcf_right_bptpx_result_row_step))) /\ bcf_value_bptpx_result_row_step = bcf_left_bptpx_result_row_step + bcf_right_bptpx_result_row_step)))))))))))

Structural proof guide

Every finite width and height has a nested beta Pascal table.

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

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00T6 beta_pascal_table_prefix_extend

Direct dependents

BT00T8 choose_exists

Formal native tactic body

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

  1. 0001intro w
  2. 0002induction r
  3. 0003exists 0
  4. 0004exists 0
  5. 0005exists 0
  6. 0006exists 0
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010cases hi
  11. 0011have hsi : S i = 0
  12. 0012specialize add_eq_zero_right x
  13. 0013specialize add_eq_zero_right (S i)
  14. 0014apply add_eq_zero_right
  15. 0015exact hi_witness
  16. 0016specialize succ_ne_zero i
  17. 0017apply succ_ne_zero
  18. 0018exact hsi
  19. 0019have hprevious : exists bb bc sb sc. (forall bcf_row_index_bptpx_previous. (exists bcf_lt_gap_bptpx_previous_row_bound. bcf_lt_gap_bptpx_previous_row_bound + S (bcf_row_index_bptpx_previous) = r) -> exists bcf_row_code_bptpx_previous bcf_row_scale_bptpx_previous. ((((exists bcf_height_bptpx_previous_decoded_row_code. bcf_height_bptpx_previous_decoded_row_code + S (bcf_row_code_bptpx_previous) = S ((S (bcf_row_index_bptpx_previous)) * bc)) /\ exists bcf_quotient_bptpx_previous_decoded_row_code. bb = bcf_quotient_bptpx_previous_decoded_row_code * S ((S (bcf_row_index_bptpx_previous)) * bc) + (bcf_row_code_bptpx_previous))) /\ ((((exists bcf_height_bptpx_previous_decoded_row_scale. bcf_height_bptpx_previous_decoded_row_scale + S (bcf_row_scale_bptpx_previous) = S ((S (bcf_row_index_bptpx_previous)) * sc)) /\ exists bcf_quotient_bptpx_previous_decoded_row_scale. sb = bcf_quotient_bptpx_previous_decoded_row_scale * S ((S (bcf_row_index_bptpx_previous)) * sc) + (bcf_row_scale_bptpx_previous))) /\ ((bcf_row_index_bptpx_previous = 0 /\ (forall bcf_index_bptpx_previous_zero_row. (exists bcf_lt_gap_bptpx_previous_zero_row_bound. bcf_lt_gap_bptpx_previous_zero_row_bound + S (bcf_index_bptpx_previous_zero_row) = w) -> exists bcf_value_bptpx_previous_zero_row. ((((exists bcf_height_bptpx_previous_zero_row_entry. bcf_height_bptpx_previous_zero_row_entry + S (bcf_value_bptpx_previous_zero_row) = S ((S (bcf_index_bptpx_previous_zero_row)) * bcf_row_scale_bptpx_previous)) /\ exists bcf_quotient_bptpx_previous_zero_row_entry. bcf_row_code_bptpx_previous = bcf_quotient_bptpx_previous_zero_row_entry * S ((S (bcf_index_bptpx_previous_zero_row)) * bcf_row_scale_bptpx_previous) + (bcf_value_bptpx_previous_zero_row))) /\ ((bcf_index_bptpx_previous_zero_row = 0 /\ bcf_value_bptpx_previous_zero_row = 1) \/ exists bcf_predecessor_bptpx_previous_zero_row. bcf_index_bptpx_previous_zero_row = S bcf_predecessor_bptpx_previous_zero_row /\ bcf_value_bptpx_previous_zero_row = 0)))) \/ exists bcf_predecessor_bptpx_previous bcf_previous_code_bptpx_previous bcf_previous_scale_bptpx_previous. bcf_row_index_bptpx_previous = S bcf_predecessor_bptpx_previous /\ ((((exists bcf_height_bptpx_previous_decoded_previous_code. bcf_height_bptpx_previous_decoded_previous_code + S (bcf_previous_code_bptpx_previous) = S ((S (bcf_predecessor_bptpx_previous)) * bc)) /\ exists bcf_quotient_bptpx_previous_decoded_previous_code. bb = bcf_quotient_bptpx_previous_decoded_previous_code * S ((S (bcf_predecessor_bptpx_previous)) * bc) + (bcf_previous_code_bptpx_previous))) /\ ((((exists bcf_height_bptpx_previous_decoded_previous_scale. bcf_height_bptpx_previous_decoded_previous_scale + S (bcf_previous_scale_bptpx_previous) = S ((S (bcf_predecessor_bptpx_previous)) * sc)) /\ exists bcf_quotient_bptpx_previous_decoded_previous_scale. sb = bcf_quotient_bptpx_previous_decoded_previous_scale * S ((S (bcf_predecessor_bptpx_previous)) * sc) + (bcf_previous_scale_bptpx_previous))) /\ (forall bcf_index_bptpx_previous_row_step. (exists bcf_lt_gap_bptpx_previous_row_step_bound. bcf_lt_gap_bptpx_previous_row_step_bound + S (bcf_index_bptpx_previous_row_step) = w) -> exists bcf_value_bptpx_previous_row_step. ((((exists bcf_height_bptpx_previous_row_step_entry. bcf_height_bptpx_previous_row_step_entry + S (bcf_value_bptpx_previous_row_step) = S ((S (bcf_index_bptpx_previous_row_step)) * bcf_row_scale_bptpx_previous)) /\ exists bcf_quotient_bptpx_previous_row_step_entry. bcf_row_code_bptpx_previous = bcf_quotient_bptpx_previous_row_step_entry * S ((S (bcf_index_bptpx_previous_row_step)) * bcf_row_scale_bptpx_previous) + (bcf_value_bptpx_previous_row_step))) /\ ((bcf_index_bptpx_previous_row_step = 0 /\ bcf_value_bptpx_previous_row_step = 1) \/ exists bcf_predecessor_bptpx_previous_row_step bcf_left_bptpx_previous_row_step bcf_right_bptpx_previous_row_step. bcf_index_bptpx_previous_row_step = S bcf_predecessor_bptpx_previous_row_step /\ ((((exists bcf_height_bptpx_previous_row_step_previous_left. bcf_height_bptpx_previous_row_step_previous_left + S (bcf_left_bptpx_previous_row_step) = S ((S (bcf_predecessor_bptpx_previous_row_step)) * bcf_previous_scale_bptpx_previous)) /\ exists bcf_quotient_bptpx_previous_row_step_previous_left. bcf_previous_code_bptpx_previous = bcf_quotient_bptpx_previous_row_step_previous_left * S ((S (bcf_predecessor_bptpx_previous_row_step)) * bcf_previous_scale_bptpx_previous) + (bcf_left_bptpx_previous_row_step))) /\ ((((exists bcf_height_bptpx_previous_row_step_previous_right. bcf_height_bptpx_previous_row_step_previous_right + S (bcf_right_bptpx_previous_row_step) = S ((S (S (bcf_predecessor_bptpx_previous_row_step))) * bcf_previous_scale_bptpx_previous)) /\ exists bcf_quotient_bptpx_previous_row_step_previous_right. bcf_previous_code_bptpx_previous = bcf_quotient_bptpx_previous_row_step_previous_right * S ((S (S (bcf_predecessor_bptpx_previous_row_step))) * bcf_previous_scale_bptpx_previous) + (bcf_right_bptpx_previous_row_step))) /\ bcf_value_bptpx_previous_row_step = bcf_left_bptpx_previous_row_step + bcf_right_bptpx_previous_row_step)))))))))))
  20. 0020exact IH
  21. 0021cases hprevious
  22. 0022cases hprevious_witness
  23. 0023cases hprevious_witness_witness
  24. 0024cases hprevious_witness_witness_witness
  25. 0025have hnext : exists bb bc sb sc. (forall bcf_row_index_bptpx_successor. (exists bcf_lt_gap_bptpx_successor_row_bound. bcf_lt_gap_bptpx_successor_row_bound + S (bcf_row_index_bptpx_successor) = S (r)) -> exists bcf_row_code_bptpx_successor bcf_row_scale_bptpx_successor. ((((exists bcf_height_bptpx_successor_decoded_row_code. bcf_height_bptpx_successor_decoded_row_code + S (bcf_row_code_bptpx_successor) = S ((S (bcf_row_index_bptpx_successor)) * bc)) /\ exists bcf_quotient_bptpx_successor_decoded_row_code. bb = bcf_quotient_bptpx_successor_decoded_row_code * S ((S (bcf_row_index_bptpx_successor)) * bc) + (bcf_row_code_bptpx_successor))) /\ ((((exists bcf_height_bptpx_successor_decoded_row_scale. bcf_height_bptpx_successor_decoded_row_scale + S (bcf_row_scale_bptpx_successor) = S ((S (bcf_row_index_bptpx_successor)) * sc)) /\ exists bcf_quotient_bptpx_successor_decoded_row_scale. sb = bcf_quotient_bptpx_successor_decoded_row_scale * S ((S (bcf_row_index_bptpx_successor)) * sc) + (bcf_row_scale_bptpx_successor))) /\ ((bcf_row_index_bptpx_successor = 0 /\ (forall bcf_index_bptpx_successor_zero_row. (exists bcf_lt_gap_bptpx_successor_zero_row_bound. bcf_lt_gap_bptpx_successor_zero_row_bound + S (bcf_index_bptpx_successor_zero_row) = w) -> exists bcf_value_bptpx_successor_zero_row. ((((exists bcf_height_bptpx_successor_zero_row_entry. bcf_height_bptpx_successor_zero_row_entry + S (bcf_value_bptpx_successor_zero_row) = S ((S (bcf_index_bptpx_successor_zero_row)) * bcf_row_scale_bptpx_successor)) /\ exists bcf_quotient_bptpx_successor_zero_row_entry. bcf_row_code_bptpx_successor = bcf_quotient_bptpx_successor_zero_row_entry * S ((S (bcf_index_bptpx_successor_zero_row)) * bcf_row_scale_bptpx_successor) + (bcf_value_bptpx_successor_zero_row))) /\ ((bcf_index_bptpx_successor_zero_row = 0 /\ bcf_value_bptpx_successor_zero_row = 1) \/ exists bcf_predecessor_bptpx_successor_zero_row. bcf_index_bptpx_successor_zero_row = S bcf_predecessor_bptpx_successor_zero_row /\ bcf_value_bptpx_successor_zero_row = 0)))) \/ exists bcf_predecessor_bptpx_successor bcf_previous_code_bptpx_successor bcf_previous_scale_bptpx_successor. bcf_row_index_bptpx_successor = S bcf_predecessor_bptpx_successor /\ ((((exists bcf_height_bptpx_successor_decoded_previous_code. bcf_height_bptpx_successor_decoded_previous_code + S (bcf_previous_code_bptpx_successor) = S ((S (bcf_predecessor_bptpx_successor)) * bc)) /\ exists bcf_quotient_bptpx_successor_decoded_previous_code. bb = bcf_quotient_bptpx_successor_decoded_previous_code * S ((S (bcf_predecessor_bptpx_successor)) * bc) + (bcf_previous_code_bptpx_successor))) /\ ((((exists bcf_height_bptpx_successor_decoded_previous_scale. bcf_height_bptpx_successor_decoded_previous_scale + S (bcf_previous_scale_bptpx_successor) = S ((S (bcf_predecessor_bptpx_successor)) * sc)) /\ exists bcf_quotient_bptpx_successor_decoded_previous_scale. sb = bcf_quotient_bptpx_successor_decoded_previous_scale * S ((S (bcf_predecessor_bptpx_successor)) * sc) + (bcf_previous_scale_bptpx_successor))) /\ (forall bcf_index_bptpx_successor_row_step. (exists bcf_lt_gap_bptpx_successor_row_step_bound. bcf_lt_gap_bptpx_successor_row_step_bound + S (bcf_index_bptpx_successor_row_step) = w) -> exists bcf_value_bptpx_successor_row_step. ((((exists bcf_height_bptpx_successor_row_step_entry. bcf_height_bptpx_successor_row_step_entry + S (bcf_value_bptpx_successor_row_step) = S ((S (bcf_index_bptpx_successor_row_step)) * bcf_row_scale_bptpx_successor)) /\ exists bcf_quotient_bptpx_successor_row_step_entry. bcf_row_code_bptpx_successor = bcf_quotient_bptpx_successor_row_step_entry * S ((S (bcf_index_bptpx_successor_row_step)) * bcf_row_scale_bptpx_successor) + (bcf_value_bptpx_successor_row_step))) /\ ((bcf_index_bptpx_successor_row_step = 0 /\ bcf_value_bptpx_successor_row_step = 1) \/ exists bcf_predecessor_bptpx_successor_row_step bcf_left_bptpx_successor_row_step bcf_right_bptpx_successor_row_step. bcf_index_bptpx_successor_row_step = S bcf_predecessor_bptpx_successor_row_step /\ ((((exists bcf_height_bptpx_successor_row_step_previous_left. bcf_height_bptpx_successor_row_step_previous_left + S (bcf_left_bptpx_successor_row_step) = S ((S (bcf_predecessor_bptpx_successor_row_step)) * bcf_previous_scale_bptpx_successor)) /\ exists bcf_quotient_bptpx_successor_row_step_previous_left. bcf_previous_code_bptpx_successor = bcf_quotient_bptpx_successor_row_step_previous_left * S ((S (bcf_predecessor_bptpx_successor_row_step)) * bcf_previous_scale_bptpx_successor) + (bcf_left_bptpx_successor_row_step))) /\ ((((exists bcf_height_bptpx_successor_row_step_previous_right. bcf_height_bptpx_successor_row_step_previous_right + S (bcf_right_bptpx_successor_row_step) = S ((S (S (bcf_predecessor_bptpx_successor_row_step))) * bcf_previous_scale_bptpx_successor)) /\ exists bcf_quotient_bptpx_successor_row_step_previous_right. bcf_previous_code_bptpx_successor = bcf_quotient_bptpx_successor_row_step_previous_right * S ((S (S (bcf_predecessor_bptpx_successor_row_step))) * bcf_previous_scale_bptpx_successor) + (bcf_right_bptpx_successor_row_step))) /\ bcf_value_bptpx_successor_row_step = bcf_left_bptpx_successor_row_step + bcf_right_bptpx_successor_row_step)))))))))))
  26. 0026specialize beta_pascal_table_prefix_extend x
  27. 0027specialize beta_pascal_table_prefix_extend x1
  28. 0028specialize beta_pascal_table_prefix_extend x2
  29. 0029specialize beta_pascal_table_prefix_extend x3
  30. 0030specialize beta_pascal_table_prefix_extend w
  31. 0031specialize beta_pascal_table_prefix_extend r
  32. 0032apply beta_pascal_table_prefix_extend
  33. 0033exact hprevious_witness_witness_witness_witness
  34. 0034exact hnext