bertrand_hj_six_block_iterate_from_total

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 b
2. 0002intro htotal
3. 0003intro hlower
4. 0004intro hupper
5. 0005induction k
6. 0006intro e
7. 0007intro h
8. 0008intro u
9. 0009intro j
10. 0010intro g
11. 0011intro hceiling
12. 0012intro hh
13. 0013intro hu
14. 0014intro hj
15. 0015intro hg
16. 0016have hroot_zero : b + 6 * 0 = b
17. 0017rewrite PA5
18. 0018apply PA3
19. 0019have hzero_lower : exists bqb_le_gap_hjas_iterator_zero_lower. bqb_le_gap_hjas_iterator_zero_lower + (32) = (b + 6 * 0)
20. 0020rewrite hroot_zero
21. 0021exact hlower
22. 0022have hzero_upper : exists bqb_le_gap_hjas_iterator_zero_upper. bqb_le_gap_hjas_iterator_zero_upper + (b + 6 * 0) = (37)
23. 0023rewrite hroot_zero
24. 0024exact hupper
25. 0025specialize bertrand_hj_base_window_thirty_two_from_total (b + 6 * 0)
26. 0026specialize bertrand_hj_base_window_thirty_two_from_total e
27. 0027specialize bertrand_hj_base_window_thirty_two_from_total h
28. 0028specialize bertrand_hj_base_window_thirty_two_from_total u
29. 0029specialize bertrand_hj_base_window_thirty_two_from_total j
30. 0030specialize bertrand_hj_base_window_thirty_two_from_total g
31. 0031apply bertrand_hj_base_window_thirty_two_from_total
32. 0032exact htotal
33. 0033exact hzero_lower
34. 0034exact hzero_upper
35. 0035exact hceiling
36. 0036exact hh
37. 0037exact hu
38. 0038exact hj
39. 0039exact hg
40. 0040intro e
41. 0041intro h
42. 0042intro u
43. 0043intro j
44. 0044intro g
45. 0045intro hceiling
46. 0046intro hh
47. 0047intro hu
48. 0048intro hj
49. 0049intro hg
50. 0050have hcurrent_ceiling : exists ce. (((exists bcs_lower_gap_hjas_current_ceiling_exists. bcs_lower_gap_hjas_current_ceiling_exists + ((b + 6 * k) * (b + 6 * k)) = 6 * (ce)) /\ exists bcs_upper_gap_hjas_current_ceiling_exists. bcs_upper_gap_hjas_current_ceiling_exists + S (6 * (ce)) = ((b + 6 * k) * (b + 6 * k)) + 6))
51. 0051specialize ceil_div_six_total ((b + 6 * k) * (b + 6 * k))
52. 0052exact ceil_div_six_total
53. 0053cases hcurrent_ceiling
54. 0054have hcurrent_h : exists hh. (exists pa_b_hjas_current_h_exists pa_c_hjas_current_h_exists. ((forall pa_i_hjas_current_h_exists_repeat. (exists pa_lt_hjas_current_h_exists_repeat_bound. pa_lt_hjas_current_h_exists_repeat_bound + S pa_i_hjas_current_h_exists_repeat = 2 * (b + 6 * k) + 2) -> (((exists pa_h_hjas_current_h_exists_repeat_decoded. pa_h_hjas_current_h_exists_repeat_decoded + S ((b + 6 * k) + 1) = S ((S (pa_i_hjas_current_h_exists_repeat)) * pa_c_hjas_current_h_exists)) /\ exists pa_q_hjas_current_h_exists_repeat_decoded. pa_b_hjas_current_h_exists = pa_q_hjas_current_h_exists_repeat_decoded * S ((S (pa_i_hjas_current_h_exists_repeat)) * pa_c_hjas_current_h_exists) + ((b + 6 * k) + 1)))) /\ (exists pa_u_hjas_current_h_exists_product pa_v_hjas_current_h_exists_product. ((((exists pa_h_hjas_current_h_exists_product_start. pa_h_hjas_current_h_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_start. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_start * S ((S (0)) * pa_v_hjas_current_h_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_h_exists_product_terminal. pa_h_hjas_current_h_exists_product_terminal + S (hh) = S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_terminal. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_terminal * S ((S (2 * (b + 6 * k) + 2)) * pa_v_hjas_current_h_exists_product) + (hh))) /\ forall pa_i_hjas_current_h_exists_product. (exists pa_lt_hjas_current_h_exists_product_bound. pa_lt_hjas_current_h_exists_product_bound + S pa_i_hjas_current_h_exists_product = 2 * (b + 6 * k) + 2) -> exists pa_p_hjas_current_h_exists_product pa_r_hjas_current_h_exists_product pa_s_hjas_current_h_exists_product. ((((exists pa_h_hjas_current_h_exists_product_factor. pa_h_hjas_current_h_exists_product_factor + S (pa_p_hjas_current_h_exists_product) = S ((S (pa_i_hjas_current_h_exists_product)) * pa_c_hjas_current_h_exists)) /\ exists pa_q_hjas_current_h_exists_product_factor. pa_b_hjas_current_h_exists = pa_q_hjas_current_h_exists_product_factor * S ((S (pa_i_hjas_current_h_exists_product)) * pa_c_hjas_current_h_exists) + (pa_p_hjas_current_h_exists_product))) /\ ((((exists pa_h_hjas_current_h_exists_product_partial. pa_h_hjas_current_h_exists_product_partial + S (pa_r_hjas_current_h_exists_product) = S ((S (pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_partial. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_partial * S ((S (pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product) + (pa_r_hjas_current_h_exists_product))) /\ ((((exists pa_h_hjas_current_h_exists_product_successor. pa_h_hjas_current_h_exists_product_successor + S (pa_s_hjas_current_h_exists_product) = S ((S (S pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product)) /\ exists pa_q_hjas_current_h_exists_product_successor. pa_u_hjas_current_h_exists_product = pa_q_hjas_current_h_exists_product_successor * S ((S (S pa_i_hjas_current_h_exists_product)) * pa_v_hjas_current_h_exists_product) + (pa_s_hjas_current_h_exists_product))) /\ pa_s_hjas_current_h_exists_product = pa_r_hjas_current_h_exists_product * pa_p_hjas_current_h_exists_product))))))))
55. 0055specialize htotal ((b + 6 * k) + 1)
56. 0056specialize htotal (2 * (b + 6 * k) + 2)
57. 0057exact htotal
58. 0058cases hcurrent_h
59. 0059have hcurrent_u : exists hu. (exists pa_b_hjas_current_u_exists pa_c_hjas_current_u_exists. ((forall pa_i_hjas_current_u_exists_repeat. (exists pa_lt_hjas_current_u_exists_repeat_bound. pa_lt_hjas_current_u_exists_repeat_bound + S pa_i_hjas_current_u_exists_repeat = x) -> (((exists pa_h_hjas_current_u_exists_repeat_decoded. pa_h_hjas_current_u_exists_repeat_decoded + S (4) = S ((S (pa_i_hjas_current_u_exists_repeat)) * pa_c_hjas_current_u_exists)) /\ exists pa_q_hjas_current_u_exists_repeat_decoded. pa_b_hjas_current_u_exists = pa_q_hjas_current_u_exists_repeat_decoded * S ((S (pa_i_hjas_current_u_exists_repeat)) * pa_c_hjas_current_u_exists) + (4)))) /\ (exists pa_u_hjas_current_u_exists_product pa_v_hjas_current_u_exists_product. ((((exists pa_h_hjas_current_u_exists_product_start. pa_h_hjas_current_u_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_start. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_start * S ((S (0)) * pa_v_hjas_current_u_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_u_exists_product_terminal. pa_h_hjas_current_u_exists_product_terminal + S (hu) = S ((S (x)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_terminal. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_terminal * S ((S (x)) * pa_v_hjas_current_u_exists_product) + (hu))) /\ forall pa_i_hjas_current_u_exists_product. (exists pa_lt_hjas_current_u_exists_product_bound. pa_lt_hjas_current_u_exists_product_bound + S pa_i_hjas_current_u_exists_product = x) -> exists pa_p_hjas_current_u_exists_product pa_r_hjas_current_u_exists_product pa_s_hjas_current_u_exists_product. ((((exists pa_h_hjas_current_u_exists_product_factor. pa_h_hjas_current_u_exists_product_factor + S (pa_p_hjas_current_u_exists_product) = S ((S (pa_i_hjas_current_u_exists_product)) * pa_c_hjas_current_u_exists)) /\ exists pa_q_hjas_current_u_exists_product_factor. pa_b_hjas_current_u_exists = pa_q_hjas_current_u_exists_product_factor * S ((S (pa_i_hjas_current_u_exists_product)) * pa_c_hjas_current_u_exists) + (pa_p_hjas_current_u_exists_product))) /\ ((((exists pa_h_hjas_current_u_exists_product_partial. pa_h_hjas_current_u_exists_product_partial + S (pa_r_hjas_current_u_exists_product) = S ((S (pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_partial. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_partial * S ((S (pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product) + (pa_r_hjas_current_u_exists_product))) /\ ((((exists pa_h_hjas_current_u_exists_product_successor. pa_h_hjas_current_u_exists_product_successor + S (pa_s_hjas_current_u_exists_product) = S ((S (S pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product)) /\ exists pa_q_hjas_current_u_exists_product_successor. pa_u_hjas_current_u_exists_product = pa_q_hjas_current_u_exists_product_successor * S ((S (S pa_i_hjas_current_u_exists_product)) * pa_v_hjas_current_u_exists_product) + (pa_s_hjas_current_u_exists_product))) /\ pa_s_hjas_current_u_exists_product = pa_r_hjas_current_u_exists_product * pa_p_hjas_current_u_exists_product))))))))
60. 0060specialize htotal 4
61. 0061specialize htotal x
62. 0062exact htotal
63. 0063cases hcurrent_u
64. 0064have hcurrent_j : exists jj. (exists pa_b_hjas_current_j_exists pa_c_hjas_current_j_exists. ((forall pa_i_hjas_current_j_exists_repeat. (exists pa_lt_hjas_current_j_exists_repeat_bound. pa_lt_hjas_current_j_exists_repeat_bound + S pa_i_hjas_current_j_exists_repeat = 12) -> (((exists pa_h_hjas_current_j_exists_repeat_decoded. pa_h_hjas_current_j_exists_repeat_decoded + S ((b + 6 * k) + 7) = S ((S (pa_i_hjas_current_j_exists_repeat)) * pa_c_hjas_current_j_exists)) /\ exists pa_q_hjas_current_j_exists_repeat_decoded. pa_b_hjas_current_j_exists = pa_q_hjas_current_j_exists_repeat_decoded * S ((S (pa_i_hjas_current_j_exists_repeat)) * pa_c_hjas_current_j_exists) + ((b + 6 * k) + 7)))) /\ (exists pa_u_hjas_current_j_exists_product pa_v_hjas_current_j_exists_product. ((((exists pa_h_hjas_current_j_exists_product_start. pa_h_hjas_current_j_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_start. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_start * S ((S (0)) * pa_v_hjas_current_j_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_j_exists_product_terminal. pa_h_hjas_current_j_exists_product_terminal + S (jj) = S ((S (12)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_terminal. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_terminal * S ((S (12)) * pa_v_hjas_current_j_exists_product) + (jj))) /\ forall pa_i_hjas_current_j_exists_product. (exists pa_lt_hjas_current_j_exists_product_bound. pa_lt_hjas_current_j_exists_product_bound + S pa_i_hjas_current_j_exists_product = 12) -> exists pa_p_hjas_current_j_exists_product pa_r_hjas_current_j_exists_product pa_s_hjas_current_j_exists_product. ((((exists pa_h_hjas_current_j_exists_product_factor. pa_h_hjas_current_j_exists_product_factor + S (pa_p_hjas_current_j_exists_product) = S ((S (pa_i_hjas_current_j_exists_product)) * pa_c_hjas_current_j_exists)) /\ exists pa_q_hjas_current_j_exists_product_factor. pa_b_hjas_current_j_exists = pa_q_hjas_current_j_exists_product_factor * S ((S (pa_i_hjas_current_j_exists_product)) * pa_c_hjas_current_j_exists) + (pa_p_hjas_current_j_exists_product))) /\ ((((exists pa_h_hjas_current_j_exists_product_partial. pa_h_hjas_current_j_exists_product_partial + S (pa_r_hjas_current_j_exists_product) = S ((S (pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_partial. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_partial * S ((S (pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product) + (pa_r_hjas_current_j_exists_product))) /\ ((((exists pa_h_hjas_current_j_exists_product_successor. pa_h_hjas_current_j_exists_product_successor + S (pa_s_hjas_current_j_exists_product) = S ((S (S pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product)) /\ exists pa_q_hjas_current_j_exists_product_successor. pa_u_hjas_current_j_exists_product = pa_q_hjas_current_j_exists_product_successor * S ((S (S pa_i_hjas_current_j_exists_product)) * pa_v_hjas_current_j_exists_product) + (pa_s_hjas_current_j_exists_product))) /\ pa_s_hjas_current_j_exists_product = pa_r_hjas_current_j_exists_product * pa_p_hjas_current_j_exists_product))))))))
65. 0065specialize htotal ((b + 6 * k) + 7)
66. 0066specialize htotal 12
67. 0067exact htotal
68. 0068cases hcurrent_j
69. 0069have hcurrent_g : exists gg. (exists pa_b_hjas_current_g_exists pa_c_hjas_current_g_exists. ((forall pa_i_hjas_current_g_exists_repeat. (exists pa_lt_hjas_current_g_exists_repeat_bound. pa_lt_hjas_current_g_exists_repeat_bound + S pa_i_hjas_current_g_exists_repeat = (b + 6 * k) + 5) -> (((exists pa_h_hjas_current_g_exists_repeat_decoded. pa_h_hjas_current_g_exists_repeat_decoded + S (4) = S ((S (pa_i_hjas_current_g_exists_repeat)) * pa_c_hjas_current_g_exists)) /\ exists pa_q_hjas_current_g_exists_repeat_decoded. pa_b_hjas_current_g_exists = pa_q_hjas_current_g_exists_repeat_decoded * S ((S (pa_i_hjas_current_g_exists_repeat)) * pa_c_hjas_current_g_exists) + (4)))) /\ (exists pa_u_hjas_current_g_exists_product pa_v_hjas_current_g_exists_product. ((((exists pa_h_hjas_current_g_exists_product_start. pa_h_hjas_current_g_exists_product_start + S (1) = S ((S (0)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_start. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_start * S ((S (0)) * pa_v_hjas_current_g_exists_product) + (1))) /\ ((((exists pa_h_hjas_current_g_exists_product_terminal. pa_h_hjas_current_g_exists_product_terminal + S (gg) = S ((S ((b + 6 * k) + 5)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_terminal. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_terminal * S ((S ((b + 6 * k) + 5)) * pa_v_hjas_current_g_exists_product) + (gg))) /\ forall pa_i_hjas_current_g_exists_product. (exists pa_lt_hjas_current_g_exists_product_bound. pa_lt_hjas_current_g_exists_product_bound + S pa_i_hjas_current_g_exists_product = (b + 6 * k) + 5) -> exists pa_p_hjas_current_g_exists_product pa_r_hjas_current_g_exists_product pa_s_hjas_current_g_exists_product. ((((exists pa_h_hjas_current_g_exists_product_factor. pa_h_hjas_current_g_exists_product_factor + S (pa_p_hjas_current_g_exists_product) = S ((S (pa_i_hjas_current_g_exists_product)) * pa_c_hjas_current_g_exists)) /\ exists pa_q_hjas_current_g_exists_product_factor. pa_b_hjas_current_g_exists = pa_q_hjas_current_g_exists_product_factor * S ((S (pa_i_hjas_current_g_exists_product)) * pa_c_hjas_current_g_exists) + (pa_p_hjas_current_g_exists_product))) /\ ((((exists pa_h_hjas_current_g_exists_product_partial. pa_h_hjas_current_g_exists_product_partial + S (pa_r_hjas_current_g_exists_product) = S ((S (pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_partial. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_partial * S ((S (pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product) + (pa_r_hjas_current_g_exists_product))) /\ ((((exists pa_h_hjas_current_g_exists_product_successor. pa_h_hjas_current_g_exists_product_successor + S (pa_s_hjas_current_g_exists_product) = S ((S (S pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product)) /\ exists pa_q_hjas_current_g_exists_product_successor. pa_u_hjas_current_g_exists_product = pa_q_hjas_current_g_exists_product_successor * S ((S (S pa_i_hjas_current_g_exists_product)) * pa_v_hjas_current_g_exists_product) + (pa_s_hjas_current_g_exists_product))) /\ pa_s_hjas_current_g_exists_product = pa_r_hjas_current_g_exists_product * pa_p_hjas_current_g_exists_product))))))))
70. 0070specialize htotal 4
71. 0071specialize htotal ((b + 6 * k) + 5)
72. 0072exact htotal
73. 0073cases hcurrent_g
74. 0074have hcurrent_bounds : ((exists bqb_le_gap_hjas_current_h_result. bqb_le_gap_hjas_current_h_result + (x1) = (x2)) /\ (exists bqb_le_gap_hjas_current_j_result. bqb_le_gap_hjas_current_j_result + (x3) = (x4)))
75. 0075specialize IH x
76. 0076specialize IH x1
77. 0077specialize IH x2
78. 0078specialize IH x3
79. 0079specialize IH x4
80. 0080apply IH
81. 0081exact hcurrent_ceiling_witness
82. 0082exact hcurrent_h_witness
83. 0083exact hcurrent_u_witness
84. 0084exact hcurrent_j_witness
85. 0085exact hcurrent_g_witness
86. 0086cases hcurrent_bounds
87. 0087have hfive_thirty_two : exists bqb_le_gap_hjas_five_le_thirty_two. bqb_le_gap_hjas_five_le_thirty_two + (5) = (32)
88. 0088exists 27
89. 0089norm_num
90. 0090have hfive_base : exists bqb_le_gap_hjas_five_le_base. bqb_le_gap_hjas_five_le_base + (5) = (b)
91. 0091specialize le_trans 5
92. 0092specialize le_trans 32
93. 0093specialize le_trans b
94. 0094apply le_trans
95. 0095exact hfive_thirty_two
96. 0096exact hlower
97. 0097have hbase_current : exists bqb_le_gap_hjas_base_le_current. bqb_le_gap_hjas_base_le_current + (b) = (b + 6 * k)
98. 0098specialize le_add_right b
99. 0099specialize le_add_right (6 * k)
100. 0100exact le_add_right
101. 0101have hfive_current : exists bqb_le_gap_hjas_five_le_current. bqb_le_gap_hjas_five_le_current + (5) = (b + 6 * k)
102. 0102specialize le_trans 5
103. 0103specialize le_trans b
104. 0104specialize le_trans (b + 6 * k)
105. 0105apply le_trans
106. 0106exact hfive_base
107. 0107exact hbase_current
108. 0108have hroot_step : b + 6 * S k = (b + 6 * k) + 6
109. 0109rewrite PA6
110. 0110symm
111. 0111specialize add_assoc b
112. 0112specialize add_assoc (6 * k)
113. 0113specialize add_assoc 6
114. 0114apply add_assoc
115. 0115have hnext_h_base : (b + 6 * S k) + 1 = (b + 6 * k) + 7
116. 0116rewrite hroot_step
117. 0117simp
118. 0118have hnext_h_exponent : 2 * (b + 6 * S k) + 2 = 2 * (b + 6 * k) + 14
119. 0119rewrite hroot_step
120. 0120simp [mul_add, add_assoc]
121. 0121have hnext_j_base : (b + 6 * S k) + 7 = (b + 6 * k) + 13
122. 0122rewrite hroot_step
123. 0123simp [add_assoc]
124. 0124have hnext_j_exponent : (b + 6 * S k) + 5 = (b + 6 * k) + 11
125. 0125rewrite hroot_step
126. 0126simp [add_assoc]
127. 0127have hnext_ceiling : ((exists bcs_lower_gap_hjas_transport_next_ceiling. bcs_lower_gap_hjas_transport_next_ceiling + (((b + 6 * k) + 6) * ((b + 6 * k) + 6)) = 6 * (e)) /\ exists bcs_upper_gap_hjas_transport_next_ceiling. bcs_upper_gap_hjas_transport_next_ceiling + S (6 * (e)) = (((b + 6 * k) + 6) * ((b + 6 * k) + 6)) + 6)
128. 0128rewrite <- hroot_step
129. 0129rewrite <- hroot_step
130. 0130rewrite <- hroot_step
131. 0131rewrite <- hroot_step
132. 0132exact hceiling
133. 0133have hnext_h : exists pa_b_hjas_transport_next_h pa_c_hjas_transport_next_h. ((forall pa_i_hjas_transport_next_h_repeat. (exists pa_lt_hjas_transport_next_h_repeat_bound. pa_lt_hjas_transport_next_h_repeat_bound + S pa_i_hjas_transport_next_h_repeat = 2 * (b + 6 * k) + 14) -> (((exists pa_h_hjas_transport_next_h_repeat_decoded. pa_h_hjas_transport_next_h_repeat_decoded + S ((b + 6 * k) + 7) = S ((S (pa_i_hjas_transport_next_h_repeat)) * pa_c_hjas_transport_next_h)) /\ exists pa_q_hjas_transport_next_h_repeat_decoded. pa_b_hjas_transport_next_h = pa_q_hjas_transport_next_h_repeat_decoded * S ((S (pa_i_hjas_transport_next_h_repeat)) * pa_c_hjas_transport_next_h) + ((b + 6 * k) + 7)))) /\ (exists pa_u_hjas_transport_next_h_product pa_v_hjas_transport_next_h_product. ((((exists pa_h_hjas_transport_next_h_product_start. pa_h_hjas_transport_next_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_start. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_start * S ((S (0)) * pa_v_hjas_transport_next_h_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_h_product_terminal. pa_h_hjas_transport_next_h_product_terminal + S (h) = S ((S (2 * (b + 6 * k) + 14)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_terminal. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_terminal * S ((S (2 * (b + 6 * k) + 14)) * pa_v_hjas_transport_next_h_product) + (h))) /\ forall pa_i_hjas_transport_next_h_product. (exists pa_lt_hjas_transport_next_h_product_bound. pa_lt_hjas_transport_next_h_product_bound + S pa_i_hjas_transport_next_h_product = 2 * (b + 6 * k) + 14) -> exists pa_p_hjas_transport_next_h_product pa_r_hjas_transport_next_h_product pa_s_hjas_transport_next_h_product. ((((exists pa_h_hjas_transport_next_h_product_factor. pa_h_hjas_transport_next_h_product_factor + S (pa_p_hjas_transport_next_h_product) = S ((S (pa_i_hjas_transport_next_h_product)) * pa_c_hjas_transport_next_h)) /\ exists pa_q_hjas_transport_next_h_product_factor. pa_b_hjas_transport_next_h = pa_q_hjas_transport_next_h_product_factor * S ((S (pa_i_hjas_transport_next_h_product)) * pa_c_hjas_transport_next_h) + (pa_p_hjas_transport_next_h_product))) /\ ((((exists pa_h_hjas_transport_next_h_product_partial. pa_h_hjas_transport_next_h_product_partial + S (pa_r_hjas_transport_next_h_product) = S ((S (pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_partial. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_partial * S ((S (pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product) + (pa_r_hjas_transport_next_h_product))) /\ ((((exists pa_h_hjas_transport_next_h_product_successor. pa_h_hjas_transport_next_h_product_successor + S (pa_s_hjas_transport_next_h_product) = S ((S (S pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product)) /\ exists pa_q_hjas_transport_next_h_product_successor. pa_u_hjas_transport_next_h_product = pa_q_hjas_transport_next_h_product_successor * S ((S (S pa_i_hjas_transport_next_h_product)) * pa_v_hjas_transport_next_h_product) + (pa_s_hjas_transport_next_h_product))) /\ pa_s_hjas_transport_next_h_product = pa_r_hjas_transport_next_h_product * pa_p_hjas_transport_next_h_product)))))))
134. 0134rewrite <- hnext_h_base
135. 0135rewrite <- hnext_h_base
136. 0136rewrite <- hnext_h_exponent
137. 0137rewrite <- hnext_h_exponent
138. 0138rewrite <- hnext_h_exponent
139. 0139rewrite <- hnext_h_exponent
140. 0140exact hh
141. 0141have hnext_j : exists pa_b_hjas_transport_next_j pa_c_hjas_transport_next_j. ((forall pa_i_hjas_transport_next_j_repeat. (exists pa_lt_hjas_transport_next_j_repeat_bound. pa_lt_hjas_transport_next_j_repeat_bound + S pa_i_hjas_transport_next_j_repeat = 12) -> (((exists pa_h_hjas_transport_next_j_repeat_decoded. pa_h_hjas_transport_next_j_repeat_decoded + S ((b + 6 * k) + 13) = S ((S (pa_i_hjas_transport_next_j_repeat)) * pa_c_hjas_transport_next_j)) /\ exists pa_q_hjas_transport_next_j_repeat_decoded. pa_b_hjas_transport_next_j = pa_q_hjas_transport_next_j_repeat_decoded * S ((S (pa_i_hjas_transport_next_j_repeat)) * pa_c_hjas_transport_next_j) + ((b + 6 * k) + 13)))) /\ (exists pa_u_hjas_transport_next_j_product pa_v_hjas_transport_next_j_product. ((((exists pa_h_hjas_transport_next_j_product_start. pa_h_hjas_transport_next_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_start. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_start * S ((S (0)) * pa_v_hjas_transport_next_j_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_j_product_terminal. pa_h_hjas_transport_next_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_terminal. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_terminal * S ((S (12)) * pa_v_hjas_transport_next_j_product) + (j))) /\ forall pa_i_hjas_transport_next_j_product. (exists pa_lt_hjas_transport_next_j_product_bound. pa_lt_hjas_transport_next_j_product_bound + S pa_i_hjas_transport_next_j_product = 12) -> exists pa_p_hjas_transport_next_j_product pa_r_hjas_transport_next_j_product pa_s_hjas_transport_next_j_product. ((((exists pa_h_hjas_transport_next_j_product_factor. pa_h_hjas_transport_next_j_product_factor + S (pa_p_hjas_transport_next_j_product) = S ((S (pa_i_hjas_transport_next_j_product)) * pa_c_hjas_transport_next_j)) /\ exists pa_q_hjas_transport_next_j_product_factor. pa_b_hjas_transport_next_j = pa_q_hjas_transport_next_j_product_factor * S ((S (pa_i_hjas_transport_next_j_product)) * pa_c_hjas_transport_next_j) + (pa_p_hjas_transport_next_j_product))) /\ ((((exists pa_h_hjas_transport_next_j_product_partial. pa_h_hjas_transport_next_j_product_partial + S (pa_r_hjas_transport_next_j_product) = S ((S (pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_partial. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_partial * S ((S (pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product) + (pa_r_hjas_transport_next_j_product))) /\ ((((exists pa_h_hjas_transport_next_j_product_successor. pa_h_hjas_transport_next_j_product_successor + S (pa_s_hjas_transport_next_j_product) = S ((S (S pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product)) /\ exists pa_q_hjas_transport_next_j_product_successor. pa_u_hjas_transport_next_j_product = pa_q_hjas_transport_next_j_product_successor * S ((S (S pa_i_hjas_transport_next_j_product)) * pa_v_hjas_transport_next_j_product) + (pa_s_hjas_transport_next_j_product))) /\ pa_s_hjas_transport_next_j_product = pa_r_hjas_transport_next_j_product * pa_p_hjas_transport_next_j_product)))))))
142. 0142rewrite <- hnext_j_base
143. 0143rewrite <- hnext_j_base
144. 0144exact hj
145. 0145have hnext_g : exists pa_b_hjas_transport_next_g pa_c_hjas_transport_next_g. ((forall pa_i_hjas_transport_next_g_repeat. (exists pa_lt_hjas_transport_next_g_repeat_bound. pa_lt_hjas_transport_next_g_repeat_bound + S pa_i_hjas_transport_next_g_repeat = (b + 6 * k) + 11) -> (((exists pa_h_hjas_transport_next_g_repeat_decoded. pa_h_hjas_transport_next_g_repeat_decoded + S (4) = S ((S (pa_i_hjas_transport_next_g_repeat)) * pa_c_hjas_transport_next_g)) /\ exists pa_q_hjas_transport_next_g_repeat_decoded. pa_b_hjas_transport_next_g = pa_q_hjas_transport_next_g_repeat_decoded * S ((S (pa_i_hjas_transport_next_g_repeat)) * pa_c_hjas_transport_next_g) + (4)))) /\ (exists pa_u_hjas_transport_next_g_product pa_v_hjas_transport_next_g_product. ((((exists pa_h_hjas_transport_next_g_product_start. pa_h_hjas_transport_next_g_product_start + S (1) = S ((S (0)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_start. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_start * S ((S (0)) * pa_v_hjas_transport_next_g_product) + (1))) /\ ((((exists pa_h_hjas_transport_next_g_product_terminal. pa_h_hjas_transport_next_g_product_terminal + S (g) = S ((S ((b + 6 * k) + 11)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_terminal. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_terminal * S ((S ((b + 6 * k) + 11)) * pa_v_hjas_transport_next_g_product) + (g))) /\ forall pa_i_hjas_transport_next_g_product. (exists pa_lt_hjas_transport_next_g_product_bound. pa_lt_hjas_transport_next_g_product_bound + S pa_i_hjas_transport_next_g_product = (b + 6 * k) + 11) -> exists pa_p_hjas_transport_next_g_product pa_r_hjas_transport_next_g_product pa_s_hjas_transport_next_g_product. ((((exists pa_h_hjas_transport_next_g_product_factor. pa_h_hjas_transport_next_g_product_factor + S (pa_p_hjas_transport_next_g_product) = S ((S (pa_i_hjas_transport_next_g_product)) * pa_c_hjas_transport_next_g)) /\ exists pa_q_hjas_transport_next_g_product_factor. pa_b_hjas_transport_next_g = pa_q_hjas_transport_next_g_product_factor * S ((S (pa_i_hjas_transport_next_g_product)) * pa_c_hjas_transport_next_g) + (pa_p_hjas_transport_next_g_product))) /\ ((((exists pa_h_hjas_transport_next_g_product_partial. pa_h_hjas_transport_next_g_product_partial + S (pa_r_hjas_transport_next_g_product) = S ((S (pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_partial. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_partial * S ((S (pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product) + (pa_r_hjas_transport_next_g_product))) /\ ((((exists pa_h_hjas_transport_next_g_product_successor. pa_h_hjas_transport_next_g_product_successor + S (pa_s_hjas_transport_next_g_product) = S ((S (S pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product)) /\ exists pa_q_hjas_transport_next_g_product_successor. pa_u_hjas_transport_next_g_product = pa_q_hjas_transport_next_g_product_successor * S ((S (S pa_i_hjas_transport_next_g_product)) * pa_v_hjas_transport_next_g_product) + (pa_s_hjas_transport_next_g_product))) /\ pa_s_hjas_transport_next_g_product = pa_r_hjas_transport_next_g_product * pa_p_hjas_transport_next_g_product)))))))
146. 0146rewrite <- hnext_j_exponent
147. 0147rewrite <- hnext_j_exponent
148. 0148rewrite <- hnext_j_exponent
149. 0149rewrite <- hnext_j_exponent
150. 0150exact hg
151. 0151specialize bertrand_hj_six_step_from_total (b + 6 * k)
152. 0152specialize bertrand_hj_six_step_from_total x
153. 0153specialize bertrand_hj_six_step_from_total e
154. 0154specialize bertrand_hj_six_step_from_total x1
155. 0155specialize bertrand_hj_six_step_from_total x2
156. 0156specialize bertrand_hj_six_step_from_total x3
157. 0157specialize bertrand_hj_six_step_from_total x4
158. 0158specialize bertrand_hj_six_step_from_total h
159. 0159specialize bertrand_hj_six_step_from_total u
160. 0160specialize bertrand_hj_six_step_from_total j
161. 0161specialize bertrand_hj_six_step_from_total g
162. 0162apply bertrand_hj_six_step_from_total
163. 0163exact htotal
164. 0164exact hfive_current
165. 0165exact hcurrent_ceiling_witness
166. 0166exact hnext_ceiling
167. 0167exact hcurrent_h_witness
168. 0168exact hcurrent_u_witness
169. 0169exact hcurrent_j_witness
170. 0170exact hcurrent_g_witness
171. 0171split
172. 0172exact hcurrent_bounds_left
173. 0173exact hcurrent_bounds_right
174. 0174exact hnext_h
175. 0175exact hu
176. 0176exact hnext_j
177. 0177exact hnext_g