BT00T4

beta_pascal_row_step_extend

Alpha body-checked · checked-use disabled

Append one Pascal successor-row value and preserve the prefix.

Exact expanded PA statement

forall pb pc b c w. (forall bcf_index_bpsre_before. (exists bcf_lt_gap_bpsre_before_bound. bcf_lt_gap_bpsre_before_bound + S (bcf_index_bpsre_before) = w) -> exists bcf_value_bpsre_before. ((((exists bcf_height_bpsre_before_entry. bcf_height_bpsre_before_entry + S (bcf_value_bpsre_before) = S ((S (bcf_index_bpsre_before)) * c)) /\ exists bcf_quotient_bpsre_before_entry. b = bcf_quotient_bpsre_before_entry * S ((S (bcf_index_bpsre_before)) * c) + (bcf_value_bpsre_before))) /\ ((bcf_index_bpsre_before = 0 /\ bcf_value_bpsre_before = 1) \/ exists bcf_predecessor_bpsre_before bcf_left_bpsre_before bcf_right_bpsre_before. bcf_index_bpsre_before = S bcf_predecessor_bpsre_before /\ ((((exists bcf_height_bpsre_before_previous_left. bcf_height_bpsre_before_previous_left + S (bcf_left_bpsre_before) = S ((S (bcf_predecessor_bpsre_before)) * pc)) /\ exists bcf_quotient_bpsre_before_previous_left. pb = bcf_quotient_bpsre_before_previous_left * S ((S (bcf_predecessor_bpsre_before)) * pc) + (bcf_left_bpsre_before))) /\ ((((exists bcf_height_bpsre_before_previous_right. bcf_height_bpsre_before_previous_right + S (bcf_right_bpsre_before) = S ((S (S (bcf_predecessor_bpsre_before))) * pc)) /\ exists bcf_quotient_bpsre_before_previous_right. pb = bcf_quotient_bpsre_before_previous_right * S ((S (S (bcf_predecessor_bpsre_before))) * pc) + (bcf_right_bpsre_before))) /\ bcf_value_bpsre_before = bcf_left_bpsre_before + bcf_right_bpsre_before))))) -> exists d e. (forall bcf_index_bpsre_after. (exists bcf_lt_gap_bpsre_after_bound. bcf_lt_gap_bpsre_after_bound + S (bcf_index_bpsre_after) = S (w)) -> exists bcf_value_bpsre_after. ((((exists bcf_height_bpsre_after_entry. bcf_height_bpsre_after_entry + S (bcf_value_bpsre_after) = S ((S (bcf_index_bpsre_after)) * e)) /\ exists bcf_quotient_bpsre_after_entry. d = bcf_quotient_bpsre_after_entry * S ((S (bcf_index_bpsre_after)) * e) + (bcf_value_bpsre_after))) /\ ((bcf_index_bpsre_after = 0 /\ bcf_value_bpsre_after = 1) \/ exists bcf_predecessor_bpsre_after bcf_left_bpsre_after bcf_right_bpsre_after. bcf_index_bpsre_after = S bcf_predecessor_bpsre_after /\ ((((exists bcf_height_bpsre_after_previous_left. bcf_height_bpsre_after_previous_left + S (bcf_left_bpsre_after) = S ((S (bcf_predecessor_bpsre_after)) * pc)) /\ exists bcf_quotient_bpsre_after_previous_left. pb = bcf_quotient_bpsre_after_previous_left * S ((S (bcf_predecessor_bpsre_after)) * pc) + (bcf_left_bpsre_after))) /\ ((((exists bcf_height_bpsre_after_previous_right. bcf_height_bpsre_after_previous_right + S (bcf_right_bpsre_after) = S ((S (S (bcf_predecessor_bpsre_after))) * pc)) /\ exists bcf_quotient_bpsre_after_previous_right. pb = bcf_quotient_bpsre_after_previous_right * S ((S (S (bcf_predecessor_bpsre_after))) * pc) + (bcf_right_bpsre_after))) /\ bcf_value_bpsre_after = bcf_left_bpsre_after + bcf_right_bpsre_after)))))

Structural proof guide

Append one Pascal successor-row value and preserve the prefix.

