BT00TM

choose_positive

Alpha body-checked · checked-use disabled

Every in-range relational Choose value is a successor.

Exact expanded PA statement

forall n k z. (exists bcf_le_gap_bcp_bound. bcf_le_gap_bcp_bound + (k) = n) -> (((exists bcf_lt_gap_bcp_source_out_of_range. bcf_lt_gap_bcp_source_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bcp_source_in_range. bcf_le_gap_bcp_source_in_range + (k) = n) /\ (exists bcf_row_code_code_bcp_source bcf_row_code_scale_bcp_source bcf_row_scale_code_bcp_source bcf_row_scale_scale_bcp_source bcf_row_code_bcp_source bcf_row_scale_bcp_source. ((forall bcf_row_index_bcp_source_table. (exists bcf_lt_gap_bcp_source_table_row_bound. bcf_lt_gap_bcp_source_table_row_bound + S (bcf_row_index_bcp_source_table) = S (n)) -> exists bcf_row_code_bcp_source_table bcf_row_scale_bcp_source_table. ((((exists bcf_height_bcp_source_table_decoded_row_code. bcf_height_bcp_source_table_decoded_row_code + S (bcf_row_code_bcp_source_table) = S ((S (bcf_row_index_bcp_source_table)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_row_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_table_decoded_row_code * S ((S (bcf_row_index_bcp_source_table)) * bcf_row_code_scale_bcp_source) + (bcf_row_code_bcp_source_table))) /\ ((((exists bcf_height_bcp_source_table_decoded_row_scale. bcf_height_bcp_source_table_decoded_row_scale + S (bcf_row_scale_bcp_source_table) = S ((S (bcf_row_index_bcp_source_table)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_row_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_table_decoded_row_scale * S ((S (bcf_row_index_bcp_source_table)) * bcf_row_scale_scale_bcp_source) + (bcf_row_scale_bcp_source_table))) /\ ((bcf_row_index_bcp_source_table = 0 /\ (forall bcf_index_bcp_source_table_zero_row. (exists bcf_lt_gap_bcp_source_table_zero_row_bound. bcf_lt_gap_bcp_source_table_zero_row_bound + S (bcf_index_bcp_source_table_zero_row) = S (n)) -> exists bcf_value_bcp_source_table_zero_row. ((((exists bcf_height_bcp_source_table_zero_row_entry. bcf_height_bcp_source_table_zero_row_entry + S (bcf_value_bcp_source_table_zero_row) = S ((S (bcf_index_bcp_source_table_zero_row)) * bcf_row_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_zero_row_entry. bcf_row_code_bcp_source_table = bcf_quotient_bcp_source_table_zero_row_entry * S ((S (bcf_index_bcp_source_table_zero_row)) * bcf_row_scale_bcp_source_table) + (bcf_value_bcp_source_table_zero_row))) /\ ((bcf_index_bcp_source_table_zero_row = 0 /\ bcf_value_bcp_source_table_zero_row = 1) \/ exists bcf_predecessor_bcp_source_table_zero_row. bcf_index_bcp_source_table_zero_row = S bcf_predecessor_bcp_source_table_zero_row /\ bcf_value_bcp_source_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_source_table bcf_previous_code_bcp_source_table bcf_previous_scale_bcp_source_table. bcf_row_index_bcp_source_table = S bcf_predecessor_bcp_source_table /\ ((((exists bcf_height_bcp_source_table_decoded_previous_code. bcf_height_bcp_source_table_decoded_previous_code + S (bcf_previous_code_bcp_source_table) = S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_previous_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_code_scale_bcp_source) + (bcf_previous_code_bcp_source_table))) /\ ((((exists bcf_height_bcp_source_table_decoded_previous_scale. bcf_height_bcp_source_table_decoded_previous_scale + S (bcf_previous_scale_bcp_source_table) = S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_previous_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_scale_scale_bcp_source) + (bcf_previous_scale_bcp_source_table))) /\ (forall bcf_index_bcp_source_table_row_step. (exists bcf_lt_gap_bcp_source_table_row_step_bound. bcf_lt_gap_bcp_source_table_row_step_bound + S (bcf_index_bcp_source_table_row_step) = S (n)) -> exists bcf_value_bcp_source_table_row_step. ((((exists bcf_height_bcp_source_table_row_step_entry. bcf_height_bcp_source_table_row_step_entry + S (bcf_value_bcp_source_table_row_step) = S ((S (bcf_index_bcp_source_table_row_step)) * bcf_row_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_entry. bcf_row_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_entry * S ((S (bcf_index_bcp_source_table_row_step)) * bcf_row_scale_bcp_source_table) + (bcf_value_bcp_source_table_row_step))) /\ ((bcf_index_bcp_source_table_row_step = 0 /\ bcf_value_bcp_source_table_row_step = 1) \/ exists bcf_predecessor_bcp_source_table_row_step bcf_left_bcp_source_table_row_step bcf_right_bcp_source_table_row_step. bcf_index_bcp_source_table_row_step = S bcf_predecessor_bcp_source_table_row_step /\ ((((exists bcf_height_bcp_source_table_row_step_previous_left. bcf_height_bcp_source_table_row_step_previous_left + S (bcf_left_bcp_source_table_row_step) = S ((S (bcf_predecessor_bcp_source_table_row_step)) * bcf_previous_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_previous_left. bcf_previous_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_source_table_row_step)) * bcf_previous_scale_bcp_source_table) + (bcf_left_bcp_source_table_row_step))) /\ ((((exists bcf_height_bcp_source_table_row_step_previous_right. bcf_height_bcp_source_table_row_step_previous_right + S (bcf_right_bcp_source_table_row_step) = S ((S (S (bcf_predecessor_bcp_source_table_row_step))) * bcf_previous_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_previous_right. bcf_previous_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_source_table_row_step))) * bcf_previous_scale_bcp_source_table) + (bcf_right_bcp_source_table_row_step))) /\ bcf_value_bcp_source_table_row_step = bcf_left_bcp_source_table_row_step + bcf_right_bcp_source_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_source_decoded_row_code. bcf_height_bcp_source_decoded_row_code + S (bcf_row_code_bcp_source) = S ((S (n)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_row_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_source) + (bcf_row_code_bcp_source))) /\ ((((exists bcf_height_bcp_source_decoded_row_scale. bcf_height_bcp_source_decoded_row_scale + S (bcf_row_scale_bcp_source) = S ((S (n)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_row_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_source) + (bcf_row_scale_bcp_source))) /\ (((exists bcf_height_bcp_source_decoded_value. bcf_height_bcp_source_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_value. bcf_row_code_bcp_source = bcf_quotient_bcp_source_decoded_value * S ((S (k)) * bcf_row_scale_bcp_source) + (z))))))))) -> exists p. z = S p

Structural proof guide

Every in-range relational Choose value is a successor.

Direct prerequisites: le_zero, le_of_succ_le_succ, add_succ_left, choose_exists, choose_zero, choose_succ_succ. The authored body proceeds by structural induction (3), case analysis (3), intermediate claims (5), equality transport (1).

Proof neighborhood

Direct dependencies

BT000Y le_zero BT0017 le_of_succ_le_succ BT0001 add_succ_left BT00T8 choose_exists BT00TE choose_zero BT00TJ choose_succ_succ

Direct dependents

BT00TP central_binom_positive BT00VJ primorial_odd_interval_le_middle

Formal native tactic body

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

  1. 0001induction n
  2. 0002induction k
  3. 0003intro z
  4. 0004intro hbound
  5. 0005intro hchoose
  6. 0006exists 0
  7. 0007specialize choose_zero 0
  8. 0008specialize choose_zero z
  9. 0009apply choose_zero
  10. 0010exact hchoose
  11. 0011intro z
  12. 0012intro hbound
  13. 0013intro hchoose
  14. 0014have hk0 : S k = 0
  15. 0015specialize le_zero (S k)
  16. 0016apply le_zero
  17. 0017exact hbound
  18. 0018exfalso
  19. 0019apply PA1
  20. 0020exact hk0
  21. 0021induction k
  22. 0022intro z
  23. 0023intro hbound
  24. 0024intro hchoose
  25. 0025exists 0
  26. 0026specialize choose_zero (S n)
  27. 0027specialize choose_zero z
  28. 0028apply choose_zero
  29. 0029exact hchoose
  30. 0030intro z
  31. 0031intro hbound
  32. 0032intro hchoose
  33. 0033have ha_exists : exists a. (((exists bcf_lt_gap_bcp_previous_left_out_of_range. bcf_lt_gap_bcp_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcp_previous_left_in_range. bcf_le_gap_bcp_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcp_previous_left bcf_row_code_scale_bcp_previous_left bcf_row_scale_code_bcp_previous_left bcf_row_scale_scale_bcp_previous_left bcf_row_code_bcp_previous_left bcf_row_scale_bcp_previous_left. ((forall bcf_row_index_bcp_previous_left_table. (exists bcf_lt_gap_bcp_previous_left_table_row_bound. bcf_lt_gap_bcp_previous_left_table_row_bound + S (bcf_row_index_bcp_previous_left_table) = S (n)) -> exists bcf_row_code_bcp_previous_left_table bcf_row_scale_bcp_previous_left_table. ((((exists bcf_height_bcp_previous_left_table_decoded_row_code. bcf_height_bcp_previous_left_table_decoded_row_code + S (bcf_row_code_bcp_previous_left_table) = S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_row_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left) + (bcf_row_code_bcp_previous_left_table))) /\ ((((exists bcf_height_bcp_previous_left_table_decoded_row_scale. bcf_height_bcp_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcp_previous_left_table) = S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_row_scale_bcp_previous_left_table))) /\ ((bcf_row_index_bcp_previous_left_table = 0 /\ (forall bcf_index_bcp_previous_left_table_zero_row. (exists bcf_lt_gap_bcp_previous_left_table_zero_row_bound. bcf_lt_gap_bcp_previous_left_table_zero_row_bound + S (bcf_index_bcp_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcp_previous_left_table_zero_row. ((((exists bcf_height_bcp_previous_left_table_zero_row_entry. bcf_height_bcp_previous_left_table_zero_row_entry + S (bcf_value_bcp_previous_left_table_zero_row) = S ((S (bcf_index_bcp_previous_left_table_zero_row)) * bcf_row_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_zero_row_entry. bcf_row_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_zero_row_entry * S ((S (bcf_index_bcp_previous_left_table_zero_row)) * bcf_row_scale_bcp_previous_left_table) + (bcf_value_bcp_previous_left_table_zero_row))) /\ ((bcf_index_bcp_previous_left_table_zero_row = 0 /\ bcf_value_bcp_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcp_previous_left_table_zero_row. bcf_index_bcp_previous_left_table_zero_row = S bcf_predecessor_bcp_previous_left_table_zero_row /\ bcf_value_bcp_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_previous_left_table bcf_previous_code_bcp_previous_left_table bcf_previous_scale_bcp_previous_left_table. bcf_row_index_bcp_previous_left_table = S bcf_predecessor_bcp_previous_left_table /\ ((((exists bcf_height_bcp_previous_left_table_decoded_previous_code. bcf_height_bcp_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcp_previous_left_table) = S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_previous_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left) + (bcf_previous_code_bcp_previous_left_table))) /\ ((((exists bcf_height_bcp_previous_left_table_decoded_previous_scale. bcf_height_bcp_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcp_previous_left_table) = S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_previous_scale_bcp_previous_left_table))) /\ (forall bcf_index_bcp_previous_left_table_row_step. (exists bcf_lt_gap_bcp_previous_left_table_row_step_bound. bcf_lt_gap_bcp_previous_left_table_row_step_bound + S (bcf_index_bcp_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcp_previous_left_table_row_step. ((((exists bcf_height_bcp_previous_left_table_row_step_entry. bcf_height_bcp_previous_left_table_row_step_entry + S (bcf_value_bcp_previous_left_table_row_step) = S ((S (bcf_index_bcp_previous_left_table_row_step)) * bcf_row_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_entry. bcf_row_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_entry * S ((S (bcf_index_bcp_previous_left_table_row_step)) * bcf_row_scale_bcp_previous_left_table) + (bcf_value_bcp_previous_left_table_row_step))) /\ ((bcf_index_bcp_previous_left_table_row_step = 0 /\ bcf_value_bcp_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcp_previous_left_table_row_step bcf_left_bcp_previous_left_table_row_step bcf_right_bcp_previous_left_table_row_step. bcf_index_bcp_previous_left_table_row_step = S bcf_predecessor_bcp_previous_left_table_row_step /\ ((((exists bcf_height_bcp_previous_left_table_row_step_previous_left. bcf_height_bcp_previous_left_table_row_step_previous_left + S (bcf_left_bcp_previous_left_table_row_step) = S ((S (bcf_predecessor_bcp_previous_left_table_row_step)) * bcf_previous_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_previous_left. bcf_previous_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_previous_left_table_row_step)) * bcf_previous_scale_bcp_previous_left_table) + (bcf_left_bcp_previous_left_table_row_step))) /\ ((((exists bcf_height_bcp_previous_left_table_row_step_previous_right. bcf_height_bcp_previous_left_table_row_step_previous_right + S (bcf_right_bcp_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcp_previous_left_table_row_step))) * bcf_previous_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_previous_right. bcf_previous_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_previous_left_table_row_step))) * bcf_previous_scale_bcp_previous_left_table) + (bcf_right_bcp_previous_left_table_row_step))) /\ bcf_value_bcp_previous_left_table_row_step = bcf_left_bcp_previous_left_table_row_step + bcf_right_bcp_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_previous_left_decoded_row_code. bcf_height_bcp_previous_left_decoded_row_code + S (bcf_row_code_bcp_previous_left) = S ((S (n)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_row_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_previous_left) + (bcf_row_code_bcp_previous_left))) /\ ((((exists bcf_height_bcp_previous_left_decoded_row_scale. bcf_height_bcp_previous_left_decoded_row_scale + S (bcf_row_scale_bcp_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_row_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_row_scale_bcp_previous_left))) /\ (((exists bcf_height_bcp_previous_left_decoded_value. bcf_height_bcp_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_value. bcf_row_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcp_previous_left) + (a)))))))))
  34. 0034specialize choose_exists n
  35. 0035specialize choose_exists k
  36. 0036exact choose_exists
  37. 0037cases ha_exists
  38. 0038have hb_exists : exists b. (((exists bcf_lt_gap_bcp_previous_right_out_of_range. bcf_lt_gap_bcp_previous_right_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcp_previous_right_in_range. bcf_le_gap_bcp_previous_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcp_previous_right bcf_row_code_scale_bcp_previous_right bcf_row_scale_code_bcp_previous_right bcf_row_scale_scale_bcp_previous_right bcf_row_code_bcp_previous_right bcf_row_scale_bcp_previous_right. ((forall bcf_row_index_bcp_previous_right_table. (exists bcf_lt_gap_bcp_previous_right_table_row_bound. bcf_lt_gap_bcp_previous_right_table_row_bound + S (bcf_row_index_bcp_previous_right_table) = S (n)) -> exists bcf_row_code_bcp_previous_right_table bcf_row_scale_bcp_previous_right_table. ((((exists bcf_height_bcp_previous_right_table_decoded_row_code. bcf_height_bcp_previous_right_table_decoded_row_code + S (bcf_row_code_bcp_previous_right_table) = S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_row_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right) + (bcf_row_code_bcp_previous_right_table))) /\ ((((exists bcf_height_bcp_previous_right_table_decoded_row_scale. bcf_height_bcp_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcp_previous_right_table) = S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_row_scale_bcp_previous_right_table))) /\ ((bcf_row_index_bcp_previous_right_table = 0 /\ (forall bcf_index_bcp_previous_right_table_zero_row. (exists bcf_lt_gap_bcp_previous_right_table_zero_row_bound. bcf_lt_gap_bcp_previous_right_table_zero_row_bound + S (bcf_index_bcp_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcp_previous_right_table_zero_row. ((((exists bcf_height_bcp_previous_right_table_zero_row_entry. bcf_height_bcp_previous_right_table_zero_row_entry + S (bcf_value_bcp_previous_right_table_zero_row) = S ((S (bcf_index_bcp_previous_right_table_zero_row)) * bcf_row_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_zero_row_entry. bcf_row_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_zero_row_entry * S ((S (bcf_index_bcp_previous_right_table_zero_row)) * bcf_row_scale_bcp_previous_right_table) + (bcf_value_bcp_previous_right_table_zero_row))) /\ ((bcf_index_bcp_previous_right_table_zero_row = 0 /\ bcf_value_bcp_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcp_previous_right_table_zero_row. bcf_index_bcp_previous_right_table_zero_row = S bcf_predecessor_bcp_previous_right_table_zero_row /\ bcf_value_bcp_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_previous_right_table bcf_previous_code_bcp_previous_right_table bcf_previous_scale_bcp_previous_right_table. bcf_row_index_bcp_previous_right_table = S bcf_predecessor_bcp_previous_right_table /\ ((((exists bcf_height_bcp_previous_right_table_decoded_previous_code. bcf_height_bcp_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcp_previous_right_table) = S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_previous_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right) + (bcf_previous_code_bcp_previous_right_table))) /\ ((((exists bcf_height_bcp_previous_right_table_decoded_previous_scale. bcf_height_bcp_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcp_previous_right_table) = S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_previous_scale_bcp_previous_right_table))) /\ (forall bcf_index_bcp_previous_right_table_row_step. (exists bcf_lt_gap_bcp_previous_right_table_row_step_bound. bcf_lt_gap_bcp_previous_right_table_row_step_bound + S (bcf_index_bcp_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcp_previous_right_table_row_step. ((((exists bcf_height_bcp_previous_right_table_row_step_entry. bcf_height_bcp_previous_right_table_row_step_entry + S (bcf_value_bcp_previous_right_table_row_step) = S ((S (bcf_index_bcp_previous_right_table_row_step)) * bcf_row_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_entry. bcf_row_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_entry * S ((S (bcf_index_bcp_previous_right_table_row_step)) * bcf_row_scale_bcp_previous_right_table) + (bcf_value_bcp_previous_right_table_row_step))) /\ ((bcf_index_bcp_previous_right_table_row_step = 0 /\ bcf_value_bcp_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcp_previous_right_table_row_step bcf_left_bcp_previous_right_table_row_step bcf_right_bcp_previous_right_table_row_step. bcf_index_bcp_previous_right_table_row_step = S bcf_predecessor_bcp_previous_right_table_row_step /\ ((((exists bcf_height_bcp_previous_right_table_row_step_previous_left. bcf_height_bcp_previous_right_table_row_step_previous_left + S (bcf_left_bcp_previous_right_table_row_step) = S ((S (bcf_predecessor_bcp_previous_right_table_row_step)) * bcf_previous_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_previous_left. bcf_previous_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_previous_right_table_row_step)) * bcf_previous_scale_bcp_previous_right_table) + (bcf_left_bcp_previous_right_table_row_step))) /\ ((((exists bcf_height_bcp_previous_right_table_row_step_previous_right. bcf_height_bcp_previous_right_table_row_step_previous_right + S (bcf_right_bcp_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcp_previous_right_table_row_step))) * bcf_previous_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_previous_right. bcf_previous_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_previous_right_table_row_step))) * bcf_previous_scale_bcp_previous_right_table) + (bcf_right_bcp_previous_right_table_row_step))) /\ bcf_value_bcp_previous_right_table_row_step = bcf_left_bcp_previous_right_table_row_step + bcf_right_bcp_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_previous_right_decoded_row_code. bcf_height_bcp_previous_right_decoded_row_code + S (bcf_row_code_bcp_previous_right) = S ((S (n)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_row_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_previous_right) + (bcf_row_code_bcp_previous_right))) /\ ((((exists bcf_height_bcp_previous_right_decoded_row_scale. bcf_height_bcp_previous_right_decoded_row_scale + S (bcf_row_scale_bcp_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_row_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_row_scale_bcp_previous_right))) /\ (((exists bcf_height_bcp_previous_right_decoded_value. bcf_height_bcp_previous_right_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_value. bcf_row_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcp_previous_right) + (b)))))))))
  39. 0039specialize choose_exists n
  40. 0040specialize choose_exists (S k)
  41. 0041exact choose_exists
  42. 0042cases hb_exists
  43. 0043have hpositive : exists p. x = S p
  44. 0044specialize IH k
  45. 0045specialize IH x
  46. 0046apply IH
  47. 0047specialize le_of_succ_le_succ k
  48. 0048specialize le_of_succ_le_succ n
  49. 0049apply le_of_succ_le_succ
  50. 0050exact hbound
  51. 0051exact ha_exists_witness
  52. 0052cases hpositive
  53. 0053have hsum : z = x + x1
  54. 0054specialize choose_succ_succ n
  55. 0055specialize choose_succ_succ k
  56. 0056specialize choose_succ_succ x
  57. 0057specialize choose_succ_succ x1
  58. 0058specialize choose_succ_succ z
  59. 0059apply choose_succ_succ
  60. 0060exact ha_exists_witness
  61. 0061exact hb_exists_witness
  62. 0062exact hchoose
  63. 0063exists x2 + x1
  64. 0064trans x + x1
  65. 0065exact hsum
  66. 0066rewrite hpositive_witness
  67. 0067specialize add_succ_left x2
  68. 0068specialize add_succ_left x1
  69. 0069exact add_succ_left