bertrand_h_root_33_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 e
2. 0002intro h
3. 0003intro u
4. 0004intro htotal
5. 0005intro hceiling
6. 0006intro hh
7. 0007intro hu
8. 0008have hh_route : exists pa_b_hj32_h_33_route pa_c_hj32_h_33_route. ((forall pa_i_hj32_h_33_route_repeat. (exists pa_lt_hj32_h_33_route_repeat_bound. pa_lt_hj32_h_33_route_repeat_bound + S pa_i_hj32_h_33_route_repeat = 2 * 34) -> (((exists pa_h_hj32_h_33_route_repeat_decoded. pa_h_hj32_h_33_route_repeat_decoded + S (34) = S ((S (pa_i_hj32_h_33_route_repeat)) * pa_c_hj32_h_33_route)) /\ exists pa_q_hj32_h_33_route_repeat_decoded. pa_b_hj32_h_33_route = pa_q_hj32_h_33_route_repeat_decoded * S ((S (pa_i_hj32_h_33_route_repeat)) * pa_c_hj32_h_33_route) + (34)))) /\ (exists pa_u_hj32_h_33_route_product pa_v_hj32_h_33_route_product. ((((exists pa_h_hj32_h_33_route_product_start. pa_h_hj32_h_33_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_start. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_start * S ((S (0)) * pa_v_hj32_h_33_route_product) + (1))) /\ ((((exists pa_h_hj32_h_33_route_product_terminal. pa_h_hj32_h_33_route_product_terminal + S (h) = S ((S (2 * 34)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_terminal. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_terminal * S ((S (2 * 34)) * pa_v_hj32_h_33_route_product) + (h))) /\ forall pa_i_hj32_h_33_route_product. (exists pa_lt_hj32_h_33_route_product_bound. pa_lt_hj32_h_33_route_product_bound + S pa_i_hj32_h_33_route_product = 2 * 34) -> exists pa_p_hj32_h_33_route_product pa_r_hj32_h_33_route_product pa_s_hj32_h_33_route_product. ((((exists pa_h_hj32_h_33_route_product_factor. pa_h_hj32_h_33_route_product_factor + S (pa_p_hj32_h_33_route_product) = S ((S (pa_i_hj32_h_33_route_product)) * pa_c_hj32_h_33_route)) /\ exists pa_q_hj32_h_33_route_product_factor. pa_b_hj32_h_33_route = pa_q_hj32_h_33_route_product_factor * S ((S (pa_i_hj32_h_33_route_product)) * pa_c_hj32_h_33_route) + (pa_p_hj32_h_33_route_product))) /\ ((((exists pa_h_hj32_h_33_route_product_partial. pa_h_hj32_h_33_route_product_partial + S (pa_r_hj32_h_33_route_product) = S ((S (pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_partial. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_partial * S ((S (pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product) + (pa_r_hj32_h_33_route_product))) /\ ((((exists pa_h_hj32_h_33_route_product_successor. pa_h_hj32_h_33_route_product_successor + S (pa_s_hj32_h_33_route_product) = S ((S (S pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product)) /\ exists pa_q_hj32_h_33_route_product_successor. pa_u_hj32_h_33_route_product = pa_q_hj32_h_33_route_product_successor * S ((S (S pa_i_hj32_h_33_route_product)) * pa_v_hj32_h_33_route_product) + (pa_s_hj32_h_33_route_product))) /\ pa_s_hj32_h_33_route_product = pa_r_hj32_h_33_route_product * pa_p_hj32_h_33_route_product)))))))
9. 0009have hh_base : 33 + 1 = 34
10. 0010norm_num
11. 0011have hh_exponent : 2 * 33 + 2 = 2 * 34
12. 0012norm_num
13. 0013rewrite <- hh_exponent
14. 0014rewrite <- hh_exponent
15. 0015rewrite <- hh_exponent
16. 0016rewrite <- hh_exponent
17. 0017rewrite <- hh_base
18. 0018rewrite <- hh_base
19. 0019exact hh
20. 0020have h33s_p36 : exists hj32_local_value_h33s_p36. (exists pa_b_hj32_local_total_h33s_p36 pa_c_hj32_local_total_h33s_p36. ((forall pa_i_hj32_local_total_h33s_p36_repeat. (exists pa_lt_hj32_local_total_h33s_p36_repeat_bound. pa_lt_hj32_local_total_h33s_p36_repeat_bound + S pa_i_hj32_local_total_h33s_p36_repeat = 2 * 34) -> (((exists pa_h_hj32_local_total_h33s_p36_repeat_decoded. pa_h_hj32_local_total_h33s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h33s_p36_repeat)) * pa_c_hj32_local_total_h33s_p36)) /\ exists pa_q_hj32_local_total_h33s_p36_repeat_decoded. pa_b_hj32_local_total_h33s_p36 = pa_q_hj32_local_total_h33s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p36_repeat)) * pa_c_hj32_local_total_h33s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h33s_p36_product pa_v_hj32_local_total_h33s_p36_product. ((((exists pa_h_hj32_local_total_h33s_p36_product_start. pa_h_hj32_local_total_h33s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_start. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_terminal. pa_h_hj32_local_total_h33s_p36_product_terminal + S (hj32_local_value_h33s_p36) = S ((S (2 * 34)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_terminal. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_terminal * S ((S (2 * 34)) * pa_v_hj32_local_total_h33s_p36_product) + (hj32_local_value_h33s_p36))) /\ forall pa_i_hj32_local_total_h33s_p36_product. (exists pa_lt_hj32_local_total_h33s_p36_product_bound. pa_lt_hj32_local_total_h33s_p36_product_bound + S pa_i_hj32_local_total_h33s_p36_product = 2 * 34) -> exists pa_p_hj32_local_total_h33s_p36_product pa_r_hj32_local_total_h33s_p36_product pa_s_hj32_local_total_h33s_p36_product. ((((exists pa_h_hj32_local_total_h33s_p36_product_factor. pa_h_hj32_local_total_h33s_p36_product_factor + S (pa_p_hj32_local_total_h33s_p36_product) = S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_c_hj32_local_total_h33s_p36)) /\ exists pa_q_hj32_local_total_h33s_p36_product_factor. pa_b_hj32_local_total_h33s_p36 = pa_q_hj32_local_total_h33s_p36_product_factor * S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_c_hj32_local_total_h33s_p36) + (pa_p_hj32_local_total_h33s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_partial. pa_h_hj32_local_total_h33s_p36_product_partial + S (pa_r_hj32_local_total_h33s_p36_product) = S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_partial. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_partial * S ((S (pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product) + (pa_r_hj32_local_total_h33s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p36_product_successor. pa_h_hj32_local_total_h33s_p36_product_successor + S (pa_s_hj32_local_total_h33s_p36_product) = S ((S (S pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product)) /\ exists pa_q_hj32_local_total_h33s_p36_product_successor. pa_u_hj32_local_total_h33s_p36_product = pa_q_hj32_local_total_h33s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p36_product)) * pa_v_hj32_local_total_h33s_p36_product) + (pa_s_hj32_local_total_h33s_p36_product))) /\ pa_s_hj32_local_total_h33s_p36_product = pa_r_hj32_local_total_h33s_p36_product * pa_p_hj32_local_total_h33s_p36_product))))))))
21. 0021specialize htotal 36
22. 0022specialize htotal 2 * 34
23. 0023exact htotal
24. 0024cases h33s_p36
25. 0025have h33s_base : exists bqb_le_gap_hj32_h33s_base. bqb_le_gap_hj32_h33s_base + (34) = (36)
26. 0026exists 2
27. 0027norm_num
28. 0028have h33s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h33s_to_36. bqb_le_gap_hj32_local_base_bound_h33s_to_36 + (h) = (x)
29. 0029specialize pow_base_monotone 34
30. 0030specialize pow_base_monotone 36
31. 0031specialize pow_base_monotone 2 * 34
32. 0032specialize pow_base_monotone h
33. 0033specialize pow_base_monotone x
34. 0034apply pow_base_monotone
35. 0035exact h33s_base
36. 0036exact hh_route
37. 0037exact h33s_p36_witness
38. 0038have h33s_p6_total : exists hj32_local_value_h33s_p6_total. (exists pa_b_hj32_local_total_h33s_p6_total pa_c_hj32_local_total_h33s_p6_total. ((forall pa_i_hj32_local_total_h33s_p6_total_repeat. (exists pa_lt_hj32_local_total_h33s_p6_total_repeat_bound. pa_lt_hj32_local_total_h33s_p6_total_repeat_bound + S pa_i_hj32_local_total_h33s_p6_total_repeat = 4 * 34) -> (((exists pa_h_hj32_local_total_h33s_p6_total_repeat_decoded. pa_h_hj32_local_total_h33s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_total_repeat)) * pa_c_hj32_local_total_h33s_p6_total)) /\ exists pa_q_hj32_local_total_h33s_p6_total_repeat_decoded. pa_b_hj32_local_total_h33s_p6_total = pa_q_hj32_local_total_h33s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_total_repeat)) * pa_c_hj32_local_total_h33s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_total_product pa_v_hj32_local_total_h33s_p6_total_product. ((((exists pa_h_hj32_local_total_h33s_p6_total_product_start. pa_h_hj32_local_total_h33s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_start. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_terminal. pa_h_hj32_local_total_h33s_p6_total_product_terminal + S (hj32_local_value_h33s_p6_total) = S ((S (4 * 34)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_terminal. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_terminal * S ((S (4 * 34)) * pa_v_hj32_local_total_h33s_p6_total_product) + (hj32_local_value_h33s_p6_total))) /\ forall pa_i_hj32_local_total_h33s_p6_total_product. (exists pa_lt_hj32_local_total_h33s_p6_total_product_bound. pa_lt_hj32_local_total_h33s_p6_total_product_bound + S pa_i_hj32_local_total_h33s_p6_total_product = 4 * 34) -> exists pa_p_hj32_local_total_h33s_p6_total_product pa_r_hj32_local_total_h33s_p6_total_product pa_s_hj32_local_total_h33s_p6_total_product. ((((exists pa_h_hj32_local_total_h33s_p6_total_product_factor. pa_h_hj32_local_total_h33s_p6_total_product_factor + S (pa_p_hj32_local_total_h33s_p6_total_product) = S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_c_hj32_local_total_h33s_p6_total)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_factor. pa_b_hj32_local_total_h33s_p6_total = pa_q_hj32_local_total_h33s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_c_hj32_local_total_h33s_p6_total) + (pa_p_hj32_local_total_h33s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_partial. pa_h_hj32_local_total_h33s_p6_total_product_partial + S (pa_r_hj32_local_total_h33s_p6_total_product) = S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_partial. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product) + (pa_r_hj32_local_total_h33s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_total_product_successor. pa_h_hj32_local_total_h33s_p6_total_product_successor + S (pa_s_hj32_local_total_h33s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product)) /\ exists pa_q_hj32_local_total_h33s_p6_total_product_successor. pa_u_hj32_local_total_h33s_p6_total_product = pa_q_hj32_local_total_h33s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_total_product)) * pa_v_hj32_local_total_h33s_p6_total_product) + (pa_s_hj32_local_total_h33s_p6_total_product))) /\ pa_s_hj32_local_total_h33s_p6_total_product = pa_r_hj32_local_total_h33s_p6_total_product * pa_p_hj32_local_total_h33s_p6_total_product))))))))
39. 0039specialize htotal 6
40. 0040specialize htotal 4 * 34
41. 0041exact htotal
42. 0042cases h33s_p6_total
43. 0043have h33s_conversion : x = x1
44. 0044specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 34
45. 0045specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x
46. 0046specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1
47. 0047apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total
48. 0048exact htotal
49. 0049exact h33s_p36_witness
50. 0050exact h33s_p6_total_witness
51. 0051rewrite h33s_conversion at h33s_to_36
52. 0052have h33s_p6_main : exists hj32_local_value_h33s_p6_main. (exists pa_b_hj32_local_total_h33s_p6_main pa_c_hj32_local_total_h33s_p6_main. ((forall pa_i_hj32_local_total_h33s_p6_main_repeat. (exists pa_lt_hj32_local_total_h33s_p6_main_repeat_bound. pa_lt_hj32_local_total_h33s_p6_main_repeat_bound + S pa_i_hj32_local_total_h33s_p6_main_repeat = 10 * 13) -> (((exists pa_h_hj32_local_total_h33s_p6_main_repeat_decoded. pa_h_hj32_local_total_h33s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_main_repeat)) * pa_c_hj32_local_total_h33s_p6_main)) /\ exists pa_q_hj32_local_total_h33s_p6_main_repeat_decoded. pa_b_hj32_local_total_h33s_p6_main = pa_q_hj32_local_total_h33s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_main_repeat)) * pa_c_hj32_local_total_h33s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_main_product pa_v_hj32_local_total_h33s_p6_main_product. ((((exists pa_h_hj32_local_total_h33s_p6_main_product_start. pa_h_hj32_local_total_h33s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_start. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_terminal. pa_h_hj32_local_total_h33s_p6_main_product_terminal + S (hj32_local_value_h33s_p6_main) = S ((S (10 * 13)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_terminal. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_terminal * S ((S (10 * 13)) * pa_v_hj32_local_total_h33s_p6_main_product) + (hj32_local_value_h33s_p6_main))) /\ forall pa_i_hj32_local_total_h33s_p6_main_product. (exists pa_lt_hj32_local_total_h33s_p6_main_product_bound. pa_lt_hj32_local_total_h33s_p6_main_product_bound + S pa_i_hj32_local_total_h33s_p6_main_product = 10 * 13) -> exists pa_p_hj32_local_total_h33s_p6_main_product pa_r_hj32_local_total_h33s_p6_main_product pa_s_hj32_local_total_h33s_p6_main_product. ((((exists pa_h_hj32_local_total_h33s_p6_main_product_factor. pa_h_hj32_local_total_h33s_p6_main_product_factor + S (pa_p_hj32_local_total_h33s_p6_main_product) = S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_c_hj32_local_total_h33s_p6_main)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_factor. pa_b_hj32_local_total_h33s_p6_main = pa_q_hj32_local_total_h33s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_c_hj32_local_total_h33s_p6_main) + (pa_p_hj32_local_total_h33s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_partial. pa_h_hj32_local_total_h33s_p6_main_product_partial + S (pa_r_hj32_local_total_h33s_p6_main_product) = S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_partial. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product) + (pa_r_hj32_local_total_h33s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_main_product_successor. pa_h_hj32_local_total_h33s_p6_main_product_successor + S (pa_s_hj32_local_total_h33s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product)) /\ exists pa_q_hj32_local_total_h33s_p6_main_product_successor. pa_u_hj32_local_total_h33s_p6_main_product = pa_q_hj32_local_total_h33s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_main_product)) * pa_v_hj32_local_total_h33s_p6_main_product) + (pa_s_hj32_local_total_h33s_p6_main_product))) /\ pa_s_hj32_local_total_h33s_p6_main_product = pa_r_hj32_local_total_h33s_p6_main_product * pa_p_hj32_local_total_h33s_p6_main_product))))))))
53. 0053specialize htotal 6
54. 0054specialize htotal 10 * 13
55. 0055exact htotal
56. 0056cases h33s_p6_main
57. 0057have h33s_p4_main : exists hj32_local_value_h33s_p4_main. (exists pa_b_hj32_local_total_h33s_p4_main pa_c_hj32_local_total_h33s_p4_main. ((forall pa_i_hj32_local_total_h33s_p4_main_repeat. (exists pa_lt_hj32_local_total_h33s_p4_main_repeat_bound. pa_lt_hj32_local_total_h33s_p4_main_repeat_bound + S pa_i_hj32_local_total_h33s_p4_main_repeat = 13 * 13) -> (((exists pa_h_hj32_local_total_h33s_p4_main_repeat_decoded. pa_h_hj32_local_total_h33s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_main_repeat)) * pa_c_hj32_local_total_h33s_p4_main)) /\ exists pa_q_hj32_local_total_h33s_p4_main_repeat_decoded. pa_b_hj32_local_total_h33s_p4_main = pa_q_hj32_local_total_h33s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_main_repeat)) * pa_c_hj32_local_total_h33s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_main_product pa_v_hj32_local_total_h33s_p4_main_product. ((((exists pa_h_hj32_local_total_h33s_p4_main_product_start. pa_h_hj32_local_total_h33s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_start. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_terminal. pa_h_hj32_local_total_h33s_p4_main_product_terminal + S (hj32_local_value_h33s_p4_main) = S ((S (13 * 13)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_terminal. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_terminal * S ((S (13 * 13)) * pa_v_hj32_local_total_h33s_p4_main_product) + (hj32_local_value_h33s_p4_main))) /\ forall pa_i_hj32_local_total_h33s_p4_main_product. (exists pa_lt_hj32_local_total_h33s_p4_main_product_bound. pa_lt_hj32_local_total_h33s_p4_main_product_bound + S pa_i_hj32_local_total_h33s_p4_main_product = 13 * 13) -> exists pa_p_hj32_local_total_h33s_p4_main_product pa_r_hj32_local_total_h33s_p4_main_product pa_s_hj32_local_total_h33s_p4_main_product. ((((exists pa_h_hj32_local_total_h33s_p4_main_product_factor. pa_h_hj32_local_total_h33s_p4_main_product_factor + S (pa_p_hj32_local_total_h33s_p4_main_product) = S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_c_hj32_local_total_h33s_p4_main)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_factor. pa_b_hj32_local_total_h33s_p4_main = pa_q_hj32_local_total_h33s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_c_hj32_local_total_h33s_p4_main) + (pa_p_hj32_local_total_h33s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_partial. pa_h_hj32_local_total_h33s_p4_main_product_partial + S (pa_r_hj32_local_total_h33s_p4_main_product) = S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_partial. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product) + (pa_r_hj32_local_total_h33s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_main_product_successor. pa_h_hj32_local_total_h33s_p4_main_product_successor + S (pa_s_hj32_local_total_h33s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product)) /\ exists pa_q_hj32_local_total_h33s_p4_main_product_successor. pa_u_hj32_local_total_h33s_p4_main_product = pa_q_hj32_local_total_h33s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_main_product)) * pa_v_hj32_local_total_h33s_p4_main_product) + (pa_s_hj32_local_total_h33s_p4_main_product))) /\ pa_s_hj32_local_total_h33s_p4_main_product = pa_r_hj32_local_total_h33s_p4_main_product * pa_p_hj32_local_total_h33s_p4_main_product))))))))
58. 0058specialize htotal 4
59. 0059specialize htotal 13 * 13
60. 0060exact htotal
61. 0061cases h33s_p4_main
62. 0062have h33s_main_bound : exists bqb_le_gap_hj32_h33s_main_bound. bqb_le_gap_hj32_h33s_main_bound + (x2) = (x3)
63. 0063specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 13
64. 0064specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2
65. 0065specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3
66. 0066apply pow_six_ten_block_le_pow_four_thirteen_block_from_total
67. 0067exact htotal
68. 0068exact h33s_p6_main_witness
69. 0069exact h33s_p4_main_witness
70. 0070have h33s_p6_residual : exists hj32_local_value_h33s_p6_residual. (exists pa_b_hj32_local_total_h33s_p6_residual pa_c_hj32_local_total_h33s_p6_residual. ((forall pa_i_hj32_local_total_h33s_p6_residual_repeat. (exists pa_lt_hj32_local_total_h33s_p6_residual_repeat_bound. pa_lt_hj32_local_total_h33s_p6_residual_repeat_bound + S pa_i_hj32_local_total_h33s_p6_residual_repeat = 6) -> (((exists pa_h_hj32_local_total_h33s_p6_residual_repeat_decoded. pa_h_hj32_local_total_h33s_p6_residual_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_repeat)) * pa_c_hj32_local_total_h33s_p6_residual)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_repeat_decoded. pa_b_hj32_local_total_h33s_p6_residual = pa_q_hj32_local_total_h33s_p6_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p6_residual_repeat)) * pa_c_hj32_local_total_h33s_p6_residual) + (6)))) /\ (exists pa_u_hj32_local_total_h33s_p6_residual_product pa_v_hj32_local_total_h33s_p6_residual_product. ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_start. pa_h_hj32_local_total_h33s_p6_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_start. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_terminal. pa_h_hj32_local_total_h33s_p6_residual_product_terminal + S (hj32_local_value_h33s_p6_residual) = S ((S (6)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_terminal. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_terminal * S ((S (6)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (hj32_local_value_h33s_p6_residual))) /\ forall pa_i_hj32_local_total_h33s_p6_residual_product. (exists pa_lt_hj32_local_total_h33s_p6_residual_product_bound. pa_lt_hj32_local_total_h33s_p6_residual_product_bound + S pa_i_hj32_local_total_h33s_p6_residual_product = 6) -> exists pa_p_hj32_local_total_h33s_p6_residual_product pa_r_hj32_local_total_h33s_p6_residual_product pa_s_hj32_local_total_h33s_p6_residual_product. ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_factor. pa_h_hj32_local_total_h33s_p6_residual_product_factor + S (pa_p_hj32_local_total_h33s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_c_hj32_local_total_h33s_p6_residual)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_factor. pa_b_hj32_local_total_h33s_p6_residual = pa_q_hj32_local_total_h33s_p6_residual_product_factor * S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_c_hj32_local_total_h33s_p6_residual) + (pa_p_hj32_local_total_h33s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_partial. pa_h_hj32_local_total_h33s_p6_residual_product_partial + S (pa_r_hj32_local_total_h33s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_partial. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_partial * S ((S (pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (pa_r_hj32_local_total_h33s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p6_residual_product_successor. pa_h_hj32_local_total_h33s_p6_residual_product_successor + S (pa_s_hj32_local_total_h33s_p6_residual_product) = S ((S (S pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p6_residual_product_successor. pa_u_hj32_local_total_h33s_p6_residual_product = pa_q_hj32_local_total_h33s_p6_residual_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p6_residual_product)) * pa_v_hj32_local_total_h33s_p6_residual_product) + (pa_s_hj32_local_total_h33s_p6_residual_product))) /\ pa_s_hj32_local_total_h33s_p6_residual_product = pa_r_hj32_local_total_h33s_p6_residual_product * pa_p_hj32_local_total_h33s_p6_residual_product))))))))
71. 0071specialize htotal 6
72. 0072specialize htotal 6
73. 0073exact htotal
74. 0074cases h33s_p6_residual
75. 0075have h33s_p4_residual : exists hj32_local_value_h33s_p4_residual. (exists pa_b_hj32_local_total_h33s_p4_residual pa_c_hj32_local_total_h33s_p4_residual. ((forall pa_i_hj32_local_total_h33s_p4_residual_repeat. (exists pa_lt_hj32_local_total_h33s_p4_residual_repeat_bound. pa_lt_hj32_local_total_h33s_p4_residual_repeat_bound + S pa_i_hj32_local_total_h33s_p4_residual_repeat = 8) -> (((exists pa_h_hj32_local_total_h33s_p4_residual_repeat_decoded. pa_h_hj32_local_total_h33s_p4_residual_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_repeat)) * pa_c_hj32_local_total_h33s_p4_residual)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_repeat_decoded. pa_b_hj32_local_total_h33s_p4_residual = pa_q_hj32_local_total_h33s_p4_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_residual_repeat)) * pa_c_hj32_local_total_h33s_p4_residual) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_residual_product pa_v_hj32_local_total_h33s_p4_residual_product. ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_start. pa_h_hj32_local_total_h33s_p4_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_start. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_terminal. pa_h_hj32_local_total_h33s_p4_residual_product_terminal + S (hj32_local_value_h33s_p4_residual) = S ((S (8)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_terminal. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_terminal * S ((S (8)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (hj32_local_value_h33s_p4_residual))) /\ forall pa_i_hj32_local_total_h33s_p4_residual_product. (exists pa_lt_hj32_local_total_h33s_p4_residual_product_bound. pa_lt_hj32_local_total_h33s_p4_residual_product_bound + S pa_i_hj32_local_total_h33s_p4_residual_product = 8) -> exists pa_p_hj32_local_total_h33s_p4_residual_product pa_r_hj32_local_total_h33s_p4_residual_product pa_s_hj32_local_total_h33s_p4_residual_product. ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_factor. pa_h_hj32_local_total_h33s_p4_residual_product_factor + S (pa_p_hj32_local_total_h33s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_c_hj32_local_total_h33s_p4_residual)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_factor. pa_b_hj32_local_total_h33s_p4_residual = pa_q_hj32_local_total_h33s_p4_residual_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_c_hj32_local_total_h33s_p4_residual) + (pa_p_hj32_local_total_h33s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_partial. pa_h_hj32_local_total_h33s_p4_residual_product_partial + S (pa_r_hj32_local_total_h33s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_partial. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (pa_r_hj32_local_total_h33s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_residual_product_successor. pa_h_hj32_local_total_h33s_p4_residual_product_successor + S (pa_s_hj32_local_total_h33s_p4_residual_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h33s_p4_residual_product_successor. pa_u_hj32_local_total_h33s_p4_residual_product = pa_q_hj32_local_total_h33s_p4_residual_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_residual_product)) * pa_v_hj32_local_total_h33s_p4_residual_product) + (pa_s_hj32_local_total_h33s_p4_residual_product))) /\ pa_s_hj32_local_total_h33s_p4_residual_product = pa_r_hj32_local_total_h33s_p4_residual_product * pa_p_hj32_local_total_h33s_p4_residual_product))))))))
76. 0076specialize htotal 4
77. 0077specialize htotal 8
78. 0078exact htotal
79. 0079cases h33s_p4_residual
80. 0080have h33s_residual_bound : exists bqb_le_gap_hj32_h33s_residual_bound. bqb_le_gap_hj32_h33s_residual_bound + (x4) = (x5)
81. 0081specialize pow_six_six_le_pow_four_eight_from_total x4
82. 0082specialize pow_six_six_le_pow_four_eight_from_total x5
83. 0083apply pow_six_six_le_pow_four_eight_from_total
84. 0084exact htotal
85. 0085exact h33s_p6_residual_witness
86. 0086exact h33s_p4_residual_witness
87. 0087have h33s_exponent : 4 * 34 = 10 * 13 + 6
88. 0088have h33s_thirty_four : 34 = 13 + 21
89. 0089norm_num
90. 0090rewrite h33s_thirty_four
91. 0091have h33s_distrib_one : 4 * (13 + 21) = 4 * 13 + 4 * 21
92. 0092specialize mul_add 4
93. 0093specialize mul_add 13
94. 0094specialize mul_add 21
95. 0095apply mul_add
96. 0096rewrite h33s_distrib_one
97. 0097have h33s_bridge : 4 * 21 = 6 * 14
98. 0098norm_num
99. 0099rewrite h33s_bridge
100. 0100have h33s_fourteen : 14 = 13 + 1
101. 0101norm_num
102. 0102rewrite h33s_fourteen
103. 0103have h33s_distrib_two : 6 * (13 + 1) = 6 * 13 + 6 * 1
104. 0104specialize mul_add 6
105. 0105specialize mul_add 13
106. 0106specialize mul_add 1
107. 0107apply mul_add
108. 0108rewrite h33s_distrib_two
109. 0109have h33s_six : 6 * 1 = 6
110. 0110norm_num
111. 0111rewrite h33s_six
112. 0112have h33s_assoc : 4 * 13 + (6 * 13 + 6) = (4 * 13 + 6 * 13) + 6
113. 0113symm
114. 0114specialize add_assoc (4 * 13)
115. 0115specialize add_assoc (6 * 13)
116. 0116specialize add_assoc 6
117. 0117apply add_assoc
118. 0118rewrite h33s_assoc
119. 0119have h33s_factor : (4 + 6) * 13 = 4 * 13 + 6 * 13
120. 0120specialize add_mul 4
121. 0121specialize add_mul 6
122. 0122specialize add_mul 13
123. 0123apply add_mul
124. 0124rewrite <- h33s_factor
125. 0125have h33s_ten : 4 + 6 = 10
126. 0126norm_num
127. 0127rewrite h33s_ten
128. 0128refl
129. 0129have h33s_left_product : x1 = x2 * x4
130. 0130specialize pow_add 6
131. 0131specialize pow_add 10 * 13
132. 0132specialize pow_add 6
133. 0133specialize pow_add 4 * 34
134. 0134specialize pow_add x2
135. 0135specialize pow_add x4
136. 0136specialize pow_add x1
137. 0137apply pow_add
138. 0138exact h33s_exponent
139. 0139exact h33s_p6_main_witness
140. 0140exact h33s_p6_residual_witness
141. 0141exact h33s_p6_total_witness
142. 0142have h33s_p4_budget : exists hj32_local_value_h33s_p4_budget. (exists pa_b_hj32_local_total_h33s_p4_budget pa_c_hj32_local_total_h33s_p4_budget. ((forall pa_i_hj32_local_total_h33s_p4_budget_repeat. (exists pa_lt_hj32_local_total_h33s_p4_budget_repeat_bound. pa_lt_hj32_local_total_h33s_p4_budget_repeat_bound + S pa_i_hj32_local_total_h33s_p4_budget_repeat = 13 * 13 + 8) -> (((exists pa_h_hj32_local_total_h33s_p4_budget_repeat_decoded. pa_h_hj32_local_total_h33s_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_repeat)) * pa_c_hj32_local_total_h33s_p4_budget)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_repeat_decoded. pa_b_hj32_local_total_h33s_p4_budget = pa_q_hj32_local_total_h33s_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h33s_p4_budget_repeat)) * pa_c_hj32_local_total_h33s_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h33s_p4_budget_product pa_v_hj32_local_total_h33s_p4_budget_product. ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_start. pa_h_hj32_local_total_h33s_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_start. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_terminal. pa_h_hj32_local_total_h33s_p4_budget_product_terminal + S (hj32_local_value_h33s_p4_budget) = S ((S (13 * 13 + 8)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_terminal. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_terminal * S ((S (13 * 13 + 8)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (hj32_local_value_h33s_p4_budget))) /\ forall pa_i_hj32_local_total_h33s_p4_budget_product. (exists pa_lt_hj32_local_total_h33s_p4_budget_product_bound. pa_lt_hj32_local_total_h33s_p4_budget_product_bound + S pa_i_hj32_local_total_h33s_p4_budget_product = 13 * 13 + 8) -> exists pa_p_hj32_local_total_h33s_p4_budget_product pa_r_hj32_local_total_h33s_p4_budget_product pa_s_hj32_local_total_h33s_p4_budget_product. ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_factor. pa_h_hj32_local_total_h33s_p4_budget_product_factor + S (pa_p_hj32_local_total_h33s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_c_hj32_local_total_h33s_p4_budget)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_factor. pa_b_hj32_local_total_h33s_p4_budget = pa_q_hj32_local_total_h33s_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_c_hj32_local_total_h33s_p4_budget) + (pa_p_hj32_local_total_h33s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_partial. pa_h_hj32_local_total_h33s_p4_budget_product_partial + S (pa_r_hj32_local_total_h33s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_partial. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (pa_r_hj32_local_total_h33s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h33s_p4_budget_product_successor. pa_h_hj32_local_total_h33s_p4_budget_product_successor + S (pa_s_hj32_local_total_h33s_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h33s_p4_budget_product_successor. pa_u_hj32_local_total_h33s_p4_budget_product = pa_q_hj32_local_total_h33s_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h33s_p4_budget_product)) * pa_v_hj32_local_total_h33s_p4_budget_product) + (pa_s_hj32_local_total_h33s_p4_budget_product))) /\ pa_s_hj32_local_total_h33s_p4_budget_product = pa_r_hj32_local_total_h33s_p4_budget_product * pa_p_hj32_local_total_h33s_p4_budget_product))))))))
143. 0143specialize htotal 4
144. 0144specialize htotal 13 * 13 + 8
145. 0145exact htotal
146. 0146cases h33s_p4_budget
147. 0147have h33s_right_product : x6 = x3 * x5
148. 0148specialize pow_add 4
149. 0149specialize pow_add 13 * 13
150. 0150specialize pow_add 8
151. 0151specialize pow_add 13 * 13 + 8
152. 0152specialize pow_add x3
153. 0153specialize pow_add x5
154. 0154specialize pow_add x6
155. 0155apply pow_add
156. 0156refl
157. 0157exact h33s_p4_main_witness
158. 0158exact h33s_p4_residual_witness
159. 0159exact h33s_p4_budget_witness
160. 0160have h33s_six_bound : exists bqb_le_gap_hj32_local_product_bound_h33s_six_bound. bqb_le_gap_hj32_local_product_bound_h33s_six_bound + (x2 * x4) = (x3 * x5)
161. 0161specialize mul_le_mul x2
162. 0162specialize mul_le_mul x3
163. 0163specialize mul_le_mul x4
164. 0164specialize mul_le_mul x5
165. 0165apply mul_le_mul
166. 0166exact h33s_main_bound
167. 0167exact h33s_residual_bound
168. 0168rewrite <- h33s_left_product at h33s_six_bound
169. 0169rewrite <- h33s_right_product at h33s_six_bound
170. 0170have h33s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h33s_to_budget. bqb_le_gap_hj32_local_trans_bound_h33s_to_budget + (h) = (x6)
171. 0171specialize le_trans h
172. 0172specialize le_trans x1
173. 0173specialize le_trans x6
174. 0174apply le_trans
175. 0175exact h33s_to_36
176. 0176exact h33s_six_bound
177. 0177have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_33. bqb_le_gap_hj32_scaled_budget_root_33 + (6 * (13 * 13 + 8)) = (33 * 33)
178. 0178apply bertrand_scaled_budget_root_33
179. 0179have hbudget_exponent : exists bqb_le_gap_hj32_h_33_budget_exponent. bqb_le_gap_hj32_h_33_budget_exponent + (13 * 13 + 8) = (e)
180. 0180specialize ceil_div_six_budget_of_scaled_le (33 * 33)
181. 0181specialize ceil_div_six_budget_of_scaled_le (13 * 13 + 8)
182. 0182specialize ceil_div_six_budget_of_scaled_le e
183. 0183apply ceil_div_six_budget_of_scaled_le
184. 0184exact hceiling
185. 0185exact hscaled
186. 0186have h33_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h33_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h33_budget_growth + (x6) = (u)
187. 0187specialize pow_exponent_monotone_from_total 4
188. 0188specialize pow_exponent_monotone_from_total 13 * 13 + 8
189. 0189specialize pow_exponent_monotone_from_total e
190. 0190specialize pow_exponent_monotone_from_total x6
191. 0191specialize pow_exponent_monotone_from_total u
192. 0192apply pow_exponent_monotone_from_total
193. 0193exact htotal
194. 0194exists 3
195. 0195norm_num
196. 0196exact hbudget_exponent
197. 0197exact h33s_p4_budget_witness
198. 0198exact hu
199. 0199have h33_result : exists bqb_le_gap_hj32_local_trans_bound_h33_result. bqb_le_gap_hj32_local_trans_bound_h33_result + (h) = (u)
200. 0200specialize le_trans h
201. 0201specialize le_trans x6
202. 0202specialize le_trans u
203. 0203apply le_trans
204. 0204exact h33s_to_budget
205. 0205exact h33_budget_growth
206. 0206exact h33_result