bertrand_j_base_thirty_two_window_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 s
2. 0002intro j
3. 0003intro g
4. 0004intro htotal
5. 0005intro hlower
6. 0006intro hupper
7. 0007intro hj
8. 0008intro hg
9. 0009have j_p11_block : exists hj32_local_value_j_p11_block. (exists pa_b_hj32_local_total_j_p11_block pa_c_hj32_local_total_j_p11_block. ((forall pa_i_hj32_local_total_j_p11_block_repeat. (exists pa_lt_hj32_local_total_j_p11_block_repeat_bound. pa_lt_hj32_local_total_j_p11_block_repeat_bound + S pa_i_hj32_local_total_j_p11_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p11_block_repeat_decoded. pa_h_hj32_local_total_j_p11_block_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_j_p11_block_repeat)) * pa_c_hj32_local_total_j_p11_block)) /\ exists pa_q_hj32_local_total_j_p11_block_repeat_decoded. pa_b_hj32_local_total_j_p11_block = pa_q_hj32_local_total_j_p11_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p11_block_repeat)) * pa_c_hj32_local_total_j_p11_block) + (11)))) /\ (exists pa_u_hj32_local_total_j_p11_block_product pa_v_hj32_local_total_j_p11_block_product. ((((exists pa_h_hj32_local_total_j_p11_block_product_start. pa_h_hj32_local_total_j_p11_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_start. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p11_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_terminal. pa_h_hj32_local_total_j_p11_block_product_terminal + S (hj32_local_value_j_p11_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_terminal. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p11_block_product) + (hj32_local_value_j_p11_block))) /\ forall pa_i_hj32_local_total_j_p11_block_product. (exists pa_lt_hj32_local_total_j_p11_block_product_bound. pa_lt_hj32_local_total_j_p11_block_product_bound + S pa_i_hj32_local_total_j_p11_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p11_block_product pa_r_hj32_local_total_j_p11_block_product pa_s_hj32_local_total_j_p11_block_product. ((((exists pa_h_hj32_local_total_j_p11_block_product_factor. pa_h_hj32_local_total_j_p11_block_product_factor + S (pa_p_hj32_local_total_j_p11_block_product) = S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_c_hj32_local_total_j_p11_block)) /\ exists pa_q_hj32_local_total_j_p11_block_product_factor. pa_b_hj32_local_total_j_p11_block = pa_q_hj32_local_total_j_p11_block_product_factor * S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_c_hj32_local_total_j_p11_block) + (pa_p_hj32_local_total_j_p11_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_partial. pa_h_hj32_local_total_j_p11_block_product_partial + S (pa_r_hj32_local_total_j_p11_block_product) = S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_partial. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_partial * S ((S (pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product) + (pa_r_hj32_local_total_j_p11_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p11_block_product_successor. pa_h_hj32_local_total_j_p11_block_product_successor + S (pa_s_hj32_local_total_j_p11_block_product) = S ((S (S pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product)) /\ exists pa_q_hj32_local_total_j_p11_block_product_successor. pa_u_hj32_local_total_j_p11_block_product = pa_q_hj32_local_total_j_p11_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p11_block_product)) * pa_v_hj32_local_total_j_p11_block_product) + (pa_s_hj32_local_total_j_p11_block_product))) /\ pa_s_hj32_local_total_j_p11_block_product = pa_r_hj32_local_total_j_p11_block_product * pa_p_hj32_local_total_j_p11_block_product))))))))
10. 0010specialize htotal 11
11. 0011specialize htotal 2 * 6
12. 0012exact htotal
13. 0013cases j_p11_block
14. 0014have j_p4_twenty_one : exists hj32_local_value_j_p4_twenty_one. (exists pa_b_hj32_local_total_j_p4_twenty_one pa_c_hj32_local_total_j_p4_twenty_one. ((forall pa_i_hj32_local_total_j_p4_twenty_one_repeat. (exists pa_lt_hj32_local_total_j_p4_twenty_one_repeat_bound. pa_lt_hj32_local_total_j_p4_twenty_one_repeat_bound + S pa_i_hj32_local_total_j_p4_twenty_one_repeat = 21) -> (((exists pa_h_hj32_local_total_j_p4_twenty_one_repeat_decoded. pa_h_hj32_local_total_j_p4_twenty_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_repeat)) * pa_c_hj32_local_total_j_p4_twenty_one)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_repeat_decoded. pa_b_hj32_local_total_j_p4_twenty_one = pa_q_hj32_local_total_j_p4_twenty_one_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_repeat)) * pa_c_hj32_local_total_j_p4_twenty_one) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_twenty_one_product pa_v_hj32_local_total_j_p4_twenty_one_product. ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_start. pa_h_hj32_local_total_j_p4_twenty_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_start. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_terminal. pa_h_hj32_local_total_j_p4_twenty_one_product_terminal + S (hj32_local_value_j_p4_twenty_one) = S ((S (21)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_terminal. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_terminal * S ((S (21)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (hj32_local_value_j_p4_twenty_one))) /\ forall pa_i_hj32_local_total_j_p4_twenty_one_product. (exists pa_lt_hj32_local_total_j_p4_twenty_one_product_bound. pa_lt_hj32_local_total_j_p4_twenty_one_product_bound + S pa_i_hj32_local_total_j_p4_twenty_one_product = 21) -> exists pa_p_hj32_local_total_j_p4_twenty_one_product pa_r_hj32_local_total_j_p4_twenty_one_product pa_s_hj32_local_total_j_p4_twenty_one_product. ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_factor. pa_h_hj32_local_total_j_p4_twenty_one_product_factor + S (pa_p_hj32_local_total_j_p4_twenty_one_product) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_c_hj32_local_total_j_p4_twenty_one)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_factor. pa_b_hj32_local_total_j_p4_twenty_one = pa_q_hj32_local_total_j_p4_twenty_one_product_factor * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_c_hj32_local_total_j_p4_twenty_one) + (pa_p_hj32_local_total_j_p4_twenty_one_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_partial. pa_h_hj32_local_total_j_p4_twenty_one_product_partial + S (pa_r_hj32_local_total_j_p4_twenty_one_product) = S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_partial. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_partial * S ((S (pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (pa_r_hj32_local_total_j_p4_twenty_one_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_twenty_one_product_successor. pa_h_hj32_local_total_j_p4_twenty_one_product_successor + S (pa_s_hj32_local_total_j_p4_twenty_one_product) = S ((S (S pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product)) /\ exists pa_q_hj32_local_total_j_p4_twenty_one_product_successor. pa_u_hj32_local_total_j_p4_twenty_one_product = pa_q_hj32_local_total_j_p4_twenty_one_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_twenty_one_product)) * pa_v_hj32_local_total_j_p4_twenty_one_product) + (pa_s_hj32_local_total_j_p4_twenty_one_product))) /\ pa_s_hj32_local_total_j_p4_twenty_one_product = pa_r_hj32_local_total_j_p4_twenty_one_product * pa_p_hj32_local_total_j_p4_twenty_one_product))))))))
15. 0015specialize htotal 4
16. 0016specialize htotal 21
17. 0017exact htotal
18. 0018cases j_p4_twenty_one
19. 0019have j_parity : 7 * 6 = 2 * 21
20. 0020norm_num
21. 0021have j_eleven_bound : exists bqb_le_gap_hj32_j_eleven_bound. bqb_le_gap_hj32_j_eleven_bound + (x) = (x1)
22. 0022specialize pow_eleven_double_block_le_pow_four_even_from_total 6
23. 0023specialize pow_eleven_double_block_le_pow_four_even_from_total 21
24. 0024specialize pow_eleven_double_block_le_pow_four_even_from_total x
25. 0025specialize pow_eleven_double_block_le_pow_four_even_from_total x1
26. 0026apply pow_eleven_double_block_le_pow_four_even_from_total
27. 0027exact htotal
28. 0028exact j_parity
29. 0029exact j_p11_block_witness
30. 0030exact j_p4_twenty_one_witness
31. 0031have j_twelve : 2 * 6 = 12
32. 0032norm_num
33. 0033have j_h_block : exists pa_b_hj32_j_h_block pa_c_hj32_j_h_block. ((forall pa_i_hj32_j_h_block_repeat. (exists pa_lt_hj32_j_h_block_repeat_bound. pa_lt_hj32_j_h_block_repeat_bound + S pa_i_hj32_j_h_block_repeat = 2 * 6) -> (((exists pa_h_hj32_j_h_block_repeat_decoded. pa_h_hj32_j_h_block_repeat_decoded + S (s + 7) = S ((S (pa_i_hj32_j_h_block_repeat)) * pa_c_hj32_j_h_block)) /\ exists pa_q_hj32_j_h_block_repeat_decoded. pa_b_hj32_j_h_block = pa_q_hj32_j_h_block_repeat_decoded * S ((S (pa_i_hj32_j_h_block_repeat)) * pa_c_hj32_j_h_block) + (s + 7)))) /\ (exists pa_u_hj32_j_h_block_product pa_v_hj32_j_h_block_product. ((((exists pa_h_hj32_j_h_block_product_start. pa_h_hj32_j_h_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_start. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_start * S ((S (0)) * pa_v_hj32_j_h_block_product) + (1))) /\ ((((exists pa_h_hj32_j_h_block_product_terminal. pa_h_hj32_j_h_block_product_terminal + S (j) = S ((S (2 * 6)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_terminal. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_j_h_block_product) + (j))) /\ forall pa_i_hj32_j_h_block_product. (exists pa_lt_hj32_j_h_block_product_bound. pa_lt_hj32_j_h_block_product_bound + S pa_i_hj32_j_h_block_product = 2 * 6) -> exists pa_p_hj32_j_h_block_product pa_r_hj32_j_h_block_product pa_s_hj32_j_h_block_product. ((((exists pa_h_hj32_j_h_block_product_factor. pa_h_hj32_j_h_block_product_factor + S (pa_p_hj32_j_h_block_product) = S ((S (pa_i_hj32_j_h_block_product)) * pa_c_hj32_j_h_block)) /\ exists pa_q_hj32_j_h_block_product_factor. pa_b_hj32_j_h_block = pa_q_hj32_j_h_block_product_factor * S ((S (pa_i_hj32_j_h_block_product)) * pa_c_hj32_j_h_block) + (pa_p_hj32_j_h_block_product))) /\ ((((exists pa_h_hj32_j_h_block_product_partial. pa_h_hj32_j_h_block_product_partial + S (pa_r_hj32_j_h_block_product) = S ((S (pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_partial. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_partial * S ((S (pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product) + (pa_r_hj32_j_h_block_product))) /\ ((((exists pa_h_hj32_j_h_block_product_successor. pa_h_hj32_j_h_block_product_successor + S (pa_s_hj32_j_h_block_product) = S ((S (S pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product)) /\ exists pa_q_hj32_j_h_block_product_successor. pa_u_hj32_j_h_block_product = pa_q_hj32_j_h_block_product_successor * S ((S (S pa_i_hj32_j_h_block_product)) * pa_v_hj32_j_h_block_product) + (pa_s_hj32_j_h_block_product))) /\ pa_s_hj32_j_h_block_product = pa_r_hj32_j_h_block_product * pa_p_hj32_j_h_block_product)))))))
34. 0034rewrite j_twelve
35. 0035rewrite j_twelve
36. 0036rewrite j_twelve
37. 0037rewrite j_twelve
38. 0038exact hj
39. 0039have j_p4_block : exists hj32_local_value_j_p4_block. (exists pa_b_hj32_local_total_j_p4_block pa_c_hj32_local_total_j_p4_block. ((forall pa_i_hj32_local_total_j_p4_block_repeat. (exists pa_lt_hj32_local_total_j_p4_block_repeat_bound. pa_lt_hj32_local_total_j_p4_block_repeat_bound + S pa_i_hj32_local_total_j_p4_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p4_block_repeat_decoded. pa_h_hj32_local_total_j_p4_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_block_repeat)) * pa_c_hj32_local_total_j_p4_block)) /\ exists pa_q_hj32_local_total_j_p4_block_repeat_decoded. pa_b_hj32_local_total_j_p4_block = pa_q_hj32_local_total_j_p4_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_block_repeat)) * pa_c_hj32_local_total_j_p4_block) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_block_product pa_v_hj32_local_total_j_p4_block_product. ((((exists pa_h_hj32_local_total_j_p4_block_product_start. pa_h_hj32_local_total_j_p4_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_start. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_terminal. pa_h_hj32_local_total_j_p4_block_product_terminal + S (hj32_local_value_j_p4_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_terminal. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p4_block_product) + (hj32_local_value_j_p4_block))) /\ forall pa_i_hj32_local_total_j_p4_block_product. (exists pa_lt_hj32_local_total_j_p4_block_product_bound. pa_lt_hj32_local_total_j_p4_block_product_bound + S pa_i_hj32_local_total_j_p4_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p4_block_product pa_r_hj32_local_total_j_p4_block_product pa_s_hj32_local_total_j_p4_block_product. ((((exists pa_h_hj32_local_total_j_p4_block_product_factor. pa_h_hj32_local_total_j_p4_block_product_factor + S (pa_p_hj32_local_total_j_p4_block_product) = S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_c_hj32_local_total_j_p4_block)) /\ exists pa_q_hj32_local_total_j_p4_block_product_factor. pa_b_hj32_local_total_j_p4_block = pa_q_hj32_local_total_j_p4_block_product_factor * S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_c_hj32_local_total_j_p4_block) + (pa_p_hj32_local_total_j_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_partial. pa_h_hj32_local_total_j_p4_block_product_partial + S (pa_r_hj32_local_total_j_p4_block_product) = S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_partial. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_partial * S ((S (pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product) + (pa_r_hj32_local_total_j_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_block_product_successor. pa_h_hj32_local_total_j_p4_block_product_successor + S (pa_s_hj32_local_total_j_p4_block_product) = S ((S (S pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product)) /\ exists pa_q_hj32_local_total_j_p4_block_product_successor. pa_u_hj32_local_total_j_p4_block_product = pa_q_hj32_local_total_j_p4_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_block_product)) * pa_v_hj32_local_total_j_p4_block_product) + (pa_s_hj32_local_total_j_p4_block_product))) /\ pa_s_hj32_local_total_j_p4_block_product = pa_r_hj32_local_total_j_p4_block_product * pa_p_hj32_local_total_j_p4_block_product))))))))
40. 0040specialize htotal 4
41. 0041specialize htotal 2 * 6
42. 0042exact htotal
43. 0043cases j_p4_block
44. 0044have j_p44_block : exists hj32_local_value_j_p44_block. (exists pa_b_hj32_local_total_j_p44_block pa_c_hj32_local_total_j_p44_block. ((forall pa_i_hj32_local_total_j_p44_block_repeat. (exists pa_lt_hj32_local_total_j_p44_block_repeat_bound. pa_lt_hj32_local_total_j_p44_block_repeat_bound + S pa_i_hj32_local_total_j_p44_block_repeat = 2 * 6) -> (((exists pa_h_hj32_local_total_j_p44_block_repeat_decoded. pa_h_hj32_local_total_j_p44_block_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_j_p44_block_repeat)) * pa_c_hj32_local_total_j_p44_block)) /\ exists pa_q_hj32_local_total_j_p44_block_repeat_decoded. pa_b_hj32_local_total_j_p44_block = pa_q_hj32_local_total_j_p44_block_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p44_block_repeat)) * pa_c_hj32_local_total_j_p44_block) + (44)))) /\ (exists pa_u_hj32_local_total_j_p44_block_product pa_v_hj32_local_total_j_p44_block_product. ((((exists pa_h_hj32_local_total_j_p44_block_product_start. pa_h_hj32_local_total_j_p44_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_start. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p44_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_terminal. pa_h_hj32_local_total_j_p44_block_product_terminal + S (hj32_local_value_j_p44_block) = S ((S (2 * 6)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_terminal. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_total_j_p44_block_product) + (hj32_local_value_j_p44_block))) /\ forall pa_i_hj32_local_total_j_p44_block_product. (exists pa_lt_hj32_local_total_j_p44_block_product_bound. pa_lt_hj32_local_total_j_p44_block_product_bound + S pa_i_hj32_local_total_j_p44_block_product = 2 * 6) -> exists pa_p_hj32_local_total_j_p44_block_product pa_r_hj32_local_total_j_p44_block_product pa_s_hj32_local_total_j_p44_block_product. ((((exists pa_h_hj32_local_total_j_p44_block_product_factor. pa_h_hj32_local_total_j_p44_block_product_factor + S (pa_p_hj32_local_total_j_p44_block_product) = S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_c_hj32_local_total_j_p44_block)) /\ exists pa_q_hj32_local_total_j_p44_block_product_factor. pa_b_hj32_local_total_j_p44_block = pa_q_hj32_local_total_j_p44_block_product_factor * S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_c_hj32_local_total_j_p44_block) + (pa_p_hj32_local_total_j_p44_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_partial. pa_h_hj32_local_total_j_p44_block_product_partial + S (pa_r_hj32_local_total_j_p44_block_product) = S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_partial. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_partial * S ((S (pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product) + (pa_r_hj32_local_total_j_p44_block_product))) /\ ((((exists pa_h_hj32_local_total_j_p44_block_product_successor. pa_h_hj32_local_total_j_p44_block_product_successor + S (pa_s_hj32_local_total_j_p44_block_product) = S ((S (S pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product)) /\ exists pa_q_hj32_local_total_j_p44_block_product_successor. pa_u_hj32_local_total_j_p44_block_product = pa_q_hj32_local_total_j_p44_block_product_successor * S ((S (S pa_i_hj32_local_total_j_p44_block_product)) * pa_v_hj32_local_total_j_p44_block_product) + (pa_s_hj32_local_total_j_p44_block_product))) /\ pa_s_hj32_local_total_j_p44_block_product = pa_r_hj32_local_total_j_p44_block_product * pa_p_hj32_local_total_j_p44_block_product))))))))
45. 0045specialize htotal 44
46. 0046specialize htotal 2 * 6
47. 0047exact htotal
48. 0048cases j_p44_block
49. 0049have j_p4_thirty_three : exists hj32_local_value_j_p4_thirty_three. (exists pa_b_hj32_local_total_j_p4_thirty_three pa_c_hj32_local_total_j_p4_thirty_three. ((forall pa_i_hj32_local_total_j_p4_thirty_three_repeat. (exists pa_lt_hj32_local_total_j_p4_thirty_three_repeat_bound. pa_lt_hj32_local_total_j_p4_thirty_three_repeat_bound + S pa_i_hj32_local_total_j_p4_thirty_three_repeat = 33) -> (((exists pa_h_hj32_local_total_j_p4_thirty_three_repeat_decoded. pa_h_hj32_local_total_j_p4_thirty_three_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_repeat)) * pa_c_hj32_local_total_j_p4_thirty_three)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_repeat_decoded. pa_b_hj32_local_total_j_p4_thirty_three = pa_q_hj32_local_total_j_p4_thirty_three_repeat_decoded * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_repeat)) * pa_c_hj32_local_total_j_p4_thirty_three) + (4)))) /\ (exists pa_u_hj32_local_total_j_p4_thirty_three_product pa_v_hj32_local_total_j_p4_thirty_three_product. ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_start. pa_h_hj32_local_total_j_p4_thirty_three_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_start. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_start * S ((S (0)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (1))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_terminal. pa_h_hj32_local_total_j_p4_thirty_three_product_terminal + S (hj32_local_value_j_p4_thirty_three) = S ((S (33)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_terminal. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_terminal * S ((S (33)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (hj32_local_value_j_p4_thirty_three))) /\ forall pa_i_hj32_local_total_j_p4_thirty_three_product. (exists pa_lt_hj32_local_total_j_p4_thirty_three_product_bound. pa_lt_hj32_local_total_j_p4_thirty_three_product_bound + S pa_i_hj32_local_total_j_p4_thirty_three_product = 33) -> exists pa_p_hj32_local_total_j_p4_thirty_three_product pa_r_hj32_local_total_j_p4_thirty_three_product pa_s_hj32_local_total_j_p4_thirty_three_product. ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_factor. pa_h_hj32_local_total_j_p4_thirty_three_product_factor + S (pa_p_hj32_local_total_j_p4_thirty_three_product) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_c_hj32_local_total_j_p4_thirty_three)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_factor. pa_b_hj32_local_total_j_p4_thirty_three = pa_q_hj32_local_total_j_p4_thirty_three_product_factor * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_c_hj32_local_total_j_p4_thirty_three) + (pa_p_hj32_local_total_j_p4_thirty_three_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_partial. pa_h_hj32_local_total_j_p4_thirty_three_product_partial + S (pa_r_hj32_local_total_j_p4_thirty_three_product) = S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_partial. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_partial * S ((S (pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (pa_r_hj32_local_total_j_p4_thirty_three_product))) /\ ((((exists pa_h_hj32_local_total_j_p4_thirty_three_product_successor. pa_h_hj32_local_total_j_p4_thirty_three_product_successor + S (pa_s_hj32_local_total_j_p4_thirty_three_product) = S ((S (S pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product)) /\ exists pa_q_hj32_local_total_j_p4_thirty_three_product_successor. pa_u_hj32_local_total_j_p4_thirty_three_product = pa_q_hj32_local_total_j_p4_thirty_three_product_successor * S ((S (S pa_i_hj32_local_total_j_p4_thirty_three_product)) * pa_v_hj32_local_total_j_p4_thirty_three_product) + (pa_s_hj32_local_total_j_p4_thirty_three_product))) /\ pa_s_hj32_local_total_j_p4_thirty_three_product = pa_r_hj32_local_total_j_p4_thirty_three_product * pa_p_hj32_local_total_j_p4_thirty_three_product))))))))
50. 0050specialize htotal 4
51. 0051specialize htotal 33
52. 0052exact htotal
53. 0053cases j_p4_thirty_three
54. 0054have j_product_44_graph : exists pa_b_hj32_local_product_j_product_44 pa_c_hj32_local_product_j_product_44. ((forall pa_i_hj32_local_product_j_product_44_repeat. (exists pa_lt_hj32_local_product_j_product_44_repeat_bound. pa_lt_hj32_local_product_j_product_44_repeat_bound + S pa_i_hj32_local_product_j_product_44_repeat = 2 * 6) -> (((exists pa_h_hj32_local_product_j_product_44_repeat_decoded. pa_h_hj32_local_product_j_product_44_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_j_product_44_repeat)) * pa_c_hj32_local_product_j_product_44)) /\ exists pa_q_hj32_local_product_j_product_44_repeat_decoded. pa_b_hj32_local_product_j_product_44 = pa_q_hj32_local_product_j_product_44_repeat_decoded * S ((S (pa_i_hj32_local_product_j_product_44_repeat)) * pa_c_hj32_local_product_j_product_44) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_j_product_44_product pa_v_hj32_local_product_j_product_44_product. ((((exists pa_h_hj32_local_product_j_product_44_product_start. pa_h_hj32_local_product_j_product_44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_start. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_start * S ((S (0)) * pa_v_hj32_local_product_j_product_44_product) + (1))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_terminal. pa_h_hj32_local_product_j_product_44_product_terminal + S (x3) = S ((S (2 * 6)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_terminal. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_terminal * S ((S (2 * 6)) * pa_v_hj32_local_product_j_product_44_product) + (x3))) /\ forall pa_i_hj32_local_product_j_product_44_product. (exists pa_lt_hj32_local_product_j_product_44_product_bound. pa_lt_hj32_local_product_j_product_44_product_bound + S pa_i_hj32_local_product_j_product_44_product = 2 * 6) -> exists pa_p_hj32_local_product_j_product_44_product pa_r_hj32_local_product_j_product_44_product pa_s_hj32_local_product_j_product_44_product. ((((exists pa_h_hj32_local_product_j_product_44_product_factor. pa_h_hj32_local_product_j_product_44_product_factor + S (pa_p_hj32_local_product_j_product_44_product) = S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_c_hj32_local_product_j_product_44)) /\ exists pa_q_hj32_local_product_j_product_44_product_factor. pa_b_hj32_local_product_j_product_44 = pa_q_hj32_local_product_j_product_44_product_factor * S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_c_hj32_local_product_j_product_44) + (pa_p_hj32_local_product_j_product_44_product))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_partial. pa_h_hj32_local_product_j_product_44_product_partial + S (pa_r_hj32_local_product_j_product_44_product) = S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_partial. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_partial * S ((S (pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product) + (pa_r_hj32_local_product_j_product_44_product))) /\ ((((exists pa_h_hj32_local_product_j_product_44_product_successor. pa_h_hj32_local_product_j_product_44_product_successor + S (pa_s_hj32_local_product_j_product_44_product) = S ((S (S pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product)) /\ exists pa_q_hj32_local_product_j_product_44_product_successor. pa_u_hj32_local_product_j_product_44_product = pa_q_hj32_local_product_j_product_44_product_successor * S ((S (S pa_i_hj32_local_product_j_product_44_product)) * pa_v_hj32_local_product_j_product_44_product) + (pa_s_hj32_local_product_j_product_44_product))) /\ pa_s_hj32_local_product_j_product_44_product = pa_r_hj32_local_product_j_product_44_product * pa_p_hj32_local_product_j_product_44_product)))))))
55. 0055have j_product_44_base : 4 * 11 = 44
56. 0056norm_num
57. 0057rewrite j_product_44_base
58. 0058rewrite j_product_44_base
59. 0059exact j_p44_block_witness
60. 0060have j_product_44 : x3 = x2 * x
61. 0061specialize pow_mul_base 4
62. 0062specialize pow_mul_base 11
63. 0063specialize pow_mul_base 2 * 6
64. 0064specialize pow_mul_base x2
65. 0065specialize pow_mul_base x
66. 0066specialize pow_mul_base x3
67. 0067apply pow_mul_base
68. 0068exact j_p4_block_witness
69. 0069exact j_p11_block_witness
70. 0070exact j_product_44_graph
71. 0071have j_product_33 : x4 = x2 * x1
72. 0072specialize pow_add 4
73. 0073specialize pow_add 2 * 6
74. 0074specialize pow_add 21
75. 0075specialize pow_add 33
76. 0076specialize pow_add x2
77. 0077specialize pow_add x1
78. 0078specialize pow_add x4
79. 0079apply pow_add
80. 0080norm_num
81. 0081exact j_p4_block_witness
82. 0082exact j_p4_twenty_one_witness
83. 0083exact j_p4_thirty_three_witness
84. 0084have j_four_refl : exists bqb_le_gap_hj32_j_four_refl. bqb_le_gap_hj32_j_four_refl + (x2) = (x2)
85. 0085specialize le_refl x2
86. 0086exact le_refl
87. 0087have j_product_bound : exists bqb_le_gap_hj32_local_product_bound_j_product_bound. bqb_le_gap_hj32_local_product_bound_j_product_bound + (x2 * x) = (x2 * x1)
88. 0088specialize mul_le_mul x2
89. 0089specialize mul_le_mul x2
90. 0090specialize mul_le_mul x
91. 0091specialize mul_le_mul x1
92. 0092apply mul_le_mul
93. 0093exact j_four_refl
94. 0094exact j_eleven_bound
95. 0095rewrite <- j_product_44 at j_product_bound
96. 0096rewrite <- j_product_33 at j_product_bound
97. 0097have j_base_to_upper : exists bqb_le_gap_hj32_j_base_to_upper. bqb_le_gap_hj32_j_base_to_upper + (s + 7) = (37 + 7)
98. 0098specialize add_le_add_right s
99. 0099specialize add_le_add_right 37
100. 0100specialize add_le_add_right 7
101. 0101apply add_le_add_right
102. 0102exact hupper
103. 0103have j_upper_value : 37 + 7 = 44
104. 0104norm_num
105. 0105have j_base_bound : exists bqb_le_gap_hj32_j_base_bound. bqb_le_gap_hj32_j_base_bound + (s + 7) = (44)
106. 0106rewrite j_upper_value at j_base_to_upper
107. 0107exact j_base_to_upper
108. 0108have j_to_44 : exists bqb_le_gap_hj32_local_base_bound_j_to_44. bqb_le_gap_hj32_local_base_bound_j_to_44 + (j) = (x3)
109. 0109specialize pow_base_monotone s + 7
110. 0110specialize pow_base_monotone 44
111. 0111specialize pow_base_monotone 2 * 6
112. 0112specialize pow_base_monotone j
113. 0113specialize pow_base_monotone x3
114. 0114apply pow_base_monotone
115. 0115exact j_base_bound
116. 0116exact j_h_block
117. 0117exact j_p44_block_witness
118. 0118have j_to_thirty_three : exists bqb_le_gap_hj32_local_trans_bound_j_to_thirty_three. bqb_le_gap_hj32_local_trans_bound_j_to_thirty_three + (j) = (x4)
119. 0119specialize le_trans j
120. 0120specialize le_trans x3
121. 0121specialize le_trans x4
122. 0122apply le_trans
123. 0123exact j_to_44
124. 0124exact j_product_bound
125. 0125have j_exponent_from_lower : exists bqb_le_gap_hj32_j_exponent_from_lower. bqb_le_gap_hj32_j_exponent_from_lower + (32 + 5) = (s + 5)
126. 0126specialize add_le_add_right 32
127. 0127specialize add_le_add_right s
128. 0128specialize add_le_add_right 5
129. 0129apply add_le_add_right
130. 0130exact hlower
131. 0131have j_lower_value : 32 + 5 = 37
132. 0132norm_num
133. 0133have j_thirty_seven_to_target : exists bqb_le_gap_hj32_j_thirty_seven_to_target. bqb_le_gap_hj32_j_thirty_seven_to_target + (37) = (s + 5)
134. 0134rewrite j_lower_value at j_exponent_from_lower
135. 0135exact j_exponent_from_lower
136. 0136have j_seed : exists bqb_le_gap_hj32_j_exponent_seed. bqb_le_gap_hj32_j_exponent_seed + (33) = (37)
137. 0137exists 4
138. 0138norm_num
139. 0139have j_exponent_bound : exists bqb_le_gap_hj32_local_trans_bound_j_exponent_bound. bqb_le_gap_hj32_local_trans_bound_j_exponent_bound + (33) = (s + 5)
140. 0140specialize le_trans 33
141. 0141specialize le_trans 37
142. 0142specialize le_trans s + 5
143. 0143apply le_trans
144. 0144exact j_seed
145. 0145exact j_thirty_seven_to_target
146. 0146have j_growth : exists bqb_le_gap_hj32_local_exponent_bound_j_growth. bqb_le_gap_hj32_local_exponent_bound_j_growth + (x4) = (g)
147. 0147specialize pow_exponent_monotone_from_total 4
148. 0148specialize pow_exponent_monotone_from_total 33
149. 0149specialize pow_exponent_monotone_from_total s + 5
150. 0150specialize pow_exponent_monotone_from_total x4
151. 0151specialize pow_exponent_monotone_from_total g
152. 0152apply pow_exponent_monotone_from_total
153. 0153exact htotal
154. 0154exists 3
155. 0155norm_num
156. 0156exact j_exponent_bound
157. 0157exact j_p4_thirty_three_witness
158. 0158exact hg
159. 0159have j_result : exists bqb_le_gap_hj32_local_trans_bound_j_result. bqb_le_gap_hj32_local_trans_bound_j_result + (j) = (g)
160. 0160specialize le_trans j
161. 0161specialize le_trans x4
162. 0162specialize le_trans g
163. 0163apply le_trans
164. 0164exact j_to_thirty_three
165. 0165exact j_growth
166. 0166exact j_result