BT00TT

choose_weighted_vertical

Alpha body-checked · checked-use disabled

Adjacent rows satisfy the constructive weighted vertical identity.

Exact expanded PA statement

forall n k j x y. k + j = n -> (((exists bcf_lt_gap_bcwv_lower_out_of_range. bcf_lt_gap_bcwv_lower_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bcwv_lower_in_range. bcf_le_gap_bcwv_lower_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_lower bcf_row_code_scale_bcwv_lower bcf_row_scale_code_bcwv_lower bcf_row_scale_scale_bcwv_lower bcf_row_code_bcwv_lower bcf_row_scale_bcwv_lower. ((forall bcf_row_index_bcwv_lower_table. (exists bcf_lt_gap_bcwv_lower_table_row_bound. bcf_lt_gap_bcwv_lower_table_row_bound + S (bcf_row_index_bcwv_lower_table) = S (n)) -> exists bcf_row_code_bcwv_lower_table bcf_row_scale_bcwv_lower_table. ((((exists bcf_height_bcwv_lower_table_decoded_row_code. bcf_height_bcwv_lower_table_decoded_row_code + S (bcf_row_code_bcwv_lower_table) = S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_row_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_row_code * S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower) + (bcf_row_code_bcwv_lower_table))) /\ ((((exists bcf_height_bcwv_lower_table_decoded_row_scale. bcf_height_bcwv_lower_table_decoded_row_scale + S (bcf_row_scale_bcwv_lower_table) = S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_row_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower) + (bcf_row_scale_bcwv_lower_table))) /\ ((bcf_row_index_bcwv_lower_table = 0 /\ (forall bcf_index_bcwv_lower_table_zero_row. (exists bcf_lt_gap_bcwv_lower_table_zero_row_bound. bcf_lt_gap_bcwv_lower_table_zero_row_bound + S (bcf_index_bcwv_lower_table_zero_row) = S (n)) -> exists bcf_value_bcwv_lower_table_zero_row. ((((exists bcf_height_bcwv_lower_table_zero_row_entry. bcf_height_bcwv_lower_table_zero_row_entry + S (bcf_value_bcwv_lower_table_zero_row) = S ((S (bcf_index_bcwv_lower_table_zero_row)) * bcf_row_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_zero_row_entry. bcf_row_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_zero_row_entry * S ((S (bcf_index_bcwv_lower_table_zero_row)) * bcf_row_scale_bcwv_lower_table) + (bcf_value_bcwv_lower_table_zero_row))) /\ ((bcf_index_bcwv_lower_table_zero_row = 0 /\ bcf_value_bcwv_lower_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_lower_table_zero_row. bcf_index_bcwv_lower_table_zero_row = S bcf_predecessor_bcwv_lower_table_zero_row /\ bcf_value_bcwv_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_lower_table bcf_previous_code_bcwv_lower_table bcf_previous_scale_bcwv_lower_table. bcf_row_index_bcwv_lower_table = S bcf_predecessor_bcwv_lower_table /\ ((((exists bcf_height_bcwv_lower_table_decoded_previous_code. bcf_height_bcwv_lower_table_decoded_previous_code + S (bcf_previous_code_bcwv_lower_table) = S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_previous_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower) + (bcf_previous_code_bcwv_lower_table))) /\ ((((exists bcf_height_bcwv_lower_table_decoded_previous_scale. bcf_height_bcwv_lower_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_lower_table) = S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_previous_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower) + (bcf_previous_scale_bcwv_lower_table))) /\ (forall bcf_index_bcwv_lower_table_row_step. (exists bcf_lt_gap_bcwv_lower_table_row_step_bound. bcf_lt_gap_bcwv_lower_table_row_step_bound + S (bcf_index_bcwv_lower_table_row_step) = S (n)) -> exists bcf_value_bcwv_lower_table_row_step. ((((exists bcf_height_bcwv_lower_table_row_step_entry. bcf_height_bcwv_lower_table_row_step_entry + S (bcf_value_bcwv_lower_table_row_step) = S ((S (bcf_index_bcwv_lower_table_row_step)) * bcf_row_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_entry. bcf_row_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_entry * S ((S (bcf_index_bcwv_lower_table_row_step)) * bcf_row_scale_bcwv_lower_table) + (bcf_value_bcwv_lower_table_row_step))) /\ ((bcf_index_bcwv_lower_table_row_step = 0 /\ bcf_value_bcwv_lower_table_row_step = 1) \/ exists bcf_predecessor_bcwv_lower_table_row_step bcf_left_bcwv_lower_table_row_step bcf_right_bcwv_lower_table_row_step. bcf_index_bcwv_lower_table_row_step = S bcf_predecessor_bcwv_lower_table_row_step /\ ((((exists bcf_height_bcwv_lower_table_row_step_previous_left. bcf_height_bcwv_lower_table_row_step_previous_left + S (bcf_left_bcwv_lower_table_row_step) = S ((S (bcf_predecessor_bcwv_lower_table_row_step)) * bcf_previous_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_previous_left. bcf_previous_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_lower_table_row_step)) * bcf_previous_scale_bcwv_lower_table) + (bcf_left_bcwv_lower_table_row_step))) /\ ((((exists bcf_height_bcwv_lower_table_row_step_previous_right. bcf_height_bcwv_lower_table_row_step_previous_right + S (bcf_right_bcwv_lower_table_row_step) = S ((S (S (bcf_predecessor_bcwv_lower_table_row_step))) * bcf_previous_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_previous_right. bcf_previous_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_lower_table_row_step))) * bcf_previous_scale_bcwv_lower_table) + (bcf_right_bcwv_lower_table_row_step))) /\ bcf_value_bcwv_lower_table_row_step = bcf_left_bcwv_lower_table_row_step + bcf_right_bcwv_lower_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_lower_decoded_row_code. bcf_height_bcwv_lower_decoded_row_code + S (bcf_row_code_bcwv_lower) = S ((S (n)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_row_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_lower) + (bcf_row_code_bcwv_lower))) /\ ((((exists bcf_height_bcwv_lower_decoded_row_scale. bcf_height_bcwv_lower_decoded_row_scale + S (bcf_row_scale_bcwv_lower) = S ((S (n)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_row_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_lower) + (bcf_row_scale_bcwv_lower))) /\ (((exists bcf_height_bcwv_lower_decoded_value. bcf_height_bcwv_lower_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_value. bcf_row_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_lower) + (x))))))))) -> (((exists bcf_lt_gap_bcwv_upper_out_of_range. bcf_lt_gap_bcwv_upper_out_of_range + S (S n) = k) /\ y = 0) \/ ((exists bcf_le_gap_bcwv_upper_in_range. bcf_le_gap_bcwv_upper_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_upper bcf_row_code_scale_bcwv_upper bcf_row_scale_code_bcwv_upper bcf_row_scale_scale_bcwv_upper bcf_row_code_bcwv_upper bcf_row_scale_bcwv_upper. ((forall bcf_row_index_bcwv_upper_table. (exists bcf_lt_gap_bcwv_upper_table_row_bound. bcf_lt_gap_bcwv_upper_table_row_bound + S (bcf_row_index_bcwv_upper_table) = S (S n)) -> exists bcf_row_code_bcwv_upper_table bcf_row_scale_bcwv_upper_table. ((((exists bcf_height_bcwv_upper_table_decoded_row_code. bcf_height_bcwv_upper_table_decoded_row_code + S (bcf_row_code_bcwv_upper_table) = S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_row_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_row_code * S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper) + (bcf_row_code_bcwv_upper_table))) /\ ((((exists bcf_height_bcwv_upper_table_decoded_row_scale. bcf_height_bcwv_upper_table_decoded_row_scale + S (bcf_row_scale_bcwv_upper_table) = S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_row_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper) + (bcf_row_scale_bcwv_upper_table))) /\ ((bcf_row_index_bcwv_upper_table = 0 /\ (forall bcf_index_bcwv_upper_table_zero_row. (exists bcf_lt_gap_bcwv_upper_table_zero_row_bound. bcf_lt_gap_bcwv_upper_table_zero_row_bound + S (bcf_index_bcwv_upper_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_upper_table_zero_row. ((((exists bcf_height_bcwv_upper_table_zero_row_entry. bcf_height_bcwv_upper_table_zero_row_entry + S (bcf_value_bcwv_upper_table_zero_row) = S ((S (bcf_index_bcwv_upper_table_zero_row)) * bcf_row_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_zero_row_entry. bcf_row_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_zero_row_entry * S ((S (bcf_index_bcwv_upper_table_zero_row)) * bcf_row_scale_bcwv_upper_table) + (bcf_value_bcwv_upper_table_zero_row))) /\ ((bcf_index_bcwv_upper_table_zero_row = 0 /\ bcf_value_bcwv_upper_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_upper_table_zero_row. bcf_index_bcwv_upper_table_zero_row = S bcf_predecessor_bcwv_upper_table_zero_row /\ bcf_value_bcwv_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_upper_table bcf_previous_code_bcwv_upper_table bcf_previous_scale_bcwv_upper_table. bcf_row_index_bcwv_upper_table = S bcf_predecessor_bcwv_upper_table /\ ((((exists bcf_height_bcwv_upper_table_decoded_previous_code. bcf_height_bcwv_upper_table_decoded_previous_code + S (bcf_previous_code_bcwv_upper_table) = S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_previous_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper) + (bcf_previous_code_bcwv_upper_table))) /\ ((((exists bcf_height_bcwv_upper_table_decoded_previous_scale. bcf_height_bcwv_upper_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_upper_table) = S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_previous_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper) + (bcf_previous_scale_bcwv_upper_table))) /\ (forall bcf_index_bcwv_upper_table_row_step. (exists bcf_lt_gap_bcwv_upper_table_row_step_bound. bcf_lt_gap_bcwv_upper_table_row_step_bound + S (bcf_index_bcwv_upper_table_row_step) = S (S n)) -> exists bcf_value_bcwv_upper_table_row_step. ((((exists bcf_height_bcwv_upper_table_row_step_entry. bcf_height_bcwv_upper_table_row_step_entry + S (bcf_value_bcwv_upper_table_row_step) = S ((S (bcf_index_bcwv_upper_table_row_step)) * bcf_row_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_entry. bcf_row_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_entry * S ((S (bcf_index_bcwv_upper_table_row_step)) * bcf_row_scale_bcwv_upper_table) + (bcf_value_bcwv_upper_table_row_step))) /\ ((bcf_index_bcwv_upper_table_row_step = 0 /\ bcf_value_bcwv_upper_table_row_step = 1) \/ exists bcf_predecessor_bcwv_upper_table_row_step bcf_left_bcwv_upper_table_row_step bcf_right_bcwv_upper_table_row_step. bcf_index_bcwv_upper_table_row_step = S bcf_predecessor_bcwv_upper_table_row_step /\ ((((exists bcf_height_bcwv_upper_table_row_step_previous_left. bcf_height_bcwv_upper_table_row_step_previous_left + S (bcf_left_bcwv_upper_table_row_step) = S ((S (bcf_predecessor_bcwv_upper_table_row_step)) * bcf_previous_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_previous_left. bcf_previous_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_upper_table_row_step)) * bcf_previous_scale_bcwv_upper_table) + (bcf_left_bcwv_upper_table_row_step))) /\ ((((exists bcf_height_bcwv_upper_table_row_step_previous_right. bcf_height_bcwv_upper_table_row_step_previous_right + S (bcf_right_bcwv_upper_table_row_step) = S ((S (S (bcf_predecessor_bcwv_upper_table_row_step))) * bcf_previous_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_previous_right. bcf_previous_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_upper_table_row_step))) * bcf_previous_scale_bcwv_upper_table) + (bcf_right_bcwv_upper_table_row_step))) /\ bcf_value_bcwv_upper_table_row_step = bcf_left_bcwv_upper_table_row_step + bcf_right_bcwv_upper_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_upper_decoded_row_code. bcf_height_bcwv_upper_decoded_row_code + S (bcf_row_code_bcwv_upper) = S ((S (S n)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_row_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_upper) + (bcf_row_code_bcwv_upper))) /\ ((((exists bcf_height_bcwv_upper_decoded_row_scale. bcf_height_bcwv_upper_decoded_row_scale + S (bcf_row_scale_bcwv_upper) = S ((S (S n)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_row_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_upper) + (bcf_row_scale_bcwv_upper))) /\ (((exists bcf_height_bcwv_upper_decoded_value. bcf_height_bcwv_upper_decoded_value + S (y) = S ((S (k)) * bcf_row_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_value. bcf_row_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_upper) + (y))))))))) -> S j * y = S n * x

Structural proof guide

Adjacent rows satisfy the constructive weighted vertical identity.

Direct prerequisites: zero_or_succ, zero_add, add_succ_left, add_assoc, mul_succ_left, mul_add, choose_exists, choose_zero, choose_self_of_eq, choose_succ_succ. The authored body proceeds by structural induction (3), case analysis (7), intermediate claims (25), equality transport (9).

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT0000 zero_add BT0001 add_succ_left BT0003 add_assoc BT0005 mul_succ_left BT0007 mul_add BT00T8 choose_exists BT00TE choose_zero BT00TK choose_self_of_eq BT00TJ choose_succ_succ

Direct dependents

BT00TU central_binom_succ_recurrence BT00TX choose_factorial_bridge BT00VL central_binom_recurrence_double_bundle

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 j
  4. 0004intro x
  5. 0005intro y
  6. 0006intro hsum
  7. 0007intro hlower
  8. 0008intro hupper
  9. 0009have hj : j = 0
  10. 0010trans 0 + j
  11. 0011symm
  12. 0012apply zero_add
  13. 0013exact hsum
  14. 0014have hx : x = 1
  15. 0015specialize choose_zero 0
  16. 0016specialize choose_zero x
  17. 0017apply choose_zero
  18. 0018exact hlower
  19. 0019have hy : y = 1
  20. 0020specialize choose_zero (S 0)
  21. 0021specialize choose_zero y
  22. 0022apply choose_zero
  23. 0023exact hupper
  24. 0024rewrite hj
  25. 0025trans S 0 * 1
  26. 0026congr
  27. 0027refl
  28. 0028exact hy
  29. 0029congr
  30. 0030refl
  31. 0031symm
  32. 0032exact hx
  33. 0033intro j
  34. 0034intro x
  35. 0035intro y
  36. 0036intro hsum
  37. 0037intro hlower
  38. 0038intro hupper
  39. 0039specialize add_succ_left k
  40. 0040specialize add_succ_left j
  41. 0041rewrite add_succ_left at hsum
  42. 0042exfalso
  43. 0043apply PA1
  44. 0044exact hsum
  45. 0045induction k
  46. 0046intro j
  47. 0047intro x
  48. 0048intro y
  49. 0049intro hsum
  50. 0050intro hlower
  51. 0051intro hupper
  52. 0052have hj : j = S n
  53. 0053trans 0 + j
  54. 0054symm
  55. 0055apply zero_add
  56. 0056exact hsum
  57. 0057have hx : x = 1
  58. 0058specialize choose_zero (S n)
  59. 0059specialize choose_zero x
  60. 0060apply choose_zero
  61. 0061exact hlower
  62. 0062have hy : y = 1
  63. 0063specialize choose_zero (S (S n))
  64. 0064specialize choose_zero y
  65. 0065apply choose_zero
  66. 0066exact hupper
  67. 0067rewrite hj
  68. 0068trans S (S n) * 1
  69. 0069congr
  70. 0070refl
  71. 0071exact hy
  72. 0072congr
  73. 0073refl
  74. 0074symm
  75. 0075exact hx
  76. 0076intro j
  77. 0077intro x
  78. 0078intro y
  79. 0079intro hsum
  80. 0080intro hlower
  81. 0081intro hupper
  82. 0082specialize zero_or_succ j
  83. 0083cases zero_or_succ
  84. 0084have ha_exists : exists a. (((exists bcf_lt_gap_bcwv_previous_left_out_of_range. bcf_lt_gap_bcwv_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcwv_previous_left_in_range. bcf_le_gap_bcwv_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_previous_left bcf_row_code_scale_bcwv_previous_left bcf_row_scale_code_bcwv_previous_left bcf_row_scale_scale_bcwv_previous_left bcf_row_code_bcwv_previous_left bcf_row_scale_bcwv_previous_left. ((forall bcf_row_index_bcwv_previous_left_table. (exists bcf_lt_gap_bcwv_previous_left_table_row_bound. bcf_lt_gap_bcwv_previous_left_table_row_bound + S (bcf_row_index_bcwv_previous_left_table) = S (n)) -> exists bcf_row_code_bcwv_previous_left_table bcf_row_scale_bcwv_previous_left_table. ((((exists bcf_height_bcwv_previous_left_table_decoded_row_code. bcf_height_bcwv_previous_left_table_decoded_row_code + S (bcf_row_code_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_row_scale. bcf_height_bcwv_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left_table))) /\ ((bcf_row_index_bcwv_previous_left_table = 0 /\ (forall bcf_index_bcwv_previous_left_table_zero_row. (exists bcf_lt_gap_bcwv_previous_left_table_zero_row_bound. bcf_lt_gap_bcwv_previous_left_table_zero_row_bound + S (bcf_index_bcwv_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_left_table_zero_row. ((((exists bcf_height_bcwv_previous_left_table_zero_row_entry. bcf_height_bcwv_previous_left_table_zero_row_entry + S (bcf_value_bcwv_previous_left_table_zero_row) = S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_zero_row_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_zero_row))) /\ ((bcf_index_bcwv_previous_left_table_zero_row = 0 /\ bcf_value_bcwv_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_zero_row. bcf_index_bcwv_previous_left_table_zero_row = S bcf_predecessor_bcwv_previous_left_table_zero_row /\ bcf_value_bcwv_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_left_table bcf_previous_code_bcwv_previous_left_table bcf_previous_scale_bcwv_previous_left_table. bcf_row_index_bcwv_previous_left_table = S bcf_predecessor_bcwv_previous_left_table /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_code. bcf_height_bcwv_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_previous_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_scale. bcf_height_bcwv_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_previous_scale_bcwv_previous_left_table))) /\ (forall bcf_index_bcwv_previous_left_table_row_step. (exists bcf_lt_gap_bcwv_previous_left_table_row_step_bound. bcf_lt_gap_bcwv_previous_left_table_row_step_bound + S (bcf_index_bcwv_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_left_table_row_step. ((((exists bcf_height_bcwv_previous_left_table_row_step_entry. bcf_height_bcwv_previous_left_table_row_step_entry + S (bcf_value_bcwv_previous_left_table_row_step) = S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_entry * S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_row_step))) /\ ((bcf_index_bcwv_previous_left_table_row_step = 0 /\ bcf_value_bcwv_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_row_step bcf_left_bcwv_previous_left_table_row_step bcf_right_bcwv_previous_left_table_row_step. bcf_index_bcwv_previous_left_table_row_step = S bcf_predecessor_bcwv_previous_left_table_row_step /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_left. bcf_height_bcwv_previous_left_table_row_step_previous_left + S (bcf_left_bcwv_previous_left_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_left. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_left_bcwv_previous_left_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_right. bcf_height_bcwv_previous_left_table_row_step_previous_right + S (bcf_right_bcwv_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_right. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_right_bcwv_previous_left_table_row_step))) /\ bcf_value_bcwv_previous_left_table_row_step = bcf_left_bcwv_previous_left_table_row_step + bcf_right_bcwv_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_code. bcf_height_bcwv_previous_left_decoded_row_code + S (bcf_row_code_bcwv_previous_left) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_scale. bcf_height_bcwv_previous_left_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left))) /\ (((exists bcf_height_bcwv_previous_left_decoded_value. bcf_height_bcwv_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_value. bcf_row_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_previous_left) + (a)))))))))
  85. 0085specialize choose_exists n
  86. 0086specialize choose_exists k
  87. 0087exact choose_exists
  88. 0088cases ha_exists
  89. 0089have hb_exists : exists b. (((exists bcf_lt_gap_bcwv_successor_left_out_of_range. bcf_lt_gap_bcwv_successor_left_out_of_range + S (S n) = k) /\ b = 0) \/ ((exists bcf_le_gap_bcwv_successor_left_in_range. bcf_le_gap_bcwv_successor_left_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_successor_left bcf_row_code_scale_bcwv_successor_left bcf_row_scale_code_bcwv_successor_left bcf_row_scale_scale_bcwv_successor_left bcf_row_code_bcwv_successor_left bcf_row_scale_bcwv_successor_left. ((forall bcf_row_index_bcwv_successor_left_table. (exists bcf_lt_gap_bcwv_successor_left_table_row_bound. bcf_lt_gap_bcwv_successor_left_table_row_bound + S (bcf_row_index_bcwv_successor_left_table) = S (S n)) -> exists bcf_row_code_bcwv_successor_left_table bcf_row_scale_bcwv_successor_left_table. ((((exists bcf_height_bcwv_successor_left_table_decoded_row_code. bcf_height_bcwv_successor_left_table_decoded_row_code + S (bcf_row_code_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_row_scale. bcf_height_bcwv_successor_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left_table))) /\ ((bcf_row_index_bcwv_successor_left_table = 0 /\ (forall bcf_index_bcwv_successor_left_table_zero_row. (exists bcf_lt_gap_bcwv_successor_left_table_zero_row_bound. bcf_lt_gap_bcwv_successor_left_table_zero_row_bound + S (bcf_index_bcwv_successor_left_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_zero_row. ((((exists bcf_height_bcwv_successor_left_table_zero_row_entry. bcf_height_bcwv_successor_left_table_zero_row_entry + S (bcf_value_bcwv_successor_left_table_zero_row) = S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_zero_row_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_zero_row_entry * S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_zero_row))) /\ ((bcf_index_bcwv_successor_left_table_zero_row = 0 /\ bcf_value_bcwv_successor_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_zero_row. bcf_index_bcwv_successor_left_table_zero_row = S bcf_predecessor_bcwv_successor_left_table_zero_row /\ bcf_value_bcwv_successor_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_successor_left_table bcf_previous_code_bcwv_successor_left_table bcf_previous_scale_bcwv_successor_left_table. bcf_row_index_bcwv_successor_left_table = S bcf_predecessor_bcwv_successor_left_table /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_code. bcf_height_bcwv_successor_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_previous_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_scale. bcf_height_bcwv_successor_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_previous_scale_bcwv_successor_left_table))) /\ (forall bcf_index_bcwv_successor_left_table_row_step. (exists bcf_lt_gap_bcwv_successor_left_table_row_step_bound. bcf_lt_gap_bcwv_successor_left_table_row_step_bound + S (bcf_index_bcwv_successor_left_table_row_step) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_row_step. ((((exists bcf_height_bcwv_successor_left_table_row_step_entry. bcf_height_bcwv_successor_left_table_row_step_entry + S (bcf_value_bcwv_successor_left_table_row_step) = S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_entry * S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_row_step))) /\ ((bcf_index_bcwv_successor_left_table_row_step = 0 /\ bcf_value_bcwv_successor_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_row_step bcf_left_bcwv_successor_left_table_row_step bcf_right_bcwv_successor_left_table_row_step. bcf_index_bcwv_successor_left_table_row_step = S bcf_predecessor_bcwv_successor_left_table_row_step /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_left. bcf_height_bcwv_successor_left_table_row_step_previous_left + S (bcf_left_bcwv_successor_left_table_row_step) = S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_left. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_left_bcwv_successor_left_table_row_step))) /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_right. bcf_height_bcwv_successor_left_table_row_step_previous_right + S (bcf_right_bcwv_successor_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_right. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_right_bcwv_successor_left_table_row_step))) /\ bcf_value_bcwv_successor_left_table_row_step = bcf_left_bcwv_successor_left_table_row_step + bcf_right_bcwv_successor_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_code. bcf_height_bcwv_successor_left_decoded_row_code + S (bcf_row_code_bcwv_successor_left) = S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_scale. bcf_height_bcwv_successor_left_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left) = S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left))) /\ (((exists bcf_height_bcwv_successor_left_decoded_value. bcf_height_bcwv_successor_left_decoded_value + S (b) = S ((S (k)) * bcf_row_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_value. bcf_row_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_successor_left) + (b)))))))))
  90. 0090specialize choose_exists (S n)
  91. 0091specialize choose_exists k
  92. 0092exact choose_exists
  93. 0093cases hb_exists
  94. 0094rewrite zero_or_succ_left at hsum
  95. 0095rewrite PA3 at hsum
  96. 0096have hk : k = n
  97. 0097apply PA2
  98. 0098exact hsum
  99. 0099have hprevious_sum : k + 0 = n
  100. 0100trans k
  101. 0101apply PA3
  102. 0102exact hk
  103. 0103have ha_one : x1 = 1
  104. 0104specialize choose_self_of_eq n
  105. 0105specialize choose_self_of_eq k
  106. 0106specialize choose_self_of_eq x1
  107. 0107apply choose_self_of_eq
  108. 0108exact hk
  109. 0109exact ha_exists_witness
  110. 0110have hx_one : x = 1
  111. 0111specialize choose_self_of_eq (S n)
  112. 0112specialize choose_self_of_eq (S k)
  113. 0113specialize choose_self_of_eq x
  114. 0114apply choose_self_of_eq
  115. 0115exact hsum
  116. 0116exact hlower
  117. 0117have hweighted : S 0 * x2 = S n * x1
  118. 0118specialize IH k
  119. 0119specialize IH 0
  120. 0120specialize IH x1
  121. 0121specialize IH x2
  122. 0122apply IH
  123. 0123exact hprevious_sum
  124. 0124exact ha_exists_witness
  125. 0125exact hb_exists_witness
  126. 0126have hy_sum : y = x2 + x
  127. 0127specialize choose_succ_succ (S n)
  128. 0128specialize choose_succ_succ k
  129. 0129specialize choose_succ_succ x2
  130. 0130specialize choose_succ_succ x
  131. 0131specialize choose_succ_succ y
  132. 0132apply choose_succ_succ
  133. 0133exact hb_exists_witness
  134. 0134exact hlower
  135. 0135exact hupper
  136. 0136have hsame_one : x1 = x
  137. 0137trans 1
  138. 0138exact ha_one
  139. 0139symm
  140. 0140exact hx_one
  141. 0141have hone_scale : S 0 * x = x
  142. 0142trans S 0 * 1
  143. 0143congr
  144. 0144refl
  145. 0145exact hx_one
  146. 0146trans 1
  147. 0147trans S 0 * 0 + S 0
  148. 0148apply PA6
  149. 0149rewrite PA5
  150. 0150apply zero_add
  151. 0151symm
  152. 0152exact hx_one
  153. 0153rewrite zero_or_succ_left
  154. 0154trans S 0 * (x2 + x)
  155. 0155congr
  156. 0156refl
  157. 0157exact hy_sum
  158. 0158trans S 0 * x2 + S 0 * x
  159. 0159apply mul_add
  160. 0160trans S n * x1 + S 0 * x
  161. 0161congr
  162. 0162exact hweighted
  163. 0163refl
  164. 0164trans S n * x + x
  165. 0165congr
  166. 0166congr
  167. 0167refl
  168. 0168exact hsame_one
  169. 0169exact hone_scale
  170. 0170specialize mul_succ_left (S n)
  171. 0171specialize mul_succ_left x
  172. 0172symm
  173. 0173exact mul_succ_left
  174. 0174cases zero_or_succ_right
  175. 0175have ha_exists : exists a. (((exists bcf_lt_gap_bcwv_previous_left_out_of_range. bcf_lt_gap_bcwv_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcwv_previous_left_in_range. bcf_le_gap_bcwv_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_previous_left bcf_row_code_scale_bcwv_previous_left bcf_row_scale_code_bcwv_previous_left bcf_row_scale_scale_bcwv_previous_left bcf_row_code_bcwv_previous_left bcf_row_scale_bcwv_previous_left. ((forall bcf_row_index_bcwv_previous_left_table. (exists bcf_lt_gap_bcwv_previous_left_table_row_bound. bcf_lt_gap_bcwv_previous_left_table_row_bound + S (bcf_row_index_bcwv_previous_left_table) = S (n)) -> exists bcf_row_code_bcwv_previous_left_table bcf_row_scale_bcwv_previous_left_table. ((((exists bcf_height_bcwv_previous_left_table_decoded_row_code. bcf_height_bcwv_previous_left_table_decoded_row_code + S (bcf_row_code_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_row_scale. bcf_height_bcwv_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left_table))) /\ ((bcf_row_index_bcwv_previous_left_table = 0 /\ (forall bcf_index_bcwv_previous_left_table_zero_row. (exists bcf_lt_gap_bcwv_previous_left_table_zero_row_bound. bcf_lt_gap_bcwv_previous_left_table_zero_row_bound + S (bcf_index_bcwv_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_left_table_zero_row. ((((exists bcf_height_bcwv_previous_left_table_zero_row_entry. bcf_height_bcwv_previous_left_table_zero_row_entry + S (bcf_value_bcwv_previous_left_table_zero_row) = S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_zero_row_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_zero_row))) /\ ((bcf_index_bcwv_previous_left_table_zero_row = 0 /\ bcf_value_bcwv_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_zero_row. bcf_index_bcwv_previous_left_table_zero_row = S bcf_predecessor_bcwv_previous_left_table_zero_row /\ bcf_value_bcwv_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_left_table bcf_previous_code_bcwv_previous_left_table bcf_previous_scale_bcwv_previous_left_table. bcf_row_index_bcwv_previous_left_table = S bcf_predecessor_bcwv_previous_left_table /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_code. bcf_height_bcwv_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_previous_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_scale. bcf_height_bcwv_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_previous_scale_bcwv_previous_left_table))) /\ (forall bcf_index_bcwv_previous_left_table_row_step. (exists bcf_lt_gap_bcwv_previous_left_table_row_step_bound. bcf_lt_gap_bcwv_previous_left_table_row_step_bound + S (bcf_index_bcwv_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_left_table_row_step. ((((exists bcf_height_bcwv_previous_left_table_row_step_entry. bcf_height_bcwv_previous_left_table_row_step_entry + S (bcf_value_bcwv_previous_left_table_row_step) = S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_entry * S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_row_step))) /\ ((bcf_index_bcwv_previous_left_table_row_step = 0 /\ bcf_value_bcwv_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_row_step bcf_left_bcwv_previous_left_table_row_step bcf_right_bcwv_previous_left_table_row_step. bcf_index_bcwv_previous_left_table_row_step = S bcf_predecessor_bcwv_previous_left_table_row_step /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_left. bcf_height_bcwv_previous_left_table_row_step_previous_left + S (bcf_left_bcwv_previous_left_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_left. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_left_bcwv_previous_left_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_right. bcf_height_bcwv_previous_left_table_row_step_previous_right + S (bcf_right_bcwv_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_right. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_right_bcwv_previous_left_table_row_step))) /\ bcf_value_bcwv_previous_left_table_row_step = bcf_left_bcwv_previous_left_table_row_step + bcf_right_bcwv_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_code. bcf_height_bcwv_previous_left_decoded_row_code + S (bcf_row_code_bcwv_previous_left) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_scale. bcf_height_bcwv_previous_left_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left))) /\ (((exists bcf_height_bcwv_previous_left_decoded_value. bcf_height_bcwv_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_value. bcf_row_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_previous_left) + (a)))))))))
  176. 0176specialize choose_exists n
  177. 0177specialize choose_exists k
  178. 0178exact choose_exists
  179. 0179cases ha_exists
  180. 0180have hb_exists : exists b. (((exists bcf_lt_gap_bcwv_previous_right_out_of_range. bcf_lt_gap_bcwv_previous_right_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcwv_previous_right_in_range. bcf_le_gap_bcwv_previous_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcwv_previous_right bcf_row_code_scale_bcwv_previous_right bcf_row_scale_code_bcwv_previous_right bcf_row_scale_scale_bcwv_previous_right bcf_row_code_bcwv_previous_right bcf_row_scale_bcwv_previous_right. ((forall bcf_row_index_bcwv_previous_right_table. (exists bcf_lt_gap_bcwv_previous_right_table_row_bound. bcf_lt_gap_bcwv_previous_right_table_row_bound + S (bcf_row_index_bcwv_previous_right_table) = S (n)) -> exists bcf_row_code_bcwv_previous_right_table bcf_row_scale_bcwv_previous_right_table. ((((exists bcf_height_bcwv_previous_right_table_decoded_row_code. bcf_height_bcwv_previous_right_table_decoded_row_code + S (bcf_row_code_bcwv_previous_right_table) = S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_row_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_row_code_bcwv_previous_right_table))) /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_row_scale. bcf_height_bcwv_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_right_table) = S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_row_scale_bcwv_previous_right_table))) /\ ((bcf_row_index_bcwv_previous_right_table = 0 /\ (forall bcf_index_bcwv_previous_right_table_zero_row. (exists bcf_lt_gap_bcwv_previous_right_table_zero_row_bound. bcf_lt_gap_bcwv_previous_right_table_zero_row_bound + S (bcf_index_bcwv_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_right_table_zero_row. ((((exists bcf_height_bcwv_previous_right_table_zero_row_entry. bcf_height_bcwv_previous_right_table_zero_row_entry + S (bcf_value_bcwv_previous_right_table_zero_row) = S ((S (bcf_index_bcwv_previous_right_table_zero_row)) * bcf_row_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_zero_row_entry. bcf_row_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_right_table_zero_row)) * bcf_row_scale_bcwv_previous_right_table) + (bcf_value_bcwv_previous_right_table_zero_row))) /\ ((bcf_index_bcwv_previous_right_table_zero_row = 0 /\ bcf_value_bcwv_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_right_table_zero_row. bcf_index_bcwv_previous_right_table_zero_row = S bcf_predecessor_bcwv_previous_right_table_zero_row /\ bcf_value_bcwv_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_right_table bcf_previous_code_bcwv_previous_right_table bcf_previous_scale_bcwv_previous_right_table. bcf_row_index_bcwv_previous_right_table = S bcf_predecessor_bcwv_previous_right_table /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_previous_code. bcf_height_bcwv_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_right_table) = S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_previous_code_bcwv_previous_right_table))) /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_previous_scale. bcf_height_bcwv_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_right_table) = S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_previous_scale_bcwv_previous_right_table))) /\ (forall bcf_index_bcwv_previous_right_table_row_step. (exists bcf_lt_gap_bcwv_previous_right_table_row_step_bound. bcf_lt_gap_bcwv_previous_right_table_row_step_bound + S (bcf_index_bcwv_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_right_table_row_step. ((((exists bcf_height_bcwv_previous_right_table_row_step_entry. bcf_height_bcwv_previous_right_table_row_step_entry + S (bcf_value_bcwv_previous_right_table_row_step) = S ((S (bcf_index_bcwv_previous_right_table_row_step)) * bcf_row_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_entry. bcf_row_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_entry * S ((S (bcf_index_bcwv_previous_right_table_row_step)) * bcf_row_scale_bcwv_previous_right_table) + (bcf_value_bcwv_previous_right_table_row_step))) /\ ((bcf_index_bcwv_previous_right_table_row_step = 0 /\ bcf_value_bcwv_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_right_table_row_step bcf_left_bcwv_previous_right_table_row_step bcf_right_bcwv_previous_right_table_row_step. bcf_index_bcwv_previous_right_table_row_step = S bcf_predecessor_bcwv_previous_right_table_row_step /\ ((((exists bcf_height_bcwv_previous_right_table_row_step_previous_left. bcf_height_bcwv_previous_right_table_row_step_previous_left + S (bcf_left_bcwv_previous_right_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_right_table_row_step)) * bcf_previous_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_previous_left. bcf_previous_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_right_table_row_step)) * bcf_previous_scale_bcwv_previous_right_table) + (bcf_left_bcwv_previous_right_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_right_table_row_step_previous_right. bcf_height_bcwv_previous_right_table_row_step_previous_right + S (bcf_right_bcwv_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_right_table_row_step))) * bcf_previous_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_previous_right. bcf_previous_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_right_table_row_step))) * bcf_previous_scale_bcwv_previous_right_table) + (bcf_right_bcwv_previous_right_table_row_step))) /\ bcf_value_bcwv_previous_right_table_row_step = bcf_left_bcwv_previous_right_table_row_step + bcf_right_bcwv_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_right_decoded_row_code. bcf_height_bcwv_previous_right_decoded_row_code + S (bcf_row_code_bcwv_previous_right) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_row_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_row_code_bcwv_previous_right))) /\ ((((exists bcf_height_bcwv_previous_right_decoded_row_scale. bcf_height_bcwv_previous_right_decoded_row_scale + S (bcf_row_scale_bcwv_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_row_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_row_scale_bcwv_previous_right))) /\ (((exists bcf_height_bcwv_previous_right_decoded_value. bcf_height_bcwv_previous_right_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_value. bcf_row_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcwv_previous_right) + (b)))))))))
  181. 0181specialize choose_exists n
  182. 0182specialize choose_exists (S k)
  183. 0183exact choose_exists
  184. 0184cases hb_exists
  185. 0185have hc_exists : exists c. (((exists bcf_lt_gap_bcwv_successor_left_out_of_range. bcf_lt_gap_bcwv_successor_left_out_of_range + S (S n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bcwv_successor_left_in_range. bcf_le_gap_bcwv_successor_left_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_successor_left bcf_row_code_scale_bcwv_successor_left bcf_row_scale_code_bcwv_successor_left bcf_row_scale_scale_bcwv_successor_left bcf_row_code_bcwv_successor_left bcf_row_scale_bcwv_successor_left. ((forall bcf_row_index_bcwv_successor_left_table. (exists bcf_lt_gap_bcwv_successor_left_table_row_bound. bcf_lt_gap_bcwv_successor_left_table_row_bound + S (bcf_row_index_bcwv_successor_left_table) = S (S n)) -> exists bcf_row_code_bcwv_successor_left_table bcf_row_scale_bcwv_successor_left_table. ((((exists bcf_height_bcwv_successor_left_table_decoded_row_code. bcf_height_bcwv_successor_left_table_decoded_row_code + S (bcf_row_code_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_row_scale. bcf_height_bcwv_successor_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left_table))) /\ ((bcf_row_index_bcwv_successor_left_table = 0 /\ (forall bcf_index_bcwv_successor_left_table_zero_row. (exists bcf_lt_gap_bcwv_successor_left_table_zero_row_bound. bcf_lt_gap_bcwv_successor_left_table_zero_row_bound + S (bcf_index_bcwv_successor_left_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_zero_row. ((((exists bcf_height_bcwv_successor_left_table_zero_row_entry. bcf_height_bcwv_successor_left_table_zero_row_entry + S (bcf_value_bcwv_successor_left_table_zero_row) = S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_zero_row_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_zero_row_entry * S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_zero_row))) /\ ((bcf_index_bcwv_successor_left_table_zero_row = 0 /\ bcf_value_bcwv_successor_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_zero_row. bcf_index_bcwv_successor_left_table_zero_row = S bcf_predecessor_bcwv_successor_left_table_zero_row /\ bcf_value_bcwv_successor_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_successor_left_table bcf_previous_code_bcwv_successor_left_table bcf_previous_scale_bcwv_successor_left_table. bcf_row_index_bcwv_successor_left_table = S bcf_predecessor_bcwv_successor_left_table /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_code. bcf_height_bcwv_successor_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_previous_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_scale. bcf_height_bcwv_successor_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_previous_scale_bcwv_successor_left_table))) /\ (forall bcf_index_bcwv_successor_left_table_row_step. (exists bcf_lt_gap_bcwv_successor_left_table_row_step_bound. bcf_lt_gap_bcwv_successor_left_table_row_step_bound + S (bcf_index_bcwv_successor_left_table_row_step) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_row_step. ((((exists bcf_height_bcwv_successor_left_table_row_step_entry. bcf_height_bcwv_successor_left_table_row_step_entry + S (bcf_value_bcwv_successor_left_table_row_step) = S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_entry * S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_row_step))) /\ ((bcf_index_bcwv_successor_left_table_row_step = 0 /\ bcf_value_bcwv_successor_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_row_step bcf_left_bcwv_successor_left_table_row_step bcf_right_bcwv_successor_left_table_row_step. bcf_index_bcwv_successor_left_table_row_step = S bcf_predecessor_bcwv_successor_left_table_row_step /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_left. bcf_height_bcwv_successor_left_table_row_step_previous_left + S (bcf_left_bcwv_successor_left_table_row_step) = S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_left. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_left_bcwv_successor_left_table_row_step))) /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_right. bcf_height_bcwv_successor_left_table_row_step_previous_right + S (bcf_right_bcwv_successor_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_right. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_right_bcwv_successor_left_table_row_step))) /\ bcf_value_bcwv_successor_left_table_row_step = bcf_left_bcwv_successor_left_table_row_step + bcf_right_bcwv_successor_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_code. bcf_height_bcwv_successor_left_decoded_row_code + S (bcf_row_code_bcwv_successor_left) = S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_scale. bcf_height_bcwv_successor_left_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left) = S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left))) /\ (((exists bcf_height_bcwv_successor_left_decoded_value. bcf_height_bcwv_successor_left_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_value. bcf_row_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_successor_left) + (c)))))))))
  186. 0186specialize choose_exists (S n)
  187. 0187specialize choose_exists k
  188. 0188exact choose_exists
  189. 0189cases hc_exists
  190. 0190rewrite zero_or_succ_right_witness at hsum
  191. 0191have hsecond_complement : S k + x1 = n
  192. 0192apply PA2
  193. 0193trans S k + S x1
  194. 0194symm
  195. 0195apply PA4
  196. 0196exact hsum
  197. 0197have hfirst_complement : k + S x1 = n
  198. 0198trans S (k + x1)
  199. 0199apply PA4
  200. 0200trans S k + x1
  201. 0201symm
  202. 0202apply add_succ_left
  203. 0203exact hsecond_complement
  204. 0204have hx_sum : x = x2 + x3
  205. 0205specialize choose_succ_succ n
  206. 0206specialize choose_succ_succ k
  207. 0207specialize choose_succ_succ x2
  208. 0208specialize choose_succ_succ x3
  209. 0209specialize choose_succ_succ x
  210. 0210apply choose_succ_succ
  211. 0211exact ha_exists_witness
  212. 0212exact hb_exists_witness
  213. 0213exact hlower
  214. 0214have hy_sum : y = x4 + x
  215. 0215specialize choose_succ_succ (S n)
  216. 0216specialize choose_succ_succ k
  217. 0217specialize choose_succ_succ x4
  218. 0218specialize choose_succ_succ x
  219. 0219specialize choose_succ_succ y
  220. 0220apply choose_succ_succ
  221. 0221exact hc_exists_witness
  222. 0222exact hlower
  223. 0223exact hupper
  224. 0224have hfirst_weight : S (S x1) * x4 = S n * x2
  225. 0225specialize IH k
  226. 0226specialize IH (S x1)
  227. 0227specialize IH x2
  228. 0228specialize IH x4
  229. 0229apply IH
  230. 0230exact hfirst_complement
  231. 0231exact ha_exists_witness
  232. 0232exact hc_exists_witness
  233. 0233have hsecond_weight : S x1 * x = S n * x3
  234. 0234specialize IH (S k)
  235. 0235specialize IH x1
  236. 0236specialize IH x3
  237. 0237specialize IH x
  238. 0238apply IH
  239. 0239exact hsecond_complement
  240. 0240exact hb_exists_witness
  241. 0241exact hlower
  242. 0242rewrite zero_or_succ_right_witness
  243. 0243trans S (S x1) * (x4 + x)
  244. 0244congr
  245. 0245refl
  246. 0246exact hy_sum
  247. 0247trans S (S x1) * x4 + S (S x1) * x
  248. 0248apply mul_add
  249. 0249trans S n * x2 + (S x1 * x + x)
  250. 0250congr
  251. 0251exact hfirst_weight
  252. 0252specialize mul_succ_left (S x1)
  253. 0253specialize mul_succ_left x
  254. 0254apply mul_succ_left
  255. 0255trans S n * x2 + (S n * x3 + x)
  256. 0256congr
  257. 0257refl
  258. 0258congr
  259. 0259exact hsecond_weight
  260. 0260refl
  261. 0261trans (S n * x2 + S n * x3) + x
  262. 0262specialize add_assoc (S n * x2)
  263. 0263specialize add_assoc (S n * x3)
  264. 0264specialize add_assoc x
  265. 0265symm
  266. 0266apply add_assoc
  267. 0267trans S n * (x2 + x3) + x
  268. 0268congr
  269. 0269specialize mul_add (S n)
  270. 0270specialize mul_add x2
  271. 0271specialize mul_add x3
  272. 0272symm
  273. 0273apply mul_add
  274. 0274refl
  275. 0275trans S n * x + x
  276. 0276congr
  277. 0277congr
  278. 0278refl
  279. 0279symm
  280. 0280exact hx_sum
  281. 0281refl
  282. 0282specialize mul_succ_left (S n)
  283. 0283specialize mul_succ_left x
  284. 0284symm
  285. 0285exact mul_succ_left