BT00T9

beta_pascal_zero_row_pointwise_functional

Alpha body-checked · checked-use disabled

Zero-row values agree pointwise across beta encodings and widths.

Exact expanded PA statement

forall b c d e w v i x y. (forall bcf_index_bzrpf_left. (exists bcf_lt_gap_bzrpf_left_bound. bcf_lt_gap_bzrpf_left_bound + S (bcf_index_bzrpf_left) = w) -> exists bcf_value_bzrpf_left. ((((exists bcf_height_bzrpf_left_entry. bcf_height_bzrpf_left_entry + S (bcf_value_bzrpf_left) = S ((S (bcf_index_bzrpf_left)) * c)) /\ exists bcf_quotient_bzrpf_left_entry. b = bcf_quotient_bzrpf_left_entry * S ((S (bcf_index_bzrpf_left)) * c) + (bcf_value_bzrpf_left))) /\ ((bcf_index_bzrpf_left = 0 /\ bcf_value_bzrpf_left = 1) \/ exists bcf_predecessor_bzrpf_left. bcf_index_bzrpf_left = S bcf_predecessor_bzrpf_left /\ bcf_value_bzrpf_left = 0))) -> (forall bcf_index_bzrpf_right. (exists bcf_lt_gap_bzrpf_right_bound. bcf_lt_gap_bzrpf_right_bound + S (bcf_index_bzrpf_right) = v) -> exists bcf_value_bzrpf_right. ((((exists bcf_height_bzrpf_right_entry. bcf_height_bzrpf_right_entry + S (bcf_value_bzrpf_right) = S ((S (bcf_index_bzrpf_right)) * e)) /\ exists bcf_quotient_bzrpf_right_entry. d = bcf_quotient_bzrpf_right_entry * S ((S (bcf_index_bzrpf_right)) * e) + (bcf_value_bzrpf_right))) /\ ((bcf_index_bzrpf_right = 0 /\ bcf_value_bzrpf_right = 1) \/ exists bcf_predecessor_bzrpf_right. bcf_index_bzrpf_right = S bcf_predecessor_bzrpf_right /\ bcf_value_bzrpf_right = 0))) -> (exists bcf_lt_gap_bzrpf_left_bound. bcf_lt_gap_bzrpf_left_bound + S (i) = w) -> (exists bcf_lt_gap_bzrpf_right_bound. bcf_lt_gap_bzrpf_right_bound + S (i) = v) -> (((exists bcf_height_bzrpf_left_at. bcf_height_bzrpf_left_at + S (x) = S ((S (i)) * c)) /\ exists bcf_quotient_bzrpf_left_at. b = bcf_quotient_bzrpf_left_at * S ((S (i)) * c) + (x))) -> (((exists bcf_height_bzrpf_right_at. bcf_height_bzrpf_right_at + S (y) = S ((S (i)) * e)) /\ exists bcf_quotient_bzrpf_right_at. d = bcf_quotient_bzrpf_right_at * S ((S (i)) * e) + (y))) -> x = y

Structural proof guide

Zero-row values agree pointwise across beta encodings and widths.

Direct prerequisites: beta_at_unique, succ_ne_zero. The authored body proceeds by case analysis (16), intermediate claims (6).

Proof neighborhood

Direct dependencies

BT0042 beta_at_unique BT000C succ_ne_zero

Direct dependents

