pow_six_six_le_pow_four_eight_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 x
2. 0002intro y
3. 0003intro htotal
4. 0004intro hx
5. 0005intro hy
6. 0006have rs_p3_five : exists hj32_local_value_rs_p3_five. (exists pa_b_hj32_local_total_rs_p3_five pa_c_hj32_local_total_rs_p3_five. ((forall pa_i_hj32_local_total_rs_p3_five_repeat. (exists pa_lt_hj32_local_total_rs_p3_five_repeat_bound. pa_lt_hj32_local_total_rs_p3_five_repeat_bound + S pa_i_hj32_local_total_rs_p3_five_repeat = 5) -> (((exists pa_h_hj32_local_total_rs_p3_five_repeat_decoded. pa_h_hj32_local_total_rs_p3_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_five_repeat)) * pa_c_hj32_local_total_rs_p3_five)) /\ exists pa_q_hj32_local_total_rs_p3_five_repeat_decoded. pa_b_hj32_local_total_rs_p3_five = pa_q_hj32_local_total_rs_p3_five_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_five_repeat)) * pa_c_hj32_local_total_rs_p3_five) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_five_product pa_v_hj32_local_total_rs_p3_five_product. ((((exists pa_h_hj32_local_total_rs_p3_five_product_start. pa_h_hj32_local_total_rs_p3_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_start. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_terminal. pa_h_hj32_local_total_rs_p3_five_product_terminal + S (hj32_local_value_rs_p3_five) = S ((S (5)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_terminal. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_rs_p3_five_product) + (hj32_local_value_rs_p3_five))) /\ forall pa_i_hj32_local_total_rs_p3_five_product. (exists pa_lt_hj32_local_total_rs_p3_five_product_bound. pa_lt_hj32_local_total_rs_p3_five_product_bound + S pa_i_hj32_local_total_rs_p3_five_product = 5) -> exists pa_p_hj32_local_total_rs_p3_five_product pa_r_hj32_local_total_rs_p3_five_product pa_s_hj32_local_total_rs_p3_five_product. ((((exists pa_h_hj32_local_total_rs_p3_five_product_factor. pa_h_hj32_local_total_rs_p3_five_product_factor + S (pa_p_hj32_local_total_rs_p3_five_product) = S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_c_hj32_local_total_rs_p3_five)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_factor. pa_b_hj32_local_total_rs_p3_five = pa_q_hj32_local_total_rs_p3_five_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_c_hj32_local_total_rs_p3_five) + (pa_p_hj32_local_total_rs_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_partial. pa_h_hj32_local_total_rs_p3_five_product_partial + S (pa_r_hj32_local_total_rs_p3_five_product) = S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_partial. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product) + (pa_r_hj32_local_total_rs_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_five_product_successor. pa_h_hj32_local_total_rs_p3_five_product_successor + S (pa_s_hj32_local_total_rs_p3_five_product) = S ((S (S pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product)) /\ exists pa_q_hj32_local_total_rs_p3_five_product_successor. pa_u_hj32_local_total_rs_p3_five_product = pa_q_hj32_local_total_rs_p3_five_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_five_product)) * pa_v_hj32_local_total_rs_p3_five_product) + (pa_s_hj32_local_total_rs_p3_five_product))) /\ pa_s_hj32_local_total_rs_p3_five_product = pa_r_hj32_local_total_rs_p3_five_product * pa_p_hj32_local_total_rs_p3_five_product))))))))
7. 0007specialize htotal 3
8. 0008specialize htotal 5
9. 0009exact htotal
10. 0010cases rs_p3_five
11. 0011have rs_p4_four : exists hj32_local_value_rs_p4_four. (exists pa_b_hj32_local_total_rs_p4_four pa_c_hj32_local_total_rs_p4_four. ((forall pa_i_hj32_local_total_rs_p4_four_repeat. (exists pa_lt_hj32_local_total_rs_p4_four_repeat_bound. pa_lt_hj32_local_total_rs_p4_four_repeat_bound + S pa_i_hj32_local_total_rs_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rs_p4_four_repeat_decoded. pa_h_hj32_local_total_rs_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_four_repeat)) * pa_c_hj32_local_total_rs_p4_four)) /\ exists pa_q_hj32_local_total_rs_p4_four_repeat_decoded. pa_b_hj32_local_total_rs_p4_four = pa_q_hj32_local_total_rs_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_four_repeat)) * pa_c_hj32_local_total_rs_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_four_product pa_v_hj32_local_total_rs_p4_four_product. ((((exists pa_h_hj32_local_total_rs_p4_four_product_start. pa_h_hj32_local_total_rs_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_start. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_terminal. pa_h_hj32_local_total_rs_p4_four_product_terminal + S (hj32_local_value_rs_p4_four) = S ((S (4)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_terminal. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rs_p4_four_product) + (hj32_local_value_rs_p4_four))) /\ forall pa_i_hj32_local_total_rs_p4_four_product. (exists pa_lt_hj32_local_total_rs_p4_four_product_bound. pa_lt_hj32_local_total_rs_p4_four_product_bound + S pa_i_hj32_local_total_rs_p4_four_product = 4) -> exists pa_p_hj32_local_total_rs_p4_four_product pa_r_hj32_local_total_rs_p4_four_product pa_s_hj32_local_total_rs_p4_four_product. ((((exists pa_h_hj32_local_total_rs_p4_four_product_factor. pa_h_hj32_local_total_rs_p4_four_product_factor + S (pa_p_hj32_local_total_rs_p4_four_product) = S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_c_hj32_local_total_rs_p4_four)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_factor. pa_b_hj32_local_total_rs_p4_four = pa_q_hj32_local_total_rs_p4_four_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_c_hj32_local_total_rs_p4_four) + (pa_p_hj32_local_total_rs_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_partial. pa_h_hj32_local_total_rs_p4_four_product_partial + S (pa_r_hj32_local_total_rs_p4_four_product) = S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_partial. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product) + (pa_r_hj32_local_total_rs_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_four_product_successor. pa_h_hj32_local_total_rs_p4_four_product_successor + S (pa_s_hj32_local_total_rs_p4_four_product) = S ((S (S pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product)) /\ exists pa_q_hj32_local_total_rs_p4_four_product_successor. pa_u_hj32_local_total_rs_p4_four_product = pa_q_hj32_local_total_rs_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_four_product)) * pa_v_hj32_local_total_rs_p4_four_product) + (pa_s_hj32_local_total_rs_p4_four_product))) /\ pa_s_hj32_local_total_rs_p4_four_product = pa_r_hj32_local_total_rs_p4_four_product * pa_p_hj32_local_total_rs_p4_four_product))))))))
12. 0012specialize htotal 4
13. 0013specialize htotal 4
14. 0014exact htotal
15. 0015cases rs_p4_four
16. 0016have rs_seed : exists bqb_le_gap_hj32_rs_seed. bqb_le_gap_hj32_rs_seed + (x1) = (x2)
17. 0017specialize pow_three_five_le_pow_four_four_from_total x1
18. 0018specialize pow_three_five_le_pow_four_four_from_total x2
19. 0019apply pow_three_five_le_pow_four_four_from_total
20. 0020exact htotal
21. 0021exact rs_p3_five_witness
22. 0022exact rs_p4_four_witness
23. 0023have rs_p3_one : exists hj32_local_value_rs_p3_one. (exists pa_b_hj32_local_total_rs_p3_one pa_c_hj32_local_total_rs_p3_one. ((forall pa_i_hj32_local_total_rs_p3_one_repeat. (exists pa_lt_hj32_local_total_rs_p3_one_repeat_bound. pa_lt_hj32_local_total_rs_p3_one_repeat_bound + S pa_i_hj32_local_total_rs_p3_one_repeat = 1) -> (((exists pa_h_hj32_local_total_rs_p3_one_repeat_decoded. pa_h_hj32_local_total_rs_p3_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_one_repeat)) * pa_c_hj32_local_total_rs_p3_one)) /\ exists pa_q_hj32_local_total_rs_p3_one_repeat_decoded. pa_b_hj32_local_total_rs_p3_one = pa_q_hj32_local_total_rs_p3_one_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_one_repeat)) * pa_c_hj32_local_total_rs_p3_one) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_one_product pa_v_hj32_local_total_rs_p3_one_product. ((((exists pa_h_hj32_local_total_rs_p3_one_product_start. pa_h_hj32_local_total_rs_p3_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_start. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_terminal. pa_h_hj32_local_total_rs_p3_one_product_terminal + S (hj32_local_value_rs_p3_one) = S ((S (1)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_terminal. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_rs_p3_one_product) + (hj32_local_value_rs_p3_one))) /\ forall pa_i_hj32_local_total_rs_p3_one_product. (exists pa_lt_hj32_local_total_rs_p3_one_product_bound. pa_lt_hj32_local_total_rs_p3_one_product_bound + S pa_i_hj32_local_total_rs_p3_one_product = 1) -> exists pa_p_hj32_local_total_rs_p3_one_product pa_r_hj32_local_total_rs_p3_one_product pa_s_hj32_local_total_rs_p3_one_product. ((((exists pa_h_hj32_local_total_rs_p3_one_product_factor. pa_h_hj32_local_total_rs_p3_one_product_factor + S (pa_p_hj32_local_total_rs_p3_one_product) = S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_c_hj32_local_total_rs_p3_one)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_factor. pa_b_hj32_local_total_rs_p3_one = pa_q_hj32_local_total_rs_p3_one_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_c_hj32_local_total_rs_p3_one) + (pa_p_hj32_local_total_rs_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_partial. pa_h_hj32_local_total_rs_p3_one_product_partial + S (pa_r_hj32_local_total_rs_p3_one_product) = S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_partial. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product) + (pa_r_hj32_local_total_rs_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_one_product_successor. pa_h_hj32_local_total_rs_p3_one_product_successor + S (pa_s_hj32_local_total_rs_p3_one_product) = S ((S (S pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product)) /\ exists pa_q_hj32_local_total_rs_p3_one_product_successor. pa_u_hj32_local_total_rs_p3_one_product = pa_q_hj32_local_total_rs_p3_one_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_one_product)) * pa_v_hj32_local_total_rs_p3_one_product) + (pa_s_hj32_local_total_rs_p3_one_product))) /\ pa_s_hj32_local_total_rs_p3_one_product = pa_r_hj32_local_total_rs_p3_one_product * pa_p_hj32_local_total_rs_p3_one_product))))))))
24. 0024specialize htotal 3
25. 0025specialize htotal 1
26. 0026exact htotal
27. 0027cases rs_p3_one
28. 0028have rs_p4_one : exists hj32_local_value_rs_p4_one. (exists pa_b_hj32_local_total_rs_p4_one pa_c_hj32_local_total_rs_p4_one. ((forall pa_i_hj32_local_total_rs_p4_one_repeat. (exists pa_lt_hj32_local_total_rs_p4_one_repeat_bound. pa_lt_hj32_local_total_rs_p4_one_repeat_bound + S pa_i_hj32_local_total_rs_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_rs_p4_one_repeat_decoded. pa_h_hj32_local_total_rs_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_one_repeat)) * pa_c_hj32_local_total_rs_p4_one)) /\ exists pa_q_hj32_local_total_rs_p4_one_repeat_decoded. pa_b_hj32_local_total_rs_p4_one = pa_q_hj32_local_total_rs_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_one_repeat)) * pa_c_hj32_local_total_rs_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_one_product pa_v_hj32_local_total_rs_p4_one_product. ((((exists pa_h_hj32_local_total_rs_p4_one_product_start. pa_h_hj32_local_total_rs_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_start. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_terminal. pa_h_hj32_local_total_rs_p4_one_product_terminal + S (hj32_local_value_rs_p4_one) = S ((S (1)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_terminal. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_rs_p4_one_product) + (hj32_local_value_rs_p4_one))) /\ forall pa_i_hj32_local_total_rs_p4_one_product. (exists pa_lt_hj32_local_total_rs_p4_one_product_bound. pa_lt_hj32_local_total_rs_p4_one_product_bound + S pa_i_hj32_local_total_rs_p4_one_product = 1) -> exists pa_p_hj32_local_total_rs_p4_one_product pa_r_hj32_local_total_rs_p4_one_product pa_s_hj32_local_total_rs_p4_one_product. ((((exists pa_h_hj32_local_total_rs_p4_one_product_factor. pa_h_hj32_local_total_rs_p4_one_product_factor + S (pa_p_hj32_local_total_rs_p4_one_product) = S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_c_hj32_local_total_rs_p4_one)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_factor. pa_b_hj32_local_total_rs_p4_one = pa_q_hj32_local_total_rs_p4_one_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_c_hj32_local_total_rs_p4_one) + (pa_p_hj32_local_total_rs_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_partial. pa_h_hj32_local_total_rs_p4_one_product_partial + S (pa_r_hj32_local_total_rs_p4_one_product) = S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_partial. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product) + (pa_r_hj32_local_total_rs_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_one_product_successor. pa_h_hj32_local_total_rs_p4_one_product_successor + S (pa_s_hj32_local_total_rs_p4_one_product) = S ((S (S pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product)) /\ exists pa_q_hj32_local_total_rs_p4_one_product_successor. pa_u_hj32_local_total_rs_p4_one_product = pa_q_hj32_local_total_rs_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_one_product)) * pa_v_hj32_local_total_rs_p4_one_product) + (pa_s_hj32_local_total_rs_p4_one_product))) /\ pa_s_hj32_local_total_rs_p4_one_product = pa_r_hj32_local_total_rs_p4_one_product * pa_p_hj32_local_total_rs_p4_one_product))))))))
29. 0029specialize htotal 4
30. 0030specialize htotal 1
31. 0031exact htotal
32. 0032cases rs_p4_one
33. 0033have rs_base : exists bqb_le_gap_hj32_rs_base. bqb_le_gap_hj32_rs_base + (3) = (4)
34. 0034exists 1
35. 0035norm_num
36. 0036have rs_one_bound : exists bqb_le_gap_hj32_local_base_bound_rs_one_bound. bqb_le_gap_hj32_local_base_bound_rs_one_bound + (x3) = (x4)
37. 0037specialize pow_base_monotone 3
38. 0038specialize pow_base_monotone 4
39. 0039specialize pow_base_monotone 1
40. 0040specialize pow_base_monotone x3
41. 0041specialize pow_base_monotone x4
42. 0042apply pow_base_monotone
43. 0043exact rs_base
44. 0044exact rs_p3_one_witness
45. 0045exact rs_p4_one_witness
46. 0046have rs_p3_six : exists hj32_local_value_rs_p3_six. (exists pa_b_hj32_local_total_rs_p3_six pa_c_hj32_local_total_rs_p3_six. ((forall pa_i_hj32_local_total_rs_p3_six_repeat. (exists pa_lt_hj32_local_total_rs_p3_six_repeat_bound. pa_lt_hj32_local_total_rs_p3_six_repeat_bound + S pa_i_hj32_local_total_rs_p3_six_repeat = 6) -> (((exists pa_h_hj32_local_total_rs_p3_six_repeat_decoded. pa_h_hj32_local_total_rs_p3_six_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rs_p3_six_repeat)) * pa_c_hj32_local_total_rs_p3_six)) /\ exists pa_q_hj32_local_total_rs_p3_six_repeat_decoded. pa_b_hj32_local_total_rs_p3_six = pa_q_hj32_local_total_rs_p3_six_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p3_six_repeat)) * pa_c_hj32_local_total_rs_p3_six) + (3)))) /\ (exists pa_u_hj32_local_total_rs_p3_six_product pa_v_hj32_local_total_rs_p3_six_product. ((((exists pa_h_hj32_local_total_rs_p3_six_product_start. pa_h_hj32_local_total_rs_p3_six_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_start. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p3_six_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_terminal. pa_h_hj32_local_total_rs_p3_six_product_terminal + S (hj32_local_value_rs_p3_six) = S ((S (6)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_terminal. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_terminal * S ((S (6)) * pa_v_hj32_local_total_rs_p3_six_product) + (hj32_local_value_rs_p3_six))) /\ forall pa_i_hj32_local_total_rs_p3_six_product. (exists pa_lt_hj32_local_total_rs_p3_six_product_bound. pa_lt_hj32_local_total_rs_p3_six_product_bound + S pa_i_hj32_local_total_rs_p3_six_product = 6) -> exists pa_p_hj32_local_total_rs_p3_six_product pa_r_hj32_local_total_rs_p3_six_product pa_s_hj32_local_total_rs_p3_six_product. ((((exists pa_h_hj32_local_total_rs_p3_six_product_factor. pa_h_hj32_local_total_rs_p3_six_product_factor + S (pa_p_hj32_local_total_rs_p3_six_product) = S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_c_hj32_local_total_rs_p3_six)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_factor. pa_b_hj32_local_total_rs_p3_six = pa_q_hj32_local_total_rs_p3_six_product_factor * S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_c_hj32_local_total_rs_p3_six) + (pa_p_hj32_local_total_rs_p3_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_partial. pa_h_hj32_local_total_rs_p3_six_product_partial + S (pa_r_hj32_local_total_rs_p3_six_product) = S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_partial. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_partial * S ((S (pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product) + (pa_r_hj32_local_total_rs_p3_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p3_six_product_successor. pa_h_hj32_local_total_rs_p3_six_product_successor + S (pa_s_hj32_local_total_rs_p3_six_product) = S ((S (S pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product)) /\ exists pa_q_hj32_local_total_rs_p3_six_product_successor. pa_u_hj32_local_total_rs_p3_six_product = pa_q_hj32_local_total_rs_p3_six_product_successor * S ((S (S pa_i_hj32_local_total_rs_p3_six_product)) * pa_v_hj32_local_total_rs_p3_six_product) + (pa_s_hj32_local_total_rs_p3_six_product))) /\ pa_s_hj32_local_total_rs_p3_six_product = pa_r_hj32_local_total_rs_p3_six_product * pa_p_hj32_local_total_rs_p3_six_product))))))))
47. 0047specialize htotal 3
48. 0048specialize htotal 6
49. 0049exact htotal
50. 0050cases rs_p3_six
51. 0051have rs_p4_five : exists hj32_local_value_rs_p4_five. (exists pa_b_hj32_local_total_rs_p4_five pa_c_hj32_local_total_rs_p4_five. ((forall pa_i_hj32_local_total_rs_p4_five_repeat. (exists pa_lt_hj32_local_total_rs_p4_five_repeat_bound. pa_lt_hj32_local_total_rs_p4_five_repeat_bound + S pa_i_hj32_local_total_rs_p4_five_repeat = 5) -> (((exists pa_h_hj32_local_total_rs_p4_five_repeat_decoded. pa_h_hj32_local_total_rs_p4_five_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_five_repeat)) * pa_c_hj32_local_total_rs_p4_five)) /\ exists pa_q_hj32_local_total_rs_p4_five_repeat_decoded. pa_b_hj32_local_total_rs_p4_five = pa_q_hj32_local_total_rs_p4_five_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_five_repeat)) * pa_c_hj32_local_total_rs_p4_five) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_five_product pa_v_hj32_local_total_rs_p4_five_product. ((((exists pa_h_hj32_local_total_rs_p4_five_product_start. pa_h_hj32_local_total_rs_p4_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_start. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_terminal. pa_h_hj32_local_total_rs_p4_five_product_terminal + S (hj32_local_value_rs_p4_five) = S ((S (5)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_terminal. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_rs_p4_five_product) + (hj32_local_value_rs_p4_five))) /\ forall pa_i_hj32_local_total_rs_p4_five_product. (exists pa_lt_hj32_local_total_rs_p4_five_product_bound. pa_lt_hj32_local_total_rs_p4_five_product_bound + S pa_i_hj32_local_total_rs_p4_five_product = 5) -> exists pa_p_hj32_local_total_rs_p4_five_product pa_r_hj32_local_total_rs_p4_five_product pa_s_hj32_local_total_rs_p4_five_product. ((((exists pa_h_hj32_local_total_rs_p4_five_product_factor. pa_h_hj32_local_total_rs_p4_five_product_factor + S (pa_p_hj32_local_total_rs_p4_five_product) = S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_c_hj32_local_total_rs_p4_five)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_factor. pa_b_hj32_local_total_rs_p4_five = pa_q_hj32_local_total_rs_p4_five_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_c_hj32_local_total_rs_p4_five) + (pa_p_hj32_local_total_rs_p4_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_partial. pa_h_hj32_local_total_rs_p4_five_product_partial + S (pa_r_hj32_local_total_rs_p4_five_product) = S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_partial. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product) + (pa_r_hj32_local_total_rs_p4_five_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_five_product_successor. pa_h_hj32_local_total_rs_p4_five_product_successor + S (pa_s_hj32_local_total_rs_p4_five_product) = S ((S (S pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product)) /\ exists pa_q_hj32_local_total_rs_p4_five_product_successor. pa_u_hj32_local_total_rs_p4_five_product = pa_q_hj32_local_total_rs_p4_five_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_five_product)) * pa_v_hj32_local_total_rs_p4_five_product) + (pa_s_hj32_local_total_rs_p4_five_product))) /\ pa_s_hj32_local_total_rs_p4_five_product = pa_r_hj32_local_total_rs_p4_five_product * pa_p_hj32_local_total_rs_p4_five_product))))))))
52. 0052specialize htotal 4
53. 0053specialize htotal 5
54. 0054exact htotal
55. 0055cases rs_p4_five
56. 0056have rs_three_product : x5 = x1 * x3
57. 0057specialize pow_add 3
58. 0058specialize pow_add 5
59. 0059specialize pow_add 1
60. 0060specialize pow_add 6
61. 0061specialize pow_add x1
62. 0062specialize pow_add x3
63. 0063specialize pow_add x5
64. 0064apply pow_add
65. 0065norm_num
66. 0066exact rs_p3_five_witness
67. 0067exact rs_p3_one_witness
68. 0068exact rs_p3_six_witness
69. 0069have rs_four_product : x6 = x2 * x4
70. 0070specialize pow_add 4
71. 0071specialize pow_add 4
72. 0072specialize pow_add 1
73. 0073specialize pow_add 5
74. 0074specialize pow_add x2
75. 0075specialize pow_add x4
76. 0076specialize pow_add x6
77. 0077apply pow_add
78. 0078norm_num
79. 0079exact rs_p4_four_witness
80. 0080exact rs_p4_one_witness
81. 0081exact rs_p4_five_witness
82. 0082have rs_three_bound : exists bqb_le_gap_hj32_local_product_bound_rs_three_bound. bqb_le_gap_hj32_local_product_bound_rs_three_bound + (x1 * x3) = (x2 * x4)
83. 0083specialize mul_le_mul x1
84. 0084specialize mul_le_mul x2
85. 0085specialize mul_le_mul x3
86. 0086specialize mul_le_mul x4
87. 0087apply mul_le_mul
88. 0088exact rs_seed
89. 0089exact rs_one_bound
90. 0090rewrite <- rs_three_product at rs_three_bound
91. 0091rewrite <- rs_four_product at rs_three_bound
92. 0092have rs_seeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product))))))))
93. 0093apply pow_two_seed_bundle_from_total
94. 0094exact htotal
95. 0095cases rs_seeds
96. 0096have rs_p2_six : exists hj32_local_value_rs_p2_six. (exists pa_b_hj32_local_total_rs_p2_six pa_c_hj32_local_total_rs_p2_six. ((forall pa_i_hj32_local_total_rs_p2_six_repeat. (exists pa_lt_hj32_local_total_rs_p2_six_repeat_bound. pa_lt_hj32_local_total_rs_p2_six_repeat_bound + S pa_i_hj32_local_total_rs_p2_six_repeat = 6) -> (((exists pa_h_hj32_local_total_rs_p2_six_repeat_decoded. pa_h_hj32_local_total_rs_p2_six_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_rs_p2_six_repeat)) * pa_c_hj32_local_total_rs_p2_six)) /\ exists pa_q_hj32_local_total_rs_p2_six_repeat_decoded. pa_b_hj32_local_total_rs_p2_six = pa_q_hj32_local_total_rs_p2_six_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p2_six_repeat)) * pa_c_hj32_local_total_rs_p2_six) + (2)))) /\ (exists pa_u_hj32_local_total_rs_p2_six_product pa_v_hj32_local_total_rs_p2_six_product. ((((exists pa_h_hj32_local_total_rs_p2_six_product_start. pa_h_hj32_local_total_rs_p2_six_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_start. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p2_six_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_terminal. pa_h_hj32_local_total_rs_p2_six_product_terminal + S (hj32_local_value_rs_p2_six) = S ((S (6)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_terminal. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_terminal * S ((S (6)) * pa_v_hj32_local_total_rs_p2_six_product) + (hj32_local_value_rs_p2_six))) /\ forall pa_i_hj32_local_total_rs_p2_six_product. (exists pa_lt_hj32_local_total_rs_p2_six_product_bound. pa_lt_hj32_local_total_rs_p2_six_product_bound + S pa_i_hj32_local_total_rs_p2_six_product = 6) -> exists pa_p_hj32_local_total_rs_p2_six_product pa_r_hj32_local_total_rs_p2_six_product pa_s_hj32_local_total_rs_p2_six_product. ((((exists pa_h_hj32_local_total_rs_p2_six_product_factor. pa_h_hj32_local_total_rs_p2_six_product_factor + S (pa_p_hj32_local_total_rs_p2_six_product) = S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_c_hj32_local_total_rs_p2_six)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_factor. pa_b_hj32_local_total_rs_p2_six = pa_q_hj32_local_total_rs_p2_six_product_factor * S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_c_hj32_local_total_rs_p2_six) + (pa_p_hj32_local_total_rs_p2_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_partial. pa_h_hj32_local_total_rs_p2_six_product_partial + S (pa_r_hj32_local_total_rs_p2_six_product) = S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_partial. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_partial * S ((S (pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product) + (pa_r_hj32_local_total_rs_p2_six_product))) /\ ((((exists pa_h_hj32_local_total_rs_p2_six_product_successor. pa_h_hj32_local_total_rs_p2_six_product_successor + S (pa_s_hj32_local_total_rs_p2_six_product) = S ((S (S pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product)) /\ exists pa_q_hj32_local_total_rs_p2_six_product_successor. pa_u_hj32_local_total_rs_p2_six_product = pa_q_hj32_local_total_rs_p2_six_product_successor * S ((S (S pa_i_hj32_local_total_rs_p2_six_product)) * pa_v_hj32_local_total_rs_p2_six_product) + (pa_s_hj32_local_total_rs_p2_six_product))) /\ pa_s_hj32_local_total_rs_p2_six_product = pa_r_hj32_local_total_rs_p2_six_product * pa_p_hj32_local_total_rs_p2_six_product))))))))
97. 0097specialize htotal 2
98. 0098specialize htotal 6
99. 0099exact htotal
100. 0100cases rs_p2_six
101. 0101have rs_p4_three : exists hj32_local_value_rs_p4_three. (exists pa_b_hj32_local_total_rs_p4_three pa_c_hj32_local_total_rs_p4_three. ((forall pa_i_hj32_local_total_rs_p4_three_repeat. (exists pa_lt_hj32_local_total_rs_p4_three_repeat_bound. pa_lt_hj32_local_total_rs_p4_three_repeat_bound + S pa_i_hj32_local_total_rs_p4_three_repeat = 3) -> (((exists pa_h_hj32_local_total_rs_p4_three_repeat_decoded. pa_h_hj32_local_total_rs_p4_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rs_p4_three_repeat)) * pa_c_hj32_local_total_rs_p4_three)) /\ exists pa_q_hj32_local_total_rs_p4_three_repeat_decoded. pa_b_hj32_local_total_rs_p4_three = pa_q_hj32_local_total_rs_p4_three_repeat_decoded * S ((S (pa_i_hj32_local_total_rs_p4_three_repeat)) * pa_c_hj32_local_total_rs_p4_three) + (4)))) /\ (exists pa_u_hj32_local_total_rs_p4_three_product pa_v_hj32_local_total_rs_p4_three_product. ((((exists pa_h_hj32_local_total_rs_p4_three_product_start. pa_h_hj32_local_total_rs_p4_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_start. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_start * S ((S (0)) * pa_v_hj32_local_total_rs_p4_three_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_terminal. pa_h_hj32_local_total_rs_p4_three_product_terminal + S (hj32_local_value_rs_p4_three) = S ((S (3)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_terminal. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_terminal * S ((S (3)) * pa_v_hj32_local_total_rs_p4_three_product) + (hj32_local_value_rs_p4_three))) /\ forall pa_i_hj32_local_total_rs_p4_three_product. (exists pa_lt_hj32_local_total_rs_p4_three_product_bound. pa_lt_hj32_local_total_rs_p4_three_product_bound + S pa_i_hj32_local_total_rs_p4_three_product = 3) -> exists pa_p_hj32_local_total_rs_p4_three_product pa_r_hj32_local_total_rs_p4_three_product pa_s_hj32_local_total_rs_p4_three_product. ((((exists pa_h_hj32_local_total_rs_p4_three_product_factor. pa_h_hj32_local_total_rs_p4_three_product_factor + S (pa_p_hj32_local_total_rs_p4_three_product) = S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_c_hj32_local_total_rs_p4_three)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_factor. pa_b_hj32_local_total_rs_p4_three = pa_q_hj32_local_total_rs_p4_three_product_factor * S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_c_hj32_local_total_rs_p4_three) + (pa_p_hj32_local_total_rs_p4_three_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_partial. pa_h_hj32_local_total_rs_p4_three_product_partial + S (pa_r_hj32_local_total_rs_p4_three_product) = S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_partial. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_partial * S ((S (pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product) + (pa_r_hj32_local_total_rs_p4_three_product))) /\ ((((exists pa_h_hj32_local_total_rs_p4_three_product_successor. pa_h_hj32_local_total_rs_p4_three_product_successor + S (pa_s_hj32_local_total_rs_p4_three_product) = S ((S (S pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product)) /\ exists pa_q_hj32_local_total_rs_p4_three_product_successor. pa_u_hj32_local_total_rs_p4_three_product = pa_q_hj32_local_total_rs_p4_three_product_successor * S ((S (S pa_i_hj32_local_total_rs_p4_three_product)) * pa_v_hj32_local_total_rs_p4_three_product) + (pa_s_hj32_local_total_rs_p4_three_product))) /\ pa_s_hj32_local_total_rs_p4_three_product = pa_r_hj32_local_total_rs_p4_three_product * pa_p_hj32_local_total_rs_p4_three_product))))))))
102. 0102specialize htotal 4
103. 0103specialize htotal 3
104. 0104exact htotal
105. 0105cases rs_p4_three
106. 0106have rs_two_bridge : x8 = x7
107. 0107specialize pow_mul_exp_from_total 2
108. 0108specialize pow_mul_exp_from_total 2
109. 0109specialize pow_mul_exp_from_total 3
110. 0110specialize pow_mul_exp_from_total 6
111. 0111specialize pow_mul_exp_from_total 4
112. 0112specialize pow_mul_exp_from_total x8
113. 0113specialize pow_mul_exp_from_total x7
114. 0114apply pow_mul_exp_from_total
115. 0115exact htotal
116. 0116norm_num
117. 0117exact rs_seeds_left
118. 0118exact rs_p4_three_witness
119. 0119exact rs_p2_six_witness
120. 0120have rs_two_bound : exists bqb_le_gap_hj32_rs_two_bound. bqb_le_gap_hj32_rs_two_bound + (x7) = (x8)
121. 0121rewrite rs_two_bridge
122. 0122specialize le_refl x7
123. 0123exact le_refl
124. 0124have rs_six_product_graph : exists pa_b_hj32_local_product_rs_six_product pa_c_hj32_local_product_rs_six_product. ((forall pa_i_hj32_local_product_rs_six_product_repeat. (exists pa_lt_hj32_local_product_rs_six_product_repeat_bound. pa_lt_hj32_local_product_rs_six_product_repeat_bound + S pa_i_hj32_local_product_rs_six_product_repeat = 6) -> (((exists pa_h_hj32_local_product_rs_six_product_repeat_decoded. pa_h_hj32_local_product_rs_six_product_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_local_product_rs_six_product_repeat)) * pa_c_hj32_local_product_rs_six_product)) /\ exists pa_q_hj32_local_product_rs_six_product_repeat_decoded. pa_b_hj32_local_product_rs_six_product = pa_q_hj32_local_product_rs_six_product_repeat_decoded * S ((S (pa_i_hj32_local_product_rs_six_product_repeat)) * pa_c_hj32_local_product_rs_six_product) + (2 * 3)))) /\ (exists pa_u_hj32_local_product_rs_six_product_product pa_v_hj32_local_product_rs_six_product_product. ((((exists pa_h_hj32_local_product_rs_six_product_product_start. pa_h_hj32_local_product_rs_six_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_start. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_start * S ((S (0)) * pa_v_hj32_local_product_rs_six_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_terminal. pa_h_hj32_local_product_rs_six_product_product_terminal + S (x) = S ((S (6)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_terminal. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_terminal * S ((S (6)) * pa_v_hj32_local_product_rs_six_product_product) + (x))) /\ forall pa_i_hj32_local_product_rs_six_product_product. (exists pa_lt_hj32_local_product_rs_six_product_product_bound. pa_lt_hj32_local_product_rs_six_product_product_bound + S pa_i_hj32_local_product_rs_six_product_product = 6) -> exists pa_p_hj32_local_product_rs_six_product_product pa_r_hj32_local_product_rs_six_product_product pa_s_hj32_local_product_rs_six_product_product. ((((exists pa_h_hj32_local_product_rs_six_product_product_factor. pa_h_hj32_local_product_rs_six_product_product_factor + S (pa_p_hj32_local_product_rs_six_product_product) = S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_c_hj32_local_product_rs_six_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_factor. pa_b_hj32_local_product_rs_six_product = pa_q_hj32_local_product_rs_six_product_product_factor * S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_c_hj32_local_product_rs_six_product) + (pa_p_hj32_local_product_rs_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_partial. pa_h_hj32_local_product_rs_six_product_product_partial + S (pa_r_hj32_local_product_rs_six_product_product) = S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_partial. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_partial * S ((S (pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product) + (pa_r_hj32_local_product_rs_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rs_six_product_product_successor. pa_h_hj32_local_product_rs_six_product_product_successor + S (pa_s_hj32_local_product_rs_six_product_product) = S ((S (S pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product)) /\ exists pa_q_hj32_local_product_rs_six_product_product_successor. pa_u_hj32_local_product_rs_six_product_product = pa_q_hj32_local_product_rs_six_product_product_successor * S ((S (S pa_i_hj32_local_product_rs_six_product_product)) * pa_v_hj32_local_product_rs_six_product_product) + (pa_s_hj32_local_product_rs_six_product_product))) /\ pa_s_hj32_local_product_rs_six_product_product = pa_r_hj32_local_product_rs_six_product_product * pa_p_hj32_local_product_rs_six_product_product)))))))
125. 0125have rs_six_product_base : 2 * 3 = 6
126. 0126norm_num
127. 0127rewrite rs_six_product_base
128. 0128rewrite rs_six_product_base
129. 0129exact hx
130. 0130have rs_six_product : x = x7 * x5
131. 0131specialize pow_mul_base 2
132. 0132specialize pow_mul_base 3
133. 0133specialize pow_mul_base 6
134. 0134specialize pow_mul_base x7
135. 0135specialize pow_mul_base x5
136. 0136specialize pow_mul_base x
137. 0137apply pow_mul_base
138. 0138exact rs_p2_six_witness
139. 0139exact rs_p3_six_witness
140. 0140exact rs_six_product_graph
141. 0141have rs_eight_product : y = x8 * x6
142. 0142specialize pow_add 4
143. 0143specialize pow_add 3
144. 0144specialize pow_add 5
145. 0145specialize pow_add 8
146. 0146specialize pow_add x8
147. 0147specialize pow_add x6
148. 0148specialize pow_add y
149. 0149apply pow_add
150. 0150norm_num
151. 0151exact rs_p4_three_witness
152. 0152exact rs_p4_five_witness
153. 0153exact hy
154. 0154have rs_result : exists bqb_le_gap_hj32_local_product_bound_rs_result. bqb_le_gap_hj32_local_product_bound_rs_result + (x7 * x5) = (x8 * x6)
155. 0155specialize mul_le_mul x7
156. 0156specialize mul_le_mul x8
157. 0157specialize mul_le_mul x5
158. 0158specialize mul_le_mul x6
159. 0159apply mul_le_mul
160. 0160exact rs_two_bound
161. 0161exact rs_three_bound
162. 0162rewrite <- rs_six_product at rs_result
163. 0163rewrite <- rs_eight_product at rs_result
164. 0164exact rs_result