bertrand_hj_envelope_thirty_two

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 e
3. 0003intro h
4. 0004intro u
5. 0005intro j
6. 0006intro g
7. 0007intro hlower
8. 0008intro hceiling
9. 0009intro hh
10. 0010intro hu
11. 0011intro hj
12. 0012intro hg
13. 0013have htotal : forall bpt_a_hjas_envelope_total bpt_e_hjas_envelope_total. exists bpt_x_hjas_envelope_total. (exists ff_b_bpt_value_hjas_envelope_total ff_c_bpt_value_hjas_envelope_total. ((forall ff_i_bpt_value_hjas_envelope_total_repeat. (exists ff_lt_bpt_value_hjas_envelope_total_repeat_bound. ff_lt_bpt_value_hjas_envelope_total_repeat_bound + S ff_i_bpt_value_hjas_envelope_total_repeat = bpt_e_hjas_envelope_total) -> (((exists ff_h_bpt_value_hjas_envelope_total_repeat_decoded. ff_h_bpt_value_hjas_envelope_total_repeat_decoded + S (bpt_a_hjas_envelope_total) = S ((S (ff_i_bpt_value_hjas_envelope_total_repeat)) * ff_c_bpt_value_hjas_envelope_total)) /\ exists ff_q_bpt_value_hjas_envelope_total_repeat_decoded. ff_b_bpt_value_hjas_envelope_total = ff_q_bpt_value_hjas_envelope_total_repeat_decoded * S ((S (ff_i_bpt_value_hjas_envelope_total_repeat)) * ff_c_bpt_value_hjas_envelope_total) + (bpt_a_hjas_envelope_total)))) /\ (exists ff_u_bpt_value_hjas_envelope_total_product ff_v_bpt_value_hjas_envelope_total_product. ((((exists ff_h_bpt_value_hjas_envelope_total_product_start. ff_h_bpt_value_hjas_envelope_total_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_start. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_start * S ((S (0)) * ff_v_bpt_value_hjas_envelope_total_product) + (1))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_terminal. ff_h_bpt_value_hjas_envelope_total_product_terminal + S (bpt_x_hjas_envelope_total) = S ((S (bpt_e_hjas_envelope_total)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_terminal. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_terminal * S ((S (bpt_e_hjas_envelope_total)) * ff_v_bpt_value_hjas_envelope_total_product) + (bpt_x_hjas_envelope_total))) /\ forall ff_i_bpt_value_hjas_envelope_total_product. (exists ff_lt_bpt_value_hjas_envelope_total_product_bound. ff_lt_bpt_value_hjas_envelope_total_product_bound + S ff_i_bpt_value_hjas_envelope_total_product = bpt_e_hjas_envelope_total) -> exists ff_p_bpt_value_hjas_envelope_total_product ff_r_bpt_value_hjas_envelope_total_product ff_s_bpt_value_hjas_envelope_total_product. ((((exists ff_h_bpt_value_hjas_envelope_total_product_factor. ff_h_bpt_value_hjas_envelope_total_product_factor + S (ff_p_bpt_value_hjas_envelope_total_product) = S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_c_bpt_value_hjas_envelope_total)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_factor. ff_b_bpt_value_hjas_envelope_total = ff_q_bpt_value_hjas_envelope_total_product_factor * S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_c_bpt_value_hjas_envelope_total) + (ff_p_bpt_value_hjas_envelope_total_product))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_partial. ff_h_bpt_value_hjas_envelope_total_product_partial + S (ff_r_bpt_value_hjas_envelope_total_product) = S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_partial. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_partial * S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product) + (ff_r_bpt_value_hjas_envelope_total_product))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_successor. ff_h_bpt_value_hjas_envelope_total_product_successor + S (ff_s_bpt_value_hjas_envelope_total_product) = S ((S (S ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_successor. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_successor * S ((S (S ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product) + (ff_s_bpt_value_hjas_envelope_total_product))) /\ ff_s_bpt_value_hjas_envelope_total_product = ff_r_bpt_value_hjas_envelope_total_product * ff_p_bpt_value_hjas_envelope_total_product))))))))
14. 0014intro a
15. 0015intro d
16. 0016specialize pow_exists a
17. 0017specialize pow_exists d
18. 0018exact pow_exists
19. 0019have hdecomposition : exists b k. (((exists bqb_le_gap_hjas_decomposition_base_lower. bqb_le_gap_hjas_decomposition_base_lower + (32) = (b)) /\ (exists bqb_le_gap_hjas_decomposition_base_upper. bqb_le_gap_hjas_decomposition_base_upper + (b) = (37))) /\ s = b + 6 * k)
20. 0020specialize six_block_window_decomposition_above_thirty_two s
21. 0021apply six_block_window_decomposition_above_thirty_two
22. 0022exact hlower
23. 0023cases hdecomposition
24. 0024cases hdecomposition_witness
25. 0025cases hdecomposition_witness_witness
26. 0026cases hdecomposition_witness_witness_left
27. 0027have hfamily : forall kk ee hh uu jj gg. (((exists bcs_lower_gap_hjas_family_ceiling. bcs_lower_gap_hjas_family_ceiling + ((x + 6 * kk) * (x + 6 * kk)) = 6 * (ee)) /\ exists bcs_upper_gap_hjas_family_ceiling. bcs_upper_gap_hjas_family_ceiling + S (6 * (ee)) = ((x + 6 * kk) * (x + 6 * kk)) + 6)) -> (exists pa_b_hjas_family_h pa_c_hjas_family_h. ((forall pa_i_hjas_family_h_repeat. (exists pa_lt_hjas_family_h_repeat_bound. pa_lt_hjas_family_h_repeat_bound + S pa_i_hjas_family_h_repeat = 2 * (x + 6 * kk) + 2) -> (((exists pa_h_hjas_family_h_repeat_decoded. pa_h_hjas_family_h_repeat_decoded + S ((x + 6 * kk) + 1) = S ((S (pa_i_hjas_family_h_repeat)) * pa_c_hjas_family_h)) /\ exists pa_q_hjas_family_h_repeat_decoded. pa_b_hjas_family_h = pa_q_hjas_family_h_repeat_decoded * S ((S (pa_i_hjas_family_h_repeat)) * pa_c_hjas_family_h) + ((x + 6 * kk) + 1)))) /\ (exists pa_u_hjas_family_h_product pa_v_hjas_family_h_product. ((((exists pa_h_hjas_family_h_product_start. pa_h_hjas_family_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_start. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_start * S ((S (0)) * pa_v_hjas_family_h_product) + (1))) /\ ((((exists pa_h_hjas_family_h_product_terminal. pa_h_hjas_family_h_product_terminal + S (hh) = S ((S (2 * (x + 6 * kk) + 2)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_terminal. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_terminal * S ((S (2 * (x + 6 * kk) + 2)) * pa_v_hjas_family_h_product) + (hh))) /\ forall pa_i_hjas_family_h_product. (exists pa_lt_hjas_family_h_product_bound. pa_lt_hjas_family_h_product_bound + S pa_i_hjas_family_h_product = 2 * (x + 6 * kk) + 2) -> exists pa_p_hjas_family_h_product pa_r_hjas_family_h_product pa_s_hjas_family_h_product. ((((exists pa_h_hjas_family_h_product_factor. pa_h_hjas_family_h_product_factor + S (pa_p_hjas_family_h_product) = S ((S (pa_i_hjas_family_h_product)) * pa_c_hjas_family_h)) /\ exists pa_q_hjas_family_h_product_factor. pa_b_hjas_family_h = pa_q_hjas_family_h_product_factor * S ((S (pa_i_hjas_family_h_product)) * pa_c_hjas_family_h) + (pa_p_hjas_family_h_product))) /\ ((((exists pa_h_hjas_family_h_product_partial. pa_h_hjas_family_h_product_partial + S (pa_r_hjas_family_h_product) = S ((S (pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_partial. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_partial * S ((S (pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product) + (pa_r_hjas_family_h_product))) /\ ((((exists pa_h_hjas_family_h_product_successor. pa_h_hjas_family_h_product_successor + S (pa_s_hjas_family_h_product) = S ((S (S pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_successor. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_successor * S ((S (S pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product) + (pa_s_hjas_family_h_product))) /\ pa_s_hjas_family_h_product = pa_r_hjas_family_h_product * pa_p_hjas_family_h_product)))))))) -> (exists pa_b_hjas_family_h_bound pa_c_hjas_family_h_bound. ((forall pa_i_hjas_family_h_bound_repeat. (exists pa_lt_hjas_family_h_bound_repeat_bound. pa_lt_hjas_family_h_bound_repeat_bound + S pa_i_hjas_family_h_bound_repeat = ee) -> (((exists pa_h_hjas_family_h_bound_repeat_decoded. pa_h_hjas_family_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_family_h_bound_repeat)) * pa_c_hjas_family_h_bound)) /\ exists pa_q_hjas_family_h_bound_repeat_decoded. pa_b_hjas_family_h_bound = pa_q_hjas_family_h_bound_repeat_decoded * S ((S (pa_i_hjas_family_h_bound_repeat)) * pa_c_hjas_family_h_bound) + (4)))) /\ (exists pa_u_hjas_family_h_bound_product pa_v_hjas_family_h_bound_product. ((((exists pa_h_hjas_family_h_bound_product_start. pa_h_hjas_family_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_start. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_start * S ((S (0)) * pa_v_hjas_family_h_bound_product) + (1))) /\ ((((exists pa_h_hjas_family_h_bound_product_terminal. pa_h_hjas_family_h_bound_product_terminal + S (uu) = S ((S (ee)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_terminal. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_terminal * S ((S (ee)) * pa_v_hjas_family_h_bound_product) + (uu))) /\ forall pa_i_hjas_family_h_bound_product. (exists pa_lt_hjas_family_h_bound_product_bound. pa_lt_hjas_family_h_bound_product_bound + S pa_i_hjas_family_h_bound_product = ee) -> exists pa_p_hjas_family_h_bound_product pa_r_hjas_family_h_bound_product pa_s_hjas_family_h_bound_product. ((((exists pa_h_hjas_family_h_bound_product_factor. pa_h_hjas_family_h_bound_product_factor + S (pa_p_hjas_family_h_bound_product) = S ((S (pa_i_hjas_family_h_bound_product)) * pa_c_hjas_family_h_bound)) /\ exists pa_q_hjas_family_h_bound_product_factor. pa_b_hjas_family_h_bound = pa_q_hjas_family_h_bound_product_factor * S ((S (pa_i_hjas_family_h_bound_product)) * pa_c_hjas_family_h_bound) + (pa_p_hjas_family_h_bound_product))) /\ ((((exists pa_h_hjas_family_h_bound_product_partial. pa_h_hjas_family_h_bound_product_partial + S (pa_r_hjas_family_h_bound_product) = S ((S (pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_partial. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_partial * S ((S (pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product) + (pa_r_hjas_family_h_bound_product))) /\ ((((exists pa_h_hjas_family_h_bound_product_successor. pa_h_hjas_family_h_bound_product_successor + S (pa_s_hjas_family_h_bound_product) = S ((S (S pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_successor. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_successor * S ((S (S pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product) + (pa_s_hjas_family_h_bound_product))) /\ pa_s_hjas_family_h_bound_product = pa_r_hjas_family_h_bound_product * pa_p_hjas_family_h_bound_product)))))))) -> (exists pa_b_hjas_family_j pa_c_hjas_family_j. ((forall pa_i_hjas_family_j_repeat. (exists pa_lt_hjas_family_j_repeat_bound. pa_lt_hjas_family_j_repeat_bound + S pa_i_hjas_family_j_repeat = 12) -> (((exists pa_h_hjas_family_j_repeat_decoded. pa_h_hjas_family_j_repeat_decoded + S ((x + 6 * kk) + 7) = S ((S (pa_i_hjas_family_j_repeat)) * pa_c_hjas_family_j)) /\ exists pa_q_hjas_family_j_repeat_decoded. pa_b_hjas_family_j = pa_q_hjas_family_j_repeat_decoded * S ((S (pa_i_hjas_family_j_repeat)) * pa_c_hjas_family_j) + ((x + 6 * kk) + 7)))) /\ (exists pa_u_hjas_family_j_product pa_v_hjas_family_j_product. ((((exists pa_h_hjas_family_j_product_start. pa_h_hjas_family_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_start. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_start * S ((S (0)) * pa_v_hjas_family_j_product) + (1))) /\ ((((exists pa_h_hjas_family_j_product_terminal. pa_h_hjas_family_j_product_terminal + S (jj) = S ((S (12)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_terminal. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_terminal * S ((S (12)) * pa_v_hjas_family_j_product) + (jj))) /\ forall pa_i_hjas_family_j_product. (exists pa_lt_hjas_family_j_product_bound. pa_lt_hjas_family_j_product_bound + S pa_i_hjas_family_j_product = 12) -> exists pa_p_hjas_family_j_product pa_r_hjas_family_j_product pa_s_hjas_family_j_product. ((((exists pa_h_hjas_family_j_product_factor. pa_h_hjas_family_j_product_factor + S (pa_p_hjas_family_j_product) = S ((S (pa_i_hjas_family_j_product)) * pa_c_hjas_family_j)) /\ exists pa_q_hjas_family_j_product_factor. pa_b_hjas_family_j = pa_q_hjas_family_j_product_factor * S ((S (pa_i_hjas_family_j_product)) * pa_c_hjas_family_j) + (pa_p_hjas_family_j_product))) /\ ((((exists pa_h_hjas_family_j_product_partial. pa_h_hjas_family_j_product_partial + S (pa_r_hjas_family_j_product) = S ((S (pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_partial. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_partial * S ((S (pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product) + (pa_r_hjas_family_j_product))) /\ ((((exists pa_h_hjas_family_j_product_successor. pa_h_hjas_family_j_product_successor + S (pa_s_hjas_family_j_product) = S ((S (S pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_successor. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_successor * S ((S (S pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product) + (pa_s_hjas_family_j_product))) /\ pa_s_hjas_family_j_product = pa_r_hjas_family_j_product * pa_p_hjas_family_j_product)))))))) -> (exists pa_b_hjas_family_j_bound pa_c_hjas_family_j_bound. ((forall pa_i_hjas_family_j_bound_repeat. (exists pa_lt_hjas_family_j_bound_repeat_bound. pa_lt_hjas_family_j_bound_repeat_bound + S pa_i_hjas_family_j_bound_repeat = (x + 6 * kk) + 5) -> (((exists pa_h_hjas_family_j_bound_repeat_decoded. pa_h_hjas_family_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_family_j_bound_repeat)) * pa_c_hjas_family_j_bound)) /\ exists pa_q_hjas_family_j_bound_repeat_decoded. pa_b_hjas_family_j_bound = pa_q_hjas_family_j_bound_repeat_decoded * S ((S (pa_i_hjas_family_j_bound_repeat)) * pa_c_hjas_family_j_bound) + (4)))) /\ (exists pa_u_hjas_family_j_bound_product pa_v_hjas_family_j_bound_product. ((((exists pa_h_hjas_family_j_bound_product_start. pa_h_hjas_family_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_start. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_start * S ((S (0)) * pa_v_hjas_family_j_bound_product) + (1))) /\ ((((exists pa_h_hjas_family_j_bound_product_terminal. pa_h_hjas_family_j_bound_product_terminal + S (gg) = S ((S ((x + 6 * kk) + 5)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_terminal. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_terminal * S ((S ((x + 6 * kk) + 5)) * pa_v_hjas_family_j_bound_product) + (gg))) /\ forall pa_i_hjas_family_j_bound_product. (exists pa_lt_hjas_family_j_bound_product_bound. pa_lt_hjas_family_j_bound_product_bound + S pa_i_hjas_family_j_bound_product = (x + 6 * kk) + 5) -> exists pa_p_hjas_family_j_bound_product pa_r_hjas_family_j_bound_product pa_s_hjas_family_j_bound_product. ((((exists pa_h_hjas_family_j_bound_product_factor. pa_h_hjas_family_j_bound_product_factor + S (pa_p_hjas_family_j_bound_product) = S ((S (pa_i_hjas_family_j_bound_product)) * pa_c_hjas_family_j_bound)) /\ exists pa_q_hjas_family_j_bound_product_factor. pa_b_hjas_family_j_bound = pa_q_hjas_family_j_bound_product_factor * S ((S (pa_i_hjas_family_j_bound_product)) * pa_c_hjas_family_j_bound) + (pa_p_hjas_family_j_bound_product))) /\ ((((exists pa_h_hjas_family_j_bound_product_partial. pa_h_hjas_family_j_bound_product_partial + S (pa_r_hjas_family_j_bound_product) = S ((S (pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_partial. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_partial * S ((S (pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product) + (pa_r_hjas_family_j_bound_product))) /\ ((((exists pa_h_hjas_family_j_bound_product_successor. pa_h_hjas_family_j_bound_product_successor + S (pa_s_hjas_family_j_bound_product) = S ((S (S pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_successor. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_successor * S ((S (S pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product) + (pa_s_hjas_family_j_bound_product))) /\ pa_s_hjas_family_j_bound_product = pa_r_hjas_family_j_bound_product * pa_p_hjas_family_j_bound_product)))))))) -> (((exists bqb_le_gap_hjas_family_h_result. bqb_le_gap_hjas_family_h_result + (hh) = (uu)) /\ (exists bqb_le_gap_hjas_family_j_result. bqb_le_gap_hjas_family_j_result + (jj) = (gg))))
28. 0028specialize bertrand_hj_six_block_iterate_from_total x
29. 0029apply bertrand_hj_six_block_iterate_from_total
30. 0030exact htotal
31. 0031exact hdecomposition_witness_witness_left_left
32. 0032exact hdecomposition_witness_witness_left_right
33. 0033have hblock_ceiling : ((exists bcs_lower_gap_hjas_block_ceiling. bcs_lower_gap_hjas_block_ceiling + ((x + 6 * x1) * (x + 6 * x1)) = 6 * (e)) /\ exists bcs_upper_gap_hjas_block_ceiling. bcs_upper_gap_hjas_block_ceiling + S (6 * (e)) = ((x + 6 * x1) * (x + 6 * x1)) + 6)
34. 0034rewrite <- hdecomposition_witness_witness_right
35. 0035rewrite <- hdecomposition_witness_witness_right
36. 0036rewrite <- hdecomposition_witness_witness_right
37. 0037rewrite <- hdecomposition_witness_witness_right
38. 0038exact hceiling
39. 0039have hblock_h : exists pa_b_hjas_block_h pa_c_hjas_block_h. ((forall pa_i_hjas_block_h_repeat. (exists pa_lt_hjas_block_h_repeat_bound. pa_lt_hjas_block_h_repeat_bound + S pa_i_hjas_block_h_repeat = 2 * (x + 6 * x1) + 2) -> (((exists pa_h_hjas_block_h_repeat_decoded. pa_h_hjas_block_h_repeat_decoded + S ((x + 6 * x1) + 1) = S ((S (pa_i_hjas_block_h_repeat)) * pa_c_hjas_block_h)) /\ exists pa_q_hjas_block_h_repeat_decoded. pa_b_hjas_block_h = pa_q_hjas_block_h_repeat_decoded * S ((S (pa_i_hjas_block_h_repeat)) * pa_c_hjas_block_h) + ((x + 6 * x1) + 1)))) /\ (exists pa_u_hjas_block_h_product pa_v_hjas_block_h_product. ((((exists pa_h_hjas_block_h_product_start. pa_h_hjas_block_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_start. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_start * S ((S (0)) * pa_v_hjas_block_h_product) + (1))) /\ ((((exists pa_h_hjas_block_h_product_terminal. pa_h_hjas_block_h_product_terminal + S (h) = S ((S (2 * (x + 6 * x1) + 2)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_terminal. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_terminal * S ((S (2 * (x + 6 * x1) + 2)) * pa_v_hjas_block_h_product) + (h))) /\ forall pa_i_hjas_block_h_product. (exists pa_lt_hjas_block_h_product_bound. pa_lt_hjas_block_h_product_bound + S pa_i_hjas_block_h_product = 2 * (x + 6 * x1) + 2) -> exists pa_p_hjas_block_h_product pa_r_hjas_block_h_product pa_s_hjas_block_h_product. ((((exists pa_h_hjas_block_h_product_factor. pa_h_hjas_block_h_product_factor + S (pa_p_hjas_block_h_product) = S ((S (pa_i_hjas_block_h_product)) * pa_c_hjas_block_h)) /\ exists pa_q_hjas_block_h_product_factor. pa_b_hjas_block_h = pa_q_hjas_block_h_product_factor * S ((S (pa_i_hjas_block_h_product)) * pa_c_hjas_block_h) + (pa_p_hjas_block_h_product))) /\ ((((exists pa_h_hjas_block_h_product_partial. pa_h_hjas_block_h_product_partial + S (pa_r_hjas_block_h_product) = S ((S (pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_partial. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_partial * S ((S (pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product) + (pa_r_hjas_block_h_product))) /\ ((((exists pa_h_hjas_block_h_product_successor. pa_h_hjas_block_h_product_successor + S (pa_s_hjas_block_h_product) = S ((S (S pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_successor. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_successor * S ((S (S pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product) + (pa_s_hjas_block_h_product))) /\ pa_s_hjas_block_h_product = pa_r_hjas_block_h_product * pa_p_hjas_block_h_product)))))))
40. 0040rewrite <- hdecomposition_witness_witness_right
41. 0041rewrite <- hdecomposition_witness_witness_right
42. 0042rewrite <- hdecomposition_witness_witness_right
43. 0043rewrite <- hdecomposition_witness_witness_right
44. 0044rewrite <- hdecomposition_witness_witness_right
45. 0045rewrite <- hdecomposition_witness_witness_right
46. 0046exact hh
47. 0047have hblock_j : exists pa_b_hjas_block_j pa_c_hjas_block_j. ((forall pa_i_hjas_block_j_repeat. (exists pa_lt_hjas_block_j_repeat_bound. pa_lt_hjas_block_j_repeat_bound + S pa_i_hjas_block_j_repeat = 12) -> (((exists pa_h_hjas_block_j_repeat_decoded. pa_h_hjas_block_j_repeat_decoded + S ((x + 6 * x1) + 7) = S ((S (pa_i_hjas_block_j_repeat)) * pa_c_hjas_block_j)) /\ exists pa_q_hjas_block_j_repeat_decoded. pa_b_hjas_block_j = pa_q_hjas_block_j_repeat_decoded * S ((S (pa_i_hjas_block_j_repeat)) * pa_c_hjas_block_j) + ((x + 6 * x1) + 7)))) /\ (exists pa_u_hjas_block_j_product pa_v_hjas_block_j_product. ((((exists pa_h_hjas_block_j_product_start. pa_h_hjas_block_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_start. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_start * S ((S (0)) * pa_v_hjas_block_j_product) + (1))) /\ ((((exists pa_h_hjas_block_j_product_terminal. pa_h_hjas_block_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_terminal. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_terminal * S ((S (12)) * pa_v_hjas_block_j_product) + (j))) /\ forall pa_i_hjas_block_j_product. (exists pa_lt_hjas_block_j_product_bound. pa_lt_hjas_block_j_product_bound + S pa_i_hjas_block_j_product = 12) -> exists pa_p_hjas_block_j_product pa_r_hjas_block_j_product pa_s_hjas_block_j_product. ((((exists pa_h_hjas_block_j_product_factor. pa_h_hjas_block_j_product_factor + S (pa_p_hjas_block_j_product) = S ((S (pa_i_hjas_block_j_product)) * pa_c_hjas_block_j)) /\ exists pa_q_hjas_block_j_product_factor. pa_b_hjas_block_j = pa_q_hjas_block_j_product_factor * S ((S (pa_i_hjas_block_j_product)) * pa_c_hjas_block_j) + (pa_p_hjas_block_j_product))) /\ ((((exists pa_h_hjas_block_j_product_partial. pa_h_hjas_block_j_product_partial + S (pa_r_hjas_block_j_product) = S ((S (pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_partial. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_partial * S ((S (pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product) + (pa_r_hjas_block_j_product))) /\ ((((exists pa_h_hjas_block_j_product_successor. pa_h_hjas_block_j_product_successor + S (pa_s_hjas_block_j_product) = S ((S (S pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_successor. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_successor * S ((S (S pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product) + (pa_s_hjas_block_j_product))) /\ pa_s_hjas_block_j_product = pa_r_hjas_block_j_product * pa_p_hjas_block_j_product)))))))
48. 0048rewrite <- hdecomposition_witness_witness_right
49. 0049rewrite <- hdecomposition_witness_witness_right
50. 0050exact hj
51. 0051have hblock_g : exists pa_b_hjas_block_g pa_c_hjas_block_g. ((forall pa_i_hjas_block_g_repeat. (exists pa_lt_hjas_block_g_repeat_bound. pa_lt_hjas_block_g_repeat_bound + S pa_i_hjas_block_g_repeat = (x + 6 * x1) + 5) -> (((exists pa_h_hjas_block_g_repeat_decoded. pa_h_hjas_block_g_repeat_decoded + S (4) = S ((S (pa_i_hjas_block_g_repeat)) * pa_c_hjas_block_g)) /\ exists pa_q_hjas_block_g_repeat_decoded. pa_b_hjas_block_g = pa_q_hjas_block_g_repeat_decoded * S ((S (pa_i_hjas_block_g_repeat)) * pa_c_hjas_block_g) + (4)))) /\ (exists pa_u_hjas_block_g_product pa_v_hjas_block_g_product. ((((exists pa_h_hjas_block_g_product_start. pa_h_hjas_block_g_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_start. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_start * S ((S (0)) * pa_v_hjas_block_g_product) + (1))) /\ ((((exists pa_h_hjas_block_g_product_terminal. pa_h_hjas_block_g_product_terminal + S (g) = S ((S ((x + 6 * x1) + 5)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_terminal. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_terminal * S ((S ((x + 6 * x1) + 5)) * pa_v_hjas_block_g_product) + (g))) /\ forall pa_i_hjas_block_g_product. (exists pa_lt_hjas_block_g_product_bound. pa_lt_hjas_block_g_product_bound + S pa_i_hjas_block_g_product = (x + 6 * x1) + 5) -> exists pa_p_hjas_block_g_product pa_r_hjas_block_g_product pa_s_hjas_block_g_product. ((((exists pa_h_hjas_block_g_product_factor. pa_h_hjas_block_g_product_factor + S (pa_p_hjas_block_g_product) = S ((S (pa_i_hjas_block_g_product)) * pa_c_hjas_block_g)) /\ exists pa_q_hjas_block_g_product_factor. pa_b_hjas_block_g = pa_q_hjas_block_g_product_factor * S ((S (pa_i_hjas_block_g_product)) * pa_c_hjas_block_g) + (pa_p_hjas_block_g_product))) /\ ((((exists pa_h_hjas_block_g_product_partial. pa_h_hjas_block_g_product_partial + S (pa_r_hjas_block_g_product) = S ((S (pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_partial. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_partial * S ((S (pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product) + (pa_r_hjas_block_g_product))) /\ ((((exists pa_h_hjas_block_g_product_successor. pa_h_hjas_block_g_product_successor + S (pa_s_hjas_block_g_product) = S ((S (S pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_successor. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_successor * S ((S (S pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product) + (pa_s_hjas_block_g_product))) /\ pa_s_hjas_block_g_product = pa_r_hjas_block_g_product * pa_p_hjas_block_g_product)))))))
52. 0052rewrite <- hdecomposition_witness_witness_right
53. 0053rewrite <- hdecomposition_witness_witness_right
54. 0054rewrite <- hdecomposition_witness_witness_right
55. 0055rewrite <- hdecomposition_witness_witness_right
56. 0056exact hg
57. 0057specialize hfamily x1
58. 0058specialize hfamily e
59. 0059specialize hfamily h
60. 0060specialize hfamily u
61. 0061specialize hfamily j
62. 0062specialize hfamily g
63. 0063apply hfamily
64. 0064exact hblock_ceiling
65. 0065exact hblock_h
66. 0066exact hu
67. 0067exact hblock_j
68. 0068exact hblock_g