BT00TB beta_pascal_table_row_pointwise_functional

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 d
  4. 0004intro e
  5. 0005intro w
  6. 0006intro v
  7. 0007intro i
  8. 0008intro x
  9. 0009intro y
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012intro hiw
  13. 0013intro hiv
  14. 0014intro hxi
  15. 0015intro hyi
  16. 0016have hleft_value : exists bcf_cell_value_bzrpf_left_cell. ((((exists bcf_height_bzrpf_left_cell_entry. bcf_height_bzrpf_left_cell_entry + S (bcf_cell_value_bzrpf_left_cell) = S ((S (i)) * c)) /\ exists bcf_quotient_bzrpf_left_cell_entry. b = bcf_quotient_bzrpf_left_cell_entry * S ((S (i)) * c) + (bcf_cell_value_bzrpf_left_cell))) /\ ((i = 0 /\ bcf_cell_value_bzrpf_left_cell = 1) \/ exists bcf_cell_predecessor_bzrpf_left_cell. i = S bcf_cell_predecessor_bzrpf_left_cell /\ bcf_cell_value_bzrpf_left_cell = 0))
  17. 0017specialize hleft i
  18. 0018apply hleft
  19. 0019exact hiw
  20. 0020cases hleft_value
  21. 0021cases hleft_value_witness
  22. 0022have hright_value : exists bcf_cell_value_bzrpf_right_cell. ((((exists bcf_height_bzrpf_right_cell_entry. bcf_height_bzrpf_right_cell_entry + S (bcf_cell_value_bzrpf_right_cell) = S ((S (i)) * e)) /\ exists bcf_quotient_bzrpf_right_cell_entry. d = bcf_quotient_bzrpf_right_cell_entry * S ((S (i)) * e) + (bcf_cell_value_bzrpf_right_cell))) /\ ((i = 0 /\ bcf_cell_value_bzrpf_right_cell = 1) \/ exists bcf_cell_predecessor_bzrpf_right_cell. i = S bcf_cell_predecessor_bzrpf_right_cell /\ bcf_cell_value_bzrpf_right_cell = 0))
  23. 0023specialize hright i
  24. 0024apply hright
  25. 0025exact hiv
  26. 0026cases hright_value
  27. 0027cases hright_value_witness
  28. 0028have hx_value : x = x1
  29. 0029specialize beta_at_unique b
  30. 0030specialize beta_at_unique c
  31. 0031specialize beta_at_unique i
  32. 0032specialize beta_at_unique x
  33. 0033specialize beta_at_unique x1
  34. 0034apply beta_at_unique
  35. 0035exact hxi
  36. 0036exact hleft_value_witness_left
  37. 0037have hy_value : y = x2
  38. 0038specialize beta_at_unique d
  39. 0039specialize beta_at_unique e
  40. 0040specialize beta_at_unique i
  41. 0041specialize beta_at_unique y
  42. 0042specialize beta_at_unique x2
  43. 0043apply beta_at_unique
  44. 0044exact hyi
  45. 0045exact hright_value_witness_left
  46. 0046cases hleft_value_witness_right
  47. 0047cases hleft_value_witness_right_left
  48. 0048cases hright_value_witness_right
  49. 0049cases hright_value_witness_right_left
  50. 0050trans x1
  51. 0051exact hx_value
  52. 0052trans 1
  53. 0053exact hleft_value_witness_right_left_right
  54. 0054trans x2
  55. 0055symm
  56. 0056exact hright_value_witness_right_left_right
  57. 0057symm
  58. 0058exact hy_value
  59. 0059cases hright_value_witness_right_right
  60. 0060cases hright_value_witness_right_right_witness
  61. 0061exfalso
  62. 0062have hbad : S x3 = 0
  63. 0063trans i
  64. 0064symm
  65. 0065exact hright_value_witness_right_right_witness_left
  66. 0066exact hleft_value_witness_right_left_left
  67. 0067specialize succ_ne_zero x3
  68. 0068apply succ_ne_zero
  69. 0069exact hbad
  70. 0070cases hleft_value_witness_right_right
  71. 0071cases hleft_value_witness_right_right_witness
  72. 0072cases hright_value_witness_right
  73. 0073cases hright_value_witness_right_left
  74. 0074exfalso
  75. 0075have hbad : S x3 = 0
  76. 0076trans i
  77. 0077symm
  78. 0078exact hleft_value_witness_right_right_witness_left
  79. 0079exact hright_value_witness_right_left_left
  80. 0080specialize succ_ne_zero x3
  81. 0081apply succ_ne_zero
  82. 0082exact hbad
  83. 0083cases hright_value_witness_right_right
  84. 0084cases hright_value_witness_right_right_witness
  85. 0085trans x1
  86. 0086exact hx_value
  87. 0087trans 0
  88. 0088exact hleft_value_witness_right_right_witness_right
  89. 0089trans x2
  90. 0090symm
  91. 0091exact hright_value_witness_right_right_witness_right
  92. 0092symm
  93. 0093exact hy_value