BT00T8

choose_exists

Alpha body-checked · checked-use disabled

The recurrence-defined Choose relation has a value for every pair.

Exact expanded PA statement

forall n k. exists z. (((exists bcf_lt_gap_bce_result_out_of_range. bcf_lt_gap_bce_result_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bce_result_in_range. bcf_le_gap_bce_result_in_range + (k) = n) /\ (exists bcf_row_code_code_bce_result bcf_row_code_scale_bce_result bcf_row_scale_code_bce_result bcf_row_scale_scale_bce_result bcf_row_code_bce_result bcf_row_scale_bce_result. ((forall bcf_row_index_bce_result_table. (exists bcf_lt_gap_bce_result_table_row_bound. bcf_lt_gap_bce_result_table_row_bound + S (bcf_row_index_bce_result_table) = S (n)) -> exists bcf_row_code_bce_result_table bcf_row_scale_bce_result_table. ((((exists bcf_height_bce_result_table_decoded_row_code. bcf_height_bce_result_table_decoded_row_code + S (bcf_row_code_bce_result_table) = S ((S (bcf_row_index_bce_result_table)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_row_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_table_decoded_row_code * S ((S (bcf_row_index_bce_result_table)) * bcf_row_code_scale_bce_result) + (bcf_row_code_bce_result_table))) /\ ((((exists bcf_height_bce_result_table_decoded_row_scale. bcf_height_bce_result_table_decoded_row_scale + S (bcf_row_scale_bce_result_table) = S ((S (bcf_row_index_bce_result_table)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_row_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_table_decoded_row_scale * S ((S (bcf_row_index_bce_result_table)) * bcf_row_scale_scale_bce_result) + (bcf_row_scale_bce_result_table))) /\ ((bcf_row_index_bce_result_table = 0 /\ (forall bcf_index_bce_result_table_zero_row. (exists bcf_lt_gap_bce_result_table_zero_row_bound. bcf_lt_gap_bce_result_table_zero_row_bound + S (bcf_index_bce_result_table_zero_row) = S (n)) -> exists bcf_value_bce_result_table_zero_row. ((((exists bcf_height_bce_result_table_zero_row_entry. bcf_height_bce_result_table_zero_row_entry + S (bcf_value_bce_result_table_zero_row) = S ((S (bcf_index_bce_result_table_zero_row)) * bcf_row_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_zero_row_entry. bcf_row_code_bce_result_table = bcf_quotient_bce_result_table_zero_row_entry * S ((S (bcf_index_bce_result_table_zero_row)) * bcf_row_scale_bce_result_table) + (bcf_value_bce_result_table_zero_row))) /\ ((bcf_index_bce_result_table_zero_row = 0 /\ bcf_value_bce_result_table_zero_row = 1) \/ exists bcf_predecessor_bce_result_table_zero_row. bcf_index_bce_result_table_zero_row = S bcf_predecessor_bce_result_table_zero_row /\ bcf_value_bce_result_table_zero_row = 0)))) \/ exists bcf_predecessor_bce_result_table bcf_previous_code_bce_result_table bcf_previous_scale_bce_result_table. bcf_row_index_bce_result_table = S bcf_predecessor_bce_result_table /\ ((((exists bcf_height_bce_result_table_decoded_previous_code. bcf_height_bce_result_table_decoded_previous_code + S (bcf_previous_code_bce_result_table) = S ((S (bcf_predecessor_bce_result_table)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_previous_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_table_decoded_previous_code * S ((S (bcf_predecessor_bce_result_table)) * bcf_row_code_scale_bce_result) + (bcf_previous_code_bce_result_table))) /\ ((((exists bcf_height_bce_result_table_decoded_previous_scale. bcf_height_bce_result_table_decoded_previous_scale + S (bcf_previous_scale_bce_result_table) = S ((S (bcf_predecessor_bce_result_table)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_previous_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_table_decoded_previous_scale * S ((S (bcf_predecessor_bce_result_table)) * bcf_row_scale_scale_bce_result) + (bcf_previous_scale_bce_result_table))) /\ (forall bcf_index_bce_result_table_row_step. (exists bcf_lt_gap_bce_result_table_row_step_bound. bcf_lt_gap_bce_result_table_row_step_bound + S (bcf_index_bce_result_table_row_step) = S (n)) -> exists bcf_value_bce_result_table_row_step. ((((exists bcf_height_bce_result_table_row_step_entry. bcf_height_bce_result_table_row_step_entry + S (bcf_value_bce_result_table_row_step) = S ((S (bcf_index_bce_result_table_row_step)) * bcf_row_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_entry. bcf_row_code_bce_result_table = bcf_quotient_bce_result_table_row_step_entry * S ((S (bcf_index_bce_result_table_row_step)) * bcf_row_scale_bce_result_table) + (bcf_value_bce_result_table_row_step))) /\ ((bcf_index_bce_result_table_row_step = 0 /\ bcf_value_bce_result_table_row_step = 1) \/ exists bcf_predecessor_bce_result_table_row_step bcf_left_bce_result_table_row_step bcf_right_bce_result_table_row_step. bcf_index_bce_result_table_row_step = S bcf_predecessor_bce_result_table_row_step /\ ((((exists bcf_height_bce_result_table_row_step_previous_left. bcf_height_bce_result_table_row_step_previous_left + S (bcf_left_bce_result_table_row_step) = S ((S (bcf_predecessor_bce_result_table_row_step)) * bcf_previous_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_previous_left. bcf_previous_code_bce_result_table = bcf_quotient_bce_result_table_row_step_previous_left * S ((S (bcf_predecessor_bce_result_table_row_step)) * bcf_previous_scale_bce_result_table) + (bcf_left_bce_result_table_row_step))) /\ ((((exists bcf_height_bce_result_table_row_step_previous_right. bcf_height_bce_result_table_row_step_previous_right + S (bcf_right_bce_result_table_row_step) = S ((S (S (bcf_predecessor_bce_result_table_row_step))) * bcf_previous_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_previous_right. bcf_previous_code_bce_result_table = bcf_quotient_bce_result_table_row_step_previous_right * S ((S (S (bcf_predecessor_bce_result_table_row_step))) * bcf_previous_scale_bce_result_table) + (bcf_right_bce_result_table_row_step))) /\ bcf_value_bce_result_table_row_step = bcf_left_bce_result_table_row_step + bcf_right_bce_result_table_row_step))))))))))) /\ ((((exists bcf_height_bce_result_decoded_row_code. bcf_height_bce_result_decoded_row_code + S (bcf_row_code_bce_result) = S ((S (n)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_row_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bce_result) + (bcf_row_code_bce_result))) /\ ((((exists bcf_height_bce_result_decoded_row_scale. bcf_height_bce_result_decoded_row_scale + S (bcf_row_scale_bce_result) = S ((S (n)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_row_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bce_result) + (bcf_row_scale_bce_result))) /\ (((exists bcf_height_bce_result_decoded_value. bcf_height_bce_result_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_value. bcf_row_code_bce_result = bcf_quotient_bce_result_decoded_value * S ((S (k)) * bcf_row_scale_bce_result) + (z)))))))))

Structural proof guide

The recurrence-defined Choose relation has a value for every pair.

Direct prerequisites: le_or_lt, beta_at_exists, beta_pascal_table_prefix_exists. The authored body proceeds by case analysis (8), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT0041 beta_at_exists BT00T7 beta_pascal_table_prefix_exists

Direct dependents

BT00TL choose_symmetry BT00TM choose_positive BT00TN central_binom_exists BT00TS central_binom_succ_double_middle BT00TT choose_weighted_vertical BT00TX choose_factorial_bridge BT00VU primorial_four_power_support_package

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. 0003specialize le_or_lt k
  4. 0004specialize le_or_lt n
  5. 0005cases le_or_lt
  6. 0006have htable : exists bb bc sb sc. (forall i. (exists gap. gap + S i = S n) -> exists b c. (((exists h. h + S b = S ((S i) * bc)) /\ exists q. bb = q * S ((S i) * bc) + b) /\ (((exists h. h + S c = S ((S i) * sc)) /\ exists q. sb = q * S ((S i) * sc) + c) /\ (((i = 0 /\ (forall j. (exists gap. gap + S j = S n) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. i = S predecessor /\ (((exists h. h + S previous_code = S ((S predecessor) * bc)) /\ exists q. bb = q * S ((S predecessor) * bc) + previous_code) /\ (((exists h. h + S previous_scale = S ((S predecessor) * sc)) /\ exists q. sb = q * S ((S predecessor) * sc) + previous_scale) /\ forall j. (exists gap. gap + S j = S n) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p u v. j = S p /\ (((exists h. h + S u = S ((S p) * previous_scale)) /\ exists q. previous_code = q * S ((S p) * previous_scale) + u) /\ (((exists h. h + S v = S ((S (S p)) * previous_scale)) /\ exists q. previous_code = q * S ((S (S p)) * previous_scale) + v) /\ value = u + v)))))))))))
  7. 0007specialize beta_pascal_table_prefix_exists (S n)
  8. 0008specialize beta_pascal_table_prefix_exists (S n)
  9. 0009exact beta_pascal_table_prefix_exists
  10. 0010cases htable
  11. 0011cases htable_witness
  12. 0012cases htable_witness_witness
  13. 0013cases htable_witness_witness_witness
  14. 0014have hrow_code : exists b. ((exists h. h + S b = S ((S n) * x1)) /\ exists q. x = q * S ((S n) * x1) + b)
  15. 0015specialize beta_at_exists x
  16. 0016specialize beta_at_exists x1
  17. 0017specialize beta_at_exists n
  18. 0018exact beta_at_exists
  19. 0019cases hrow_code
  20. 0020have hrow_scale : exists c. ((exists h. h + S c = S ((S n) * x3)) /\ exists q. x2 = q * S ((S n) * x3) + c)
  21. 0021specialize beta_at_exists x2
  22. 0022specialize beta_at_exists x3
  23. 0023specialize beta_at_exists n
  24. 0024exact beta_at_exists
  25. 0025cases hrow_scale
  26. 0026have hvalue : exists z. ((exists h. h + S z = S ((S k) * x5)) /\ exists q. x4 = q * S ((S k) * x5) + z)
  27. 0027specialize beta_at_exists x4
  28. 0028specialize beta_at_exists x5
  29. 0029specialize beta_at_exists k
  30. 0030exact beta_at_exists
  31. 0031cases hvalue
  32. 0032exists x6
  33. 0033right
  34. 0034split
  35. 0035exact le_or_lt_left
  36. 0036exists x
  37. 0037exists x1
  38. 0038exists x2
  39. 0039exists x3
  40. 0040exists x4
  41. 0041exists x5
  42. 0042split
  43. 0043exact htable_witness_witness_witness_witness
  44. 0044split
  45. 0045exact hrow_code_witness
  46. 0046split
  47. 0047exact hrow_scale_witness
  48. 0048exact hvalue_witness
  49. 0049exists 0
  50. 0050left
  51. 0051split
  52. 0052exact le_or_lt_right
  53. 0053refl