BT00T2

beta_pascal_zero_row_extend

Alpha body-checked · checked-use disabled

Append the next fixed zero-row value while preserving all earlier cells.

Exact expanded PA statement

forall b c w. (forall bcf_index_bpzre_before. (exists bcf_lt_gap_bpzre_before_bound. bcf_lt_gap_bpzre_before_bound + S (bcf_index_bpzre_before) = w) -> exists bcf_value_bpzre_before. ((((exists bcf_height_bpzre_before_entry. bcf_height_bpzre_before_entry + S (bcf_value_bpzre_before) = S ((S (bcf_index_bpzre_before)) * c)) /\ exists bcf_quotient_bpzre_before_entry. b = bcf_quotient_bpzre_before_entry * S ((S (bcf_index_bpzre_before)) * c) + (bcf_value_bpzre_before))) /\ ((bcf_index_bpzre_before = 0 /\ bcf_value_bpzre_before = 1) \/ exists bcf_predecessor_bpzre_before. bcf_index_bpzre_before = S bcf_predecessor_bpzre_before /\ bcf_value_bpzre_before = 0))) -> exists d e. (forall bcf_index_bpzre_after. (exists bcf_lt_gap_bpzre_after_bound. bcf_lt_gap_bpzre_after_bound + S (bcf_index_bpzre_after) = S (w)) -> exists bcf_value_bpzre_after. ((((exists bcf_height_bpzre_after_entry. bcf_height_bpzre_after_entry + S (bcf_value_bpzre_after) = S ((S (bcf_index_bpzre_after)) * e)) /\ exists bcf_quotient_bpzre_after_entry. d = bcf_quotient_bpzre_after_entry * S ((S (bcf_index_bpzre_after)) * e) + (bcf_value_bpzre_after))) /\ ((bcf_index_bpzre_after = 0 /\ bcf_value_bpzre_after = 1) \/ exists bcf_predecessor_bpzre_after. bcf_index_bpzre_after = S bcf_predecessor_bpzre_after /\ bcf_value_bpzre_after = 0)))

Structural proof guide

Append the next fixed zero-row value while preserving all earlier cells.

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

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00T3 beta_pascal_zero_row_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 b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro hrow
  5. 0005specialize zero_or_succ w
  6. 0006cases zero_or_succ
  7. 0007specialize beta_prefix_extend w
  8. 0008specialize beta_prefix_extend b
  9. 0009specialize beta_prefix_extend c
  10. 0010specialize beta_prefix_extend 1
  11. 0011cases beta_prefix_extend
  12. 0012cases beta_prefix_extend_witness
  13. 0013cases beta_prefix_extend_witness_witness
  14. 0014exists x
  15. 0015exists x1
  16. 0016intro i
  17. 0017intro hi
  18. 0018have hsplit : i = w \/ exists gap. gap + S i = w
  19. 0019specialize finite_lt_succ_eq_or_lt w
  20. 0020specialize finite_lt_succ_eq_or_lt i
  21. 0021apply finite_lt_succ_eq_or_lt
  22. 0022exact hi
  23. 0023cases hsplit
  24. 0024exists 1
  25. 0025split
  26. 0026rewrite hsplit_left
  27. 0027rewrite hsplit_left
  28. 0028exact beta_prefix_extend_witness_witness_left
  29. 0029left
  30. 0030split
  31. 0031trans w
  32. 0032exact hsplit_left
  33. 0033exact zero_or_succ_left
  34. 0034refl
  35. 0035specialize hrow i
  36. 0036have 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 predecessor. i = S predecessor /\ value = 0))
  37. 0037apply hrow
  38. 0038exact hsplit_right
  39. 0039cases hold
  40. 0040cases hold_witness
  41. 0041exists x2
  42. 0042split
  43. 0043specialize beta_prefix_extend_witness_witness_right i
  44. 0044specialize beta_prefix_extend_witness_witness_right x2
  45. 0045apply beta_prefix_extend_witness_witness_right
  46. 0046exact hsplit_right
  47. 0047exact hold_witness_left
  48. 0048exact hold_witness_right
  49. 0049cases zero_or_succ_right
  50. 0050specialize beta_prefix_extend w
  51. 0051specialize beta_prefix_extend b
  52. 0052specialize beta_prefix_extend c
  53. 0053specialize beta_prefix_extend 0
  54. 0054cases beta_prefix_extend
  55. 0055cases beta_prefix_extend_witness
  56. 0056cases beta_prefix_extend_witness_witness
  57. 0057exists x1
  58. 0058exists x2
  59. 0059intro i
  60. 0060intro hi
  61. 0061have hsplit : i = w \/ exists gap. gap + S i = w
  62. 0062specialize finite_lt_succ_eq_or_lt w
  63. 0063specialize finite_lt_succ_eq_or_lt i
  64. 0064apply finite_lt_succ_eq_or_lt
  65. 0065exact hi
  66. 0066cases hsplit
  67. 0067exists 0
  68. 0068split
  69. 0069rewrite hsplit_left
  70. 0070rewrite hsplit_left
  71. 0071exact beta_prefix_extend_witness_witness_left
  72. 0072right
  73. 0073exists x
  74. 0074split
  75. 0075trans w
  76. 0076exact hsplit_left
  77. 0077exact zero_or_succ_right_witness
  78. 0078refl
  79. 0079specialize hrow i
  80. 0080have 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 predecessor. i = S predecessor /\ value = 0))
  81. 0081apply hrow
  82. 0082exact hsplit_right
  83. 0083cases hold
  84. 0084cases hold_witness
  85. 0085exists x3
  86. 0086split
  87. 0087specialize beta_prefix_extend_witness_witness_right i
  88. 0088specialize beta_prefix_extend_witness_witness_right x3
  89. 0089apply beta_prefix_extend_witness_witness_right
  90. 0090exact hsplit_right
  91. 0091exact hold_witness_left
  92. 0092exact hold_witness_right