beta_pascal_table_diagonal_boundary

Proof neighborhood

Direct dependencies

Direct dependents

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. 0008intro i
9. 0009induction i
10. 0010intro hir
11. 0011intro b
12. 0012intro c
13. 0013intro hbb
14. 0014intro hsb
15. 0015have hrow : exists bcf_row_code_bptdb_base_row bcf_row_scale_bptdb_base_row. ((((exists bcf_height_bptdb_base_row_decoded_row_code. bcf_height_bptdb_base_row_decoded_row_code + S (bcf_row_code_bptdb_base_row) = S ((S (0)) * bc)) /\ exists bcf_quotient_bptdb_base_row_decoded_row_code. bb = bcf_quotient_bptdb_base_row_decoded_row_code * S ((S (0)) * bc) + (bcf_row_code_bptdb_base_row))) /\ ((((exists bcf_height_bptdb_base_row_decoded_row_scale. bcf_height_bptdb_base_row_decoded_row_scale + S (bcf_row_scale_bptdb_base_row) = S ((S (0)) * sc)) /\ exists bcf_quotient_bptdb_base_row_decoded_row_scale. sb = bcf_quotient_bptdb_base_row_decoded_row_scale * S ((S (0)) * sc) + (bcf_row_scale_bptdb_base_row))) /\ ((0 = 0 /\ (forall bcf_index_bptdb_base_row_zero_row. (exists bcf_lt_gap_bptdb_base_row_zero_row_bound. bcf_lt_gap_bptdb_base_row_zero_row_bound + S (bcf_index_bptdb_base_row_zero_row) = w) -> exists bcf_value_bptdb_base_row_zero_row. ((((exists bcf_height_bptdb_base_row_zero_row_entry. bcf_height_bptdb_base_row_zero_row_entry + S (bcf_value_bptdb_base_row_zero_row) = S ((S (bcf_index_bptdb_base_row_zero_row)) * bcf_row_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_zero_row_entry. bcf_row_code_bptdb_base_row = bcf_quotient_bptdb_base_row_zero_row_entry * S ((S (bcf_index_bptdb_base_row_zero_row)) * bcf_row_scale_bptdb_base_row) + (bcf_value_bptdb_base_row_zero_row))) /\ ((bcf_index_bptdb_base_row_zero_row = 0 /\ bcf_value_bptdb_base_row_zero_row = 1) \/ exists bcf_predecessor_bptdb_base_row_zero_row. bcf_index_bptdb_base_row_zero_row = S bcf_predecessor_bptdb_base_row_zero_row /\ bcf_value_bptdb_base_row_zero_row = 0)))) \/ exists bcf_predecessor_bptdb_base_row bcf_previous_code_bptdb_base_row bcf_previous_scale_bptdb_base_row. 0 = S bcf_predecessor_bptdb_base_row /\ ((((exists bcf_height_bptdb_base_row_decoded_previous_code. bcf_height_bptdb_base_row_decoded_previous_code + S (bcf_previous_code_bptdb_base_row) = S ((S (bcf_predecessor_bptdb_base_row)) * bc)) /\ exists bcf_quotient_bptdb_base_row_decoded_previous_code. bb = bcf_quotient_bptdb_base_row_decoded_previous_code * S ((S (bcf_predecessor_bptdb_base_row)) * bc) + (bcf_previous_code_bptdb_base_row))) /\ ((((exists bcf_height_bptdb_base_row_decoded_previous_scale. bcf_height_bptdb_base_row_decoded_previous_scale + S (bcf_previous_scale_bptdb_base_row) = S ((S (bcf_predecessor_bptdb_base_row)) * sc)) /\ exists bcf_quotient_bptdb_base_row_decoded_previous_scale. sb = bcf_quotient_bptdb_base_row_decoded_previous_scale * S ((S (bcf_predecessor_bptdb_base_row)) * sc) + (bcf_previous_scale_bptdb_base_row))) /\ (forall bcf_index_bptdb_base_row_row_step. (exists bcf_lt_gap_bptdb_base_row_row_step_bound. bcf_lt_gap_bptdb_base_row_row_step_bound + S (bcf_index_bptdb_base_row_row_step) = w) -> exists bcf_value_bptdb_base_row_row_step. ((((exists bcf_height_bptdb_base_row_row_step_entry. bcf_height_bptdb_base_row_row_step_entry + S (bcf_value_bptdb_base_row_row_step) = S ((S (bcf_index_bptdb_base_row_row_step)) * bcf_row_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_entry. bcf_row_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_entry * S ((S (bcf_index_bptdb_base_row_row_step)) * bcf_row_scale_bptdb_base_row) + (bcf_value_bptdb_base_row_row_step))) /\ ((bcf_index_bptdb_base_row_row_step = 0 /\ bcf_value_bptdb_base_row_row_step = 1) \/ exists bcf_predecessor_bptdb_base_row_row_step bcf_left_bptdb_base_row_row_step bcf_right_bptdb_base_row_row_step. bcf_index_bptdb_base_row_row_step = S bcf_predecessor_bptdb_base_row_row_step /\ ((((exists bcf_height_bptdb_base_row_row_step_previous_left. bcf_height_bptdb_base_row_row_step_previous_left + S (bcf_left_bptdb_base_row_row_step) = S ((S (bcf_predecessor_bptdb_base_row_row_step)) * bcf_previous_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_previous_left. bcf_previous_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_previous_left * S ((S (bcf_predecessor_bptdb_base_row_row_step)) * bcf_previous_scale_bptdb_base_row) + (bcf_left_bptdb_base_row_row_step))) /\ ((((exists bcf_height_bptdb_base_row_row_step_previous_right. bcf_height_bptdb_base_row_row_step_previous_right + S (bcf_right_bptdb_base_row_row_step) = S ((S (S (bcf_predecessor_bptdb_base_row_row_step))) * bcf_previous_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_previous_right. bcf_previous_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptdb_base_row_row_step))) * bcf_previous_scale_bptdb_base_row) + (bcf_right_bptdb_base_row_row_step))) /\ bcf_value_bptdb_base_row_row_step = bcf_left_bptdb_base_row_row_step + bcf_right_bptdb_base_row_row_step))))))))))
16. 0016specialize htable 0
17. 0017apply htable
18. 0018exact hir
19. 0019cases hrow
20. 0020cases hrow_witness
21. 0021cases hrow_witness_witness
22. 0022cases hrow_witness_witness_right
23. 0023have hcode : b = x
24. 0024specialize beta_at_unique bb
25. 0025specialize beta_at_unique bc
26. 0026specialize beta_at_unique 0
27. 0027specialize beta_at_unique b
28. 0028specialize beta_at_unique x
29. 0029apply beta_at_unique
30. 0030exact hbb
31. 0031exact hrow_witness_witness_left
32. 0032have hscale : c = x1
33. 0033specialize beta_at_unique sb
34. 0034specialize beta_at_unique sc
35. 0035specialize beta_at_unique 0
36. 0036specialize beta_at_unique c
37. 0037specialize beta_at_unique x1
38. 0038apply beta_at_unique
39. 0039exact hsb
40. 0040exact hrow_witness_witness_right_left
41. 0041cases hrow_witness_witness_right_right
42. 0042cases hrow_witness_witness_right_right_left
43. 0043split
44. 0044intro hiw
45. 0045intro z
46. 0046intro htarget
47. 0047have hsemantic : ((exists bcf_height_bptdb_base_diagonal_semantic. bcf_height_bptdb_base_diagonal_semantic + S (z) = S ((S (0)) * x1)) /\ exists bcf_quotient_bptdb_base_diagonal_semantic. x = bcf_quotient_bptdb_base_diagonal_semantic * S ((S (0)) * x1) + (z))
48. 0048rewrite <- hcode
49. 0049rewrite <- hscale
50. 0050rewrite <- hscale
51. 0051exact htarget
52. 0052have hcell : exists bcf_cell_value_bptdb_base_diagonal_cell. ((((exists bcf_height_bptdb_base_diagonal_cell_entry. bcf_height_bptdb_base_diagonal_cell_entry + S (bcf_cell_value_bptdb_base_diagonal_cell) = S ((S (0)) * x1)) /\ exists bcf_quotient_bptdb_base_diagonal_cell_entry. x = bcf_quotient_bptdb_base_diagonal_cell_entry * S ((S (0)) * x1) + (bcf_cell_value_bptdb_base_diagonal_cell))) /\ ((0 = 0 /\ bcf_cell_value_bptdb_base_diagonal_cell = 1) \/ exists bcf_cell_predecessor_bptdb_base_diagonal_cell. 0 = S bcf_cell_predecessor_bptdb_base_diagonal_cell /\ bcf_cell_value_bptdb_base_diagonal_cell = 0))
53. 0053specialize hrow_witness_witness_right_right_left_right 0
54. 0054apply hrow_witness_witness_right_right_left_right
55. 0055exact hiw
56. 0056cases hcell
57. 0057cases hcell_witness
58. 0058have hvalue : z = x2
59. 0059specialize beta_at_unique x
60. 0060specialize beta_at_unique x1
61. 0061specialize beta_at_unique 0
62. 0062specialize beta_at_unique z
63. 0063specialize beta_at_unique x2
64. 0064apply beta_at_unique
65. 0065exact hsemantic
66. 0066exact hcell_witness_left
67. 0067cases hcell_witness_right
68. 0068cases hcell_witness_right_left
69. 0069trans x2
70. 0070exact hvalue
71. 0071exact hcell_witness_right_left_right
72. 0072cases hcell_witness_right_right
73. 0073cases hcell_witness_right_right_witness
74. 0074exfalso
75. 0075have hbad : S x3 = 0
76. 0076symm
77. 0077exact hcell_witness_right_right_witness_left
78. 0078specialize succ_ne_zero x3
79. 0079apply succ_ne_zero
80. 0080exact hbad
81. 0081intro j
82. 0082intro z
83. 0083intro hij
84. 0084intro hjw
85. 0085intro htarget
86. 0086have hsemantic : ((exists bcf_height_bptdb_base_above_semantic. bcf_height_bptdb_base_above_semantic + S (z) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_base_above_semantic. x = bcf_quotient_bptdb_base_above_semantic * S ((S (j)) * x1) + (z))
87. 0087rewrite <- hcode
88. 0088rewrite <- hscale
89. 0089rewrite <- hscale
90. 0090exact htarget
91. 0091have hcell : exists bcf_cell_value_bptdb_base_above_cell. ((((exists bcf_height_bptdb_base_above_cell_entry. bcf_height_bptdb_base_above_cell_entry + S (bcf_cell_value_bptdb_base_above_cell) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_base_above_cell_entry. x = bcf_quotient_bptdb_base_above_cell_entry * S ((S (j)) * x1) + (bcf_cell_value_bptdb_base_above_cell))) /\ ((j = 0 /\ bcf_cell_value_bptdb_base_above_cell = 1) \/ exists bcf_cell_predecessor_bptdb_base_above_cell. j = S bcf_cell_predecessor_bptdb_base_above_cell /\ bcf_cell_value_bptdb_base_above_cell = 0))
92. 0092specialize hrow_witness_witness_right_right_left_right j
93. 0093apply hrow_witness_witness_right_right_left_right
94. 0094exact hjw
95. 0095cases hcell
96. 0096cases hcell_witness
97. 0097have hvalue : z = x2
98. 0098specialize beta_at_unique x
99. 0099specialize beta_at_unique x1
100. 0100specialize beta_at_unique j
101. 0101specialize beta_at_unique z
102. 0102specialize beta_at_unique x2
103. 0103apply beta_at_unique
104. 0104exact hsemantic
105. 0105exact hcell_witness_left
106. 0106cases hcell_witness_right
107. 0107cases hcell_witness_right_left
108. 0108cases hij
109. 0109have hbad : S 0 = 0
110. 0110specialize add_eq_zero_right x3
111. 0111specialize add_eq_zero_right (S 0)
112. 0112apply add_eq_zero_right
113. 0113trans j
114. 0114exact hij_witness
115. 0115exact hcell_witness_right_left_left
116. 0116exfalso
117. 0117specialize succ_ne_zero 0
118. 0118apply succ_ne_zero
119. 0119exact hbad
120. 0120cases hcell_witness_right_right
121. 0121cases hcell_witness_right_right_witness
122. 0122trans x2
123. 0123exact hvalue
124. 0124exact hcell_witness_right_right_witness_right
125. 0125cases hrow_witness_witness_right_right_right
126. 0126cases hrow_witness_witness_right_right_right_witness
127. 0127cases hrow_witness_witness_right_right_right_witness_witness
128. 0128cases hrow_witness_witness_right_right_right_witness_witness_witness
129. 0129exfalso
130. 0130have hbad : S x2 = 0
131. 0131symm
132. 0132exact hrow_witness_witness_right_right_right_witness_witness_witness_left
133. 0133specialize succ_ne_zero x2
134. 0134apply succ_ne_zero
135. 0135exact hbad
136. 0136intro hir
137. 0137intro b
138. 0138intro c
139. 0139intro hbb
140. 0140intro hsb
141. 0141have hrow : exists bcf_row_code_bptdb_step_row bcf_row_scale_bptdb_step_row. ((((exists bcf_height_bptdb_step_row_decoded_row_code. bcf_height_bptdb_step_row_decoded_row_code + S (bcf_row_code_bptdb_step_row) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptdb_step_row_decoded_row_code. bb = bcf_quotient_bptdb_step_row_decoded_row_code * S ((S (S i)) * bc) + (bcf_row_code_bptdb_step_row))) /\ ((((exists bcf_height_bptdb_step_row_decoded_row_scale. bcf_height_bptdb_step_row_decoded_row_scale + S (bcf_row_scale_bptdb_step_row) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptdb_step_row_decoded_row_scale. sb = bcf_quotient_bptdb_step_row_decoded_row_scale * S ((S (S i)) * sc) + (bcf_row_scale_bptdb_step_row))) /\ ((S i = 0 /\ (forall bcf_index_bptdb_step_row_zero_row. (exists bcf_lt_gap_bptdb_step_row_zero_row_bound. bcf_lt_gap_bptdb_step_row_zero_row_bound + S (bcf_index_bptdb_step_row_zero_row) = w) -> exists bcf_value_bptdb_step_row_zero_row. ((((exists bcf_height_bptdb_step_row_zero_row_entry. bcf_height_bptdb_step_row_zero_row_entry + S (bcf_value_bptdb_step_row_zero_row) = S ((S (bcf_index_bptdb_step_row_zero_row)) * bcf_row_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_zero_row_entry. bcf_row_code_bptdb_step_row = bcf_quotient_bptdb_step_row_zero_row_entry * S ((S (bcf_index_bptdb_step_row_zero_row)) * bcf_row_scale_bptdb_step_row) + (bcf_value_bptdb_step_row_zero_row))) /\ ((bcf_index_bptdb_step_row_zero_row = 0 /\ bcf_value_bptdb_step_row_zero_row = 1) \/ exists bcf_predecessor_bptdb_step_row_zero_row. bcf_index_bptdb_step_row_zero_row = S bcf_predecessor_bptdb_step_row_zero_row /\ bcf_value_bptdb_step_row_zero_row = 0)))) \/ exists bcf_predecessor_bptdb_step_row bcf_previous_code_bptdb_step_row bcf_previous_scale_bptdb_step_row. S i = S bcf_predecessor_bptdb_step_row /\ ((((exists bcf_height_bptdb_step_row_decoded_previous_code. bcf_height_bptdb_step_row_decoded_previous_code + S (bcf_previous_code_bptdb_step_row) = S ((S (bcf_predecessor_bptdb_step_row)) * bc)) /\ exists bcf_quotient_bptdb_step_row_decoded_previous_code. bb = bcf_quotient_bptdb_step_row_decoded_previous_code * S ((S (bcf_predecessor_bptdb_step_row)) * bc) + (bcf_previous_code_bptdb_step_row))) /\ ((((exists bcf_height_bptdb_step_row_decoded_previous_scale. bcf_height_bptdb_step_row_decoded_previous_scale + S (bcf_previous_scale_bptdb_step_row) = S ((S (bcf_predecessor_bptdb_step_row)) * sc)) /\ exists bcf_quotient_bptdb_step_row_decoded_previous_scale. sb = bcf_quotient_bptdb_step_row_decoded_previous_scale * S ((S (bcf_predecessor_bptdb_step_row)) * sc) + (bcf_previous_scale_bptdb_step_row))) /\ (forall bcf_index_bptdb_step_row_row_step. (exists bcf_lt_gap_bptdb_step_row_row_step_bound. bcf_lt_gap_bptdb_step_row_row_step_bound + S (bcf_index_bptdb_step_row_row_step) = w) -> exists bcf_value_bptdb_step_row_row_step. ((((exists bcf_height_bptdb_step_row_row_step_entry. bcf_height_bptdb_step_row_row_step_entry + S (bcf_value_bptdb_step_row_row_step) = S ((S (bcf_index_bptdb_step_row_row_step)) * bcf_row_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_entry. bcf_row_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_entry * S ((S (bcf_index_bptdb_step_row_row_step)) * bcf_row_scale_bptdb_step_row) + (bcf_value_bptdb_step_row_row_step))) /\ ((bcf_index_bptdb_step_row_row_step = 0 /\ bcf_value_bptdb_step_row_row_step = 1) \/ exists bcf_predecessor_bptdb_step_row_row_step bcf_left_bptdb_step_row_row_step bcf_right_bptdb_step_row_row_step. bcf_index_bptdb_step_row_row_step = S bcf_predecessor_bptdb_step_row_row_step /\ ((((exists bcf_height_bptdb_step_row_row_step_previous_left. bcf_height_bptdb_step_row_row_step_previous_left + S (bcf_left_bptdb_step_row_row_step) = S ((S (bcf_predecessor_bptdb_step_row_row_step)) * bcf_previous_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_previous_left. bcf_previous_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_previous_left * S ((S (bcf_predecessor_bptdb_step_row_row_step)) * bcf_previous_scale_bptdb_step_row) + (bcf_left_bptdb_step_row_row_step))) /\ ((((exists bcf_height_bptdb_step_row_row_step_previous_right. bcf_height_bptdb_step_row_row_step_previous_right + S (bcf_right_bptdb_step_row_row_step) = S ((S (S (bcf_predecessor_bptdb_step_row_row_step))) * bcf_previous_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_previous_right. bcf_previous_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptdb_step_row_row_step))) * bcf_previous_scale_bptdb_step_row) + (bcf_right_bptdb_step_row_row_step))) /\ bcf_value_bptdb_step_row_row_step = bcf_left_bptdb_step_row_row_step + bcf_right_bptdb_step_row_row_step))))))))))
142. 0142specialize htable (S i)
143. 0143apply htable
144. 0144exact hir
145. 0145cases hrow
146. 0146cases hrow_witness
147. 0147cases hrow_witness_witness
148. 0148cases hrow_witness_witness_right
149. 0149have hcode : b = x
150. 0150specialize beta_at_unique bb
151. 0151specialize beta_at_unique bc
152. 0152specialize beta_at_unique (S i)
153. 0153specialize beta_at_unique b
154. 0154specialize beta_at_unique x
155. 0155apply beta_at_unique
156. 0156exact hbb
157. 0157exact hrow_witness_witness_left
158. 0158have hscale : c = x1
159. 0159specialize beta_at_unique sb
160. 0160specialize beta_at_unique sc
161. 0161specialize beta_at_unique (S i)
162. 0162specialize beta_at_unique c
163. 0163specialize beta_at_unique x1
164. 0164apply beta_at_unique
165. 0165exact hsb
166. 0166exact hrow_witness_witness_right_left
167. 0167cases hrow_witness_witness_right_right
168. 0168cases hrow_witness_witness_right_right_left
169. 0169exfalso
170. 0170specialize succ_ne_zero i
171. 0171apply succ_ne_zero
172. 0172exact hrow_witness_witness_right_right_left_left
173. 0173cases hrow_witness_witness_right_right_right
174. 0174cases hrow_witness_witness_right_right_right_witness
175. 0175cases hrow_witness_witness_right_right_right_witness_witness
176. 0176cases hrow_witness_witness_right_right_right_witness_witness_witness
177. 0177cases hrow_witness_witness_right_right_right_witness_witness_witness_right
178. 0178cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
179. 0179have hpredecessor : i = x2
180. 0180specialize succ_injective i
181. 0181specialize succ_injective x2
182. 0182apply succ_injective
183. 0183exact hrow_witness_witness_right_right_right_witness_witness_witness_left
184. 0184have hprevious_row_bound : exists bcf_lt_gap_bptdb_previous_row_bound. bcf_lt_gap_bptdb_previous_row_bound + S (i) = r
185. 0185specialize lt_to_le (S i)
186. 0186specialize lt_to_le r
187. 0187apply lt_to_le
188. 0188exact hir
189. 0189have hprevious_code : ((exists bcf_height_bptdb_previous_code_at. bcf_height_bptdb_previous_code_at + S (x3) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptdb_previous_code_at. bb = bcf_quotient_bptdb_previous_code_at * S ((S (i)) * bc) + (x3))
190. 0190rewrite hpredecessor
191. 0191rewrite hpredecessor
192. 0192exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
193. 0193have hprevious_scale : ((exists bcf_height_bptdb_previous_scale_at. bcf_height_bptdb_previous_scale_at + S (x4) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptdb_previous_scale_at. sb = bcf_quotient_bptdb_previous_scale_at * S ((S (i)) * sc) + (x4))
194. 0194rewrite hpredecessor
195. 0195rewrite hpredecessor
196. 0196exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
197. 0197have hprevious_family : forall bcf_row_code_bptdb_previous_family bcf_row_scale_bptdb_previous_family. (((exists bcf_height_bptdb_previous_family_code_at. bcf_height_bptdb_previous_family_code_at + S (bcf_row_code_bptdb_previous_family) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptdb_previous_family_code_at. bb = bcf_quotient_bptdb_previous_family_code_at * S ((S (i)) * bc) + (bcf_row_code_bptdb_previous_family))) -> (((exists bcf_height_bptdb_previous_family_scale_at. bcf_height_bptdb_previous_family_scale_at + S (bcf_row_scale_bptdb_previous_family) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptdb_previous_family_scale_at. sb = bcf_quotient_bptdb_previous_family_scale_at * S ((S (i)) * sc) + (bcf_row_scale_bptdb_previous_family))) -> ((((exists bcf_lt_gap_bptdb_previous_family_boundary_diagonal_bound. bcf_lt_gap_bptdb_previous_family_boundary_diagonal_bound + S (i) = w) -> forall bcf_diagonal_value_bptdb_previous_family_boundary. (((exists bcf_height_bptdb_previous_family_boundary_diagonal_at. bcf_height_bptdb_previous_family_boundary_diagonal_at + S (bcf_diagonal_value_bptdb_previous_family_boundary) = S ((S (i)) * bcf_row_scale_bptdb_previous_family)) /\ exists bcf_quotient_bptdb_previous_family_boundary_diagonal_at. bcf_row_code_bptdb_previous_family = bcf_quotient_bptdb_previous_family_boundary_diagonal_at * S ((S (i)) * bcf_row_scale_bptdb_previous_family) + (bcf_diagonal_value_bptdb_previous_family_boundary))) -> bcf_diagonal_value_bptdb_previous_family_boundary = 1) /\ forall bcf_above_index_bptdb_previous_family_boundary bcf_above_value_bptdb_previous_family_boundary. (exists bcf_lt_gap_bptdb_previous_family_boundary_above_order. bcf_lt_gap_bptdb_previous_family_boundary_above_order + S (i) = bcf_above_index_bptdb_previous_family_boundary) -> (exists bcf_lt_gap_bptdb_previous_family_boundary_above_bound. bcf_lt_gap_bptdb_previous_family_boundary_above_bound + S (bcf_above_index_bptdb_previous_family_boundary) = w) -> (((exists bcf_height_bptdb_previous_family_boundary_above_at. bcf_height_bptdb_previous_family_boundary_above_at + S (bcf_above_value_bptdb_previous_family_boundary) = S ((S (bcf_above_index_bptdb_previous_family_boundary)) * bcf_row_scale_bptdb_previous_family)) /\ exists bcf_quotient_bptdb_previous_family_boundary_above_at. bcf_row_code_bptdb_previous_family = bcf_quotient_bptdb_previous_family_boundary_above_at * S ((S (bcf_above_index_bptdb_previous_family_boundary)) * bcf_row_scale_bptdb_previous_family) + (bcf_above_value_bptdb_previous_family_boundary))) -> bcf_above_value_bptdb_previous_family_boundary = 0))
198. 0198apply IH
199. 0199exact hprevious_row_bound
200. 0200have hprevious_boundary : (((exists bcf_lt_gap_bptdb_previous_boundary_diagonal_bound. bcf_lt_gap_bptdb_previous_boundary_diagonal_bound + S (i) = w) -> forall bcf_diagonal_value_bptdb_previous_boundary. (((exists bcf_height_bptdb_previous_boundary_diagonal_at. bcf_height_bptdb_previous_boundary_diagonal_at + S (bcf_diagonal_value_bptdb_previous_boundary) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_previous_boundary_diagonal_at. x3 = bcf_quotient_bptdb_previous_boundary_diagonal_at * S ((S (i)) * x4) + (bcf_diagonal_value_bptdb_previous_boundary))) -> bcf_diagonal_value_bptdb_previous_boundary = 1) /\ forall bcf_above_index_bptdb_previous_boundary bcf_above_value_bptdb_previous_boundary. (exists bcf_lt_gap_bptdb_previous_boundary_above_order. bcf_lt_gap_bptdb_previous_boundary_above_order + S (i) = bcf_above_index_bptdb_previous_boundary) -> (exists bcf_lt_gap_bptdb_previous_boundary_above_bound. bcf_lt_gap_bptdb_previous_boundary_above_bound + S (bcf_above_index_bptdb_previous_boundary) = w) -> (((exists bcf_height_bptdb_previous_boundary_above_at. bcf_height_bptdb_previous_boundary_above_at + S (bcf_above_value_bptdb_previous_boundary) = S ((S (bcf_above_index_bptdb_previous_boundary)) * x4)) /\ exists bcf_quotient_bptdb_previous_boundary_above_at. x3 = bcf_quotient_bptdb_previous_boundary_above_at * S ((S (bcf_above_index_bptdb_previous_boundary)) * x4) + (bcf_above_value_bptdb_previous_boundary))) -> bcf_above_value_bptdb_previous_boundary = 0)
201. 0201specialize hprevious_family x3
202. 0202specialize hprevious_family x4
203. 0203apply hprevious_family
204. 0204exact hprevious_code
205. 0205exact hprevious_scale
206. 0206cases hprevious_boundary
207. 0207split
208. 0208intro hiw
209. 0209intro z
210. 0210intro htarget
211. 0211have hsemantic : ((exists bcf_height_bptdb_step_diagonal_semantic. bcf_height_bptdb_step_diagonal_semantic + S (z) = S ((S (S i)) * x1)) /\ exists bcf_quotient_bptdb_step_diagonal_semantic. x = bcf_quotient_bptdb_step_diagonal_semantic * S ((S (S i)) * x1) + (z))
212. 0212rewrite <- hcode
213. 0213rewrite <- hscale
214. 0214rewrite <- hscale
215. 0215exact htarget
216. 0216have hcell : exists bcf_cell_value_bptdb_step_diagonal_cell. ((((exists bcf_height_bptdb_step_diagonal_cell_entry. bcf_height_bptdb_step_diagonal_cell_entry + S (bcf_cell_value_bptdb_step_diagonal_cell) = S ((S (S i)) * x1)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_entry. x = bcf_quotient_bptdb_step_diagonal_cell_entry * S ((S (S i)) * x1) + (bcf_cell_value_bptdb_step_diagonal_cell))) /\ ((S i = 0 /\ bcf_cell_value_bptdb_step_diagonal_cell = 1) \/ exists bcf_cell_predecessor_bptdb_step_diagonal_cell bcf_cell_left_bptdb_step_diagonal_cell bcf_cell_right_bptdb_step_diagonal_cell. S i = S bcf_cell_predecessor_bptdb_step_diagonal_cell /\ ((((exists bcf_height_bptdb_step_diagonal_cell_previous_left. bcf_height_bptdb_step_diagonal_cell_previous_left + S (bcf_cell_left_bptdb_step_diagonal_cell) = S ((S (bcf_cell_predecessor_bptdb_step_diagonal_cell)) * x4)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_previous_left. x3 = bcf_quotient_bptdb_step_diagonal_cell_previous_left * S ((S (bcf_cell_predecessor_bptdb_step_diagonal_cell)) * x4) + (bcf_cell_left_bptdb_step_diagonal_cell))) /\ ((((exists bcf_height_bptdb_step_diagonal_cell_previous_right. bcf_height_bptdb_step_diagonal_cell_previous_right + S (bcf_cell_right_bptdb_step_diagonal_cell) = S ((S (S (bcf_cell_predecessor_bptdb_step_diagonal_cell))) * x4)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_previous_right. x3 = bcf_quotient_bptdb_step_diagonal_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptdb_step_diagonal_cell))) * x4) + (bcf_cell_right_bptdb_step_diagonal_cell))) /\ bcf_cell_value_bptdb_step_diagonal_cell = bcf_cell_left_bptdb_step_diagonal_cell + bcf_cell_right_bptdb_step_diagonal_cell))))
217. 0217specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S i)
218. 0218apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
219. 0219exact hiw
220. 0220cases hcell
221. 0221cases hcell_witness
222. 0222have hvalue : z = x5
223. 0223specialize beta_at_unique x
224. 0224specialize beta_at_unique x1
225. 0225specialize beta_at_unique (S i)
226. 0226specialize beta_at_unique z
227. 0227specialize beta_at_unique x5
228. 0228apply beta_at_unique
229. 0229exact hsemantic
230. 0230exact hcell_witness_left
231. 0231cases hcell_witness_right
232. 0232cases hcell_witness_right_left
233. 0233exfalso
234. 0234specialize succ_ne_zero i
235. 0235apply succ_ne_zero
236. 0236exact hcell_witness_right_left_left
237. 0237cases hcell_witness_right_right
238. 0238cases hcell_witness_right_right_witness
239. 0239cases hcell_witness_right_right_witness_witness
240. 0240cases hcell_witness_right_right_witness_witness_witness
241. 0241cases hcell_witness_right_right_witness_witness_witness_right
242. 0242cases hcell_witness_right_right_witness_witness_witness_right_right
243. 0243have hcell_predecessor : i = x6
244. 0244specialize succ_injective i
245. 0245specialize succ_injective x6
246. 0246apply succ_injective
247. 0247exact hcell_witness_right_right_witness_witness_witness_left
248. 0248have hleft_at : ((exists bcf_height_bptdb_step_previous_left. bcf_height_bptdb_step_previous_left + S (x7) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_step_previous_left. x3 = bcf_quotient_bptdb_step_previous_left * S ((S (i)) * x4) + (x7))
249. 0249rewrite hcell_predecessor
250. 0250rewrite hcell_predecessor
251. 0251exact hcell_witness_right_right_witness_witness_witness_right_left
252. 0252have hright_at : ((exists bcf_height_bptdb_step_previous_right. bcf_height_bptdb_step_previous_right + S (x8) = S ((S (S i)) * x4)) /\ exists bcf_quotient_bptdb_step_previous_right. x3 = bcf_quotient_bptdb_step_previous_right * S ((S (S i)) * x4) + (x8))
253. 0253rewrite hcell_predecessor
254. 0254rewrite hcell_predecessor
255. 0255exact hcell_witness_right_right_witness_witness_witness_right_right_left
256. 0256have hprevious_diagonal_bound : exists bcf_lt_gap_bptdb_previous_diagonal_bound. bcf_lt_gap_bptdb_previous_diagonal_bound + S (i) = w
257. 0257specialize lt_to_le (S i)
258. 0258specialize lt_to_le w
259. 0259apply lt_to_le
260. 0260exact hiw
261. 0261have hdiagonal_family : forall z. (((exists bcf_height_bptdb_previous_diagonal_family. bcf_height_bptdb_previous_diagonal_family + S (z) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_previous_diagonal_family. x3 = bcf_quotient_bptdb_previous_diagonal_family * S ((S (i)) * x4) + (z))) -> z = 1
262. 0262apply hprevious_boundary_left
263. 0263exact hprevious_diagonal_bound
264. 0264have hleft_one : x7 = 1
265. 0265specialize hdiagonal_family x7
266. 0266apply hdiagonal_family
267. 0267exact hleft_at
268. 0268have hstrict_successor : exists bcf_lt_gap_bptdb_strict_successor. bcf_lt_gap_bptdb_strict_successor + S (i) = S i
269. 0269specialize le_refl (S i)
270. 0270exact le_refl
271. 0271have hright_zero : x8 = 0
272. 0272specialize hprevious_boundary_right (S i)
273. 0273specialize hprevious_boundary_right x8
274. 0274apply hprevious_boundary_right
275. 0275exact hstrict_successor
276. 0276exact hiw
277. 0277exact hright_at
278. 0278trans x5
279. 0279exact hvalue
280. 0280rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
281. 0281simp [hleft_one, hright_zero]
282. 0282intro j
283. 0283intro z
284. 0284intro hij
285. 0285intro hjw
286. 0286intro htarget
287. 0287have hsemantic : ((exists bcf_height_bptdb_step_above_semantic. bcf_height_bptdb_step_above_semantic + S (z) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_step_above_semantic. x = bcf_quotient_bptdb_step_above_semantic * S ((S (j)) * x1) + (z))
288. 0288rewrite <- hcode
289. 0289rewrite <- hscale
290. 0290rewrite <- hscale
291. 0291exact htarget
292. 0292have hcell : exists bcf_cell_value_bptdb_step_above_cell. ((((exists bcf_height_bptdb_step_above_cell_entry. bcf_height_bptdb_step_above_cell_entry + S (bcf_cell_value_bptdb_step_above_cell) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_step_above_cell_entry. x = bcf_quotient_bptdb_step_above_cell_entry * S ((S (j)) * x1) + (bcf_cell_value_bptdb_step_above_cell))) /\ ((j = 0 /\ bcf_cell_value_bptdb_step_above_cell = 1) \/ exists bcf_cell_predecessor_bptdb_step_above_cell bcf_cell_left_bptdb_step_above_cell bcf_cell_right_bptdb_step_above_cell. j = S bcf_cell_predecessor_bptdb_step_above_cell /\ ((((exists bcf_height_bptdb_step_above_cell_previous_left. bcf_height_bptdb_step_above_cell_previous_left + S (bcf_cell_left_bptdb_step_above_cell) = S ((S (bcf_cell_predecessor_bptdb_step_above_cell)) * x4)) /\ exists bcf_quotient_bptdb_step_above_cell_previous_left. x3 = bcf_quotient_bptdb_step_above_cell_previous_left * S ((S (bcf_cell_predecessor_bptdb_step_above_cell)) * x4) + (bcf_cell_left_bptdb_step_above_cell))) /\ ((((exists bcf_height_bptdb_step_above_cell_previous_right. bcf_height_bptdb_step_above_cell_previous_right + S (bcf_cell_right_bptdb_step_above_cell) = S ((S (S (bcf_cell_predecessor_bptdb_step_above_cell))) * x4)) /\ exists bcf_quotient_bptdb_step_above_cell_previous_right. x3 = bcf_quotient_bptdb_step_above_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptdb_step_above_cell))) * x4) + (bcf_cell_right_bptdb_step_above_cell))) /\ bcf_cell_value_bptdb_step_above_cell = bcf_cell_left_bptdb_step_above_cell + bcf_cell_right_bptdb_step_above_cell))))
293. 0293specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right j
294. 0294apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
295. 0295exact hjw
296. 0296cases hcell
297. 0297cases hcell_witness
298. 0298have hvalue : z = x5
299. 0299specialize beta_at_unique x
300. 0300specialize beta_at_unique x1
301. 0301specialize beta_at_unique j
302. 0302specialize beta_at_unique z
303. 0303specialize beta_at_unique x5
304. 0304apply beta_at_unique
305. 0305exact hsemantic
306. 0306exact hcell_witness_left
307. 0307cases hcell_witness_right
308. 0308cases hcell_witness_right_left
309. 0309cases hij
310. 0310have hbad : S (S i) = 0
311. 0311specialize add_eq_zero_right x6
312. 0312specialize add_eq_zero_right (S (S i))
313. 0313apply add_eq_zero_right
314. 0314trans j
315. 0315exact hij_witness
316. 0316exact hcell_witness_right_left_left
317. 0317exfalso
318. 0318specialize succ_ne_zero (S i)
319. 0319apply succ_ne_zero
320. 0320exact hbad
321. 0321cases hcell_witness_right_right
322. 0322cases hcell_witness_right_right_witness
323. 0323cases hcell_witness_right_right_witness_witness
324. 0324cases hcell_witness_right_right_witness_witness_witness
325. 0325cases hcell_witness_right_right_witness_witness_witness_right
326. 0326cases hcell_witness_right_right_witness_witness_witness_right_right
327. 0327have hshifted_order : exists bcf_lt_gap_bptdb_shifted_above_order. bcf_lt_gap_bptdb_shifted_above_order + S (S i) = S x6
328. 0328rewrite <- hcell_witness_right_right_witness_witness_witness_left
329. 0329exact hij
330. 0330have hprevious_left_order : exists bcf_lt_gap_bptdb_previous_left_order. bcf_lt_gap_bptdb_previous_left_order + S (i) = x6
331. 0331specialize le_of_succ_le_succ (S i)
332. 0332specialize le_of_succ_le_succ x6
333. 0333apply le_of_succ_le_succ
334. 0334exact hshifted_order
335. 0335have hprevious_right_order : exists bcf_lt_gap_bptdb_previous_right_order. bcf_lt_gap_bptdb_previous_right_order + S (i) = S x6
336. 0336specialize lt_to_le (S i)
337. 0337specialize lt_to_le (S x6)
338. 0338apply lt_to_le
339. 0339exact hshifted_order
340. 0340have hprevious_right_bound : exists bcf_lt_gap_bptdb_previous_right_bound. bcf_lt_gap_bptdb_previous_right_bound + S (S x6) = w
341. 0341rewrite <- hcell_witness_right_right_witness_witness_witness_left
342. 0342exact hjw
343. 0343have hprevious_left_bound : exists bcf_lt_gap_bptdb_previous_left_bound. bcf_lt_gap_bptdb_previous_left_bound + S (x6) = w
344. 0344specialize lt_to_le (S x6)
345. 0345specialize lt_to_le w
346. 0346apply lt_to_le
347. 0347exact hprevious_right_bound
348. 0348have hleft_at : ((exists bcf_height_bptdb_above_previous_left. bcf_height_bptdb_above_previous_left + S (x7) = S ((S (x6)) * x4)) /\ exists bcf_quotient_bptdb_above_previous_left. x3 = bcf_quotient_bptdb_above_previous_left * S ((S (x6)) * x4) + (x7))
349. 0349exact hcell_witness_right_right_witness_witness_witness_right_left
350. 0350have hright_at : ((exists bcf_height_bptdb_above_previous_right. bcf_height_bptdb_above_previous_right + S (x8) = S ((S (S x6)) * x4)) /\ exists bcf_quotient_bptdb_above_previous_right. x3 = bcf_quotient_bptdb_above_previous_right * S ((S (S x6)) * x4) + (x8))
351. 0351exact hcell_witness_right_right_witness_witness_witness_right_right_left
352. 0352have hleft_zero : x7 = 0
353. 0353specialize hprevious_boundary_right x6
354. 0354specialize hprevious_boundary_right x7
355. 0355apply hprevious_boundary_right
356. 0356exact hprevious_left_order
357. 0357exact hprevious_left_bound
358. 0358exact hleft_at
359. 0359have hright_zero : x8 = 0
360. 0360specialize hprevious_boundary_right (S x6)
361. 0361specialize hprevious_boundary_right x8
362. 0362apply hprevious_boundary_right
363. 0363exact hprevious_right_order
364. 0364exact hprevious_right_bound
365. 0365exact hright_at
366. 0366trans x5
367. 0367exact hvalue
368. 0368rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
369. 0369simp [hleft_zero, hright_zero]