bertrand_h_root_35_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_35_route pa_c_hj32_h_35_route. ((forall pa_i_hj32_h_35_route_repeat. (exists pa_lt_hj32_h_35_route_repeat_bound. pa_lt_hj32_h_35_route_repeat_bound + S pa_i_hj32_h_35_route_repeat = 2 * 36) -> (((exists pa_h_hj32_h_35_route_repeat_decoded. pa_h_hj32_h_35_route_repeat_decoded + S (36) = S ((S (pa_i_hj32_h_35_route_repeat)) * pa_c_hj32_h_35_route)) /\ exists pa_q_hj32_h_35_route_repeat_decoded. pa_b_hj32_h_35_route = pa_q_hj32_h_35_route_repeat_decoded * S ((S (pa_i_hj32_h_35_route_repeat)) * pa_c_hj32_h_35_route) + (36)))) /\ (exists pa_u_hj32_h_35_route_product pa_v_hj32_h_35_route_product. ((((exists pa_h_hj32_h_35_route_product_start. pa_h_hj32_h_35_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_start. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_start * S ((S (0)) * pa_v_hj32_h_35_route_product) + (1))) /\ ((((exists pa_h_hj32_h_35_route_product_terminal. pa_h_hj32_h_35_route_product_terminal + S (h) = S ((S (2 * 36)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_terminal. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_terminal * S ((S (2 * 36)) * pa_v_hj32_h_35_route_product) + (h))) /\ forall pa_i_hj32_h_35_route_product. (exists pa_lt_hj32_h_35_route_product_bound. pa_lt_hj32_h_35_route_product_bound + S pa_i_hj32_h_35_route_product = 2 * 36) -> exists pa_p_hj32_h_35_route_product pa_r_hj32_h_35_route_product pa_s_hj32_h_35_route_product. ((((exists pa_h_hj32_h_35_route_product_factor. pa_h_hj32_h_35_route_product_factor + S (pa_p_hj32_h_35_route_product) = S ((S (pa_i_hj32_h_35_route_product)) * pa_c_hj32_h_35_route)) /\ exists pa_q_hj32_h_35_route_product_factor. pa_b_hj32_h_35_route = pa_q_hj32_h_35_route_product_factor * S ((S (pa_i_hj32_h_35_route_product)) * pa_c_hj32_h_35_route) + (pa_p_hj32_h_35_route_product))) /\ ((((exists pa_h_hj32_h_35_route_product_partial. pa_h_hj32_h_35_route_product_partial + S (pa_r_hj32_h_35_route_product) = S ((S (pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_partial. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_partial * S ((S (pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product) + (pa_r_hj32_h_35_route_product))) /\ ((((exists pa_h_hj32_h_35_route_product_successor. pa_h_hj32_h_35_route_product_successor + S (pa_s_hj32_h_35_route_product) = S ((S (S pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product)) /\ exists pa_q_hj32_h_35_route_product_successor. pa_u_hj32_h_35_route_product = pa_q_hj32_h_35_route_product_successor * S ((S (S pa_i_hj32_h_35_route_product)) * pa_v_hj32_h_35_route_product) + (pa_s_hj32_h_35_route_product))) /\ pa_s_hj32_h_35_route_product = pa_r_hj32_h_35_route_product * pa_p_hj32_h_35_route_product)))))))
9. 0009have hh_base : 35 + 1 = 36
10. 0010norm_num
11. 0011have hh_exponent : 2 * 35 + 2 = 2 * 36
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 h35s_p36 : exists hj32_local_value_h35s_p36. (exists pa_b_hj32_local_total_h35s_p36 pa_c_hj32_local_total_h35s_p36. ((forall pa_i_hj32_local_total_h35s_p36_repeat. (exists pa_lt_hj32_local_total_h35s_p36_repeat_bound. pa_lt_hj32_local_total_h35s_p36_repeat_bound + S pa_i_hj32_local_total_h35s_p36_repeat = 2 * 36) -> (((exists pa_h_hj32_local_total_h35s_p36_repeat_decoded. pa_h_hj32_local_total_h35s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h35s_p36_repeat)) * pa_c_hj32_local_total_h35s_p36)) /\ exists pa_q_hj32_local_total_h35s_p36_repeat_decoded. pa_b_hj32_local_total_h35s_p36 = pa_q_hj32_local_total_h35s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p36_repeat)) * pa_c_hj32_local_total_h35s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h35s_p36_product pa_v_hj32_local_total_h35s_p36_product. ((((exists pa_h_hj32_local_total_h35s_p36_product_start. pa_h_hj32_local_total_h35s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_start. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_terminal. pa_h_hj32_local_total_h35s_p36_product_terminal + S (hj32_local_value_h35s_p36) = S ((S (2 * 36)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_terminal. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_terminal * S ((S (2 * 36)) * pa_v_hj32_local_total_h35s_p36_product) + (hj32_local_value_h35s_p36))) /\ forall pa_i_hj32_local_total_h35s_p36_product. (exists pa_lt_hj32_local_total_h35s_p36_product_bound. pa_lt_hj32_local_total_h35s_p36_product_bound + S pa_i_hj32_local_total_h35s_p36_product = 2 * 36) -> exists pa_p_hj32_local_total_h35s_p36_product pa_r_hj32_local_total_h35s_p36_product pa_s_hj32_local_total_h35s_p36_product. ((((exists pa_h_hj32_local_total_h35s_p36_product_factor. pa_h_hj32_local_total_h35s_p36_product_factor + S (pa_p_hj32_local_total_h35s_p36_product) = S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_c_hj32_local_total_h35s_p36)) /\ exists pa_q_hj32_local_total_h35s_p36_product_factor. pa_b_hj32_local_total_h35s_p36 = pa_q_hj32_local_total_h35s_p36_product_factor * S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_c_hj32_local_total_h35s_p36) + (pa_p_hj32_local_total_h35s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_partial. pa_h_hj32_local_total_h35s_p36_product_partial + S (pa_r_hj32_local_total_h35s_p36_product) = S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_partial. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_partial * S ((S (pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product) + (pa_r_hj32_local_total_h35s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p36_product_successor. pa_h_hj32_local_total_h35s_p36_product_successor + S (pa_s_hj32_local_total_h35s_p36_product) = S ((S (S pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product)) /\ exists pa_q_hj32_local_total_h35s_p36_product_successor. pa_u_hj32_local_total_h35s_p36_product = pa_q_hj32_local_total_h35s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p36_product)) * pa_v_hj32_local_total_h35s_p36_product) + (pa_s_hj32_local_total_h35s_p36_product))) /\ pa_s_hj32_local_total_h35s_p36_product = pa_r_hj32_local_total_h35s_p36_product * pa_p_hj32_local_total_h35s_p36_product))))))))
21. 0021specialize htotal 36
22. 0022specialize htotal 2 * 36
23. 0023exact htotal
24. 0024cases h35s_p36
25. 0025have h35s_base : exists bqb_le_gap_hj32_h35s_base. bqb_le_gap_hj32_h35s_base + (36) = (36)
26. 0026exists 0
27. 0027norm_num
28. 0028have h35s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h35s_to_36. bqb_le_gap_hj32_local_base_bound_h35s_to_36 + (h) = (x)
29. 0029specialize pow_base_monotone 36
30. 0030specialize pow_base_monotone 36
31. 0031specialize pow_base_monotone 2 * 36
32. 0032specialize pow_base_monotone h
33. 0033specialize pow_base_monotone x
34. 0034apply pow_base_monotone
35. 0035exact h35s_base
36. 0036exact hh_route
37. 0037exact h35s_p36_witness
38. 0038have h35s_p6_total : exists hj32_local_value_h35s_p6_total. (exists pa_b_hj32_local_total_h35s_p6_total pa_c_hj32_local_total_h35s_p6_total. ((forall pa_i_hj32_local_total_h35s_p6_total_repeat. (exists pa_lt_hj32_local_total_h35s_p6_total_repeat_bound. pa_lt_hj32_local_total_h35s_p6_total_repeat_bound + S pa_i_hj32_local_total_h35s_p6_total_repeat = 4 * 36) -> (((exists pa_h_hj32_local_total_h35s_p6_total_repeat_decoded. pa_h_hj32_local_total_h35s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_total_repeat)) * pa_c_hj32_local_total_h35s_p6_total)) /\ exists pa_q_hj32_local_total_h35s_p6_total_repeat_decoded. pa_b_hj32_local_total_h35s_p6_total = pa_q_hj32_local_total_h35s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_total_repeat)) * pa_c_hj32_local_total_h35s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_total_product pa_v_hj32_local_total_h35s_p6_total_product. ((((exists pa_h_hj32_local_total_h35s_p6_total_product_start. pa_h_hj32_local_total_h35s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_start. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_terminal. pa_h_hj32_local_total_h35s_p6_total_product_terminal + S (hj32_local_value_h35s_p6_total) = S ((S (4 * 36)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_terminal. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_terminal * S ((S (4 * 36)) * pa_v_hj32_local_total_h35s_p6_total_product) + (hj32_local_value_h35s_p6_total))) /\ forall pa_i_hj32_local_total_h35s_p6_total_product. (exists pa_lt_hj32_local_total_h35s_p6_total_product_bound. pa_lt_hj32_local_total_h35s_p6_total_product_bound + S pa_i_hj32_local_total_h35s_p6_total_product = 4 * 36) -> exists pa_p_hj32_local_total_h35s_p6_total_product pa_r_hj32_local_total_h35s_p6_total_product pa_s_hj32_local_total_h35s_p6_total_product. ((((exists pa_h_hj32_local_total_h35s_p6_total_product_factor. pa_h_hj32_local_total_h35s_p6_total_product_factor + S (pa_p_hj32_local_total_h35s_p6_total_product) = S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_c_hj32_local_total_h35s_p6_total)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_factor. pa_b_hj32_local_total_h35s_p6_total = pa_q_hj32_local_total_h35s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_c_hj32_local_total_h35s_p6_total) + (pa_p_hj32_local_total_h35s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_partial. pa_h_hj32_local_total_h35s_p6_total_product_partial + S (pa_r_hj32_local_total_h35s_p6_total_product) = S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_partial. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product) + (pa_r_hj32_local_total_h35s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_total_product_successor. pa_h_hj32_local_total_h35s_p6_total_product_successor + S (pa_s_hj32_local_total_h35s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product)) /\ exists pa_q_hj32_local_total_h35s_p6_total_product_successor. pa_u_hj32_local_total_h35s_p6_total_product = pa_q_hj32_local_total_h35s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_total_product)) * pa_v_hj32_local_total_h35s_p6_total_product) + (pa_s_hj32_local_total_h35s_p6_total_product))) /\ pa_s_hj32_local_total_h35s_p6_total_product = pa_r_hj32_local_total_h35s_p6_total_product * pa_p_hj32_local_total_h35s_p6_total_product))))))))
39. 0039specialize htotal 6
40. 0040specialize htotal 4 * 36
41. 0041exact htotal
42. 0042cases h35s_p6_total
43. 0043have h35s_conversion : x = x1
44. 0044specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 36
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 h35s_p36_witness
50. 0050exact h35s_p6_total_witness
51. 0051rewrite h35s_conversion at h35s_to_36
52. 0052have h35s_p6_main : exists hj32_local_value_h35s_p6_main. (exists pa_b_hj32_local_total_h35s_p6_main pa_c_hj32_local_total_h35s_p6_main. ((forall pa_i_hj32_local_total_h35s_p6_main_repeat. (exists pa_lt_hj32_local_total_h35s_p6_main_repeat_bound. pa_lt_hj32_local_total_h35s_p6_main_repeat_bound + S pa_i_hj32_local_total_h35s_p6_main_repeat = 10 * 14) -> (((exists pa_h_hj32_local_total_h35s_p6_main_repeat_decoded. pa_h_hj32_local_total_h35s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_main_repeat)) * pa_c_hj32_local_total_h35s_p6_main)) /\ exists pa_q_hj32_local_total_h35s_p6_main_repeat_decoded. pa_b_hj32_local_total_h35s_p6_main = pa_q_hj32_local_total_h35s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_main_repeat)) * pa_c_hj32_local_total_h35s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_main_product pa_v_hj32_local_total_h35s_p6_main_product. ((((exists pa_h_hj32_local_total_h35s_p6_main_product_start. pa_h_hj32_local_total_h35s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_start. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_terminal. pa_h_hj32_local_total_h35s_p6_main_product_terminal + S (hj32_local_value_h35s_p6_main) = S ((S (10 * 14)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_terminal. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_terminal * S ((S (10 * 14)) * pa_v_hj32_local_total_h35s_p6_main_product) + (hj32_local_value_h35s_p6_main))) /\ forall pa_i_hj32_local_total_h35s_p6_main_product. (exists pa_lt_hj32_local_total_h35s_p6_main_product_bound. pa_lt_hj32_local_total_h35s_p6_main_product_bound + S pa_i_hj32_local_total_h35s_p6_main_product = 10 * 14) -> exists pa_p_hj32_local_total_h35s_p6_main_product pa_r_hj32_local_total_h35s_p6_main_product pa_s_hj32_local_total_h35s_p6_main_product. ((((exists pa_h_hj32_local_total_h35s_p6_main_product_factor. pa_h_hj32_local_total_h35s_p6_main_product_factor + S (pa_p_hj32_local_total_h35s_p6_main_product) = S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_c_hj32_local_total_h35s_p6_main)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_factor. pa_b_hj32_local_total_h35s_p6_main = pa_q_hj32_local_total_h35s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_c_hj32_local_total_h35s_p6_main) + (pa_p_hj32_local_total_h35s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_partial. pa_h_hj32_local_total_h35s_p6_main_product_partial + S (pa_r_hj32_local_total_h35s_p6_main_product) = S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_partial. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product) + (pa_r_hj32_local_total_h35s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_main_product_successor. pa_h_hj32_local_total_h35s_p6_main_product_successor + S (pa_s_hj32_local_total_h35s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product)) /\ exists pa_q_hj32_local_total_h35s_p6_main_product_successor. pa_u_hj32_local_total_h35s_p6_main_product = pa_q_hj32_local_total_h35s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_main_product)) * pa_v_hj32_local_total_h35s_p6_main_product) + (pa_s_hj32_local_total_h35s_p6_main_product))) /\ pa_s_hj32_local_total_h35s_p6_main_product = pa_r_hj32_local_total_h35s_p6_main_product * pa_p_hj32_local_total_h35s_p6_main_product))))))))
53. 0053specialize htotal 6
54. 0054specialize htotal 10 * 14
55. 0055exact htotal
56. 0056cases h35s_p6_main
57. 0057have h35s_p4_main : exists hj32_local_value_h35s_p4_main. (exists pa_b_hj32_local_total_h35s_p4_main pa_c_hj32_local_total_h35s_p4_main. ((forall pa_i_hj32_local_total_h35s_p4_main_repeat. (exists pa_lt_hj32_local_total_h35s_p4_main_repeat_bound. pa_lt_hj32_local_total_h35s_p4_main_repeat_bound + S pa_i_hj32_local_total_h35s_p4_main_repeat = 13 * 14) -> (((exists pa_h_hj32_local_total_h35s_p4_main_repeat_decoded. pa_h_hj32_local_total_h35s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_main_repeat)) * pa_c_hj32_local_total_h35s_p4_main)) /\ exists pa_q_hj32_local_total_h35s_p4_main_repeat_decoded. pa_b_hj32_local_total_h35s_p4_main = pa_q_hj32_local_total_h35s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_main_repeat)) * pa_c_hj32_local_total_h35s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_main_product pa_v_hj32_local_total_h35s_p4_main_product. ((((exists pa_h_hj32_local_total_h35s_p4_main_product_start. pa_h_hj32_local_total_h35s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_start. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_terminal. pa_h_hj32_local_total_h35s_p4_main_product_terminal + S (hj32_local_value_h35s_p4_main) = S ((S (13 * 14)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_terminal. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_terminal * S ((S (13 * 14)) * pa_v_hj32_local_total_h35s_p4_main_product) + (hj32_local_value_h35s_p4_main))) /\ forall pa_i_hj32_local_total_h35s_p4_main_product. (exists pa_lt_hj32_local_total_h35s_p4_main_product_bound. pa_lt_hj32_local_total_h35s_p4_main_product_bound + S pa_i_hj32_local_total_h35s_p4_main_product = 13 * 14) -> exists pa_p_hj32_local_total_h35s_p4_main_product pa_r_hj32_local_total_h35s_p4_main_product pa_s_hj32_local_total_h35s_p4_main_product. ((((exists pa_h_hj32_local_total_h35s_p4_main_product_factor. pa_h_hj32_local_total_h35s_p4_main_product_factor + S (pa_p_hj32_local_total_h35s_p4_main_product) = S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_c_hj32_local_total_h35s_p4_main)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_factor. pa_b_hj32_local_total_h35s_p4_main = pa_q_hj32_local_total_h35s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_c_hj32_local_total_h35s_p4_main) + (pa_p_hj32_local_total_h35s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_partial. pa_h_hj32_local_total_h35s_p4_main_product_partial + S (pa_r_hj32_local_total_h35s_p4_main_product) = S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_partial. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product) + (pa_r_hj32_local_total_h35s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_main_product_successor. pa_h_hj32_local_total_h35s_p4_main_product_successor + S (pa_s_hj32_local_total_h35s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product)) /\ exists pa_q_hj32_local_total_h35s_p4_main_product_successor. pa_u_hj32_local_total_h35s_p4_main_product = pa_q_hj32_local_total_h35s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_main_product)) * pa_v_hj32_local_total_h35s_p4_main_product) + (pa_s_hj32_local_total_h35s_p4_main_product))) /\ pa_s_hj32_local_total_h35s_p4_main_product = pa_r_hj32_local_total_h35s_p4_main_product * pa_p_hj32_local_total_h35s_p4_main_product))))))))
58. 0058specialize htotal 4
59. 0059specialize htotal 13 * 14
60. 0060exact htotal
61. 0061cases h35s_p4_main
62. 0062have h35s_main_bound : exists bqb_le_gap_hj32_h35s_main_bound. bqb_le_gap_hj32_h35s_main_bound + (x2) = (x3)
63. 0063specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14
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 h35s_p6_main_witness
69. 0069exact h35s_p4_main_witness
70. 0070have h35s_p6_residual : exists hj32_local_value_h35s_p6_residual. (exists pa_b_hj32_local_total_h35s_p6_residual pa_c_hj32_local_total_h35s_p6_residual. ((forall pa_i_hj32_local_total_h35s_p6_residual_repeat. (exists pa_lt_hj32_local_total_h35s_p6_residual_repeat_bound. pa_lt_hj32_local_total_h35s_p6_residual_repeat_bound + S pa_i_hj32_local_total_h35s_p6_residual_repeat = 4) -> (((exists pa_h_hj32_local_total_h35s_p6_residual_repeat_decoded. pa_h_hj32_local_total_h35s_p6_residual_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_repeat)) * pa_c_hj32_local_total_h35s_p6_residual)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_repeat_decoded. pa_b_hj32_local_total_h35s_p6_residual = pa_q_hj32_local_total_h35s_p6_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p6_residual_repeat)) * pa_c_hj32_local_total_h35s_p6_residual) + (6)))) /\ (exists pa_u_hj32_local_total_h35s_p6_residual_product pa_v_hj32_local_total_h35s_p6_residual_product. ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_start. pa_h_hj32_local_total_h35s_p6_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_start. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_terminal. pa_h_hj32_local_total_h35s_p6_residual_product_terminal + S (hj32_local_value_h35s_p6_residual) = S ((S (4)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_terminal. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_terminal * S ((S (4)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (hj32_local_value_h35s_p6_residual))) /\ forall pa_i_hj32_local_total_h35s_p6_residual_product. (exists pa_lt_hj32_local_total_h35s_p6_residual_product_bound. pa_lt_hj32_local_total_h35s_p6_residual_product_bound + S pa_i_hj32_local_total_h35s_p6_residual_product = 4) -> exists pa_p_hj32_local_total_h35s_p6_residual_product pa_r_hj32_local_total_h35s_p6_residual_product pa_s_hj32_local_total_h35s_p6_residual_product. ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_factor. pa_h_hj32_local_total_h35s_p6_residual_product_factor + S (pa_p_hj32_local_total_h35s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_c_hj32_local_total_h35s_p6_residual)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_factor. pa_b_hj32_local_total_h35s_p6_residual = pa_q_hj32_local_total_h35s_p6_residual_product_factor * S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_c_hj32_local_total_h35s_p6_residual) + (pa_p_hj32_local_total_h35s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_partial. pa_h_hj32_local_total_h35s_p6_residual_product_partial + S (pa_r_hj32_local_total_h35s_p6_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_partial. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_partial * S ((S (pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (pa_r_hj32_local_total_h35s_p6_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p6_residual_product_successor. pa_h_hj32_local_total_h35s_p6_residual_product_successor + S (pa_s_hj32_local_total_h35s_p6_residual_product) = S ((S (S pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p6_residual_product_successor. pa_u_hj32_local_total_h35s_p6_residual_product = pa_q_hj32_local_total_h35s_p6_residual_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p6_residual_product)) * pa_v_hj32_local_total_h35s_p6_residual_product) + (pa_s_hj32_local_total_h35s_p6_residual_product))) /\ pa_s_hj32_local_total_h35s_p6_residual_product = pa_r_hj32_local_total_h35s_p6_residual_product * pa_p_hj32_local_total_h35s_p6_residual_product))))))))
71. 0071specialize htotal 6
72. 0072specialize htotal 4
73. 0073exact htotal
74. 0074cases h35s_p6_residual
75. 0075have h35s_p4_residual : exists hj32_local_value_h35s_p4_residual. (exists pa_b_hj32_local_total_h35s_p4_residual pa_c_hj32_local_total_h35s_p4_residual. ((forall pa_i_hj32_local_total_h35s_p4_residual_repeat. (exists pa_lt_hj32_local_total_h35s_p4_residual_repeat_bound. pa_lt_hj32_local_total_h35s_p4_residual_repeat_bound + S pa_i_hj32_local_total_h35s_p4_residual_repeat = 6) -> (((exists pa_h_hj32_local_total_h35s_p4_residual_repeat_decoded. pa_h_hj32_local_total_h35s_p4_residual_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_repeat)) * pa_c_hj32_local_total_h35s_p4_residual)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_repeat_decoded. pa_b_hj32_local_total_h35s_p4_residual = pa_q_hj32_local_total_h35s_p4_residual_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_residual_repeat)) * pa_c_hj32_local_total_h35s_p4_residual) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_residual_product pa_v_hj32_local_total_h35s_p4_residual_product. ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_start. pa_h_hj32_local_total_h35s_p4_residual_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_start. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_terminal. pa_h_hj32_local_total_h35s_p4_residual_product_terminal + S (hj32_local_value_h35s_p4_residual) = S ((S (6)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_terminal. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_terminal * S ((S (6)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (hj32_local_value_h35s_p4_residual))) /\ forall pa_i_hj32_local_total_h35s_p4_residual_product. (exists pa_lt_hj32_local_total_h35s_p4_residual_product_bound. pa_lt_hj32_local_total_h35s_p4_residual_product_bound + S pa_i_hj32_local_total_h35s_p4_residual_product = 6) -> exists pa_p_hj32_local_total_h35s_p4_residual_product pa_r_hj32_local_total_h35s_p4_residual_product pa_s_hj32_local_total_h35s_p4_residual_product. ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_factor. pa_h_hj32_local_total_h35s_p4_residual_product_factor + S (pa_p_hj32_local_total_h35s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_c_hj32_local_total_h35s_p4_residual)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_factor. pa_b_hj32_local_total_h35s_p4_residual = pa_q_hj32_local_total_h35s_p4_residual_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_c_hj32_local_total_h35s_p4_residual) + (pa_p_hj32_local_total_h35s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_partial. pa_h_hj32_local_total_h35s_p4_residual_product_partial + S (pa_r_hj32_local_total_h35s_p4_residual_product) = S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_partial. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (pa_r_hj32_local_total_h35s_p4_residual_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_residual_product_successor. pa_h_hj32_local_total_h35s_p4_residual_product_successor + S (pa_s_hj32_local_total_h35s_p4_residual_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product)) /\ exists pa_q_hj32_local_total_h35s_p4_residual_product_successor. pa_u_hj32_local_total_h35s_p4_residual_product = pa_q_hj32_local_total_h35s_p4_residual_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_residual_product)) * pa_v_hj32_local_total_h35s_p4_residual_product) + (pa_s_hj32_local_total_h35s_p4_residual_product))) /\ pa_s_hj32_local_total_h35s_p4_residual_product = pa_r_hj32_local_total_h35s_p4_residual_product * pa_p_hj32_local_total_h35s_p4_residual_product))))))))
76. 0076specialize htotal 4
77. 0077specialize htotal 6
78. 0078exact htotal
79. 0079cases h35s_p4_residual
80. 0080have h35s_residual_bound : exists bqb_le_gap_hj32_h35s_residual_bound. bqb_le_gap_hj32_h35s_residual_bound + (x4) = (x5)
81. 0081specialize pow_six_four_le_pow_four_six_from_total x4
82. 0082specialize pow_six_four_le_pow_four_six_from_total x5
83. 0083apply pow_six_four_le_pow_four_six_from_total
84. 0084exact htotal
85. 0085exact h35s_p6_residual_witness
86. 0086exact h35s_p4_residual_witness
87. 0087have h35s_exponent : 4 * 36 = 10 * 14 + 4
88. 0088have h35s_thirty_six : 36 = 5 * 7 + 1
89. 0089norm_num
90. 0090rewrite h35s_thirty_six
91. 0091have h35s_distrib : 4 * (5 * 7 + 1) = 4 * (5 * 7) + 4 * 1
92. 0092specialize mul_add 4
93. 0093specialize mul_add (5 * 7)
94. 0094specialize mul_add 1
95. 0095apply mul_add
96. 0096rewrite h35s_distrib
97. 0097have h35s_left_assoc : 4 * (5 * 7) = (4 * 5) * 7
98. 0098symm
99. 0099specialize mul_assoc 4
100. 0100specialize mul_assoc 5
101. 0101specialize mul_assoc 7
102. 0102apply mul_assoc
103. 0103rewrite h35s_left_assoc
104. 0104have h35s_fourteen : 14 = 2 * 7
105. 0105norm_num
106. 0106rewrite h35s_fourteen
107. 0107have h35s_right_assoc : 10 * (2 * 7) = (10 * 2) * 7
108. 0108symm
109. 0109specialize mul_assoc 10
110. 0110specialize mul_assoc 2
111. 0111specialize mul_assoc 7
112. 0112apply mul_assoc
113. 0113rewrite h35s_right_assoc
114. 0114have h35s_right_twenty : 10 * 2 = 20
115. 0115norm_num
116. 0116rewrite h35s_right_twenty
117. 0117have h35s_twenty : 4 * 5 = 20
118. 0118norm_num
119. 0119rewrite h35s_twenty
120. 0120have h35s_four : 4 * 1 = 4
121. 0121norm_num
122. 0122rewrite h35s_four
123. 0123refl
124. 0124have h35s_left_product : x1 = x2 * x4
125. 0125specialize pow_add 6
126. 0126specialize pow_add 10 * 14
127. 0127specialize pow_add 4
128. 0128specialize pow_add 4 * 36
129. 0129specialize pow_add x2
130. 0130specialize pow_add x4
131. 0131specialize pow_add x1
132. 0132apply pow_add
133. 0133exact h35s_exponent
134. 0134exact h35s_p6_main_witness
135. 0135exact h35s_p6_residual_witness
136. 0136exact h35s_p6_total_witness
137. 0137have h35s_p4_budget : exists hj32_local_value_h35s_p4_budget. (exists pa_b_hj32_local_total_h35s_p4_budget pa_c_hj32_local_total_h35s_p4_budget. ((forall pa_i_hj32_local_total_h35s_p4_budget_repeat. (exists pa_lt_hj32_local_total_h35s_p4_budget_repeat_bound. pa_lt_hj32_local_total_h35s_p4_budget_repeat_bound + S pa_i_hj32_local_total_h35s_p4_budget_repeat = 13 * 14 + 6) -> (((exists pa_h_hj32_local_total_h35s_p4_budget_repeat_decoded. pa_h_hj32_local_total_h35s_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_repeat)) * pa_c_hj32_local_total_h35s_p4_budget)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_repeat_decoded. pa_b_hj32_local_total_h35s_p4_budget = pa_q_hj32_local_total_h35s_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h35s_p4_budget_repeat)) * pa_c_hj32_local_total_h35s_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h35s_p4_budget_product pa_v_hj32_local_total_h35s_p4_budget_product. ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_start. pa_h_hj32_local_total_h35s_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_start. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_terminal. pa_h_hj32_local_total_h35s_p4_budget_product_terminal + S (hj32_local_value_h35s_p4_budget) = S ((S (13 * 14 + 6)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_terminal. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_terminal * S ((S (13 * 14 + 6)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (hj32_local_value_h35s_p4_budget))) /\ forall pa_i_hj32_local_total_h35s_p4_budget_product. (exists pa_lt_hj32_local_total_h35s_p4_budget_product_bound. pa_lt_hj32_local_total_h35s_p4_budget_product_bound + S pa_i_hj32_local_total_h35s_p4_budget_product = 13 * 14 + 6) -> exists pa_p_hj32_local_total_h35s_p4_budget_product pa_r_hj32_local_total_h35s_p4_budget_product pa_s_hj32_local_total_h35s_p4_budget_product. ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_factor. pa_h_hj32_local_total_h35s_p4_budget_product_factor + S (pa_p_hj32_local_total_h35s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_c_hj32_local_total_h35s_p4_budget)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_factor. pa_b_hj32_local_total_h35s_p4_budget = pa_q_hj32_local_total_h35s_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_c_hj32_local_total_h35s_p4_budget) + (pa_p_hj32_local_total_h35s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_partial. pa_h_hj32_local_total_h35s_p4_budget_product_partial + S (pa_r_hj32_local_total_h35s_p4_budget_product) = S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_partial. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (pa_r_hj32_local_total_h35s_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h35s_p4_budget_product_successor. pa_h_hj32_local_total_h35s_p4_budget_product_successor + S (pa_s_hj32_local_total_h35s_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product)) /\ exists pa_q_hj32_local_total_h35s_p4_budget_product_successor. pa_u_hj32_local_total_h35s_p4_budget_product = pa_q_hj32_local_total_h35s_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h35s_p4_budget_product)) * pa_v_hj32_local_total_h35s_p4_budget_product) + (pa_s_hj32_local_total_h35s_p4_budget_product))) /\ pa_s_hj32_local_total_h35s_p4_budget_product = pa_r_hj32_local_total_h35s_p4_budget_product * pa_p_hj32_local_total_h35s_p4_budget_product))))))))
138. 0138specialize htotal 4
139. 0139specialize htotal 13 * 14 + 6
140. 0140exact htotal
141. 0141cases h35s_p4_budget
142. 0142have h35s_right_product : x6 = x3 * x5
143. 0143specialize pow_add 4
144. 0144specialize pow_add 13 * 14
145. 0145specialize pow_add 6
146. 0146specialize pow_add 13 * 14 + 6
147. 0147specialize pow_add x3
148. 0148specialize pow_add x5
149. 0149specialize pow_add x6
150. 0150apply pow_add
151. 0151refl
152. 0152exact h35s_p4_main_witness
153. 0153exact h35s_p4_residual_witness
154. 0154exact h35s_p4_budget_witness
155. 0155have h35s_six_bound : exists bqb_le_gap_hj32_local_product_bound_h35s_six_bound. bqb_le_gap_hj32_local_product_bound_h35s_six_bound + (x2 * x4) = (x3 * x5)
156. 0156specialize mul_le_mul x2
157. 0157specialize mul_le_mul x3
158. 0158specialize mul_le_mul x4
159. 0159specialize mul_le_mul x5
160. 0160apply mul_le_mul
161. 0161exact h35s_main_bound
162. 0162exact h35s_residual_bound
163. 0163rewrite <- h35s_left_product at h35s_six_bound
164. 0164rewrite <- h35s_right_product at h35s_six_bound
165. 0165have h35s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h35s_to_budget. bqb_le_gap_hj32_local_trans_bound_h35s_to_budget + (h) = (x6)
166. 0166specialize le_trans h
167. 0167specialize le_trans x1
168. 0168specialize le_trans x6
169. 0169apply le_trans
170. 0170exact h35s_to_36
171. 0171exact h35s_six_bound
172. 0172have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_35. bqb_le_gap_hj32_scaled_budget_root_35 + (6 * (13 * 14 + 6)) = (35 * 35)
173. 0173apply bertrand_scaled_budget_root_35
174. 0174have hbudget_exponent : exists bqb_le_gap_hj32_h_35_budget_exponent. bqb_le_gap_hj32_h_35_budget_exponent + (13 * 14 + 6) = (e)
175. 0175specialize ceil_div_six_budget_of_scaled_le (35 * 35)
176. 0176specialize ceil_div_six_budget_of_scaled_le (13 * 14 + 6)
177. 0177specialize ceil_div_six_budget_of_scaled_le e
178. 0178apply ceil_div_six_budget_of_scaled_le
179. 0179exact hceiling
180. 0180exact hscaled
181. 0181have h35_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h35_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h35_budget_growth + (x6) = (u)
182. 0182specialize pow_exponent_monotone_from_total 4
183. 0183specialize pow_exponent_monotone_from_total 13 * 14 + 6
184. 0184specialize pow_exponent_monotone_from_total e
185. 0185specialize pow_exponent_monotone_from_total x6
186. 0186specialize pow_exponent_monotone_from_total u
187. 0187apply pow_exponent_monotone_from_total
188. 0188exact htotal
189. 0189exists 3
190. 0190norm_num
191. 0191exact hbudget_exponent
192. 0192exact h35s_p4_budget_witness
193. 0193exact hu
194. 0194have h35_result : exists bqb_le_gap_hj32_local_trans_bound_h35_result. bqb_le_gap_hj32_local_trans_bound_h35_result + (h) = (u)
195. 0195specialize le_trans h
196. 0196specialize le_trans x6
197. 0197specialize le_trans u
198. 0198apply le_trans
199. 0199exact h35s_to_budget
200. 0200exact h35_budget_growth
201. 0201exact h35_result