beta_pascal_table_successor_cell_recurrence

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 i
8. 0008intro j
9. 0009intro b
10. 0010intro c
11. 0011intro z
12. 0012intro htable
13. 0013intro hrow_bound
14. 0014intro hcell_bound
15. 0015intro hrow_code
16. 0016intro hrow_scale
17. 0017intro hcurrent
18. 0018have hrow : exists bcf_row_code_bptscr_semantic_row bcf_row_scale_bptscr_semantic_row. ((((exists bcf_height_bptscr_semantic_row_decoded_row_code. bcf_height_bptscr_semantic_row_decoded_row_code + S (bcf_row_code_bptscr_semantic_row) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_row_code. bb = bcf_quotient_bptscr_semantic_row_decoded_row_code * S ((S (S i)) * bc) + (bcf_row_code_bptscr_semantic_row))) /\ ((((exists bcf_height_bptscr_semantic_row_decoded_row_scale. bcf_height_bptscr_semantic_row_decoded_row_scale + S (bcf_row_scale_bptscr_semantic_row) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_row_scale. sb = bcf_quotient_bptscr_semantic_row_decoded_row_scale * S ((S (S i)) * sc) + (bcf_row_scale_bptscr_semantic_row))) /\ ((S i = 0 /\ (forall bcf_index_bptscr_semantic_row_zero_row. (exists bcf_lt_gap_bptscr_semantic_row_zero_row_bound. bcf_lt_gap_bptscr_semantic_row_zero_row_bound + S (bcf_index_bptscr_semantic_row_zero_row) = w) -> exists bcf_value_bptscr_semantic_row_zero_row. ((((exists bcf_height_bptscr_semantic_row_zero_row_entry. bcf_height_bptscr_semantic_row_zero_row_entry + S (bcf_value_bptscr_semantic_row_zero_row) = S ((S (bcf_index_bptscr_semantic_row_zero_row)) * bcf_row_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_zero_row_entry. bcf_row_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_zero_row_entry * S ((S (bcf_index_bptscr_semantic_row_zero_row)) * bcf_row_scale_bptscr_semantic_row) + (bcf_value_bptscr_semantic_row_zero_row))) /\ ((bcf_index_bptscr_semantic_row_zero_row = 0 /\ bcf_value_bptscr_semantic_row_zero_row = 1) \/ exists bcf_predecessor_bptscr_semantic_row_zero_row. bcf_index_bptscr_semantic_row_zero_row = S bcf_predecessor_bptscr_semantic_row_zero_row /\ bcf_value_bptscr_semantic_row_zero_row = 0)))) \/ exists bcf_predecessor_bptscr_semantic_row bcf_previous_code_bptscr_semantic_row bcf_previous_scale_bptscr_semantic_row. S i = S bcf_predecessor_bptscr_semantic_row /\ ((((exists bcf_height_bptscr_semantic_row_decoded_previous_code. bcf_height_bptscr_semantic_row_decoded_previous_code + S (bcf_previous_code_bptscr_semantic_row) = S ((S (bcf_predecessor_bptscr_semantic_row)) * bc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_previous_code. bb = bcf_quotient_bptscr_semantic_row_decoded_previous_code * S ((S (bcf_predecessor_bptscr_semantic_row)) * bc) + (bcf_previous_code_bptscr_semantic_row))) /\ ((((exists bcf_height_bptscr_semantic_row_decoded_previous_scale. bcf_height_bptscr_semantic_row_decoded_previous_scale + S (bcf_previous_scale_bptscr_semantic_row) = S ((S (bcf_predecessor_bptscr_semantic_row)) * sc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_previous_scale. sb = bcf_quotient_bptscr_semantic_row_decoded_previous_scale * S ((S (bcf_predecessor_bptscr_semantic_row)) * sc) + (bcf_previous_scale_bptscr_semantic_row))) /\ (forall bcf_index_bptscr_semantic_row_row_step. (exists bcf_lt_gap_bptscr_semantic_row_row_step_bound. bcf_lt_gap_bptscr_semantic_row_row_step_bound + S (bcf_index_bptscr_semantic_row_row_step) = w) -> exists bcf_value_bptscr_semantic_row_row_step. ((((exists bcf_height_bptscr_semantic_row_row_step_entry. bcf_height_bptscr_semantic_row_row_step_entry + S (bcf_value_bptscr_semantic_row_row_step) = S ((S (bcf_index_bptscr_semantic_row_row_step)) * bcf_row_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_entry. bcf_row_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_entry * S ((S (bcf_index_bptscr_semantic_row_row_step)) * bcf_row_scale_bptscr_semantic_row) + (bcf_value_bptscr_semantic_row_row_step))) /\ ((bcf_index_bptscr_semantic_row_row_step = 0 /\ bcf_value_bptscr_semantic_row_row_step = 1) \/ exists bcf_predecessor_bptscr_semantic_row_row_step bcf_left_bptscr_semantic_row_row_step bcf_right_bptscr_semantic_row_row_step. bcf_index_bptscr_semantic_row_row_step = S bcf_predecessor_bptscr_semantic_row_row_step /\ ((((exists bcf_height_bptscr_semantic_row_row_step_previous_left. bcf_height_bptscr_semantic_row_row_step_previous_left + S (bcf_left_bptscr_semantic_row_row_step) = S ((S (bcf_predecessor_bptscr_semantic_row_row_step)) * bcf_previous_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_previous_left. bcf_previous_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_previous_left * S ((S (bcf_predecessor_bptscr_semantic_row_row_step)) * bcf_previous_scale_bptscr_semantic_row) + (bcf_left_bptscr_semantic_row_row_step))) /\ ((((exists bcf_height_bptscr_semantic_row_row_step_previous_right. bcf_height_bptscr_semantic_row_row_step_previous_right + S (bcf_right_bptscr_semantic_row_row_step) = S ((S (S (bcf_predecessor_bptscr_semantic_row_row_step))) * bcf_previous_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_previous_right. bcf_previous_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptscr_semantic_row_row_step))) * bcf_previous_scale_bptscr_semantic_row) + (bcf_right_bptscr_semantic_row_row_step))) /\ bcf_value_bptscr_semantic_row_row_step = bcf_left_bptscr_semantic_row_row_step + bcf_right_bptscr_semantic_row_row_step))))))))))
19. 0019specialize htable (S i)
20. 0020apply htable
21. 0021exact hrow_bound
22. 0022cases hrow
23. 0023cases hrow_witness
24. 0024cases hrow_witness_witness
25. 0025cases hrow_witness_witness_right
26. 0026have hcode : b = x
27. 0027specialize beta_at_unique bb
28. 0028specialize beta_at_unique bc
29. 0029specialize beta_at_unique (S i)
30. 0030specialize beta_at_unique b
31. 0031specialize beta_at_unique x
32. 0032apply beta_at_unique
33. 0033exact hrow_code
34. 0034exact hrow_witness_witness_left
35. 0035have hscale : c = x1
36. 0036specialize beta_at_unique sb
37. 0037specialize beta_at_unique sc
38. 0038specialize beta_at_unique (S i)
39. 0039specialize beta_at_unique c
40. 0040specialize beta_at_unique x1
41. 0041apply beta_at_unique
42. 0042exact hrow_scale
43. 0043exact hrow_witness_witness_right_left
44. 0044cases hrow_witness_witness_right_right
45. 0045cases hrow_witness_witness_right_right_left
46. 0046exfalso
47. 0047specialize succ_ne_zero i
48. 0048apply succ_ne_zero
49. 0049exact hrow_witness_witness_right_right_left_left
50. 0050cases hrow_witness_witness_right_right_right
51. 0051cases hrow_witness_witness_right_right_right_witness
52. 0052cases hrow_witness_witness_right_right_right_witness_witness
53. 0053cases hrow_witness_witness_right_right_right_witness_witness_witness
54. 0054cases hrow_witness_witness_right_right_right_witness_witness_witness_right
55. 0055cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
56. 0056have hpredecessor : i = x2
57. 0057specialize succ_injective i
58. 0058specialize succ_injective x2
59. 0059apply succ_injective
60. 0060exact hrow_witness_witness_right_right_right_witness_witness_witness_left
61. 0061have hprevious_code : ((exists bcf_height_bptscr_previous_code_at. bcf_height_bptscr_previous_code_at + S (x3) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptscr_previous_code_at. bb = bcf_quotient_bptscr_previous_code_at * S ((S (i)) * bc) + (x3))
62. 0062rewrite hpredecessor
63. 0063rewrite hpredecessor
64. 0064exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
65. 0065have hprevious_scale : ((exists bcf_height_bptscr_previous_scale_at. bcf_height_bptscr_previous_scale_at + S (x4) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptscr_previous_scale_at. sb = bcf_quotient_bptscr_previous_scale_at * S ((S (i)) * sc) + (x4))
66. 0066rewrite hpredecessor
67. 0067rewrite hpredecessor
68. 0068exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
69. 0069have hsemantic_current : ((exists bcf_height_bptscr_semantic_current_at. bcf_height_bptscr_semantic_current_at + S (z) = S ((S (S j)) * x1)) /\ exists bcf_quotient_bptscr_semantic_current_at. x = bcf_quotient_bptscr_semantic_current_at * S ((S (S j)) * x1) + (z))
70. 0070rewrite <- hcode
71. 0071rewrite <- hscale
72. 0072rewrite <- hscale
73. 0073exact hcurrent
74. 0074have hcell : exists bcf_cell_value_bptscr_semantic_cell. ((((exists bcf_height_bptscr_semantic_cell_entry. bcf_height_bptscr_semantic_cell_entry + S (bcf_cell_value_bptscr_semantic_cell) = S ((S (S j)) * x1)) /\ exists bcf_quotient_bptscr_semantic_cell_entry. x = bcf_quotient_bptscr_semantic_cell_entry * S ((S (S j)) * x1) + (bcf_cell_value_bptscr_semantic_cell))) /\ ((S j = 0 /\ bcf_cell_value_bptscr_semantic_cell = 1) \/ exists bcf_cell_predecessor_bptscr_semantic_cell bcf_cell_left_bptscr_semantic_cell bcf_cell_right_bptscr_semantic_cell. S j = S bcf_cell_predecessor_bptscr_semantic_cell /\ ((((exists bcf_height_bptscr_semantic_cell_previous_left. bcf_height_bptscr_semantic_cell_previous_left + S (bcf_cell_left_bptscr_semantic_cell) = S ((S (bcf_cell_predecessor_bptscr_semantic_cell)) * x4)) /\ exists bcf_quotient_bptscr_semantic_cell_previous_left. x3 = bcf_quotient_bptscr_semantic_cell_previous_left * S ((S (bcf_cell_predecessor_bptscr_semantic_cell)) * x4) + (bcf_cell_left_bptscr_semantic_cell))) /\ ((((exists bcf_height_bptscr_semantic_cell_previous_right. bcf_height_bptscr_semantic_cell_previous_right + S (bcf_cell_right_bptscr_semantic_cell) = S ((S (S (bcf_cell_predecessor_bptscr_semantic_cell))) * x4)) /\ exists bcf_quotient_bptscr_semantic_cell_previous_right. x3 = bcf_quotient_bptscr_semantic_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptscr_semantic_cell))) * x4) + (bcf_cell_right_bptscr_semantic_cell))) /\ bcf_cell_value_bptscr_semantic_cell = bcf_cell_left_bptscr_semantic_cell + bcf_cell_right_bptscr_semantic_cell))))
75. 0075specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S j)
76. 0076apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
77. 0077exact hcell_bound
78. 0078cases hcell
79. 0079cases hcell_witness
80. 0080have hvalue : z = x5
81. 0081specialize beta_at_unique x
82. 0082specialize beta_at_unique x1
83. 0083specialize beta_at_unique (S j)
84. 0084specialize beta_at_unique z
85. 0085specialize beta_at_unique x5
86. 0086apply beta_at_unique
87. 0087exact hsemantic_current
88. 0088exact hcell_witness_left
89. 0089cases hcell_witness_right
90. 0090cases hcell_witness_right_left
91. 0091exfalso
92. 0092specialize succ_ne_zero j
93. 0093apply succ_ne_zero
94. 0094exact hcell_witness_right_left_left
95. 0095cases hcell_witness_right_right
96. 0096cases hcell_witness_right_right_witness
97. 0097cases hcell_witness_right_right_witness_witness
98. 0098cases hcell_witness_right_right_witness_witness_witness
99. 0099cases hcell_witness_right_right_witness_witness_witness_right
100. 0100cases hcell_witness_right_right_witness_witness_witness_right_right
101. 0101have hcell_predecessor : j = x6
102. 0102specialize succ_injective j
103. 0103specialize succ_injective x6
104. 0104apply succ_injective
105. 0105exact hcell_witness_right_right_witness_witness_witness_left
106. 0106have hleft : ((exists bcf_height_bptscr_returned_left_at. bcf_height_bptscr_returned_left_at + S (x7) = S ((S (j)) * x4)) /\ exists bcf_quotient_bptscr_returned_left_at. x3 = bcf_quotient_bptscr_returned_left_at * S ((S (j)) * x4) + (x7))
107. 0107rewrite hcell_predecessor
108. 0108rewrite hcell_predecessor
109. 0109exact hcell_witness_right_right_witness_witness_witness_right_left
110. 0110have hright : ((exists bcf_height_bptscr_returned_right_at. bcf_height_bptscr_returned_right_at + S (x8) = S ((S (S j)) * x4)) /\ exists bcf_quotient_bptscr_returned_right_at. x3 = bcf_quotient_bptscr_returned_right_at * S ((S (S j)) * x4) + (x8))
111. 0111rewrite hcell_predecessor
112. 0112rewrite hcell_predecessor
113. 0113exact hcell_witness_right_right_witness_witness_witness_right_right_left
114. 0114exists x3
115. 0115exists x4
116. 0116exists x7
117. 0117exists x8
118. 0118split
119. 0119exact hprevious_code
120. 0120split
121. 0121exact hprevious_scale
122. 0122split
123. 0123exact hleft
124. 0124split
125. 0125exact hright
126. 0126trans x5
127. 0127exact hvalue
128. 0128exact hcell_witness_right_right_witness_witness_witness_right_right_right