bertrand_hj_six_step_from_total

Exact expanded PA statement

forall s e f h u j g hn un jn gn. (forall bpt_a_hjt_combined bpt_e_hjt_combined. exists bpt_x_hjt_combined. (exists ff_b_bpt_value_hjt_combined ff_c_bpt_value_hjt_combined. ((forall ff_i_bpt_value_hjt_combined_repeat. (exists ff_lt_bpt_value_hjt_combined_repeat_bound. ff_lt_bpt_value_hjt_combined_repeat_bound + S ff_i_bpt_value_hjt_combined_repeat = bpt_e_hjt_combined) -> (((exists ff_h_bpt_value_hjt_combined_repeat_decoded. ff_h_bpt_value_hjt_combined_repeat_decoded + S (bpt_a_hjt_combined) = S ((S (ff_i_bpt_value_hjt_combined_repeat)) * ff_c_bpt_value_hjt_combined)) /\ exists ff_q_bpt_value_hjt_combined_repeat_decoded. ff_b_bpt_value_hjt_combined = ff_q_bpt_value_hjt_combined_repeat_decoded * S ((S (ff_i_bpt_value_hjt_combined_repeat)) * ff_c_bpt_value_hjt_combined) + (bpt_a_hjt_combined)))) /\ (exists ff_u_bpt_value_hjt_combined_product ff_v_bpt_value_hjt_combined_product. ((((exists ff_h_bpt_value_hjt_combined_product_start. ff_h_bpt_value_hjt_combined_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjt_combined_product)) /\ exists ff_q_bpt_value_hjt_combined_product_start. ff_u_bpt_value_hjt_combined_product = ff_q_bpt_value_hjt_combined_product_start * S ((S (0)) * ff_v_bpt_value_hjt_combined_product) + (1))) /\ ((((exists ff_h_bpt_value_hjt_combined_product_terminal. ff_h_bpt_value_hjt_combined_product_terminal + S (bpt_x_hjt_combined) = S ((S (bpt_e_hjt_combined)) * ff_v_bpt_value_hjt_combined_product)) /\ exists ff_q_bpt_value_hjt_combined_product_terminal. ff_u_bpt_value_hjt_combined_product = ff_q_bpt_value_hjt_combined_product_terminal * S ((S (bpt_e_hjt_combined)) * ff_v_bpt_value_hjt_combined_product) + (bpt_x_hjt_combined))) /\ forall ff_i_bpt_value_hjt_combined_product. (exists ff_lt_bpt_value_hjt_combined_product_bound. ff_lt_bpt_value_hjt_combined_product_bound + S ff_i_bpt_value_hjt_combined_product = bpt_e_hjt_combined) -> exists ff_p_bpt_value_hjt_combined_product ff_r_bpt_value_hjt_combined_product ff_s_bpt_value_hjt_combined_product. ((((exists ff_h_bpt_value_hjt_combined_product_factor. ff_h_bpt_value_hjt_combined_product_factor + S (ff_p_bpt_value_hjt_combined_product) = S ((S (ff_i_bpt_value_hjt_combined_product)) * ff_c_bpt_value_hjt_combined)) /\ exists ff_q_bpt_value_hjt_combined_product_factor. ff_b_bpt_value_hjt_combined = ff_q_bpt_value_hjt_combined_product_factor * S ((S (ff_i_bpt_value_hjt_combined_product)) * ff_c_bpt_value_hjt_combined) + (ff_p_bpt_value_hjt_combined_product))) /\ ((((exists ff_h_bpt_value_hjt_combined_product_partial. ff_h_bpt_value_hjt_combined_product_partial + S (ff_r_bpt_value_hjt_combined_product) = S ((S (ff_i_bpt_value_hjt_combined_product)) * ff_v_bpt_value_hjt_combined_product)) /\ exists ff_q_bpt_value_hjt_combined_product_partial. ff_u_bpt_value_hjt_combined_product = ff_q_bpt_value_hjt_combined_product_partial * S ((S (ff_i_bpt_value_hjt_combined_product)) * ff_v_bpt_value_hjt_combined_product) + (ff_r_bpt_value_hjt_combined_product))) /\ ((((exists ff_h_bpt_value_hjt_combined_product_successor. ff_h_bpt_value_hjt_combined_product_successor + S (ff_s_bpt_value_hjt_combined_product) = S ((S (S ff_i_bpt_value_hjt_combined_product)) * ff_v_bpt_value_hjt_combined_product)) /\ exists ff_q_bpt_value_hjt_combined_product_successor. ff_u_bpt_value_hjt_combined_product = ff_q_bpt_value_hjt_combined_product_successor * S ((S (S ff_i_bpt_value_hjt_combined_product)) * ff_v_bpt_value_hjt_combined_product) + (ff_s_bpt_value_hjt_combined_product))) /\ ff_s_bpt_value_hjt_combined_product = ff_r_bpt_value_hjt_combined_product * ff_p_bpt_value_hjt_combined_product))))))))) -> (exists bqb_le_gap_hjt_combined_lower. bqb_le_gap_hjt_combined_lower + (5) = (s)) -> (((exists bcs_lower_gap_hjt_combined_ceiling. bcs_lower_gap_hjt_combined_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_hjt_combined_ceiling. bcs_upper_gap_hjt_combined_ceiling + S (6 * (e)) = (s * s) + 6)) -> (((exists bcs_lower_gap_hjt_combined_next_ceiling. bcs_lower_gap_hjt_combined_next_ceiling + ((s + 6) * (s + 6)) = 6 * (f)) /\ exists bcs_upper_gap_hjt_combined_next_ceiling. bcs_upper_gap_hjt_combined_next_ceiling + S (6 * (f)) = ((s + 6) * (s + 6)) + 6)) -> (exists pa_b_hjt_combined_h pa_c_hjt_combined_h. ((forall pa_i_hjt_combined_h_repeat. (exists pa_lt_hjt_combined_h_repeat_bound. pa_lt_hjt_combined_h_repeat_bound + S pa_i_hjt_combined_h_repeat = 2 * s + 2) -> (((exists pa_h_hjt_combined_h_repeat_decoded. pa_h_hjt_combined_h_repeat_decoded + S (s + 1) = S ((S (pa_i_hjt_combined_h_repeat)) * pa_c_hjt_combined_h)) /\ exists pa_q_hjt_combined_h_repeat_decoded. pa_b_hjt_combined_h = pa_q_hjt_combined_h_repeat_decoded * S ((S (pa_i_hjt_combined_h_repeat)) * pa_c_hjt_combined_h) + (s + 1)))) /\ (exists pa_u_hjt_combined_h_product pa_v_hjt_combined_h_product. ((((exists pa_h_hjt_combined_h_product_start. pa_h_hjt_combined_h_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_h_product)) /\ exists pa_q_hjt_combined_h_product_start. pa_u_hjt_combined_h_product = pa_q_hjt_combined_h_product_start * S ((S (0)) * pa_v_hjt_combined_h_product) + (1))) /\ ((((exists pa_h_hjt_combined_h_product_terminal. pa_h_hjt_combined_h_product_terminal + S (h) = S ((S (2 * s + 2)) * pa_v_hjt_combined_h_product)) /\ exists pa_q_hjt_combined_h_product_terminal. pa_u_hjt_combined_h_product = pa_q_hjt_combined_h_product_terminal * S ((S (2 * s + 2)) * pa_v_hjt_combined_h_product) + (h))) /\ forall pa_i_hjt_combined_h_product. (exists pa_lt_hjt_combined_h_product_bound. pa_lt_hjt_combined_h_product_bound + S pa_i_hjt_combined_h_product = 2 * s + 2) -> exists pa_p_hjt_combined_h_product pa_r_hjt_combined_h_product pa_s_hjt_combined_h_product. ((((exists pa_h_hjt_combined_h_product_factor. pa_h_hjt_combined_h_product_factor + S (pa_p_hjt_combined_h_product) = S ((S (pa_i_hjt_combined_h_product)) * pa_c_hjt_combined_h)) /\ exists pa_q_hjt_combined_h_product_factor. pa_b_hjt_combined_h = pa_q_hjt_combined_h_product_factor * S ((S (pa_i_hjt_combined_h_product)) * pa_c_hjt_combined_h) + (pa_p_hjt_combined_h_product))) /\ ((((exists pa_h_hjt_combined_h_product_partial. pa_h_hjt_combined_h_product_partial + S (pa_r_hjt_combined_h_product) = S ((S (pa_i_hjt_combined_h_product)) * pa_v_hjt_combined_h_product)) /\ exists pa_q_hjt_combined_h_product_partial. pa_u_hjt_combined_h_product = pa_q_hjt_combined_h_product_partial * S ((S (pa_i_hjt_combined_h_product)) * pa_v_hjt_combined_h_product) + (pa_r_hjt_combined_h_product))) /\ ((((exists pa_h_hjt_combined_h_product_successor. pa_h_hjt_combined_h_product_successor + S (pa_s_hjt_combined_h_product) = S ((S (S pa_i_hjt_combined_h_product)) * pa_v_hjt_combined_h_product)) /\ exists pa_q_hjt_combined_h_product_successor. pa_u_hjt_combined_h_product = pa_q_hjt_combined_h_product_successor * S ((S (S pa_i_hjt_combined_h_product)) * pa_v_hjt_combined_h_product) + (pa_s_hjt_combined_h_product))) /\ pa_s_hjt_combined_h_product = pa_r_hjt_combined_h_product * pa_p_hjt_combined_h_product)))))))) -> (exists pa_b_hjt_combined_h_bound pa_c_hjt_combined_h_bound. ((forall pa_i_hjt_combined_h_bound_repeat. (exists pa_lt_hjt_combined_h_bound_repeat_bound. pa_lt_hjt_combined_h_bound_repeat_bound + S pa_i_hjt_combined_h_bound_repeat = e) -> (((exists pa_h_hjt_combined_h_bound_repeat_decoded. pa_h_hjt_combined_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_combined_h_bound_repeat)) * pa_c_hjt_combined_h_bound)) /\ exists pa_q_hjt_combined_h_bound_repeat_decoded. pa_b_hjt_combined_h_bound = pa_q_hjt_combined_h_bound_repeat_decoded * S ((S (pa_i_hjt_combined_h_bound_repeat)) * pa_c_hjt_combined_h_bound) + (4)))) /\ (exists pa_u_hjt_combined_h_bound_product pa_v_hjt_combined_h_bound_product. ((((exists pa_h_hjt_combined_h_bound_product_start. pa_h_hjt_combined_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_h_bound_product)) /\ exists pa_q_hjt_combined_h_bound_product_start. pa_u_hjt_combined_h_bound_product = pa_q_hjt_combined_h_bound_product_start * S ((S (0)) * pa_v_hjt_combined_h_bound_product) + (1))) /\ ((((exists pa_h_hjt_combined_h_bound_product_terminal. pa_h_hjt_combined_h_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hjt_combined_h_bound_product)) /\ exists pa_q_hjt_combined_h_bound_product_terminal. pa_u_hjt_combined_h_bound_product = pa_q_hjt_combined_h_bound_product_terminal * S ((S (e)) * pa_v_hjt_combined_h_bound_product) + (u))) /\ forall pa_i_hjt_combined_h_bound_product. (exists pa_lt_hjt_combined_h_bound_product_bound. pa_lt_hjt_combined_h_bound_product_bound + S pa_i_hjt_combined_h_bound_product = e) -> exists pa_p_hjt_combined_h_bound_product pa_r_hjt_combined_h_bound_product pa_s_hjt_combined_h_bound_product. ((((exists pa_h_hjt_combined_h_bound_product_factor. pa_h_hjt_combined_h_bound_product_factor + S (pa_p_hjt_combined_h_bound_product) = S ((S (pa_i_hjt_combined_h_bound_product)) * pa_c_hjt_combined_h_bound)) /\ exists pa_q_hjt_combined_h_bound_product_factor. pa_b_hjt_combined_h_bound = pa_q_hjt_combined_h_bound_product_factor * S ((S (pa_i_hjt_combined_h_bound_product)) * pa_c_hjt_combined_h_bound) + (pa_p_hjt_combined_h_bound_product))) /\ ((((exists pa_h_hjt_combined_h_bound_product_partial. pa_h_hjt_combined_h_bound_product_partial + S (pa_r_hjt_combined_h_bound_product) = S ((S (pa_i_hjt_combined_h_bound_product)) * pa_v_hjt_combined_h_bound_product)) /\ exists pa_q_hjt_combined_h_bound_product_partial. pa_u_hjt_combined_h_bound_product = pa_q_hjt_combined_h_bound_product_partial * S ((S (pa_i_hjt_combined_h_bound_product)) * pa_v_hjt_combined_h_bound_product) + (pa_r_hjt_combined_h_bound_product))) /\ ((((exists pa_h_hjt_combined_h_bound_product_successor. pa_h_hjt_combined_h_bound_product_successor + S (pa_s_hjt_combined_h_bound_product) = S ((S (S pa_i_hjt_combined_h_bound_product)) * pa_v_hjt_combined_h_bound_product)) /\ exists pa_q_hjt_combined_h_bound_product_successor. pa_u_hjt_combined_h_bound_product = pa_q_hjt_combined_h_bound_product_successor * S ((S (S pa_i_hjt_combined_h_bound_product)) * pa_v_hjt_combined_h_bound_product) + (pa_s_hjt_combined_h_bound_product))) /\ pa_s_hjt_combined_h_bound_product = pa_r_hjt_combined_h_bound_product * pa_p_hjt_combined_h_bound_product)))))))) -> (exists pa_b_hjt_combined_j pa_c_hjt_combined_j. ((forall pa_i_hjt_combined_j_repeat. (exists pa_lt_hjt_combined_j_repeat_bound. pa_lt_hjt_combined_j_repeat_bound + S pa_i_hjt_combined_j_repeat = 12) -> (((exists pa_h_hjt_combined_j_repeat_decoded. pa_h_hjt_combined_j_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_combined_j_repeat)) * pa_c_hjt_combined_j)) /\ exists pa_q_hjt_combined_j_repeat_decoded. pa_b_hjt_combined_j = pa_q_hjt_combined_j_repeat_decoded * S ((S (pa_i_hjt_combined_j_repeat)) * pa_c_hjt_combined_j) + (s + 7)))) /\ (exists pa_u_hjt_combined_j_product pa_v_hjt_combined_j_product. ((((exists pa_h_hjt_combined_j_product_start. pa_h_hjt_combined_j_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_j_product)) /\ exists pa_q_hjt_combined_j_product_start. pa_u_hjt_combined_j_product = pa_q_hjt_combined_j_product_start * S ((S (0)) * pa_v_hjt_combined_j_product) + (1))) /\ ((((exists pa_h_hjt_combined_j_product_terminal. pa_h_hjt_combined_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjt_combined_j_product)) /\ exists pa_q_hjt_combined_j_product_terminal. pa_u_hjt_combined_j_product = pa_q_hjt_combined_j_product_terminal * S ((S (12)) * pa_v_hjt_combined_j_product) + (j))) /\ forall pa_i_hjt_combined_j_product. (exists pa_lt_hjt_combined_j_product_bound. pa_lt_hjt_combined_j_product_bound + S pa_i_hjt_combined_j_product = 12) -> exists pa_p_hjt_combined_j_product pa_r_hjt_combined_j_product pa_s_hjt_combined_j_product. ((((exists pa_h_hjt_combined_j_product_factor. pa_h_hjt_combined_j_product_factor + S (pa_p_hjt_combined_j_product) = S ((S (pa_i_hjt_combined_j_product)) * pa_c_hjt_combined_j)) /\ exists pa_q_hjt_combined_j_product_factor. pa_b_hjt_combined_j = pa_q_hjt_combined_j_product_factor * S ((S (pa_i_hjt_combined_j_product)) * pa_c_hjt_combined_j) + (pa_p_hjt_combined_j_product))) /\ ((((exists pa_h_hjt_combined_j_product_partial. pa_h_hjt_combined_j_product_partial + S (pa_r_hjt_combined_j_product) = S ((S (pa_i_hjt_combined_j_product)) * pa_v_hjt_combined_j_product)) /\ exists pa_q_hjt_combined_j_product_partial. pa_u_hjt_combined_j_product = pa_q_hjt_combined_j_product_partial * S ((S (pa_i_hjt_combined_j_product)) * pa_v_hjt_combined_j_product) + (pa_r_hjt_combined_j_product))) /\ ((((exists pa_h_hjt_combined_j_product_successor. pa_h_hjt_combined_j_product_successor + S (pa_s_hjt_combined_j_product) = S ((S (S pa_i_hjt_combined_j_product)) * pa_v_hjt_combined_j_product)) /\ exists pa_q_hjt_combined_j_product_successor. pa_u_hjt_combined_j_product = pa_q_hjt_combined_j_product_successor * S ((S (S pa_i_hjt_combined_j_product)) * pa_v_hjt_combined_j_product) + (pa_s_hjt_combined_j_product))) /\ pa_s_hjt_combined_j_product = pa_r_hjt_combined_j_product * pa_p_hjt_combined_j_product)))))))) -> (exists pa_b_hjt_combined_j_bound pa_c_hjt_combined_j_bound. ((forall pa_i_hjt_combined_j_bound_repeat. (exists pa_lt_hjt_combined_j_bound_repeat_bound. pa_lt_hjt_combined_j_bound_repeat_bound + S pa_i_hjt_combined_j_bound_repeat = s + 5) -> (((exists pa_h_hjt_combined_j_bound_repeat_decoded. pa_h_hjt_combined_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_combined_j_bound_repeat)) * pa_c_hjt_combined_j_bound)) /\ exists pa_q_hjt_combined_j_bound_repeat_decoded. pa_b_hjt_combined_j_bound = pa_q_hjt_combined_j_bound_repeat_decoded * S ((S (pa_i_hjt_combined_j_bound_repeat)) * pa_c_hjt_combined_j_bound) + (4)))) /\ (exists pa_u_hjt_combined_j_bound_product pa_v_hjt_combined_j_bound_product. ((((exists pa_h_hjt_combined_j_bound_product_start. pa_h_hjt_combined_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_j_bound_product)) /\ exists pa_q_hjt_combined_j_bound_product_start. pa_u_hjt_combined_j_bound_product = pa_q_hjt_combined_j_bound_product_start * S ((S (0)) * pa_v_hjt_combined_j_bound_product) + (1))) /\ ((((exists pa_h_hjt_combined_j_bound_product_terminal. pa_h_hjt_combined_j_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hjt_combined_j_bound_product)) /\ exists pa_q_hjt_combined_j_bound_product_terminal. pa_u_hjt_combined_j_bound_product = pa_q_hjt_combined_j_bound_product_terminal * S ((S (s + 5)) * pa_v_hjt_combined_j_bound_product) + (g))) /\ forall pa_i_hjt_combined_j_bound_product. (exists pa_lt_hjt_combined_j_bound_product_bound. pa_lt_hjt_combined_j_bound_product_bound + S pa_i_hjt_combined_j_bound_product = s + 5) -> exists pa_p_hjt_combined_j_bound_product pa_r_hjt_combined_j_bound_product pa_s_hjt_combined_j_bound_product. ((((exists pa_h_hjt_combined_j_bound_product_factor. pa_h_hjt_combined_j_bound_product_factor + S (pa_p_hjt_combined_j_bound_product) = S ((S (pa_i_hjt_combined_j_bound_product)) * pa_c_hjt_combined_j_bound)) /\ exists pa_q_hjt_combined_j_bound_product_factor. pa_b_hjt_combined_j_bound = pa_q_hjt_combined_j_bound_product_factor * S ((S (pa_i_hjt_combined_j_bound_product)) * pa_c_hjt_combined_j_bound) + (pa_p_hjt_combined_j_bound_product))) /\ ((((exists pa_h_hjt_combined_j_bound_product_partial. pa_h_hjt_combined_j_bound_product_partial + S (pa_r_hjt_combined_j_bound_product) = S ((S (pa_i_hjt_combined_j_bound_product)) * pa_v_hjt_combined_j_bound_product)) /\ exists pa_q_hjt_combined_j_bound_product_partial. pa_u_hjt_combined_j_bound_product = pa_q_hjt_combined_j_bound_product_partial * S ((S (pa_i_hjt_combined_j_bound_product)) * pa_v_hjt_combined_j_bound_product) + (pa_r_hjt_combined_j_bound_product))) /\ ((((exists pa_h_hjt_combined_j_bound_product_successor. pa_h_hjt_combined_j_bound_product_successor + S (pa_s_hjt_combined_j_bound_product) = S ((S (S pa_i_hjt_combined_j_bound_product)) * pa_v_hjt_combined_j_bound_product)) /\ exists pa_q_hjt_combined_j_bound_product_successor. pa_u_hjt_combined_j_bound_product = pa_q_hjt_combined_j_bound_product_successor * S ((S (S pa_i_hjt_combined_j_bound_product)) * pa_v_hjt_combined_j_bound_product) + (pa_s_hjt_combined_j_bound_product))) /\ pa_s_hjt_combined_j_bound_product = pa_r_hjt_combined_j_bound_product * pa_p_hjt_combined_j_bound_product)))))))) -> (((exists bqb_le_gap_hjt_combined_h_result. bqb_le_gap_hjt_combined_h_result + (h) = (u)) /\ (exists bqb_le_gap_hjt_combined_j_result. bqb_le_gap_hjt_combined_j_result + (j) = (g)))) -> (exists pa_b_hjt_combined_h_next pa_c_hjt_combined_h_next. ((forall pa_i_hjt_combined_h_next_repeat. (exists pa_lt_hjt_combined_h_next_repeat_bound. pa_lt_hjt_combined_h_next_repeat_bound + S pa_i_hjt_combined_h_next_repeat = 2 * s + 14) -> (((exists pa_h_hjt_combined_h_next_repeat_decoded. pa_h_hjt_combined_h_next_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_combined_h_next_repeat)) * pa_c_hjt_combined_h_next)) /\ exists pa_q_hjt_combined_h_next_repeat_decoded. pa_b_hjt_combined_h_next = pa_q_hjt_combined_h_next_repeat_decoded * S ((S (pa_i_hjt_combined_h_next_repeat)) * pa_c_hjt_combined_h_next) + (s + 7)))) /\ (exists pa_u_hjt_combined_h_next_product pa_v_hjt_combined_h_next_product. ((((exists pa_h_hjt_combined_h_next_product_start. pa_h_hjt_combined_h_next_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_h_next_product)) /\ exists pa_q_hjt_combined_h_next_product_start. pa_u_hjt_combined_h_next_product = pa_q_hjt_combined_h_next_product_start * S ((S (0)) * pa_v_hjt_combined_h_next_product) + (1))) /\ ((((exists pa_h_hjt_combined_h_next_product_terminal. pa_h_hjt_combined_h_next_product_terminal + S (hn) = S ((S (2 * s + 14)) * pa_v_hjt_combined_h_next_product)) /\ exists pa_q_hjt_combined_h_next_product_terminal. pa_u_hjt_combined_h_next_product = pa_q_hjt_combined_h_next_product_terminal * S ((S (2 * s + 14)) * pa_v_hjt_combined_h_next_product) + (hn))) /\ forall pa_i_hjt_combined_h_next_product. (exists pa_lt_hjt_combined_h_next_product_bound. pa_lt_hjt_combined_h_next_product_bound + S pa_i_hjt_combined_h_next_product = 2 * s + 14) -> exists pa_p_hjt_combined_h_next_product pa_r_hjt_combined_h_next_product pa_s_hjt_combined_h_next_product. ((((exists pa_h_hjt_combined_h_next_product_factor. pa_h_hjt_combined_h_next_product_factor + S (pa_p_hjt_combined_h_next_product) = S ((S (pa_i_hjt_combined_h_next_product)) * pa_c_hjt_combined_h_next)) /\ exists pa_q_hjt_combined_h_next_product_factor. pa_b_hjt_combined_h_next = pa_q_hjt_combined_h_next_product_factor * S ((S (pa_i_hjt_combined_h_next_product)) * pa_c_hjt_combined_h_next) + (pa_p_hjt_combined_h_next_product))) /\ ((((exists pa_h_hjt_combined_h_next_product_partial. pa_h_hjt_combined_h_next_product_partial + S (pa_r_hjt_combined_h_next_product) = S ((S (pa_i_hjt_combined_h_next_product)) * pa_v_hjt_combined_h_next_product)) /\ exists pa_q_hjt_combined_h_next_product_partial. pa_u_hjt_combined_h_next_product = pa_q_hjt_combined_h_next_product_partial * S ((S (pa_i_hjt_combined_h_next_product)) * pa_v_hjt_combined_h_next_product) + (pa_r_hjt_combined_h_next_product))) /\ ((((exists pa_h_hjt_combined_h_next_product_successor. pa_h_hjt_combined_h_next_product_successor + S (pa_s_hjt_combined_h_next_product) = S ((S (S pa_i_hjt_combined_h_next_product)) * pa_v_hjt_combined_h_next_product)) /\ exists pa_q_hjt_combined_h_next_product_successor. pa_u_hjt_combined_h_next_product = pa_q_hjt_combined_h_next_product_successor * S ((S (S pa_i_hjt_combined_h_next_product)) * pa_v_hjt_combined_h_next_product) + (pa_s_hjt_combined_h_next_product))) /\ pa_s_hjt_combined_h_next_product = pa_r_hjt_combined_h_next_product * pa_p_hjt_combined_h_next_product)))))))) -> (exists pa_b_hjt_combined_h_next_bound pa_c_hjt_combined_h_next_bound. ((forall pa_i_hjt_combined_h_next_bound_repeat. (exists pa_lt_hjt_combined_h_next_bound_repeat_bound. pa_lt_hjt_combined_h_next_bound_repeat_bound + S pa_i_hjt_combined_h_next_bound_repeat = f) -> (((exists pa_h_hjt_combined_h_next_bound_repeat_decoded. pa_h_hjt_combined_h_next_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_combined_h_next_bound_repeat)) * pa_c_hjt_combined_h_next_bound)) /\ exists pa_q_hjt_combined_h_next_bound_repeat_decoded. pa_b_hjt_combined_h_next_bound = pa_q_hjt_combined_h_next_bound_repeat_decoded * S ((S (pa_i_hjt_combined_h_next_bound_repeat)) * pa_c_hjt_combined_h_next_bound) + (4)))) /\ (exists pa_u_hjt_combined_h_next_bound_product pa_v_hjt_combined_h_next_bound_product. ((((exists pa_h_hjt_combined_h_next_bound_product_start. pa_h_hjt_combined_h_next_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_h_next_bound_product)) /\ exists pa_q_hjt_combined_h_next_bound_product_start. pa_u_hjt_combined_h_next_bound_product = pa_q_hjt_combined_h_next_bound_product_start * S ((S (0)) * pa_v_hjt_combined_h_next_bound_product) + (1))) /\ ((((exists pa_h_hjt_combined_h_next_bound_product_terminal. pa_h_hjt_combined_h_next_bound_product_terminal + S (un) = S ((S (f)) * pa_v_hjt_combined_h_next_bound_product)) /\ exists pa_q_hjt_combined_h_next_bound_product_terminal. pa_u_hjt_combined_h_next_bound_product = pa_q_hjt_combined_h_next_bound_product_terminal * S ((S (f)) * pa_v_hjt_combined_h_next_bound_product) + (un))) /\ forall pa_i_hjt_combined_h_next_bound_product. (exists pa_lt_hjt_combined_h_next_bound_product_bound. pa_lt_hjt_combined_h_next_bound_product_bound + S pa_i_hjt_combined_h_next_bound_product = f) -> exists pa_p_hjt_combined_h_next_bound_product pa_r_hjt_combined_h_next_bound_product pa_s_hjt_combined_h_next_bound_product. ((((exists pa_h_hjt_combined_h_next_bound_product_factor. pa_h_hjt_combined_h_next_bound_product_factor + S (pa_p_hjt_combined_h_next_bound_product) = S ((S (pa_i_hjt_combined_h_next_bound_product)) * pa_c_hjt_combined_h_next_bound)) /\ exists pa_q_hjt_combined_h_next_bound_product_factor. pa_b_hjt_combined_h_next_bound = pa_q_hjt_combined_h_next_bound_product_factor * S ((S (pa_i_hjt_combined_h_next_bound_product)) * pa_c_hjt_combined_h_next_bound) + (pa_p_hjt_combined_h_next_bound_product))) /\ ((((exists pa_h_hjt_combined_h_next_bound_product_partial. pa_h_hjt_combined_h_next_bound_product_partial + S (pa_r_hjt_combined_h_next_bound_product) = S ((S (pa_i_hjt_combined_h_next_bound_product)) * pa_v_hjt_combined_h_next_bound_product)) /\ exists pa_q_hjt_combined_h_next_bound_product_partial. pa_u_hjt_combined_h_next_bound_product = pa_q_hjt_combined_h_next_bound_product_partial * S ((S (pa_i_hjt_combined_h_next_bound_product)) * pa_v_hjt_combined_h_next_bound_product) + (pa_r_hjt_combined_h_next_bound_product))) /\ ((((exists pa_h_hjt_combined_h_next_bound_product_successor. pa_h_hjt_combined_h_next_bound_product_successor + S (pa_s_hjt_combined_h_next_bound_product) = S ((S (S pa_i_hjt_combined_h_next_bound_product)) * pa_v_hjt_combined_h_next_bound_product)) /\ exists pa_q_hjt_combined_h_next_bound_product_successor. pa_u_hjt_combined_h_next_bound_product = pa_q_hjt_combined_h_next_bound_product_successor * S ((S (S pa_i_hjt_combined_h_next_bound_product)) * pa_v_hjt_combined_h_next_bound_product) + (pa_s_hjt_combined_h_next_bound_product))) /\ pa_s_hjt_combined_h_next_bound_product = pa_r_hjt_combined_h_next_bound_product * pa_p_hjt_combined_h_next_bound_product)))))))) -> (exists pa_b_hjt_combined_j_next pa_c_hjt_combined_j_next. ((forall pa_i_hjt_combined_j_next_repeat. (exists pa_lt_hjt_combined_j_next_repeat_bound. pa_lt_hjt_combined_j_next_repeat_bound + S pa_i_hjt_combined_j_next_repeat = 12) -> (((exists pa_h_hjt_combined_j_next_repeat_decoded. pa_h_hjt_combined_j_next_repeat_decoded + S (s + 13) = S ((S (pa_i_hjt_combined_j_next_repeat)) * pa_c_hjt_combined_j_next)) /\ exists pa_q_hjt_combined_j_next_repeat_decoded. pa_b_hjt_combined_j_next = pa_q_hjt_combined_j_next_repeat_decoded * S ((S (pa_i_hjt_combined_j_next_repeat)) * pa_c_hjt_combined_j_next) + (s + 13)))) /\ (exists pa_u_hjt_combined_j_next_product pa_v_hjt_combined_j_next_product. ((((exists pa_h_hjt_combined_j_next_product_start. pa_h_hjt_combined_j_next_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_j_next_product)) /\ exists pa_q_hjt_combined_j_next_product_start. pa_u_hjt_combined_j_next_product = pa_q_hjt_combined_j_next_product_start * S ((S (0)) * pa_v_hjt_combined_j_next_product) + (1))) /\ ((((exists pa_h_hjt_combined_j_next_product_terminal. pa_h_hjt_combined_j_next_product_terminal + S (jn) = S ((S (12)) * pa_v_hjt_combined_j_next_product)) /\ exists pa_q_hjt_combined_j_next_product_terminal. pa_u_hjt_combined_j_next_product = pa_q_hjt_combined_j_next_product_terminal * S ((S (12)) * pa_v_hjt_combined_j_next_product) + (jn))) /\ forall pa_i_hjt_combined_j_next_product. (exists pa_lt_hjt_combined_j_next_product_bound. pa_lt_hjt_combined_j_next_product_bound + S pa_i_hjt_combined_j_next_product = 12) -> exists pa_p_hjt_combined_j_next_product pa_r_hjt_combined_j_next_product pa_s_hjt_combined_j_next_product. ((((exists pa_h_hjt_combined_j_next_product_factor. pa_h_hjt_combined_j_next_product_factor + S (pa_p_hjt_combined_j_next_product) = S ((S (pa_i_hjt_combined_j_next_product)) * pa_c_hjt_combined_j_next)) /\ exists pa_q_hjt_combined_j_next_product_factor. pa_b_hjt_combined_j_next = pa_q_hjt_combined_j_next_product_factor * S ((S (pa_i_hjt_combined_j_next_product)) * pa_c_hjt_combined_j_next) + (pa_p_hjt_combined_j_next_product))) /\ ((((exists pa_h_hjt_combined_j_next_product_partial. pa_h_hjt_combined_j_next_product_partial + S (pa_r_hjt_combined_j_next_product) = S ((S (pa_i_hjt_combined_j_next_product)) * pa_v_hjt_combined_j_next_product)) /\ exists pa_q_hjt_combined_j_next_product_partial. pa_u_hjt_combined_j_next_product = pa_q_hjt_combined_j_next_product_partial * S ((S (pa_i_hjt_combined_j_next_product)) * pa_v_hjt_combined_j_next_product) + (pa_r_hjt_combined_j_next_product))) /\ ((((exists pa_h_hjt_combined_j_next_product_successor. pa_h_hjt_combined_j_next_product_successor + S (pa_s_hjt_combined_j_next_product) = S ((S (S pa_i_hjt_combined_j_next_product)) * pa_v_hjt_combined_j_next_product)) /\ exists pa_q_hjt_combined_j_next_product_successor. pa_u_hjt_combined_j_next_product = pa_q_hjt_combined_j_next_product_successor * S ((S (S pa_i_hjt_combined_j_next_product)) * pa_v_hjt_combined_j_next_product) + (pa_s_hjt_combined_j_next_product))) /\ pa_s_hjt_combined_j_next_product = pa_r_hjt_combined_j_next_product * pa_p_hjt_combined_j_next_product)))))))) -> (exists pa_b_hjt_combined_j_next_bound pa_c_hjt_combined_j_next_bound. ((forall pa_i_hjt_combined_j_next_bound_repeat. (exists pa_lt_hjt_combined_j_next_bound_repeat_bound. pa_lt_hjt_combined_j_next_bound_repeat_bound + S pa_i_hjt_combined_j_next_bound_repeat = s + 11) -> (((exists pa_h_hjt_combined_j_next_bound_repeat_decoded. pa_h_hjt_combined_j_next_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_combined_j_next_bound_repeat)) * pa_c_hjt_combined_j_next_bound)) /\ exists pa_q_hjt_combined_j_next_bound_repeat_decoded. pa_b_hjt_combined_j_next_bound = pa_q_hjt_combined_j_next_bound_repeat_decoded * S ((S (pa_i_hjt_combined_j_next_bound_repeat)) * pa_c_hjt_combined_j_next_bound) + (4)))) /\ (exists pa_u_hjt_combined_j_next_bound_product pa_v_hjt_combined_j_next_bound_product. ((((exists pa_h_hjt_combined_j_next_bound_product_start. pa_h_hjt_combined_j_next_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_combined_j_next_bound_product)) /\ exists pa_q_hjt_combined_j_next_bound_product_start. pa_u_hjt_combined_j_next_bound_product = pa_q_hjt_combined_j_next_bound_product_start * S ((S (0)) * pa_v_hjt_combined_j_next_bound_product) + (1))) /\ ((((exists pa_h_hjt_combined_j_next_bound_product_terminal. pa_h_hjt_combined_j_next_bound_product_terminal + S (gn) = S ((S (s + 11)) * pa_v_hjt_combined_j_next_bound_product)) /\ exists pa_q_hjt_combined_j_next_bound_product_terminal. pa_u_hjt_combined_j_next_bound_product = pa_q_hjt_combined_j_next_bound_product_terminal * S ((S (s + 11)) * pa_v_hjt_combined_j_next_bound_product) + (gn))) /\ forall pa_i_hjt_combined_j_next_bound_product. (exists pa_lt_hjt_combined_j_next_bound_product_bound. pa_lt_hjt_combined_j_next_bound_product_bound + S pa_i_hjt_combined_j_next_bound_product = s + 11) -> exists pa_p_hjt_combined_j_next_bound_product pa_r_hjt_combined_j_next_bound_product pa_s_hjt_combined_j_next_bound_product. ((((exists pa_h_hjt_combined_j_next_bound_product_factor. pa_h_hjt_combined_j_next_bound_product_factor + S (pa_p_hjt_combined_j_next_bound_product) = S ((S (pa_i_hjt_combined_j_next_bound_product)) * pa_c_hjt_combined_j_next_bound)) /\ exists pa_q_hjt_combined_j_next_bound_product_factor. pa_b_hjt_combined_j_next_bound = pa_q_hjt_combined_j_next_bound_product_factor * S ((S (pa_i_hjt_combined_j_next_bound_product)) * pa_c_hjt_combined_j_next_bound) + (pa_p_hjt_combined_j_next_bound_product))) /\ ((((exists pa_h_hjt_combined_j_next_bound_product_partial. pa_h_hjt_combined_j_next_bound_product_partial + S (pa_r_hjt_combined_j_next_bound_product) = S ((S (pa_i_hjt_combined_j_next_bound_product)) * pa_v_hjt_combined_j_next_bound_product)) /\ exists pa_q_hjt_combined_j_next_bound_product_partial. pa_u_hjt_combined_j_next_bound_product = pa_q_hjt_combined_j_next_bound_product_partial * S ((S (pa_i_hjt_combined_j_next_bound_product)) * pa_v_hjt_combined_j_next_bound_product) + (pa_r_hjt_combined_j_next_bound_product))) /\ ((((exists pa_h_hjt_combined_j_next_bound_product_successor. pa_h_hjt_combined_j_next_bound_product_successor + S (pa_s_hjt_combined_j_next_bound_product) = S ((S (S pa_i_hjt_combined_j_next_bound_product)) * pa_v_hjt_combined_j_next_bound_product)) /\ exists pa_q_hjt_combined_j_next_bound_product_successor. pa_u_hjt_combined_j_next_bound_product = pa_q_hjt_combined_j_next_bound_product_successor * S ((S (S pa_i_hjt_combined_j_next_bound_product)) * pa_v_hjt_combined_j_next_bound_product) + (pa_s_hjt_combined_j_next_bound_product))) /\ pa_s_hjt_combined_j_next_bound_product = pa_r_hjt_combined_j_next_bound_product * pa_p_hjt_combined_j_next_bound_product)))))))) -> (((exists bqb_le_gap_hjt_combined_h_next_result. bqb_le_gap_hjt_combined_h_next_result + (hn) = (un)) /\ (exists bqb_le_gap_hjt_combined_j_next_result. bqb_le_gap_hjt_combined_j_next_result + (jn) = (gn))))