choose_zero

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 n
2. 0002intro z
3. 0003intro hchoose
4. 0004cases hchoose
5. 0005cases hchoose_left
6. 0006exfalso
7. 0007specialize lt_not_le n
8. 0008specialize lt_not_le 0
9. 0009apply lt_not_le
10. 0010exact hchoose_left_left
11. 0011specialize zero_le n
12. 0012exact zero_le
13. 0013cases hchoose_right
14. 0014cases hchoose_right_right
15. 0015cases hchoose_right_right_witness
16. 0016cases hchoose_right_right_witness_witness
17. 0017cases hchoose_right_right_witness_witness_witness
18. 0018cases hchoose_right_right_witness_witness_witness_witness
19. 0019cases hchoose_right_right_witness_witness_witness_witness_witness
20. 0020cases hchoose_right_right_witness_witness_witness_witness_witness_witness
21. 0021cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
22. 0022cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
23. 0023have hrow_bound : exists bcf_lt_gap_bclz_row_bound. bcf_lt_gap_bclz_row_bound + S (n) = S n
24. 0024specialize le_refl (S n)
25. 0025exact le_refl
26. 0026have hinner_bound : exists bcf_lt_gap_bclz_inner_bound. bcf_lt_gap_bclz_inner_bound + S (0) = S n
27. 0027specialize succ_le_succ 0
28. 0028specialize succ_le_succ n
29. 0029apply succ_le_succ
30. 0030specialize zero_le n
31. 0031exact zero_le
32. 0032have hrow : exists bcf_row_code_bclz_table_row bcf_row_scale_bclz_table_row. ((((exists bcf_height_bclz_table_row_decoded_row_code. bcf_height_bclz_table_row_decoded_row_code + S (bcf_row_code_bclz_table_row) = S ((S (n)) * x1)) /\ exists bcf_quotient_bclz_table_row_decoded_row_code. x = bcf_quotient_bclz_table_row_decoded_row_code * S ((S (n)) * x1) + (bcf_row_code_bclz_table_row))) /\ ((((exists bcf_height_bclz_table_row_decoded_row_scale. bcf_height_bclz_table_row_decoded_row_scale + S (bcf_row_scale_bclz_table_row) = S ((S (n)) * x3)) /\ exists bcf_quotient_bclz_table_row_decoded_row_scale. x2 = bcf_quotient_bclz_table_row_decoded_row_scale * S ((S (n)) * x3) + (bcf_row_scale_bclz_table_row))) /\ ((n = 0 /\ (forall bcf_index_bclz_table_row_zero_row. (exists bcf_lt_gap_bclz_table_row_zero_row_bound. bcf_lt_gap_bclz_table_row_zero_row_bound + S (bcf_index_bclz_table_row_zero_row) = S n) -> exists bcf_value_bclz_table_row_zero_row. ((((exists bcf_height_bclz_table_row_zero_row_entry. bcf_height_bclz_table_row_zero_row_entry + S (bcf_value_bclz_table_row_zero_row) = S ((S (bcf_index_bclz_table_row_zero_row)) * bcf_row_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_zero_row_entry. bcf_row_code_bclz_table_row = bcf_quotient_bclz_table_row_zero_row_entry * S ((S (bcf_index_bclz_table_row_zero_row)) * bcf_row_scale_bclz_table_row) + (bcf_value_bclz_table_row_zero_row))) /\ ((bcf_index_bclz_table_row_zero_row = 0 /\ bcf_value_bclz_table_row_zero_row = 1) \/ exists bcf_predecessor_bclz_table_row_zero_row. bcf_index_bclz_table_row_zero_row = S bcf_predecessor_bclz_table_row_zero_row /\ bcf_value_bclz_table_row_zero_row = 0)))) \/ exists bcf_predecessor_bclz_table_row bcf_previous_code_bclz_table_row bcf_previous_scale_bclz_table_row. n = S bcf_predecessor_bclz_table_row /\ ((((exists bcf_height_bclz_table_row_decoded_previous_code. bcf_height_bclz_table_row_decoded_previous_code + S (bcf_previous_code_bclz_table_row) = S ((S (bcf_predecessor_bclz_table_row)) * x1)) /\ exists bcf_quotient_bclz_table_row_decoded_previous_code. x = bcf_quotient_bclz_table_row_decoded_previous_code * S ((S (bcf_predecessor_bclz_table_row)) * x1) + (bcf_previous_code_bclz_table_row))) /\ ((((exists bcf_height_bclz_table_row_decoded_previous_scale. bcf_height_bclz_table_row_decoded_previous_scale + S (bcf_previous_scale_bclz_table_row) = S ((S (bcf_predecessor_bclz_table_row)) * x3)) /\ exists bcf_quotient_bclz_table_row_decoded_previous_scale. x2 = bcf_quotient_bclz_table_row_decoded_previous_scale * S ((S (bcf_predecessor_bclz_table_row)) * x3) + (bcf_previous_scale_bclz_table_row))) /\ (forall bcf_index_bclz_table_row_row_step. (exists bcf_lt_gap_bclz_table_row_row_step_bound. bcf_lt_gap_bclz_table_row_row_step_bound + S (bcf_index_bclz_table_row_row_step) = S n) -> exists bcf_value_bclz_table_row_row_step. ((((exists bcf_height_bclz_table_row_row_step_entry. bcf_height_bclz_table_row_row_step_entry + S (bcf_value_bclz_table_row_row_step) = S ((S (bcf_index_bclz_table_row_row_step)) * bcf_row_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_entry. bcf_row_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_entry * S ((S (bcf_index_bclz_table_row_row_step)) * bcf_row_scale_bclz_table_row) + (bcf_value_bclz_table_row_row_step))) /\ ((bcf_index_bclz_table_row_row_step = 0 /\ bcf_value_bclz_table_row_row_step = 1) \/ exists bcf_predecessor_bclz_table_row_row_step bcf_left_bclz_table_row_row_step bcf_right_bclz_table_row_row_step. bcf_index_bclz_table_row_row_step = S bcf_predecessor_bclz_table_row_row_step /\ ((((exists bcf_height_bclz_table_row_row_step_previous_left. bcf_height_bclz_table_row_row_step_previous_left + S (bcf_left_bclz_table_row_row_step) = S ((S (bcf_predecessor_bclz_table_row_row_step)) * bcf_previous_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_previous_left. bcf_previous_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_previous_left * S ((S (bcf_predecessor_bclz_table_row_row_step)) * bcf_previous_scale_bclz_table_row) + (bcf_left_bclz_table_row_row_step))) /\ ((((exists bcf_height_bclz_table_row_row_step_previous_right. bcf_height_bclz_table_row_row_step_previous_right + S (bcf_right_bclz_table_row_row_step) = S ((S (S (bcf_predecessor_bclz_table_row_row_step))) * bcf_previous_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_previous_right. bcf_previous_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_previous_right * S ((S (S (bcf_predecessor_bclz_table_row_row_step))) * bcf_previous_scale_bclz_table_row) + (bcf_right_bclz_table_row_row_step))) /\ bcf_value_bclz_table_row_row_step = bcf_left_bclz_table_row_row_step + bcf_right_bclz_table_row_row_step))))))))))
33. 0033specialize hchoose_right_right_witness_witness_witness_witness_witness_witness_left n
34. 0034apply hchoose_right_right_witness_witness_witness_witness_witness_witness_left
35. 0035exact hrow_bound
36. 0036cases hrow
37. 0037cases hrow_witness
38. 0038cases hrow_witness_witness
39. 0039cases hrow_witness_witness_right
40. 0040have hcode : x4 = x6
41. 0041specialize beta_at_unique x
42. 0042specialize beta_at_unique x1
43. 0043specialize beta_at_unique n
44. 0044specialize beta_at_unique x4
45. 0045specialize beta_at_unique x6
46. 0046apply beta_at_unique
47. 0047exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
48. 0048exact hrow_witness_witness_left
49. 0049have hscale : x5 = x7
50. 0050specialize beta_at_unique x2
51. 0051specialize beta_at_unique x3
52. 0052specialize beta_at_unique n
53. 0053specialize beta_at_unique x5
54. 0054specialize beta_at_unique x7
55. 0055apply beta_at_unique
56. 0056exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
57. 0057exact hrow_witness_witness_right_left
58. 0058have hvalue : ((exists bcf_height_bclz_semantic_at. bcf_height_bclz_semantic_at + S (z) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_semantic_at. x6 = bcf_quotient_bclz_semantic_at * S ((S (0)) * x7) + (z))
59. 0059rewrite <- hcode
60. 0060rewrite <- hscale
61. 0061rewrite <- hscale
62. 0062exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right
63. 0063cases hrow_witness_witness_right_right
64. 0064cases hrow_witness_witness_right_right_left
65. 0065have hcell : exists bcf_cell_value_bclz_zero_cell. ((((exists bcf_height_bclz_zero_cell_entry. bcf_height_bclz_zero_cell_entry + S (bcf_cell_value_bclz_zero_cell) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_zero_cell_entry. x6 = bcf_quotient_bclz_zero_cell_entry * S ((S (0)) * x7) + (bcf_cell_value_bclz_zero_cell))) /\ ((0 = 0 /\ bcf_cell_value_bclz_zero_cell = 1) \/ exists bcf_cell_predecessor_bclz_zero_cell. 0 = S bcf_cell_predecessor_bclz_zero_cell /\ bcf_cell_value_bclz_zero_cell = 0))
66. 0066specialize hrow_witness_witness_right_right_left_right 0
67. 0067apply hrow_witness_witness_right_right_left_right
68. 0068exact hinner_bound
69. 0069cases hcell
70. 0070cases hcell_witness
71. 0071have hzvalue : z = x8
72. 0072specialize beta_at_unique x6
73. 0073specialize beta_at_unique x7
74. 0074specialize beta_at_unique 0
75. 0075specialize beta_at_unique z
76. 0076specialize beta_at_unique x8
77. 0077apply beta_at_unique
78. 0078exact hvalue
79. 0079exact hcell_witness_left
80. 0080cases hcell_witness_right
81. 0081cases hcell_witness_right_left
82. 0082trans x8
83. 0083exact hzvalue
84. 0084exact hcell_witness_right_left_right
85. 0085cases hcell_witness_right_right
86. 0086cases hcell_witness_right_right_witness
87. 0087exfalso
88. 0088have hbad : S x9 = 0
89. 0089symm
90. 0090exact hcell_witness_right_right_witness_left
91. 0091specialize succ_ne_zero x9
92. 0092apply succ_ne_zero
93. 0093exact hbad
94. 0094cases hrow_witness_witness_right_right_right
95. 0095cases hrow_witness_witness_right_right_right_witness
96. 0096cases hrow_witness_witness_right_right_right_witness_witness
97. 0097cases hrow_witness_witness_right_right_right_witness_witness_witness
98. 0098cases hrow_witness_witness_right_right_right_witness_witness_witness_right
99. 0099cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
100. 0100have hcell : exists bcf_cell_value_bclz_step_cell. ((((exists bcf_height_bclz_step_cell_entry. bcf_height_bclz_step_cell_entry + S (bcf_cell_value_bclz_step_cell) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_step_cell_entry. x6 = bcf_quotient_bclz_step_cell_entry * S ((S (0)) * x7) + (bcf_cell_value_bclz_step_cell))) /\ ((0 = 0 /\ bcf_cell_value_bclz_step_cell = 1) \/ exists bcf_cell_predecessor_bclz_step_cell bcf_cell_left_bclz_step_cell bcf_cell_right_bclz_step_cell. 0 = S bcf_cell_predecessor_bclz_step_cell /\ ((((exists bcf_height_bclz_step_cell_previous_left. bcf_height_bclz_step_cell_previous_left + S (bcf_cell_left_bclz_step_cell) = S ((S (bcf_cell_predecessor_bclz_step_cell)) * x10)) /\ exists bcf_quotient_bclz_step_cell_previous_left. x9 = bcf_quotient_bclz_step_cell_previous_left * S ((S (bcf_cell_predecessor_bclz_step_cell)) * x10) + (bcf_cell_left_bclz_step_cell))) /\ ((((exists bcf_height_bclz_step_cell_previous_right. bcf_height_bclz_step_cell_previous_right + S (bcf_cell_right_bclz_step_cell) = S ((S (S (bcf_cell_predecessor_bclz_step_cell))) * x10)) /\ exists bcf_quotient_bclz_step_cell_previous_right. x9 = bcf_quotient_bclz_step_cell_previous_right * S ((S (S (bcf_cell_predecessor_bclz_step_cell))) * x10) + (bcf_cell_right_bclz_step_cell))) /\ bcf_cell_value_bclz_step_cell = bcf_cell_left_bclz_step_cell + bcf_cell_right_bclz_step_cell))))
101. 0101specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right 0
102. 0102apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
103. 0103exact hinner_bound
104. 0104cases hcell
105. 0105cases hcell_witness
106. 0106have hzvalue : z = x11
107. 0107specialize beta_at_unique x6
108. 0108specialize beta_at_unique x7
109. 0109specialize beta_at_unique 0
110. 0110specialize beta_at_unique z
111. 0111specialize beta_at_unique x11
112. 0112apply beta_at_unique
113. 0113exact hvalue
114. 0114exact hcell_witness_left
115. 0115cases hcell_witness_right
116. 0116cases hcell_witness_right_left
117. 0117trans x11
118. 0118exact hzvalue
119. 0119exact hcell_witness_right_left_right
120. 0120cases hcell_witness_right_right
121. 0121cases hcell_witness_right_right_witness
122. 0122cases hcell_witness_right_right_witness_witness
123. 0123cases hcell_witness_right_right_witness_witness_witness
124. 0124exfalso
125. 0125have hbad : S x12 = 0
126. 0126symm
127. 0127exact hcell_witness_right_right_witness_witness_witness_left
128. 0128specialize succ_ne_zero x12
129. 0129apply succ_ne_zero
130. 0130exact hbad