bertrand_h_root_32_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_32_route pa_c_hj32_h_32_route. ((forall pa_i_hj32_h_32_route_repeat. (exists pa_lt_hj32_h_32_route_repeat_bound. pa_lt_hj32_h_32_route_repeat_bound + S pa_i_hj32_h_32_route_repeat = 2 * 33) -> (((exists pa_h_hj32_h_32_route_repeat_decoded. pa_h_hj32_h_32_route_repeat_decoded + S (33) = S ((S (pa_i_hj32_h_32_route_repeat)) * pa_c_hj32_h_32_route)) /\ exists pa_q_hj32_h_32_route_repeat_decoded. pa_b_hj32_h_32_route = pa_q_hj32_h_32_route_repeat_decoded * S ((S (pa_i_hj32_h_32_route_repeat)) * pa_c_hj32_h_32_route) + (33)))) /\ (exists pa_u_hj32_h_32_route_product pa_v_hj32_h_32_route_product. ((((exists pa_h_hj32_h_32_route_product_start. pa_h_hj32_h_32_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_start. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_start * S ((S (0)) * pa_v_hj32_h_32_route_product) + (1))) /\ ((((exists pa_h_hj32_h_32_route_product_terminal. pa_h_hj32_h_32_route_product_terminal + S (h) = S ((S (2 * 33)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_terminal. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_terminal * S ((S (2 * 33)) * pa_v_hj32_h_32_route_product) + (h))) /\ forall pa_i_hj32_h_32_route_product. (exists pa_lt_hj32_h_32_route_product_bound. pa_lt_hj32_h_32_route_product_bound + S pa_i_hj32_h_32_route_product = 2 * 33) -> exists pa_p_hj32_h_32_route_product pa_r_hj32_h_32_route_product pa_s_hj32_h_32_route_product. ((((exists pa_h_hj32_h_32_route_product_factor. pa_h_hj32_h_32_route_product_factor + S (pa_p_hj32_h_32_route_product) = S ((S (pa_i_hj32_h_32_route_product)) * pa_c_hj32_h_32_route)) /\ exists pa_q_hj32_h_32_route_product_factor. pa_b_hj32_h_32_route = pa_q_hj32_h_32_route_product_factor * S ((S (pa_i_hj32_h_32_route_product)) * pa_c_hj32_h_32_route) + (pa_p_hj32_h_32_route_product))) /\ ((((exists pa_h_hj32_h_32_route_product_partial. pa_h_hj32_h_32_route_product_partial + S (pa_r_hj32_h_32_route_product) = S ((S (pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_partial. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_partial * S ((S (pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product) + (pa_r_hj32_h_32_route_product))) /\ ((((exists pa_h_hj32_h_32_route_product_successor. pa_h_hj32_h_32_route_product_successor + S (pa_s_hj32_h_32_route_product) = S ((S (S pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product)) /\ exists pa_q_hj32_h_32_route_product_successor. pa_u_hj32_h_32_route_product = pa_q_hj32_h_32_route_product_successor * S ((S (S pa_i_hj32_h_32_route_product)) * pa_v_hj32_h_32_route_product) + (pa_s_hj32_h_32_route_product))) /\ pa_s_hj32_h_32_route_product = pa_r_hj32_h_32_route_product * pa_p_hj32_h_32_route_product)))))))
9. 0009have hh_base : 32 + 1 = 33
10. 0010norm_num
11. 0011have hh_exponent : 2 * 32 + 2 = 2 * 33
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 h32t_p3_exp : exists hj32_local_value_h32t_p3_exp. (exists pa_b_hj32_local_total_h32t_p3_exp pa_c_hj32_local_total_h32t_p3_exp. ((forall pa_i_hj32_local_total_h32t_p3_exp_repeat. (exists pa_lt_hj32_local_total_h32t_p3_exp_repeat_bound. pa_lt_hj32_local_total_h32t_p3_exp_repeat_bound + S pa_i_hj32_local_total_h32t_p3_exp_repeat = 2 * 33) -> (((exists pa_h_hj32_local_total_h32t_p3_exp_repeat_decoded. pa_h_hj32_local_total_h32t_p3_exp_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_repeat)) * pa_c_hj32_local_total_h32t_p3_exp)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_repeat_decoded. pa_b_hj32_local_total_h32t_p3_exp = pa_q_hj32_local_total_h32t_p3_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p3_exp_repeat)) * pa_c_hj32_local_total_h32t_p3_exp) + (3)))) /\ (exists pa_u_hj32_local_total_h32t_p3_exp_product pa_v_hj32_local_total_h32t_p3_exp_product. ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_start. pa_h_hj32_local_total_h32t_p3_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_start. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_terminal. pa_h_hj32_local_total_h32t_p3_exp_product_terminal + S (hj32_local_value_h32t_p3_exp) = S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_terminal. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (hj32_local_value_h32t_p3_exp))) /\ forall pa_i_hj32_local_total_h32t_p3_exp_product. (exists pa_lt_hj32_local_total_h32t_p3_exp_product_bound. pa_lt_hj32_local_total_h32t_p3_exp_product_bound + S pa_i_hj32_local_total_h32t_p3_exp_product = 2 * 33) -> exists pa_p_hj32_local_total_h32t_p3_exp_product pa_r_hj32_local_total_h32t_p3_exp_product pa_s_hj32_local_total_h32t_p3_exp_product. ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_factor. pa_h_hj32_local_total_h32t_p3_exp_product_factor + S (pa_p_hj32_local_total_h32t_p3_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_c_hj32_local_total_h32t_p3_exp)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_factor. pa_b_hj32_local_total_h32t_p3_exp = pa_q_hj32_local_total_h32t_p3_exp_product_factor * S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_c_hj32_local_total_h32t_p3_exp) + (pa_p_hj32_local_total_h32t_p3_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_partial. pa_h_hj32_local_total_h32t_p3_exp_product_partial + S (pa_r_hj32_local_total_h32t_p3_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_partial. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_partial * S ((S (pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (pa_r_hj32_local_total_h32t_p3_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p3_exp_product_successor. pa_h_hj32_local_total_h32t_p3_exp_product_successor + S (pa_s_hj32_local_total_h32t_p3_exp_product) = S ((S (S pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p3_exp_product_successor. pa_u_hj32_local_total_h32t_p3_exp_product = pa_q_hj32_local_total_h32t_p3_exp_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p3_exp_product)) * pa_v_hj32_local_total_h32t_p3_exp_product) + (pa_s_hj32_local_total_h32t_p3_exp_product))) /\ pa_s_hj32_local_total_h32t_p3_exp_product = pa_r_hj32_local_total_h32t_p3_exp_product * pa_p_hj32_local_total_h32t_p3_exp_product))))))))
21. 0021specialize htotal 3
22. 0022specialize htotal 2 * 33
23. 0023exact htotal
24. 0024cases h32t_p3_exp
25. 0025have h32t_p11_exp : exists hj32_local_value_h32t_p11_exp. (exists pa_b_hj32_local_total_h32t_p11_exp pa_c_hj32_local_total_h32t_p11_exp. ((forall pa_i_hj32_local_total_h32t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h32t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h32t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h32t_p11_exp_repeat = 2 * 33) -> (((exists pa_h_hj32_local_total_h32t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h32t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_repeat)) * pa_c_hj32_local_total_h32t_p11_exp)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h32t_p11_exp = pa_q_hj32_local_total_h32t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p11_exp_repeat)) * pa_c_hj32_local_total_h32t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h32t_p11_exp_product pa_v_hj32_local_total_h32t_p11_exp_product. ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_start. pa_h_hj32_local_total_h32t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_start. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_terminal. pa_h_hj32_local_total_h32t_p11_exp_product_terminal + S (hj32_local_value_h32t_p11_exp) = S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_terminal. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (hj32_local_value_h32t_p11_exp))) /\ forall pa_i_hj32_local_total_h32t_p11_exp_product. (exists pa_lt_hj32_local_total_h32t_p11_exp_product_bound. pa_lt_hj32_local_total_h32t_p11_exp_product_bound + S pa_i_hj32_local_total_h32t_p11_exp_product = 2 * 33) -> exists pa_p_hj32_local_total_h32t_p11_exp_product pa_r_hj32_local_total_h32t_p11_exp_product pa_s_hj32_local_total_h32t_p11_exp_product. ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_factor. pa_h_hj32_local_total_h32t_p11_exp_product_factor + S (pa_p_hj32_local_total_h32t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_c_hj32_local_total_h32t_p11_exp)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_factor. pa_b_hj32_local_total_h32t_p11_exp = pa_q_hj32_local_total_h32t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_c_hj32_local_total_h32t_p11_exp) + (pa_p_hj32_local_total_h32t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_partial. pa_h_hj32_local_total_h32t_p11_exp_product_partial + S (pa_r_hj32_local_total_h32t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_partial. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (pa_r_hj32_local_total_h32t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p11_exp_product_successor. pa_h_hj32_local_total_h32t_p11_exp_product_successor + S (pa_s_hj32_local_total_h32t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h32t_p11_exp_product_successor. pa_u_hj32_local_total_h32t_p11_exp_product = pa_q_hj32_local_total_h32t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p11_exp_product)) * pa_v_hj32_local_total_h32t_p11_exp_product) + (pa_s_hj32_local_total_h32t_p11_exp_product))) /\ pa_s_hj32_local_total_h32t_p11_exp_product = pa_r_hj32_local_total_h32t_p11_exp_product * pa_p_hj32_local_total_h32t_p11_exp_product))))))))
26. 0026specialize htotal 11
27. 0027specialize htotal 2 * 33
28. 0028exact htotal
29. 0029cases h32t_p11_exp
30. 0030have h32t_product_graph : exists pa_b_hj32_local_product_h32t_product pa_c_hj32_local_product_h32t_product. ((forall pa_i_hj32_local_product_h32t_product_repeat. (exists pa_lt_hj32_local_product_h32t_product_repeat_bound. pa_lt_hj32_local_product_h32t_product_repeat_bound + S pa_i_hj32_local_product_h32t_product_repeat = 2 * 33) -> (((exists pa_h_hj32_local_product_h32t_product_repeat_decoded. pa_h_hj32_local_product_h32t_product_repeat_decoded + S (3 * 11) = S ((S (pa_i_hj32_local_product_h32t_product_repeat)) * pa_c_hj32_local_product_h32t_product)) /\ exists pa_q_hj32_local_product_h32t_product_repeat_decoded. pa_b_hj32_local_product_h32t_product = pa_q_hj32_local_product_h32t_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h32t_product_repeat)) * pa_c_hj32_local_product_h32t_product) + (3 * 11)))) /\ (exists pa_u_hj32_local_product_h32t_product_product pa_v_hj32_local_product_h32t_product_product. ((((exists pa_h_hj32_local_product_h32t_product_product_start. pa_h_hj32_local_product_h32t_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_start. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h32t_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_terminal. pa_h_hj32_local_product_h32t_product_product_terminal + S (h) = S ((S (2 * 33)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_terminal. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_terminal * S ((S (2 * 33)) * pa_v_hj32_local_product_h32t_product_product) + (h))) /\ forall pa_i_hj32_local_product_h32t_product_product. (exists pa_lt_hj32_local_product_h32t_product_product_bound. pa_lt_hj32_local_product_h32t_product_product_bound + S pa_i_hj32_local_product_h32t_product_product = 2 * 33) -> exists pa_p_hj32_local_product_h32t_product_product pa_r_hj32_local_product_h32t_product_product pa_s_hj32_local_product_h32t_product_product. ((((exists pa_h_hj32_local_product_h32t_product_product_factor. pa_h_hj32_local_product_h32t_product_product_factor + S (pa_p_hj32_local_product_h32t_product_product) = S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_c_hj32_local_product_h32t_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_factor. pa_b_hj32_local_product_h32t_product = pa_q_hj32_local_product_h32t_product_product_factor * S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_c_hj32_local_product_h32t_product) + (pa_p_hj32_local_product_h32t_product_product))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_partial. pa_h_hj32_local_product_h32t_product_product_partial + S (pa_r_hj32_local_product_h32t_product_product) = S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_partial. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_partial * S ((S (pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product) + (pa_r_hj32_local_product_h32t_product_product))) /\ ((((exists pa_h_hj32_local_product_h32t_product_product_successor. pa_h_hj32_local_product_h32t_product_product_successor + S (pa_s_hj32_local_product_h32t_product_product) = S ((S (S pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product)) /\ exists pa_q_hj32_local_product_h32t_product_product_successor. pa_u_hj32_local_product_h32t_product_product = pa_q_hj32_local_product_h32t_product_product_successor * S ((S (S pa_i_hj32_local_product_h32t_product_product)) * pa_v_hj32_local_product_h32t_product_product) + (pa_s_hj32_local_product_h32t_product_product))) /\ pa_s_hj32_local_product_h32t_product_product = pa_r_hj32_local_product_h32t_product_product * pa_p_hj32_local_product_h32t_product_product)))))))
31. 0031have h32t_product_base : 3 * 11 = 33
32. 0032norm_num
33. 0033rewrite h32t_product_base
34. 0034rewrite h32t_product_base
35. 0035exact hh_route
36. 0036have h32t_product : h = x * x1
37. 0037specialize pow_mul_base 3
38. 0038specialize pow_mul_base 11
39. 0039specialize pow_mul_base 2 * 33
40. 0040specialize pow_mul_base x
41. 0041specialize pow_mul_base x1
42. 0042specialize pow_mul_base h
43. 0043apply pow_mul_base
44. 0044exact h32t_p3_exp_witness
45. 0045exact h32t_p11_exp_witness
46. 0046exact h32t_product_graph
47. 0047have h32t_three_power : exists pa_b_hj32_h32t_three_power pa_c_hj32_h32t_three_power. ((forall pa_i_hj32_h32t_three_power_repeat. (exists pa_lt_hj32_h32t_three_power_repeat_bound. pa_lt_hj32_h32t_three_power_repeat_bound + S pa_i_hj32_h32t_three_power_repeat = 5 * 13 + 1) -> (((exists pa_h_hj32_h32t_three_power_repeat_decoded. pa_h_hj32_h32t_three_power_repeat_decoded + S (3) = S ((S (pa_i_hj32_h32t_three_power_repeat)) * pa_c_hj32_h32t_three_power)) /\ exists pa_q_hj32_h32t_three_power_repeat_decoded. pa_b_hj32_h32t_three_power = pa_q_hj32_h32t_three_power_repeat_decoded * S ((S (pa_i_hj32_h32t_three_power_repeat)) * pa_c_hj32_h32t_three_power) + (3)))) /\ (exists pa_u_hj32_h32t_three_power_product pa_v_hj32_h32t_three_power_product. ((((exists pa_h_hj32_h32t_three_power_product_start. pa_h_hj32_h32t_three_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_start. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_start * S ((S (0)) * pa_v_hj32_h32t_three_power_product) + (1))) /\ ((((exists pa_h_hj32_h32t_three_power_product_terminal. pa_h_hj32_h32t_three_power_product_terminal + S (x) = S ((S (5 * 13 + 1)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_terminal. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_terminal * S ((S (5 * 13 + 1)) * pa_v_hj32_h32t_three_power_product) + (x))) /\ forall pa_i_hj32_h32t_three_power_product. (exists pa_lt_hj32_h32t_three_power_product_bound. pa_lt_hj32_h32t_three_power_product_bound + S pa_i_hj32_h32t_three_power_product = 5 * 13 + 1) -> exists pa_p_hj32_h32t_three_power_product pa_r_hj32_h32t_three_power_product pa_s_hj32_h32t_three_power_product. ((((exists pa_h_hj32_h32t_three_power_product_factor. pa_h_hj32_h32t_three_power_product_factor + S (pa_p_hj32_h32t_three_power_product) = S ((S (pa_i_hj32_h32t_three_power_product)) * pa_c_hj32_h32t_three_power)) /\ exists pa_q_hj32_h32t_three_power_product_factor. pa_b_hj32_h32t_three_power = pa_q_hj32_h32t_three_power_product_factor * S ((S (pa_i_hj32_h32t_three_power_product)) * pa_c_hj32_h32t_three_power) + (pa_p_hj32_h32t_three_power_product))) /\ ((((exists pa_h_hj32_h32t_three_power_product_partial. pa_h_hj32_h32t_three_power_product_partial + S (pa_r_hj32_h32t_three_power_product) = S ((S (pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_partial. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_partial * S ((S (pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product) + (pa_r_hj32_h32t_three_power_product))) /\ ((((exists pa_h_hj32_h32t_three_power_product_successor. pa_h_hj32_h32t_three_power_product_successor + S (pa_s_hj32_h32t_three_power_product) = S ((S (S pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product)) /\ exists pa_q_hj32_h32t_three_power_product_successor. pa_u_hj32_h32t_three_power_product = pa_q_hj32_h32t_three_power_product_successor * S ((S (S pa_i_hj32_h32t_three_power_product)) * pa_v_hj32_h32t_three_power_product) + (pa_s_hj32_h32t_three_power_product))) /\ pa_s_hj32_h32t_three_power_product = pa_r_hj32_h32t_three_power_product * pa_p_hj32_h32t_three_power_product)))))))
48. 0048have h32t_three_exponent : 2 * 33 = 5 * 13 + 1
49. 0049norm_num
50. 0050rewrite <- h32t_three_exponent
51. 0051rewrite <- h32t_three_exponent
52. 0052rewrite <- h32t_three_exponent
53. 0053rewrite <- h32t_three_exponent
54. 0054exact h32t_p3_exp_witness
55. 0055have h32t_p4_head : exists hj32_local_value_h32t_p4_head. (exists pa_b_hj32_local_total_h32t_p4_head pa_c_hj32_local_total_h32t_p4_head. ((forall pa_i_hj32_local_total_h32t_p4_head_repeat. (exists pa_lt_hj32_local_total_h32t_p4_head_repeat_bound. pa_lt_hj32_local_total_h32t_p4_head_repeat_bound + S pa_i_hj32_local_total_h32t_p4_head_repeat = 4 * 13 + 1) -> (((exists pa_h_hj32_local_total_h32t_p4_head_repeat_decoded. pa_h_hj32_local_total_h32t_p4_head_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_head_repeat)) * pa_c_hj32_local_total_h32t_p4_head)) /\ exists pa_q_hj32_local_total_h32t_p4_head_repeat_decoded. pa_b_hj32_local_total_h32t_p4_head = pa_q_hj32_local_total_h32t_p4_head_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_head_repeat)) * pa_c_hj32_local_total_h32t_p4_head) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_head_product pa_v_hj32_local_total_h32t_p4_head_product. ((((exists pa_h_hj32_local_total_h32t_p4_head_product_start. pa_h_hj32_local_total_h32t_p4_head_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_start. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_head_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_terminal. pa_h_hj32_local_total_h32t_p4_head_product_terminal + S (hj32_local_value_h32t_p4_head) = S ((S (4 * 13 + 1)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_terminal. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_terminal * S ((S (4 * 13 + 1)) * pa_v_hj32_local_total_h32t_p4_head_product) + (hj32_local_value_h32t_p4_head))) /\ forall pa_i_hj32_local_total_h32t_p4_head_product. (exists pa_lt_hj32_local_total_h32t_p4_head_product_bound. pa_lt_hj32_local_total_h32t_p4_head_product_bound + S pa_i_hj32_local_total_h32t_p4_head_product = 4 * 13 + 1) -> exists pa_p_hj32_local_total_h32t_p4_head_product pa_r_hj32_local_total_h32t_p4_head_product pa_s_hj32_local_total_h32t_p4_head_product. ((((exists pa_h_hj32_local_total_h32t_p4_head_product_factor. pa_h_hj32_local_total_h32t_p4_head_product_factor + S (pa_p_hj32_local_total_h32t_p4_head_product) = S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_c_hj32_local_total_h32t_p4_head)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_factor. pa_b_hj32_local_total_h32t_p4_head = pa_q_hj32_local_total_h32t_p4_head_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_c_hj32_local_total_h32t_p4_head) + (pa_p_hj32_local_total_h32t_p4_head_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_partial. pa_h_hj32_local_total_h32t_p4_head_product_partial + S (pa_r_hj32_local_total_h32t_p4_head_product) = S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_partial. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product) + (pa_r_hj32_local_total_h32t_p4_head_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_head_product_successor. pa_h_hj32_local_total_h32t_p4_head_product_successor + S (pa_s_hj32_local_total_h32t_p4_head_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product)) /\ exists pa_q_hj32_local_total_h32t_p4_head_product_successor. pa_u_hj32_local_total_h32t_p4_head_product = pa_q_hj32_local_total_h32t_p4_head_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_head_product)) * pa_v_hj32_local_total_h32t_p4_head_product) + (pa_s_hj32_local_total_h32t_p4_head_product))) /\ pa_s_hj32_local_total_h32t_p4_head_product = pa_r_hj32_local_total_h32t_p4_head_product * pa_p_hj32_local_total_h32t_p4_head_product))))))))
56. 0056specialize htotal 4
57. 0057specialize htotal 4 * 13 + 1
58. 0058exact htotal
59. 0059cases h32t_p4_head
60. 0060have h32t_three_bound : exists bqb_le_gap_hj32_h32t_three_bound. bqb_le_gap_hj32_h32t_three_bound + (x) = (x2)
61. 0061specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total 13
62. 0062specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x
63. 0063specialize pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total x2
64. 0064apply pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total
65. 0065exact htotal
66. 0066exact h32t_three_power
67. 0067exact h32t_p4_head_witness
68. 0068have h32t_p4_tail : exists hj32_local_value_h32t_p4_tail. (exists pa_b_hj32_local_total_h32t_p4_tail pa_c_hj32_local_total_h32t_p4_tail. ((forall pa_i_hj32_local_total_h32t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h32t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h32t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h32t_p4_tail_repeat = 4 * 29) -> (((exists pa_h_hj32_local_total_h32t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h32t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_repeat)) * pa_c_hj32_local_total_h32t_p4_tail)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h32t_p4_tail = pa_q_hj32_local_total_h32t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_tail_repeat)) * pa_c_hj32_local_total_h32t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_tail_product pa_v_hj32_local_total_h32t_p4_tail_product. ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_start. pa_h_hj32_local_total_h32t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_start. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_terminal. pa_h_hj32_local_total_h32t_p4_tail_product_terminal + S (hj32_local_value_h32t_p4_tail) = S ((S (4 * 29)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_terminal. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_terminal * S ((S (4 * 29)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (hj32_local_value_h32t_p4_tail))) /\ forall pa_i_hj32_local_total_h32t_p4_tail_product. (exists pa_lt_hj32_local_total_h32t_p4_tail_product_bound. pa_lt_hj32_local_total_h32t_p4_tail_product_bound + S pa_i_hj32_local_total_h32t_p4_tail_product = 4 * 29) -> exists pa_p_hj32_local_total_h32t_p4_tail_product pa_r_hj32_local_total_h32t_p4_tail_product pa_s_hj32_local_total_h32t_p4_tail_product. ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_factor. pa_h_hj32_local_total_h32t_p4_tail_product_factor + S (pa_p_hj32_local_total_h32t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_c_hj32_local_total_h32t_p4_tail)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_factor. pa_b_hj32_local_total_h32t_p4_tail = pa_q_hj32_local_total_h32t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_c_hj32_local_total_h32t_p4_tail) + (pa_p_hj32_local_total_h32t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_partial. pa_h_hj32_local_total_h32t_p4_tail_product_partial + S (pa_r_hj32_local_total_h32t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_partial. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (pa_r_hj32_local_total_h32t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_tail_product_successor. pa_h_hj32_local_total_h32t_p4_tail_product_successor + S (pa_s_hj32_local_total_h32t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h32t_p4_tail_product_successor. pa_u_hj32_local_total_h32t_p4_tail_product = pa_q_hj32_local_total_h32t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_tail_product)) * pa_v_hj32_local_total_h32t_p4_tail_product) + (pa_s_hj32_local_total_h32t_p4_tail_product))) /\ pa_s_hj32_local_total_h32t_p4_tail_product = pa_r_hj32_local_total_h32t_p4_tail_product * pa_p_hj32_local_total_h32t_p4_tail_product))))))))
69. 0069specialize htotal 4
70. 0070specialize htotal 4 * 29
71. 0071exact htotal
72. 0072cases h32t_p4_tail
73. 0073have h32t_tail_power : exists pa_b_hj32_h32t_tail_power pa_c_hj32_h32t_tail_power. ((forall pa_i_hj32_h32t_tail_power_repeat. (exists pa_lt_hj32_h32t_tail_power_repeat_bound. pa_lt_hj32_h32t_tail_power_repeat_bound + S pa_i_hj32_h32t_tail_power_repeat = (14 * 8 + 3) + 1) -> (((exists pa_h_hj32_h32t_tail_power_repeat_decoded. pa_h_hj32_h32t_tail_power_repeat_decoded + S (4) = S ((S (pa_i_hj32_h32t_tail_power_repeat)) * pa_c_hj32_h32t_tail_power)) /\ exists pa_q_hj32_h32t_tail_power_repeat_decoded. pa_b_hj32_h32t_tail_power = pa_q_hj32_h32t_tail_power_repeat_decoded * S ((S (pa_i_hj32_h32t_tail_power_repeat)) * pa_c_hj32_h32t_tail_power) + (4)))) /\ (exists pa_u_hj32_h32t_tail_power_product pa_v_hj32_h32t_tail_power_product. ((((exists pa_h_hj32_h32t_tail_power_product_start. pa_h_hj32_h32t_tail_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_start. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_start * S ((S (0)) * pa_v_hj32_h32t_tail_power_product) + (1))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_terminal. pa_h_hj32_h32t_tail_power_product_terminal + S (x3) = S ((S ((14 * 8 + 3) + 1)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_terminal. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_terminal * S ((S ((14 * 8 + 3) + 1)) * pa_v_hj32_h32t_tail_power_product) + (x3))) /\ forall pa_i_hj32_h32t_tail_power_product. (exists pa_lt_hj32_h32t_tail_power_product_bound. pa_lt_hj32_h32t_tail_power_product_bound + S pa_i_hj32_h32t_tail_power_product = (14 * 8 + 3) + 1) -> exists pa_p_hj32_h32t_tail_power_product pa_r_hj32_h32t_tail_power_product pa_s_hj32_h32t_tail_power_product. ((((exists pa_h_hj32_h32t_tail_power_product_factor. pa_h_hj32_h32t_tail_power_product_factor + S (pa_p_hj32_h32t_tail_power_product) = S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_c_hj32_h32t_tail_power)) /\ exists pa_q_hj32_h32t_tail_power_product_factor. pa_b_hj32_h32t_tail_power = pa_q_hj32_h32t_tail_power_product_factor * S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_c_hj32_h32t_tail_power) + (pa_p_hj32_h32t_tail_power_product))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_partial. pa_h_hj32_h32t_tail_power_product_partial + S (pa_r_hj32_h32t_tail_power_product) = S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_partial. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_partial * S ((S (pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product) + (pa_r_hj32_h32t_tail_power_product))) /\ ((((exists pa_h_hj32_h32t_tail_power_product_successor. pa_h_hj32_h32t_tail_power_product_successor + S (pa_s_hj32_h32t_tail_power_product) = S ((S (S pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product)) /\ exists pa_q_hj32_h32t_tail_power_product_successor. pa_u_hj32_h32t_tail_power_product = pa_q_hj32_h32t_tail_power_product_successor * S ((S (S pa_i_hj32_h32t_tail_power_product)) * pa_v_hj32_h32t_tail_power_product) + (pa_s_hj32_h32t_tail_power_product))) /\ pa_s_hj32_h32t_tail_power_product = pa_r_hj32_h32t_tail_power_product * pa_p_hj32_h32t_tail_power_product)))))))
74. 0074have h32t_tail_exponent : (14 * 8 + 3) + 1 = 4 * 29
75. 0075norm_num
76. 0076rewrite h32t_tail_exponent
77. 0077rewrite h32t_tail_exponent
78. 0078rewrite h32t_tail_exponent
79. 0079rewrite h32t_tail_exponent
80. 0080exact h32t_p4_tail_witness
81. 0081have h32t_parity : 7 * 33 = 2 * (14 * 8 + 3) + 1
82. 0082have h32t_parity_left : 7 * 33 = 28 * 8 + 7
83. 0083have h32t_root : 33 = 4 * 8 + 1
84. 0084norm_num
85. 0085rewrite h32t_root
86. 0086have h32t_left_distrib : 7 * (4 * 8 + 1) = 7 * (4 * 8) + 7 * 1
87. 0087specialize mul_add 7
88. 0088specialize mul_add (4 * 8)
89. 0089specialize mul_add 1
90. 0090apply mul_add
91. 0091rewrite h32t_left_distrib
92. 0092have h32t_left_assoc : 7 * (4 * 8) = (7 * 4) * 8
93. 0093symm
94. 0094specialize mul_assoc 7
95. 0095specialize mul_assoc 4
96. 0096specialize mul_assoc 8
97. 0097apply mul_assoc
98. 0098rewrite h32t_left_assoc
99. 0099have h32t_twenty_eight : 7 * 4 = 28
100. 0100norm_num
101. 0101rewrite h32t_twenty_eight
102. 0102have h32t_seven : 7 * 1 = 7
103. 0103norm_num
104. 0104rewrite h32t_seven
105. 0105refl
106. 0106have h32t_parity_right : 2 * (14 * 8 + 3) + 1 = 28 * 8 + 7
107. 0107have h32t_right_distrib : 2 * (14 * 8 + 3) = 2 * (14 * 8) + 2 * 3
108. 0108specialize mul_add 2
109. 0109specialize mul_add (14 * 8)
110. 0110specialize mul_add 3
111. 0111apply mul_add
112. 0112rewrite h32t_right_distrib
113. 0113have h32t_right_assoc : 2 * (14 * 8) = (2 * 14) * 8
114. 0114symm
115. 0115specialize mul_assoc 2
116. 0116specialize mul_assoc 14
117. 0117specialize mul_assoc 8
118. 0118apply mul_assoc
119. 0119rewrite h32t_right_assoc
120. 0120have h32t_right_twenty_eight : 2 * 14 = 28
121. 0121norm_num
122. 0122rewrite h32t_right_twenty_eight
123. 0123have h32t_right_assoc_add : (28 * 8 + 2 * 3) + 1 = 28 * 8 + (2 * 3 + 1)
124. 0124specialize add_assoc (28 * 8)
125. 0125specialize add_assoc (2 * 3)
126. 0126specialize add_assoc 1
127. 0127apply add_assoc
128. 0128rewrite h32t_right_assoc_add
129. 0129have h32t_right_seven : 2 * 3 + 1 = 7
130. 0130norm_num
131. 0131rewrite h32t_right_seven
132. 0132refl
133. 0133trans 28 * 8 + 7
134. 0134exact h32t_parity_left
135. 0135symm
136. 0136exact h32t_parity_right
137. 0137have h32t_eleven_bound : exists bqb_le_gap_hj32_h32t_eleven_bound. bqb_le_gap_hj32_h32t_eleven_bound + (x1) = (x3)
138. 0138specialize pow_eleven_double_block_le_pow_four_odd_from_total 33
139. 0139specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 8 + 3)
140. 0140specialize pow_eleven_double_block_le_pow_four_odd_from_total x1
141. 0141specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
142. 0142apply pow_eleven_double_block_le_pow_four_odd_from_total
143. 0143exact htotal
144. 0144exact h32t_parity
145. 0145exact h32t_p11_exp_witness
146. 0146exact h32t_tail_power
147. 0147have h32t_total_bound : exists bqb_le_gap_hj32_local_product_bound_h32t_total_bound. bqb_le_gap_hj32_local_product_bound_h32t_total_bound + (x * x1) = (x2 * x3)
148. 0148specialize mul_le_mul x
149. 0149specialize mul_le_mul x2
150. 0150specialize mul_le_mul x1
151. 0151specialize mul_le_mul x3
152. 0152apply mul_le_mul
153. 0153exact h32t_three_bound
154. 0154exact h32t_eleven_bound
155. 0155have h32t_p4_budget : exists hj32_local_value_h32t_p4_budget. (exists pa_b_hj32_local_total_h32t_p4_budget pa_c_hj32_local_total_h32t_p4_budget. ((forall pa_i_hj32_local_total_h32t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h32t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h32t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h32t_p4_budget_repeat = (4 * 13 + 1) + 4 * 29) -> (((exists pa_h_hj32_local_total_h32t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h32t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_repeat)) * pa_c_hj32_local_total_h32t_p4_budget)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h32t_p4_budget = pa_q_hj32_local_total_h32t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h32t_p4_budget_repeat)) * pa_c_hj32_local_total_h32t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h32t_p4_budget_product pa_v_hj32_local_total_h32t_p4_budget_product. ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_start. pa_h_hj32_local_total_h32t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_start. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_terminal. pa_h_hj32_local_total_h32t_p4_budget_product_terminal + S (hj32_local_value_h32t_p4_budget) = S ((S ((4 * 13 + 1) + 4 * 29)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_terminal. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_terminal * S ((S ((4 * 13 + 1) + 4 * 29)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (hj32_local_value_h32t_p4_budget))) /\ forall pa_i_hj32_local_total_h32t_p4_budget_product. (exists pa_lt_hj32_local_total_h32t_p4_budget_product_bound. pa_lt_hj32_local_total_h32t_p4_budget_product_bound + S pa_i_hj32_local_total_h32t_p4_budget_product = (4 * 13 + 1) + 4 * 29) -> exists pa_p_hj32_local_total_h32t_p4_budget_product pa_r_hj32_local_total_h32t_p4_budget_product pa_s_hj32_local_total_h32t_p4_budget_product. ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_factor. pa_h_hj32_local_total_h32t_p4_budget_product_factor + S (pa_p_hj32_local_total_h32t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_c_hj32_local_total_h32t_p4_budget)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_factor. pa_b_hj32_local_total_h32t_p4_budget = pa_q_hj32_local_total_h32t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_c_hj32_local_total_h32t_p4_budget) + (pa_p_hj32_local_total_h32t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_partial. pa_h_hj32_local_total_h32t_p4_budget_product_partial + S (pa_r_hj32_local_total_h32t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_partial. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (pa_r_hj32_local_total_h32t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h32t_p4_budget_product_successor. pa_h_hj32_local_total_h32t_p4_budget_product_successor + S (pa_s_hj32_local_total_h32t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h32t_p4_budget_product_successor. pa_u_hj32_local_total_h32t_p4_budget_product = pa_q_hj32_local_total_h32t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h32t_p4_budget_product)) * pa_v_hj32_local_total_h32t_p4_budget_product) + (pa_s_hj32_local_total_h32t_p4_budget_product))) /\ pa_s_hj32_local_total_h32t_p4_budget_product = pa_r_hj32_local_total_h32t_p4_budget_product * pa_p_hj32_local_total_h32t_p4_budget_product))))))))
156. 0156specialize htotal 4
157. 0157specialize htotal (4 * 13 + 1) + 4 * 29
158. 0158exact htotal
159. 0159cases h32t_p4_budget
160. 0160have h32t_budget_product : x4 = x2 * x3
161. 0161specialize pow_add 4
162. 0162specialize pow_add 4 * 13 + 1
163. 0163specialize pow_add 4 * 29
164. 0164specialize pow_add (4 * 13 + 1) + 4 * 29
165. 0165specialize pow_add x2
166. 0166specialize pow_add x3
167. 0167specialize pow_add x4
168. 0168apply pow_add
169. 0169refl
170. 0170exact h32t_p4_head_witness
171. 0171exact h32t_p4_tail_witness
172. 0172exact h32t_p4_budget_witness
173. 0173rewrite <- h32t_product at h32t_total_bound
174. 0174rewrite <- h32t_budget_product at h32t_total_bound
175. 0175have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_32. bqb_le_gap_hj32_scaled_budget_root_32 + (6 * ((4 * 13 + 1) + 4 * 29)) = (32 * 32)
176. 0176apply bertrand_scaled_budget_root_32
177. 0177have hbudget_exponent : exists bqb_le_gap_hj32_h_32_budget_exponent. bqb_le_gap_hj32_h_32_budget_exponent + ((4 * 13 + 1) + 4 * 29) = (e)
178. 0178specialize ceil_div_six_budget_of_scaled_le (32 * 32)
179. 0179specialize ceil_div_six_budget_of_scaled_le ((4 * 13 + 1) + 4 * 29)
180. 0180specialize ceil_div_six_budget_of_scaled_le e
181. 0181apply ceil_div_six_budget_of_scaled_le
182. 0182exact hceiling
183. 0183exact hscaled
184. 0184have h32_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h32_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h32_budget_growth + (x4) = (u)
185. 0185specialize pow_exponent_monotone_from_total 4
186. 0186specialize pow_exponent_monotone_from_total (4 * 13 + 1) + 4 * 29
187. 0187specialize pow_exponent_monotone_from_total e
188. 0188specialize pow_exponent_monotone_from_total x4
189. 0189specialize pow_exponent_monotone_from_total u
190. 0190apply pow_exponent_monotone_from_total
191. 0191exact htotal
192. 0192exists 3
193. 0193norm_num
194. 0194exact hbudget_exponent
195. 0195exact h32t_p4_budget_witness
196. 0196exact hu
197. 0197have h32_result : exists bqb_le_gap_hj32_local_trans_bound_h32_result. bqb_le_gap_hj32_local_trans_bound_h32_result + (h) = (u)
198. 0198specialize le_trans h
199. 0199specialize le_trans x4
200. 0200specialize le_trans u
201. 0201apply le_trans
202. 0202exact h32t_total_bound
203. 0203exact h32_budget_growth
204. 0204exact h32_result