BT00T6

beta_pascal_table_prefix_extend

Alpha body-checked · checked-use disabled

Append one semantic Pascal row to both outer beta prefixes.

Exact expanded PA statement

forall bb bc sb sc w r. (forall bcf_row_index_bptpe_before. (exists bcf_lt_gap_bptpe_before_row_bound. bcf_lt_gap_bptpe_before_row_bound + S (bcf_row_index_bptpe_before) = r) -> exists bcf_row_code_bptpe_before bcf_row_scale_bptpe_before. ((((exists bcf_height_bptpe_before_decoded_row_code. bcf_height_bptpe_before_decoded_row_code + S (bcf_row_code_bptpe_before) = S ((S (bcf_row_index_bptpe_before)) * bc)) /\ exists bcf_quotient_bptpe_before_decoded_row_code. bb = bcf_quotient_bptpe_before_decoded_row_code * S ((S (bcf_row_index_bptpe_before)) * bc) + (bcf_row_code_bptpe_before))) /\ ((((exists bcf_height_bptpe_before_decoded_row_scale. bcf_height_bptpe_before_decoded_row_scale + S (bcf_row_scale_bptpe_before) = S ((S (bcf_row_index_bptpe_before)) * sc)) /\ exists bcf_quotient_bptpe_before_decoded_row_scale. sb = bcf_quotient_bptpe_before_decoded_row_scale * S ((S (bcf_row_index_bptpe_before)) * sc) + (bcf_row_scale_bptpe_before))) /\ ((bcf_row_index_bptpe_before = 0 /\ (forall bcf_index_bptpe_before_zero_row. (exists bcf_lt_gap_bptpe_before_zero_row_bound. bcf_lt_gap_bptpe_before_zero_row_bound + S (bcf_index_bptpe_before_zero_row) = w) -> exists bcf_value_bptpe_before_zero_row. ((((exists bcf_height_bptpe_before_zero_row_entry. bcf_height_bptpe_before_zero_row_entry + S (bcf_value_bptpe_before_zero_row) = S ((S (bcf_index_bptpe_before_zero_row)) * bcf_row_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_zero_row_entry. bcf_row_code_bptpe_before = bcf_quotient_bptpe_before_zero_row_entry * S ((S (bcf_index_bptpe_before_zero_row)) * bcf_row_scale_bptpe_before) + (bcf_value_bptpe_before_zero_row))) /\ ((bcf_index_bptpe_before_zero_row = 0 /\ bcf_value_bptpe_before_zero_row = 1) \/ exists bcf_predecessor_bptpe_before_zero_row. bcf_index_bptpe_before_zero_row = S bcf_predecessor_bptpe_before_zero_row /\ bcf_value_bptpe_before_zero_row = 0)))) \/ exists bcf_predecessor_bptpe_before bcf_previous_code_bptpe_before bcf_previous_scale_bptpe_before. bcf_row_index_bptpe_before = S bcf_predecessor_bptpe_before /\ ((((exists bcf_height_bptpe_before_decoded_previous_code. bcf_height_bptpe_before_decoded_previous_code + S (bcf_previous_code_bptpe_before) = S ((S (bcf_predecessor_bptpe_before)) * bc)) /\ exists bcf_quotient_bptpe_before_decoded_previous_code. bb = bcf_quotient_bptpe_before_decoded_previous_code * S ((S (bcf_predecessor_bptpe_before)) * bc) + (bcf_previous_code_bptpe_before))) /\ ((((exists bcf_height_bptpe_before_decoded_previous_scale. bcf_height_bptpe_before_decoded_previous_scale + S (bcf_previous_scale_bptpe_before) = S ((S (bcf_predecessor_bptpe_before)) * sc)) /\ exists bcf_quotient_bptpe_before_decoded_previous_scale. sb = bcf_quotient_bptpe_before_decoded_previous_scale * S ((S (bcf_predecessor_bptpe_before)) * sc) + (bcf_previous_scale_bptpe_before))) /\ (forall bcf_index_bptpe_before_row_step. (exists bcf_lt_gap_bptpe_before_row_step_bound. bcf_lt_gap_bptpe_before_row_step_bound + S (bcf_index_bptpe_before_row_step) = w) -> exists bcf_value_bptpe_before_row_step. ((((exists bcf_height_bptpe_before_row_step_entry. bcf_height_bptpe_before_row_step_entry + S (bcf_value_bptpe_before_row_step) = S ((S (bcf_index_bptpe_before_row_step)) * bcf_row_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_entry. bcf_row_code_bptpe_before = bcf_quotient_bptpe_before_row_step_entry * S ((S (bcf_index_bptpe_before_row_step)) * bcf_row_scale_bptpe_before) + (bcf_value_bptpe_before_row_step))) /\ ((bcf_index_bptpe_before_row_step = 0 /\ bcf_value_bptpe_before_row_step = 1) \/ exists bcf_predecessor_bptpe_before_row_step bcf_left_bptpe_before_row_step bcf_right_bptpe_before_row_step. bcf_index_bptpe_before_row_step = S bcf_predecessor_bptpe_before_row_step /\ ((((exists bcf_height_bptpe_before_row_step_previous_left. bcf_height_bptpe_before_row_step_previous_left + S (bcf_left_bptpe_before_row_step) = S ((S (bcf_predecessor_bptpe_before_row_step)) * bcf_previous_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_previous_left. bcf_previous_code_bptpe_before = bcf_quotient_bptpe_before_row_step_previous_left * S ((S (bcf_predecessor_bptpe_before_row_step)) * bcf_previous_scale_bptpe_before) + (bcf_left_bptpe_before_row_step))) /\ ((((exists bcf_height_bptpe_before_row_step_previous_right. bcf_height_bptpe_before_row_step_previous_right + S (bcf_right_bptpe_before_row_step) = S ((S (S (bcf_predecessor_bptpe_before_row_step))) * bcf_previous_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_previous_right. bcf_previous_code_bptpe_before = bcf_quotient_bptpe_before_row_step_previous_right * S ((S (S (bcf_predecessor_bptpe_before_row_step))) * bcf_previous_scale_bptpe_before) + (bcf_right_bptpe_before_row_step))) /\ bcf_value_bptpe_before_row_step = bcf_left_bptpe_before_row_step + bcf_right_bptpe_before_row_step))))))))))) -> exists db dc eb ec. (forall bcf_row_index_bptpe_after. (exists bcf_lt_gap_bptpe_after_row_bound. bcf_lt_gap_bptpe_after_row_bound + S (bcf_row_index_bptpe_after) = S (r)) -> exists bcf_row_code_bptpe_after bcf_row_scale_bptpe_after. ((((exists bcf_height_bptpe_after_decoded_row_code. bcf_height_bptpe_after_decoded_row_code + S (bcf_row_code_bptpe_after) = S ((S (bcf_row_index_bptpe_after)) * dc)) /\ exists bcf_quotient_bptpe_after_decoded_row_code. db = bcf_quotient_bptpe_after_decoded_row_code * S ((S (bcf_row_index_bptpe_after)) * dc) + (bcf_row_code_bptpe_after))) /\ ((((exists bcf_height_bptpe_after_decoded_row_scale. bcf_height_bptpe_after_decoded_row_scale + S (bcf_row_scale_bptpe_after) = S ((S (bcf_row_index_bptpe_after)) * ec)) /\ exists bcf_quotient_bptpe_after_decoded_row_scale. eb = bcf_quotient_bptpe_after_decoded_row_scale * S ((S (bcf_row_index_bptpe_after)) * ec) + (bcf_row_scale_bptpe_after))) /\ ((bcf_row_index_bptpe_after = 0 /\ (forall bcf_index_bptpe_after_zero_row. (exists bcf_lt_gap_bptpe_after_zero_row_bound. bcf_lt_gap_bptpe_after_zero_row_bound + S (bcf_index_bptpe_after_zero_row) = w) -> exists bcf_value_bptpe_after_zero_row. ((((exists bcf_height_bptpe_after_zero_row_entry. bcf_height_bptpe_after_zero_row_entry + S (bcf_value_bptpe_after_zero_row) = S ((S (bcf_index_bptpe_after_zero_row)) * bcf_row_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_zero_row_entry. bcf_row_code_bptpe_after = bcf_quotient_bptpe_after_zero_row_entry * S ((S (bcf_index_bptpe_after_zero_row)) * bcf_row_scale_bptpe_after) + (bcf_value_bptpe_after_zero_row))) /\ ((bcf_index_bptpe_after_zero_row = 0 /\ bcf_value_bptpe_after_zero_row = 1) \/ exists bcf_predecessor_bptpe_after_zero_row. bcf_index_bptpe_after_zero_row = S bcf_predecessor_bptpe_after_zero_row /\ bcf_value_bptpe_after_zero_row = 0)))) \/ exists bcf_predecessor_bptpe_after bcf_previous_code_bptpe_after bcf_previous_scale_bptpe_after. bcf_row_index_bptpe_after = S bcf_predecessor_bptpe_after /\ ((((exists bcf_height_bptpe_after_decoded_previous_code. bcf_height_bptpe_after_decoded_previous_code + S (bcf_previous_code_bptpe_after) = S ((S (bcf_predecessor_bptpe_after)) * dc)) /\ exists bcf_quotient_bptpe_after_decoded_previous_code. db = bcf_quotient_bptpe_after_decoded_previous_code * S ((S (bcf_predecessor_bptpe_after)) * dc) + (bcf_previous_code_bptpe_after))) /\ ((((exists bcf_height_bptpe_after_decoded_previous_scale. bcf_height_bptpe_after_decoded_previous_scale + S (bcf_previous_scale_bptpe_after) = S ((S (bcf_predecessor_bptpe_after)) * ec)) /\ exists bcf_quotient_bptpe_after_decoded_previous_scale. eb = bcf_quotient_bptpe_after_decoded_previous_scale * S ((S (bcf_predecessor_bptpe_after)) * ec) + (bcf_previous_scale_bptpe_after))) /\ (forall bcf_index_bptpe_after_row_step. (exists bcf_lt_gap_bptpe_after_row_step_bound. bcf_lt_gap_bptpe_after_row_step_bound + S (bcf_index_bptpe_after_row_step) = w) -> exists bcf_value_bptpe_after_row_step. ((((exists bcf_height_bptpe_after_row_step_entry. bcf_height_bptpe_after_row_step_entry + S (bcf_value_bptpe_after_row_step) = S ((S (bcf_index_bptpe_after_row_step)) * bcf_row_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_entry. bcf_row_code_bptpe_after = bcf_quotient_bptpe_after_row_step_entry * S ((S (bcf_index_bptpe_after_row_step)) * bcf_row_scale_bptpe_after) + (bcf_value_bptpe_after_row_step))) /\ ((bcf_index_bptpe_after_row_step = 0 /\ bcf_value_bptpe_after_row_step = 1) \/ exists bcf_predecessor_bptpe_after_row_step bcf_left_bptpe_after_row_step bcf_right_bptpe_after_row_step. bcf_index_bptpe_after_row_step = S bcf_predecessor_bptpe_after_row_step /\ ((((exists bcf_height_bptpe_after_row_step_previous_left. bcf_height_bptpe_after_row_step_previous_left + S (bcf_left_bptpe_after_row_step) = S ((S (bcf_predecessor_bptpe_after_row_step)) * bcf_previous_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_previous_left. bcf_previous_code_bptpe_after = bcf_quotient_bptpe_after_row_step_previous_left * S ((S (bcf_predecessor_bptpe_after_row_step)) * bcf_previous_scale_bptpe_after) + (bcf_left_bptpe_after_row_step))) /\ ((((exists bcf_height_bptpe_after_row_step_previous_right. bcf_height_bptpe_after_row_step_previous_right + S (bcf_right_bptpe_after_row_step) = S ((S (S (bcf_predecessor_bptpe_after_row_step))) * bcf_previous_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_previous_right. bcf_previous_code_bptpe_after = bcf_quotient_bptpe_after_row_step_previous_right * S ((S (S (bcf_predecessor_bptpe_after_row_step))) * bcf_previous_scale_bptpe_after) + (bcf_right_bptpe_after_row_step))) /\ bcf_value_bptpe_after_row_step = bcf_left_bptpe_after_row_step + bcf_right_bptpe_after_row_step)))))))))))

Structural proof guide

Append one semantic Pascal row to both outer beta prefixes.

Direct prerequisites: zero_or_succ, le_refl, lt_to_le, beta_prefix_extend, finite_lt_succ_eq_or_lt, beta_pascal_zero_row_exists, beta_pascal_row_step_exists. The authored body proceeds by case analysis (46), intermediate claims (17), equality transport (12).

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT000E le_refl BT0019 lt_to_le BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt BT00T3 beta_pascal_zero_row_exists BT00T5 beta_pascal_row_step_exists

Direct dependents

BT00T7 beta_pascal_table_prefix_exists

Formal native tactic body

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

  1. 0001intro bb
  2. 0002intro bc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro w
  6. 0006intro r
  7. 0007intro htable
  8. 0008specialize zero_or_succ r
  9. 0009cases zero_or_succ
  10. 0010have hzero : exists b c. (forall j. (exists gap. gap + S j = w) -> 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)))
  11. 0011specialize beta_pascal_zero_row_exists w
  12. 0012exact beta_pascal_zero_row_exists
  13. 0013cases hzero
  14. 0014cases hzero_witness
  15. 0015have hcode_extend : exists db dc. ((((exists bcf_height_bptpe_code_append. bcf_height_bptpe_code_append + S (x) = S ((S (r)) * dc)) /\ exists bcf_quotient_bptpe_code_append. db = bcf_quotient_bptpe_code_append * S ((S (r)) * dc) + (x))) /\ forall i a. (exists bcf_lt_gap_bptpe_code_old_bound. bcf_lt_gap_bptpe_code_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_code_old. bcf_height_bptpe_code_old + S (a) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptpe_code_old. bb = bcf_quotient_bptpe_code_old * S ((S (i)) * bc) + (a))) -> (((exists bcf_height_bptpe_code_new. bcf_height_bptpe_code_new + S (a) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptpe_code_new. db = bcf_quotient_bptpe_code_new * S ((S (i)) * dc) + (a))))
  16. 0016specialize beta_prefix_extend r
  17. 0017specialize beta_prefix_extend bb
  18. 0018specialize beta_prefix_extend bc
  19. 0019specialize beta_prefix_extend x
  20. 0020exact beta_prefix_extend
  21. 0021cases hcode_extend
  22. 0022cases hcode_extend_witness
  23. 0023cases hcode_extend_witness_witness
  24. 0024have hscale_extend : exists eb ec. ((((exists bcf_height_bptpe_scale_append. bcf_height_bptpe_scale_append + S (x1) = S ((S (r)) * ec)) /\ exists bcf_quotient_bptpe_scale_append. eb = bcf_quotient_bptpe_scale_append * S ((S (r)) * ec) + (x1))) /\ forall i a. (exists bcf_lt_gap_bptpe_scale_old_bound. bcf_lt_gap_bptpe_scale_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_scale_old. bcf_height_bptpe_scale_old + S (a) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptpe_scale_old. sb = bcf_quotient_bptpe_scale_old * S ((S (i)) * sc) + (a))) -> (((exists bcf_height_bptpe_scale_new. bcf_height_bptpe_scale_new + S (a) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptpe_scale_new. eb = bcf_quotient_bptpe_scale_new * S ((S (i)) * ec) + (a))))
  25. 0025specialize beta_prefix_extend r
  26. 0026specialize beta_prefix_extend sb
  27. 0027specialize beta_prefix_extend sc
  28. 0028specialize beta_prefix_extend x1
  29. 0029exact beta_prefix_extend
  30. 0030cases hscale_extend
  31. 0031cases hscale_extend_witness
  32. 0032cases hscale_extend_witness_witness
  33. 0033exists x2
  34. 0034exists x3
  35. 0035exists x4
  36. 0036exists x5
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hsplit : i = r \/ exists gap. gap + S i = r
  40. 0040specialize finite_lt_succ_eq_or_lt r
  41. 0041specialize finite_lt_succ_eq_or_lt i
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hsplit
  45. 0045exists x
  46. 0046exists x1
  47. 0047split
  48. 0048rewrite hsplit_left
  49. 0049rewrite hsplit_left
  50. 0050exact hcode_extend_witness_witness_left
  51. 0051split
  52. 0052rewrite hsplit_left
  53. 0053rewrite hsplit_left
  54. 0054exact hscale_extend_witness_witness_left
  55. 0055left
  56. 0056split
  57. 0057trans r
  58. 0058exact hsplit_left
  59. 0059exact zero_or_succ_left
  60. 0060exact hzero_witness_witness
  61. 0061specialize htable i
  62. 0062have hold : 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 = w) -> 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 = w) -> 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))))))))))
  63. 0063apply htable
  64. 0064exact hsplit_right
  65. 0065cases hold
  66. 0066cases hold_witness
  67. 0067cases hold_witness_witness
  68. 0068cases hold_witness_witness_right
  69. 0069exists x6
  70. 0070exists x7
  71. 0071split
  72. 0072specialize hcode_extend_witness_witness_right i
  73. 0073specialize hcode_extend_witness_witness_right x6
  74. 0074apply hcode_extend_witness_witness_right
  75. 0075exact hsplit_right
  76. 0076exact hold_witness_witness_left
  77. 0077split
  78. 0078specialize hscale_extend_witness_witness_right i
  79. 0079specialize hscale_extend_witness_witness_right x7
  80. 0080apply hscale_extend_witness_witness_right
  81. 0081exact hsplit_right
  82. 0082exact hold_witness_witness_right_left
  83. 0083cases hold_witness_witness_right_right
  84. 0084left
  85. 0085exact hold_witness_witness_right_right_left
  86. 0086cases hold_witness_witness_right_right_right
  87. 0087cases hold_witness_witness_right_right_right_witness
  88. 0088cases hold_witness_witness_right_right_right_witness_witness
  89. 0089cases hold_witness_witness_right_right_right_witness_witness_witness
  90. 0090cases hold_witness_witness_right_right_right_witness_witness_witness_right
  91. 0091cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  92. 0092right
  93. 0093exists x8
  94. 0094exists x9
  95. 0095exists x10
  96. 0096split
  97. 0097exact hold_witness_witness_right_right_right_witness_witness_witness_left
  98. 0098have hpred_bound : exists gap. gap + S x8 = r
  99. 0099have hi_le : exists gap. gap + i = r
  100. 0100specialize lt_to_le i
  101. 0101specialize lt_to_le r
  102. 0102apply lt_to_le
  103. 0103exact hsplit_right
  104. 0104rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  105. 0105exact hi_le
  106. 0106split
  107. 0107specialize hcode_extend_witness_witness_right x8
  108. 0108specialize hcode_extend_witness_witness_right x9
  109. 0109apply hcode_extend_witness_witness_right
  110. 0110exact hpred_bound
  111. 0111exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
  112. 0112split
  113. 0113specialize hscale_extend_witness_witness_right x8
  114. 0114specialize hscale_extend_witness_witness_right x10
  115. 0115apply hscale_extend_witness_witness_right
  116. 0116exact hpred_bound
  117. 0117exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  118. 0118exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right
  119. 0119cases zero_or_succ_right
  120. 0120have hbound : exists gap. gap + S x = r
  121. 0121rewrite zero_or_succ_right_witness
  122. 0122specialize le_refl (S x)
  123. 0123exact le_refl
  124. 0124have hprevious : exists pb pc. (((exists h. h + S pb = S ((S x) * bc)) /\ exists q. bb = q * S ((S x) * bc) + pb) /\ (((exists h. h + S pc = S ((S x) * sc)) /\ exists q. sb = q * S ((S x) * sc) + pc) /\ (((x = 0 /\ (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * pc)) /\ exists q. pb = q * S ((S j) * pc) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. x = 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 = w) -> exists value. (((exists h. h + S value = S ((S j) * pc)) /\ exists q. pb = q * S ((S j) * pc) + 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))))))))))
  125. 0125specialize htable x
  126. 0126apply htable
  127. 0127exact hbound
  128. 0128cases hprevious
  129. 0129cases hprevious_witness
  130. 0130cases hprevious_witness_witness
  131. 0131cases hprevious_witness_witness_right
  132. 0132have hstep : exists b c. (forall j. (exists gap. gap + S j = w) -> 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 predecessor u v. j = S predecessor /\ (((exists h. h + S u = S ((S predecessor) * x2)) /\ exists q. x1 = q * S ((S predecessor) * x2) + u) /\ (((exists h. h + S v = S ((S (S predecessor)) * x2)) /\ exists q. x1 = q * S ((S (S predecessor)) * x2) + v) /\ value = u + v)))))
  133. 0133specialize beta_pascal_row_step_exists x1
  134. 0134specialize beta_pascal_row_step_exists x2
  135. 0135specialize beta_pascal_row_step_exists w
  136. 0136exact beta_pascal_row_step_exists
  137. 0137cases hstep
  138. 0138cases hstep_witness
  139. 0139have hcode_extend : exists db dc. ((((exists bcf_height_bptpe_code_append. bcf_height_bptpe_code_append + S (x3) = S ((S (r)) * dc)) /\ exists bcf_quotient_bptpe_code_append. db = bcf_quotient_bptpe_code_append * S ((S (r)) * dc) + (x3))) /\ forall i a. (exists bcf_lt_gap_bptpe_code_old_bound. bcf_lt_gap_bptpe_code_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_code_old. bcf_height_bptpe_code_old + S (a) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptpe_code_old. bb = bcf_quotient_bptpe_code_old * S ((S (i)) * bc) + (a))) -> (((exists bcf_height_bptpe_code_new. bcf_height_bptpe_code_new + S (a) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptpe_code_new. db = bcf_quotient_bptpe_code_new * S ((S (i)) * dc) + (a))))
  140. 0140specialize beta_prefix_extend r
  141. 0141specialize beta_prefix_extend bb
  142. 0142specialize beta_prefix_extend bc
  143. 0143specialize beta_prefix_extend x3
  144. 0144exact beta_prefix_extend
  145. 0145cases hcode_extend
  146. 0146cases hcode_extend_witness
  147. 0147cases hcode_extend_witness_witness
  148. 0148have hscale_extend : exists eb ec. ((((exists bcf_height_bptpe_scale_append. bcf_height_bptpe_scale_append + S (x4) = S ((S (r)) * ec)) /\ exists bcf_quotient_bptpe_scale_append. eb = bcf_quotient_bptpe_scale_append * S ((S (r)) * ec) + (x4))) /\ forall i a. (exists bcf_lt_gap_bptpe_scale_old_bound. bcf_lt_gap_bptpe_scale_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_scale_old. bcf_height_bptpe_scale_old + S (a) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptpe_scale_old. sb = bcf_quotient_bptpe_scale_old * S ((S (i)) * sc) + (a))) -> (((exists bcf_height_bptpe_scale_new. bcf_height_bptpe_scale_new + S (a) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptpe_scale_new. eb = bcf_quotient_bptpe_scale_new * S ((S (i)) * ec) + (a))))
  149. 0149specialize beta_prefix_extend r
  150. 0150specialize beta_prefix_extend sb
  151. 0151specialize beta_prefix_extend sc
  152. 0152specialize beta_prefix_extend x4
  153. 0153exact beta_prefix_extend
  154. 0154cases hscale_extend
  155. 0155cases hscale_extend_witness
  156. 0156cases hscale_extend_witness_witness
  157. 0157exists x5
  158. 0158exists x6
  159. 0159exists x7
  160. 0160exists x8
  161. 0161intro i
  162. 0162intro hi
  163. 0163have hsplit : i = r \/ exists gap. gap + S i = r
  164. 0164specialize finite_lt_succ_eq_or_lt r
  165. 0165specialize finite_lt_succ_eq_or_lt i
  166. 0166apply finite_lt_succ_eq_or_lt
  167. 0167exact hi
  168. 0168cases hsplit
  169. 0169exists x3
  170. 0170exists x4
  171. 0171split
  172. 0172rewrite hsplit_left
  173. 0173rewrite hsplit_left
  174. 0174exact hcode_extend_witness_witness_left
  175. 0175split
  176. 0176rewrite hsplit_left
  177. 0177rewrite hsplit_left
  178. 0178exact hscale_extend_witness_witness_left
  179. 0179right
  180. 0180exists x
  181. 0181exists x1
  182. 0182exists x2
  183. 0183split
  184. 0184trans r
  185. 0185exact hsplit_left
  186. 0186exact zero_or_succ_right_witness
  187. 0187have hpred_bound : exists gap. gap + S x = r
  188. 0188rewrite zero_or_succ_right_witness
  189. 0189specialize le_refl (S x)
  190. 0190exact le_refl
  191. 0191split
  192. 0192specialize hcode_extend_witness_witness_right x
  193. 0193specialize hcode_extend_witness_witness_right x1
  194. 0194apply hcode_extend_witness_witness_right
  195. 0195exact hpred_bound
  196. 0196exact hprevious_witness_witness_left
  197. 0197split
  198. 0198specialize hscale_extend_witness_witness_right x
  199. 0199specialize hscale_extend_witness_witness_right x2
  200. 0200apply hscale_extend_witness_witness_right
  201. 0201exact hpred_bound
  202. 0202exact hprevious_witness_witness_right_left
  203. 0203exact hstep_witness_witness
  204. 0204specialize htable i
  205. 0205have hold : 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 = w) -> 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 = w) -> 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))))))))))
  206. 0206apply htable
  207. 0207exact hsplit_right
  208. 0208cases hold
  209. 0209cases hold_witness
  210. 0210cases hold_witness_witness
  211. 0211cases hold_witness_witness_right
  212. 0212exists x9
  213. 0213exists x10
  214. 0214split
  215. 0215specialize hcode_extend_witness_witness_right i
  216. 0216specialize hcode_extend_witness_witness_right x9
  217. 0217apply hcode_extend_witness_witness_right
  218. 0218exact hsplit_right
  219. 0219exact hold_witness_witness_left
  220. 0220split
  221. 0221specialize hscale_extend_witness_witness_right i
  222. 0222specialize hscale_extend_witness_witness_right x10
  223. 0223apply hscale_extend_witness_witness_right
  224. 0224exact hsplit_right
  225. 0225exact hold_witness_witness_right_left
  226. 0226cases hold_witness_witness_right_right
  227. 0227left
  228. 0228exact hold_witness_witness_right_right_left
  229. 0229cases hold_witness_witness_right_right_right
  230. 0230cases hold_witness_witness_right_right_right_witness
  231. 0231cases hold_witness_witness_right_right_right_witness_witness
  232. 0232cases hold_witness_witness_right_right_right_witness_witness_witness
  233. 0233cases hold_witness_witness_right_right_right_witness_witness_witness_right
  234. 0234cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  235. 0235right
  236. 0236exists x11
  237. 0237exists x12
  238. 0238exists x13
  239. 0239split
  240. 0240exact hold_witness_witness_right_right_right_witness_witness_witness_left
  241. 0241have hpred_bound : exists gap. gap + S x11 = r
  242. 0242have hi_le : exists gap. gap + i = r
  243. 0243specialize lt_to_le i
  244. 0244specialize lt_to_le r
  245. 0245apply lt_to_le
  246. 0246exact hsplit_right
  247. 0247rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  248. 0248exact hi_le
  249. 0249split
  250. 0250specialize hcode_extend_witness_witness_right x11
  251. 0251specialize hcode_extend_witness_witness_right x12
  252. 0252apply hcode_extend_witness_witness_right
  253. 0253exact hpred_bound
  254. 0254exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
  255. 0255split
  256. 0256specialize hscale_extend_witness_witness_right x11
  257. 0257specialize hscale_extend_witness_witness_right x13
  258. 0258apply hscale_extend_witness_witness_right
  259. 0259exact hpred_bound
  260. 0260exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  261. 0261exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right