Direct prerequisites: zero_or_succ, beta_at_exists, beta_prefix_extend, finite_lt_succ_eq_or_lt. The authored body proceeds by case analysis (16), intermediate claims (6), equality transport (4).

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT0041 beta_at_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00T5 beta_pascal_row_step_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 pb
  2. 0002intro pc
  3. 0003intro b
  4. 0004intro c
  5. 0005intro w
  6. 0006intro hrow
  7. 0007specialize zero_or_succ w
  8. 0008cases zero_or_succ
  9. 0009specialize beta_prefix_extend w
  10. 0010specialize beta_prefix_extend b
  11. 0011specialize beta_prefix_extend c
  12. 0012specialize beta_prefix_extend 1
  13. 0013cases beta_prefix_extend
  14. 0014cases beta_prefix_extend_witness
  15. 0015cases beta_prefix_extend_witness_witness
  16. 0016exists x
  17. 0017exists x1
  18. 0018intro i
  19. 0019intro hi
  20. 0020have hsplit : i = w \/ exists gap. gap + S i = w
  21. 0021specialize finite_lt_succ_eq_or_lt w
  22. 0022specialize finite_lt_succ_eq_or_lt i
  23. 0023apply finite_lt_succ_eq_or_lt
  24. 0024exact hi
  25. 0025cases hsplit
  26. 0026exists 1
  27. 0027split
  28. 0028rewrite hsplit_left
  29. 0029rewrite hsplit_left
  30. 0030exact beta_prefix_extend_witness_witness_left
  31. 0031left
  32. 0032split
  33. 0033trans w
  34. 0034exact hsplit_left
  35. 0035exact zero_or_succ_left
  36. 0036refl
  37. 0037specialize hrow i
  38. 0038have hold : exists value. (((exists height. height + S value = S ((S i) * c)) /\ exists quotient. b = quotient * S ((S i) * c) + value) /\ ((i = 0 /\ value = 1) \/ exists p u v. i = S p /\ (((exists h. h + S u = S ((S p) * pc)) /\ exists q. pb = q * S ((S p) * pc) + u) /\ (((exists h. h + S v = S ((S (S p)) * pc)) /\ exists q. pb = q * S ((S (S p)) * pc) + v) /\ value = u + v))))
  39. 0039apply hrow
  40. 0040exact hsplit_right
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043exists x2
  44. 0044split
  45. 0045specialize beta_prefix_extend_witness_witness_right i
  46. 0046specialize beta_prefix_extend_witness_witness_right x2
  47. 0047apply beta_prefix_extend_witness_witness_right
  48. 0048exact hsplit_right
  49. 0049exact hold_witness_left
  50. 0050exact hold_witness_right
  51. 0051cases zero_or_succ_right
  52. 0052have hleft : exists u. ((exists h. h + S u = S ((S x) * pc)) /\ exists q. pb = q * S ((S x) * pc) + u)
  53. 0053specialize beta_at_exists pb
  54. 0054specialize beta_at_exists pc
  55. 0055specialize beta_at_exists x
  56. 0056exact beta_at_exists
  57. 0057cases hleft
  58. 0058have hright : exists v. ((exists h. h + S v = S ((S (S x)) * pc)) /\ exists q. pb = q * S ((S (S x)) * pc) + v)
  59. 0059specialize beta_at_exists pb
  60. 0060specialize beta_at_exists pc
  61. 0061specialize beta_at_exists (S x)
  62. 0062exact beta_at_exists
  63. 0063cases hright
  64. 0064specialize beta_prefix_extend w
  65. 0065specialize beta_prefix_extend b
  66. 0066specialize beta_prefix_extend c
  67. 0067specialize beta_prefix_extend (x1 + x2)
  68. 0068cases beta_prefix_extend
  69. 0069cases beta_prefix_extend_witness
  70. 0070cases beta_prefix_extend_witness_witness
  71. 0071exists x3
  72. 0072exists x4
  73. 0073intro i
  74. 0074intro hi
  75. 0075have hsplit : i = w \/ exists gap. gap + S i = w
  76. 0076specialize finite_lt_succ_eq_or_lt w
  77. 0077specialize finite_lt_succ_eq_or_lt i
  78. 0078apply finite_lt_succ_eq_or_lt
  79. 0079exact hi
  80. 0080cases hsplit
  81. 0081exists x1 + x2
  82. 0082split
  83. 0083rewrite hsplit_left
  84. 0084rewrite hsplit_left
  85. 0085exact beta_prefix_extend_witness_witness_left
  86. 0086right
  87. 0087exists x
  88. 0088exists x1
  89. 0089exists x2
  90. 0090split
  91. 0091trans w
  92. 0092exact hsplit_left
  93. 0093exact zero_or_succ_right_witness
  94. 0094split
  95. 0095exact hleft_witness
  96. 0096split
  97. 0097exact hright_witness
  98. 0098refl
  99. 0099specialize hrow i
  100. 0100have hold : exists value. (((exists height. height + S value = S ((S i) * c)) /\ exists quotient. b = quotient * S ((S i) * c) + value) /\ ((i = 0 /\ value = 1) \/ exists p u v. i = S p /\ (((exists h. h + S u = S ((S p) * pc)) /\ exists q. pb = q * S ((S p) * pc) + u) /\ (((exists h. h + S v = S ((S (S p)) * pc)) /\ exists q. pb = q * S ((S (S p)) * pc) + v) /\ value = u + v))))
  101. 0101apply hrow
  102. 0102exact hsplit_right
  103. 0103cases hold
  104. 0104cases hold_witness
  105. 0105exists x5
  106. 0106split
  107. 0107specialize beta_prefix_extend_witness_witness_right i
  108. 0108specialize beta_prefix_extend_witness_witness_right x5
  109. 0109apply beta_prefix_extend_witness_witness_right
  110. 0110exact hsplit_right
  111. 0111exact hold_witness_left
  112. 0112exact hold_witness_right