BT00SW

bertrand_h_six_step_transport_from_total

Alpha body-checked · checked-use disabled

H(s) and J(s) together imply H(s+6).

Exact expanded PA statement

forall s e f h u j g hn un. (forall bpt_a_hjt_h bpt_e_hjt_h. exists bpt_x_hjt_h. (exists ff_b_bpt_value_hjt_h ff_c_bpt_value_hjt_h. ((forall ff_i_bpt_value_hjt_h_repeat. (exists ff_lt_bpt_value_hjt_h_repeat_bound. ff_lt_bpt_value_hjt_h_repeat_bound + S ff_i_bpt_value_hjt_h_repeat = bpt_e_hjt_h) -> (((exists ff_h_bpt_value_hjt_h_repeat_decoded. ff_h_bpt_value_hjt_h_repeat_decoded + S (bpt_a_hjt_h) = S ((S (ff_i_bpt_value_hjt_h_repeat)) * ff_c_bpt_value_hjt_h)) /\ exists ff_q_bpt_value_hjt_h_repeat_decoded. ff_b_bpt_value_hjt_h = ff_q_bpt_value_hjt_h_repeat_decoded * S ((S (ff_i_bpt_value_hjt_h_repeat)) * ff_c_bpt_value_hjt_h) + (bpt_a_hjt_h)))) /\ (exists ff_u_bpt_value_hjt_h_product ff_v_bpt_value_hjt_h_product. ((((exists ff_h_bpt_value_hjt_h_product_start. ff_h_bpt_value_hjt_h_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjt_h_product)) /\ exists ff_q_bpt_value_hjt_h_product_start. ff_u_bpt_value_hjt_h_product = ff_q_bpt_value_hjt_h_product_start * S ((S (0)) * ff_v_bpt_value_hjt_h_product) + (1))) /\ ((((exists ff_h_bpt_value_hjt_h_product_terminal. ff_h_bpt_value_hjt_h_product_terminal + S (bpt_x_hjt_h) = S ((S (bpt_e_hjt_h)) * ff_v_bpt_value_hjt_h_product)) /\ exists ff_q_bpt_value_hjt_h_product_terminal. ff_u_bpt_value_hjt_h_product = ff_q_bpt_value_hjt_h_product_terminal * S ((S (bpt_e_hjt_h)) * ff_v_bpt_value_hjt_h_product) + (bpt_x_hjt_h))) /\ forall ff_i_bpt_value_hjt_h_product. (exists ff_lt_bpt_value_hjt_h_product_bound. ff_lt_bpt_value_hjt_h_product_bound + S ff_i_bpt_value_hjt_h_product = bpt_e_hjt_h) -> exists ff_p_bpt_value_hjt_h_product ff_r_bpt_value_hjt_h_product ff_s_bpt_value_hjt_h_product. ((((exists ff_h_bpt_value_hjt_h_product_factor. ff_h_bpt_value_hjt_h_product_factor + S (ff_p_bpt_value_hjt_h_product) = S ((S (ff_i_bpt_value_hjt_h_product)) * ff_c_bpt_value_hjt_h)) /\ exists ff_q_bpt_value_hjt_h_product_factor. ff_b_bpt_value_hjt_h = ff_q_bpt_value_hjt_h_product_factor * S ((S (ff_i_bpt_value_hjt_h_product)) * ff_c_bpt_value_hjt_h) + (ff_p_bpt_value_hjt_h_product))) /\ ((((exists ff_h_bpt_value_hjt_h_product_partial. ff_h_bpt_value_hjt_h_product_partial + S (ff_r_bpt_value_hjt_h_product) = S ((S (ff_i_bpt_value_hjt_h_product)) * ff_v_bpt_value_hjt_h_product)) /\ exists ff_q_bpt_value_hjt_h_product_partial. ff_u_bpt_value_hjt_h_product = ff_q_bpt_value_hjt_h_product_partial * S ((S (ff_i_bpt_value_hjt_h_product)) * ff_v_bpt_value_hjt_h_product) + (ff_r_bpt_value_hjt_h_product))) /\ ((((exists ff_h_bpt_value_hjt_h_product_successor. ff_h_bpt_value_hjt_h_product_successor + S (ff_s_bpt_value_hjt_h_product) = S ((S (S ff_i_bpt_value_hjt_h_product)) * ff_v_bpt_value_hjt_h_product)) /\ exists ff_q_bpt_value_hjt_h_product_successor. ff_u_bpt_value_hjt_h_product = ff_q_bpt_value_hjt_h_product_successor * S ((S (S ff_i_bpt_value_hjt_h_product)) * ff_v_bpt_value_hjt_h_product) + (ff_s_bpt_value_hjt_h_product))) /\ ff_s_bpt_value_hjt_h_product = ff_r_bpt_value_hjt_h_product * ff_p_bpt_value_hjt_h_product))))))))) -> (exists bqb_le_gap_hjt_h_lower. bqb_le_gap_hjt_h_lower + (5) = (s)) -> (((exists bcs_lower_gap_hjt_h_ceiling. bcs_lower_gap_hjt_h_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_hjt_h_ceiling. bcs_upper_gap_hjt_h_ceiling + S (6 * (e)) = (s * s) + 6)) -> (((exists bcs_lower_gap_hjt_h_next_ceiling. bcs_lower_gap_hjt_h_next_ceiling + ((s + 6) * (s + 6)) = 6 * (f)) /\ exists bcs_upper_gap_hjt_h_next_ceiling. bcs_upper_gap_hjt_h_next_ceiling + S (6 * (f)) = ((s + 6) * (s + 6)) + 6)) -> (exists pa_b_hjt_h_now pa_c_hjt_h_now. ((forall pa_i_hjt_h_now_repeat. (exists pa_lt_hjt_h_now_repeat_bound. pa_lt_hjt_h_now_repeat_bound + S pa_i_hjt_h_now_repeat = 2 * s + 2) -> (((exists pa_h_hjt_h_now_repeat_decoded. pa_h_hjt_h_now_repeat_decoded + S (s + 1) = S ((S (pa_i_hjt_h_now_repeat)) * pa_c_hjt_h_now)) /\ exists pa_q_hjt_h_now_repeat_decoded. pa_b_hjt_h_now = pa_q_hjt_h_now_repeat_decoded * S ((S (pa_i_hjt_h_now_repeat)) * pa_c_hjt_h_now) + (s + 1)))) /\ (exists pa_u_hjt_h_now_product pa_v_hjt_h_now_product. ((((exists pa_h_hjt_h_now_product_start. pa_h_hjt_h_now_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_now_product)) /\ exists pa_q_hjt_h_now_product_start. pa_u_hjt_h_now_product = pa_q_hjt_h_now_product_start * S ((S (0)) * pa_v_hjt_h_now_product) + (1))) /\ ((((exists pa_h_hjt_h_now_product_terminal. pa_h_hjt_h_now_product_terminal + S (h) = S ((S (2 * s + 2)) * pa_v_hjt_h_now_product)) /\ exists pa_q_hjt_h_now_product_terminal. pa_u_hjt_h_now_product = pa_q_hjt_h_now_product_terminal * S ((S (2 * s + 2)) * pa_v_hjt_h_now_product) + (h))) /\ forall pa_i_hjt_h_now_product. (exists pa_lt_hjt_h_now_product_bound. pa_lt_hjt_h_now_product_bound + S pa_i_hjt_h_now_product = 2 * s + 2) -> exists pa_p_hjt_h_now_product pa_r_hjt_h_now_product pa_s_hjt_h_now_product. ((((exists pa_h_hjt_h_now_product_factor. pa_h_hjt_h_now_product_factor + S (pa_p_hjt_h_now_product) = S ((S (pa_i_hjt_h_now_product)) * pa_c_hjt_h_now)) /\ exists pa_q_hjt_h_now_product_factor. pa_b_hjt_h_now = pa_q_hjt_h_now_product_factor * S ((S (pa_i_hjt_h_now_product)) * pa_c_hjt_h_now) + (pa_p_hjt_h_now_product))) /\ ((((exists pa_h_hjt_h_now_product_partial. pa_h_hjt_h_now_product_partial + S (pa_r_hjt_h_now_product) = S ((S (pa_i_hjt_h_now_product)) * pa_v_hjt_h_now_product)) /\ exists pa_q_hjt_h_now_product_partial. pa_u_hjt_h_now_product = pa_q_hjt_h_now_product_partial * S ((S (pa_i_hjt_h_now_product)) * pa_v_hjt_h_now_product) + (pa_r_hjt_h_now_product))) /\ ((((exists pa_h_hjt_h_now_product_successor. pa_h_hjt_h_now_product_successor + S (pa_s_hjt_h_now_product) = S ((S (S pa_i_hjt_h_now_product)) * pa_v_hjt_h_now_product)) /\ exists pa_q_hjt_h_now_product_successor. pa_u_hjt_h_now_product = pa_q_hjt_h_now_product_successor * S ((S (S pa_i_hjt_h_now_product)) * pa_v_hjt_h_now_product) + (pa_s_hjt_h_now_product))) /\ pa_s_hjt_h_now_product = pa_r_hjt_h_now_product * pa_p_hjt_h_now_product)))))))) -> (exists pa_b_hjt_h_now_bound pa_c_hjt_h_now_bound. ((forall pa_i_hjt_h_now_bound_repeat. (exists pa_lt_hjt_h_now_bound_repeat_bound. pa_lt_hjt_h_now_bound_repeat_bound + S pa_i_hjt_h_now_bound_repeat = e) -> (((exists pa_h_hjt_h_now_bound_repeat_decoded. pa_h_hjt_h_now_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_h_now_bound_repeat)) * pa_c_hjt_h_now_bound)) /\ exists pa_q_hjt_h_now_bound_repeat_decoded. pa_b_hjt_h_now_bound = pa_q_hjt_h_now_bound_repeat_decoded * S ((S (pa_i_hjt_h_now_bound_repeat)) * pa_c_hjt_h_now_bound) + (4)))) /\ (exists pa_u_hjt_h_now_bound_product pa_v_hjt_h_now_bound_product. ((((exists pa_h_hjt_h_now_bound_product_start. pa_h_hjt_h_now_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_now_bound_product)) /\ exists pa_q_hjt_h_now_bound_product_start. pa_u_hjt_h_now_bound_product = pa_q_hjt_h_now_bound_product_start * S ((S (0)) * pa_v_hjt_h_now_bound_product) + (1))) /\ ((((exists pa_h_hjt_h_now_bound_product_terminal. pa_h_hjt_h_now_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hjt_h_now_bound_product)) /\ exists pa_q_hjt_h_now_bound_product_terminal. pa_u_hjt_h_now_bound_product = pa_q_hjt_h_now_bound_product_terminal * S ((S (e)) * pa_v_hjt_h_now_bound_product) + (u))) /\ forall pa_i_hjt_h_now_bound_product. (exists pa_lt_hjt_h_now_bound_product_bound. pa_lt_hjt_h_now_bound_product_bound + S pa_i_hjt_h_now_bound_product = e) -> exists pa_p_hjt_h_now_bound_product pa_r_hjt_h_now_bound_product pa_s_hjt_h_now_bound_product. ((((exists pa_h_hjt_h_now_bound_product_factor. pa_h_hjt_h_now_bound_product_factor + S (pa_p_hjt_h_now_bound_product) = S ((S (pa_i_hjt_h_now_bound_product)) * pa_c_hjt_h_now_bound)) /\ exists pa_q_hjt_h_now_bound_product_factor. pa_b_hjt_h_now_bound = pa_q_hjt_h_now_bound_product_factor * S ((S (pa_i_hjt_h_now_bound_product)) * pa_c_hjt_h_now_bound) + (pa_p_hjt_h_now_bound_product))) /\ ((((exists pa_h_hjt_h_now_bound_product_partial. pa_h_hjt_h_now_bound_product_partial + S (pa_r_hjt_h_now_bound_product) = S ((S (pa_i_hjt_h_now_bound_product)) * pa_v_hjt_h_now_bound_product)) /\ exists pa_q_hjt_h_now_bound_product_partial. pa_u_hjt_h_now_bound_product = pa_q_hjt_h_now_bound_product_partial * S ((S (pa_i_hjt_h_now_bound_product)) * pa_v_hjt_h_now_bound_product) + (pa_r_hjt_h_now_bound_product))) /\ ((((exists pa_h_hjt_h_now_bound_product_successor. pa_h_hjt_h_now_bound_product_successor + S (pa_s_hjt_h_now_bound_product) = S ((S (S pa_i_hjt_h_now_bound_product)) * pa_v_hjt_h_now_bound_product)) /\ exists pa_q_hjt_h_now_bound_product_successor. pa_u_hjt_h_now_bound_product = pa_q_hjt_h_now_bound_product_successor * S ((S (S pa_i_hjt_h_now_bound_product)) * pa_v_hjt_h_now_bound_product) + (pa_s_hjt_h_now_bound_product))) /\ pa_s_hjt_h_now_bound_product = pa_r_hjt_h_now_bound_product * pa_p_hjt_h_now_bound_product)))))))) -> (exists bqb_le_gap_hjt_h_now_result. bqb_le_gap_hjt_h_now_result + (h) = (u)) -> (exists pa_b_hjt_h_guard pa_c_hjt_h_guard. ((forall pa_i_hjt_h_guard_repeat. (exists pa_lt_hjt_h_guard_repeat_bound. pa_lt_hjt_h_guard_repeat_bound + S pa_i_hjt_h_guard_repeat = 12) -> (((exists pa_h_hjt_h_guard_repeat_decoded. pa_h_hjt_h_guard_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_h_guard_repeat)) * pa_c_hjt_h_guard)) /\ exists pa_q_hjt_h_guard_repeat_decoded. pa_b_hjt_h_guard = pa_q_hjt_h_guard_repeat_decoded * S ((S (pa_i_hjt_h_guard_repeat)) * pa_c_hjt_h_guard) + (s + 7)))) /\ (exists pa_u_hjt_h_guard_product pa_v_hjt_h_guard_product. ((((exists pa_h_hjt_h_guard_product_start. pa_h_hjt_h_guard_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_guard_product)) /\ exists pa_q_hjt_h_guard_product_start. pa_u_hjt_h_guard_product = pa_q_hjt_h_guard_product_start * S ((S (0)) * pa_v_hjt_h_guard_product) + (1))) /\ ((((exists pa_h_hjt_h_guard_product_terminal. pa_h_hjt_h_guard_product_terminal + S (j) = S ((S (12)) * pa_v_hjt_h_guard_product)) /\ exists pa_q_hjt_h_guard_product_terminal. pa_u_hjt_h_guard_product = pa_q_hjt_h_guard_product_terminal * S ((S (12)) * pa_v_hjt_h_guard_product) + (j))) /\ forall pa_i_hjt_h_guard_product. (exists pa_lt_hjt_h_guard_product_bound. pa_lt_hjt_h_guard_product_bound + S pa_i_hjt_h_guard_product = 12) -> exists pa_p_hjt_h_guard_product pa_r_hjt_h_guard_product pa_s_hjt_h_guard_product. ((((exists pa_h_hjt_h_guard_product_factor. pa_h_hjt_h_guard_product_factor + S (pa_p_hjt_h_guard_product) = S ((S (pa_i_hjt_h_guard_product)) * pa_c_hjt_h_guard)) /\ exists pa_q_hjt_h_guard_product_factor. pa_b_hjt_h_guard = pa_q_hjt_h_guard_product_factor * S ((S (pa_i_hjt_h_guard_product)) * pa_c_hjt_h_guard) + (pa_p_hjt_h_guard_product))) /\ ((((exists pa_h_hjt_h_guard_product_partial. pa_h_hjt_h_guard_product_partial + S (pa_r_hjt_h_guard_product) = S ((S (pa_i_hjt_h_guard_product)) * pa_v_hjt_h_guard_product)) /\ exists pa_q_hjt_h_guard_product_partial. pa_u_hjt_h_guard_product = pa_q_hjt_h_guard_product_partial * S ((S (pa_i_hjt_h_guard_product)) * pa_v_hjt_h_guard_product) + (pa_r_hjt_h_guard_product))) /\ ((((exists pa_h_hjt_h_guard_product_successor. pa_h_hjt_h_guard_product_successor + S (pa_s_hjt_h_guard_product) = S ((S (S pa_i_hjt_h_guard_product)) * pa_v_hjt_h_guard_product)) /\ exists pa_q_hjt_h_guard_product_successor. pa_u_hjt_h_guard_product = pa_q_hjt_h_guard_product_successor * S ((S (S pa_i_hjt_h_guard_product)) * pa_v_hjt_h_guard_product) + (pa_s_hjt_h_guard_product))) /\ pa_s_hjt_h_guard_product = pa_r_hjt_h_guard_product * pa_p_hjt_h_guard_product)))))))) -> (exists pa_b_hjt_h_guard_bound pa_c_hjt_h_guard_bound. ((forall pa_i_hjt_h_guard_bound_repeat. (exists pa_lt_hjt_h_guard_bound_repeat_bound. pa_lt_hjt_h_guard_bound_repeat_bound + S pa_i_hjt_h_guard_bound_repeat = s + 5) -> (((exists pa_h_hjt_h_guard_bound_repeat_decoded. pa_h_hjt_h_guard_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_h_guard_bound_repeat)) * pa_c_hjt_h_guard_bound)) /\ exists pa_q_hjt_h_guard_bound_repeat_decoded. pa_b_hjt_h_guard_bound = pa_q_hjt_h_guard_bound_repeat_decoded * S ((S (pa_i_hjt_h_guard_bound_repeat)) * pa_c_hjt_h_guard_bound) + (4)))) /\ (exists pa_u_hjt_h_guard_bound_product pa_v_hjt_h_guard_bound_product. ((((exists pa_h_hjt_h_guard_bound_product_start. pa_h_hjt_h_guard_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_guard_bound_product)) /\ exists pa_q_hjt_h_guard_bound_product_start. pa_u_hjt_h_guard_bound_product = pa_q_hjt_h_guard_bound_product_start * S ((S (0)) * pa_v_hjt_h_guard_bound_product) + (1))) /\ ((((exists pa_h_hjt_h_guard_bound_product_terminal. pa_h_hjt_h_guard_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hjt_h_guard_bound_product)) /\ exists pa_q_hjt_h_guard_bound_product_terminal. pa_u_hjt_h_guard_bound_product = pa_q_hjt_h_guard_bound_product_terminal * S ((S (s + 5)) * pa_v_hjt_h_guard_bound_product) + (g))) /\ forall pa_i_hjt_h_guard_bound_product. (exists pa_lt_hjt_h_guard_bound_product_bound. pa_lt_hjt_h_guard_bound_product_bound + S pa_i_hjt_h_guard_bound_product = s + 5) -> exists pa_p_hjt_h_guard_bound_product pa_r_hjt_h_guard_bound_product pa_s_hjt_h_guard_bound_product. ((((exists pa_h_hjt_h_guard_bound_product_factor. pa_h_hjt_h_guard_bound_product_factor + S (pa_p_hjt_h_guard_bound_product) = S ((S (pa_i_hjt_h_guard_bound_product)) * pa_c_hjt_h_guard_bound)) /\ exists pa_q_hjt_h_guard_bound_product_factor. pa_b_hjt_h_guard_bound = pa_q_hjt_h_guard_bound_product_factor * S ((S (pa_i_hjt_h_guard_bound_product)) * pa_c_hjt_h_guard_bound) + (pa_p_hjt_h_guard_bound_product))) /\ ((((exists pa_h_hjt_h_guard_bound_product_partial. pa_h_hjt_h_guard_bound_product_partial + S (pa_r_hjt_h_guard_bound_product) = S ((S (pa_i_hjt_h_guard_bound_product)) * pa_v_hjt_h_guard_bound_product)) /\ exists pa_q_hjt_h_guard_bound_product_partial. pa_u_hjt_h_guard_bound_product = pa_q_hjt_h_guard_bound_product_partial * S ((S (pa_i_hjt_h_guard_bound_product)) * pa_v_hjt_h_guard_bound_product) + (pa_r_hjt_h_guard_bound_product))) /\ ((((exists pa_h_hjt_h_guard_bound_product_successor. pa_h_hjt_h_guard_bound_product_successor + S (pa_s_hjt_h_guard_bound_product) = S ((S (S pa_i_hjt_h_guard_bound_product)) * pa_v_hjt_h_guard_bound_product)) /\ exists pa_q_hjt_h_guard_bound_product_successor. pa_u_hjt_h_guard_bound_product = pa_q_hjt_h_guard_bound_product_successor * S ((S (S pa_i_hjt_h_guard_bound_product)) * pa_v_hjt_h_guard_bound_product) + (pa_s_hjt_h_guard_bound_product))) /\ pa_s_hjt_h_guard_bound_product = pa_r_hjt_h_guard_bound_product * pa_p_hjt_h_guard_bound_product)))))))) -> (exists bqb_le_gap_hjt_h_guard_result. bqb_le_gap_hjt_h_guard_result + (j) = (g)) -> (exists pa_b_hjt_h_next pa_c_hjt_h_next. ((forall pa_i_hjt_h_next_repeat. (exists pa_lt_hjt_h_next_repeat_bound. pa_lt_hjt_h_next_repeat_bound + S pa_i_hjt_h_next_repeat = 2 * s + 14) -> (((exists pa_h_hjt_h_next_repeat_decoded. pa_h_hjt_h_next_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_h_next_repeat)) * pa_c_hjt_h_next)) /\ exists pa_q_hjt_h_next_repeat_decoded. pa_b_hjt_h_next = pa_q_hjt_h_next_repeat_decoded * S ((S (pa_i_hjt_h_next_repeat)) * pa_c_hjt_h_next) + (s + 7)))) /\ (exists pa_u_hjt_h_next_product pa_v_hjt_h_next_product. ((((exists pa_h_hjt_h_next_product_start. pa_h_hjt_h_next_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_next_product)) /\ exists pa_q_hjt_h_next_product_start. pa_u_hjt_h_next_product = pa_q_hjt_h_next_product_start * S ((S (0)) * pa_v_hjt_h_next_product) + (1))) /\ ((((exists pa_h_hjt_h_next_product_terminal. pa_h_hjt_h_next_product_terminal + S (hn) = S ((S (2 * s + 14)) * pa_v_hjt_h_next_product)) /\ exists pa_q_hjt_h_next_product_terminal. pa_u_hjt_h_next_product = pa_q_hjt_h_next_product_terminal * S ((S (2 * s + 14)) * pa_v_hjt_h_next_product) + (hn))) /\ forall pa_i_hjt_h_next_product. (exists pa_lt_hjt_h_next_product_bound. pa_lt_hjt_h_next_product_bound + S pa_i_hjt_h_next_product = 2 * s + 14) -> exists pa_p_hjt_h_next_product pa_r_hjt_h_next_product pa_s_hjt_h_next_product. ((((exists pa_h_hjt_h_next_product_factor. pa_h_hjt_h_next_product_factor + S (pa_p_hjt_h_next_product) = S ((S (pa_i_hjt_h_next_product)) * pa_c_hjt_h_next)) /\ exists pa_q_hjt_h_next_product_factor. pa_b_hjt_h_next = pa_q_hjt_h_next_product_factor * S ((S (pa_i_hjt_h_next_product)) * pa_c_hjt_h_next) + (pa_p_hjt_h_next_product))) /\ ((((exists pa_h_hjt_h_next_product_partial. pa_h_hjt_h_next_product_partial + S (pa_r_hjt_h_next_product) = S ((S (pa_i_hjt_h_next_product)) * pa_v_hjt_h_next_product)) /\ exists pa_q_hjt_h_next_product_partial. pa_u_hjt_h_next_product = pa_q_hjt_h_next_product_partial * S ((S (pa_i_hjt_h_next_product)) * pa_v_hjt_h_next_product) + (pa_r_hjt_h_next_product))) /\ ((((exists pa_h_hjt_h_next_product_successor. pa_h_hjt_h_next_product_successor + S (pa_s_hjt_h_next_product) = S ((S (S pa_i_hjt_h_next_product)) * pa_v_hjt_h_next_product)) /\ exists pa_q_hjt_h_next_product_successor. pa_u_hjt_h_next_product = pa_q_hjt_h_next_product_successor * S ((S (S pa_i_hjt_h_next_product)) * pa_v_hjt_h_next_product) + (pa_s_hjt_h_next_product))) /\ pa_s_hjt_h_next_product = pa_r_hjt_h_next_product * pa_p_hjt_h_next_product)))))))) -> (exists pa_b_hjt_h_next_bound pa_c_hjt_h_next_bound. ((forall pa_i_hjt_h_next_bound_repeat. (exists pa_lt_hjt_h_next_bound_repeat_bound. pa_lt_hjt_h_next_bound_repeat_bound + S pa_i_hjt_h_next_bound_repeat = f) -> (((exists pa_h_hjt_h_next_bound_repeat_decoded. pa_h_hjt_h_next_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_h_next_bound_repeat)) * pa_c_hjt_h_next_bound)) /\ exists pa_q_hjt_h_next_bound_repeat_decoded. pa_b_hjt_h_next_bound = pa_q_hjt_h_next_bound_repeat_decoded * S ((S (pa_i_hjt_h_next_bound_repeat)) * pa_c_hjt_h_next_bound) + (4)))) /\ (exists pa_u_hjt_h_next_bound_product pa_v_hjt_h_next_bound_product. ((((exists pa_h_hjt_h_next_bound_product_start. pa_h_hjt_h_next_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_next_bound_product)) /\ exists pa_q_hjt_h_next_bound_product_start. pa_u_hjt_h_next_bound_product = pa_q_hjt_h_next_bound_product_start * S ((S (0)) * pa_v_hjt_h_next_bound_product) + (1))) /\ ((((exists pa_h_hjt_h_next_bound_product_terminal. pa_h_hjt_h_next_bound_product_terminal + S (un) = S ((S (f)) * pa_v_hjt_h_next_bound_product)) /\ exists pa_q_hjt_h_next_bound_product_terminal. pa_u_hjt_h_next_bound_product = pa_q_hjt_h_next_bound_product_terminal * S ((S (f)) * pa_v_hjt_h_next_bound_product) + (un))) /\ forall pa_i_hjt_h_next_bound_product. (exists pa_lt_hjt_h_next_bound_product_bound. pa_lt_hjt_h_next_bound_product_bound + S pa_i_hjt_h_next_bound_product = f) -> exists pa_p_hjt_h_next_bound_product pa_r_hjt_h_next_bound_product pa_s_hjt_h_next_bound_product. ((((exists pa_h_hjt_h_next_bound_product_factor. pa_h_hjt_h_next_bound_product_factor + S (pa_p_hjt_h_next_bound_product) = S ((S (pa_i_hjt_h_next_bound_product)) * pa_c_hjt_h_next_bound)) /\ exists pa_q_hjt_h_next_bound_product_factor. pa_b_hjt_h_next_bound = pa_q_hjt_h_next_bound_product_factor * S ((S (pa_i_hjt_h_next_bound_product)) * pa_c_hjt_h_next_bound) + (pa_p_hjt_h_next_bound_product))) /\ ((((exists pa_h_hjt_h_next_bound_product_partial. pa_h_hjt_h_next_bound_product_partial + S (pa_r_hjt_h_next_bound_product) = S ((S (pa_i_hjt_h_next_bound_product)) * pa_v_hjt_h_next_bound_product)) /\ exists pa_q_hjt_h_next_bound_product_partial. pa_u_hjt_h_next_bound_product = pa_q_hjt_h_next_bound_product_partial * S ((S (pa_i_hjt_h_next_bound_product)) * pa_v_hjt_h_next_bound_product) + (pa_r_hjt_h_next_bound_product))) /\ ((((exists pa_h_hjt_h_next_bound_product_successor. pa_h_hjt_h_next_bound_product_successor + S (pa_s_hjt_h_next_bound_product) = S ((S (S pa_i_hjt_h_next_bound_product)) * pa_v_hjt_h_next_bound_product)) /\ exists pa_q_hjt_h_next_bound_product_successor. pa_u_hjt_h_next_bound_product = pa_q_hjt_h_next_bound_product_successor * S ((S (S pa_i_hjt_h_next_bound_product)) * pa_v_hjt_h_next_bound_product) + (pa_s_hjt_h_next_bound_product))) /\ pa_s_hjt_h_next_bound_product = pa_r_hjt_h_next_bound_product * pa_p_hjt_h_next_bound_product)))))))) -> (exists bqb_le_gap_hjt_h_next_result. bqb_le_gap_hjt_h_next_result + (hn) = (un))

Structural proof guide

H(s) and J(s) together imply H(s+6).

Direct prerequisites: ceil_div_six_square_six_step, two_mul_eq_add_self, pow_base_monotone, pow_mul_base, pow_two_seed_bundle_from_total, pow_mul_exp_from_total, pow_add, mul_le_mul, le_refl, le_trans, add_assoc, add_comm, add_succ_left. The authored body proceeds by case analysis (7), intermediate claims (21), equality transport (10).

Proof neighborhood

Direct dependencies

BT00R5 ceil_div_six_square_six_step BT00QU two_mul_eq_add_self BT00PY pow_base_monotone BT00QV pow_mul_base BT00SO pow_two_seed_bundle_from_total BT00SM pow_mul_exp_from_total BT009X pow_add BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0003 add_assoc BT0002 add_comm BT0001 add_succ_left

Direct dependents

BT00SY bertrand_hj_six_step_from_total

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 f
  4. 0004intro h
  5. 0005intro u
  6. 0006intro j
  7. 0007intro g
  8. 0008intro hn
  9. 0009intro un
  10. 0010intro htotal
  11. 0011intro hlower
  12. 0012intro hceiling
  13. 0013intro hnextceiling
  14. 0014intro hh
  15. 0015intro hu
  16. 0016intro hhu
  17. 0017intro hj
  18. 0018intro hg
  19. 0019intro hjg
  20. 0020intro hhn
  21. 0021intro hun
  22. 0022have hceilshift : f = e + (2 * s + 6)
  23. 0023specialize ceil_div_six_square_six_step s
  24. 0024specialize ceil_div_six_square_six_step e
  25. 0025specialize ceil_div_six_square_six_step f
  26. 0026apply ceil_div_six_square_six_step
  27. 0027exact hceiling
  28. 0028exact hnextceiling
  29. 0029cases hlower
  30. 0030have hbase : exists bqb_le_gap_hjt_h_base. bqb_le_gap_hjt_h_base + (s + 7) = (2 * (s + 1))
  31. 0031exists x
  32. 0032rewrite <- hlower_witness
  33. 0033simp [two_mul_eq_add_self, add_assoc, add_comm]
  34. 0034rewrite <- hlower_witness
  35. 0035rewrite <- hlower_witness
  36. 0036simp [add_assoc, add_comm]
  37. 0037have hone : s + 1 = S s
  38. 0038trans S (s + 0)
  39. 0039apply PA4
  40. 0040congr
  41. 0041apply PA3
  42. 0042have hdouble_exponent : 2 * (s + 1) = 2 * s + 2
  43. 0043rewrite hone
  44. 0044apply PA6
  45. 0045have hprefix_exists : exists hp. (exists pa_b_hjt_h_prefix pa_c_hjt_h_prefix. ((forall pa_i_hjt_h_prefix_repeat. (exists pa_lt_hjt_h_prefix_repeat_bound. pa_lt_hjt_h_prefix_repeat_bound + S pa_i_hjt_h_prefix_repeat = 2 * s + 2) -> (((exists pa_h_hjt_h_prefix_repeat_decoded. pa_h_hjt_h_prefix_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_h_prefix_repeat)) * pa_c_hjt_h_prefix)) /\ exists pa_q_hjt_h_prefix_repeat_decoded. pa_b_hjt_h_prefix = pa_q_hjt_h_prefix_repeat_decoded * S ((S (pa_i_hjt_h_prefix_repeat)) * pa_c_hjt_h_prefix) + (s + 7)))) /\ (exists pa_u_hjt_h_prefix_product pa_v_hjt_h_prefix_product. ((((exists pa_h_hjt_h_prefix_product_start. pa_h_hjt_h_prefix_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_prefix_product)) /\ exists pa_q_hjt_h_prefix_product_start. pa_u_hjt_h_prefix_product = pa_q_hjt_h_prefix_product_start * S ((S (0)) * pa_v_hjt_h_prefix_product) + (1))) /\ ((((exists pa_h_hjt_h_prefix_product_terminal. pa_h_hjt_h_prefix_product_terminal + S (hp) = S ((S (2 * s + 2)) * pa_v_hjt_h_prefix_product)) /\ exists pa_q_hjt_h_prefix_product_terminal. pa_u_hjt_h_prefix_product = pa_q_hjt_h_prefix_product_terminal * S ((S (2 * s + 2)) * pa_v_hjt_h_prefix_product) + (hp))) /\ forall pa_i_hjt_h_prefix_product. (exists pa_lt_hjt_h_prefix_product_bound. pa_lt_hjt_h_prefix_product_bound + S pa_i_hjt_h_prefix_product = 2 * s + 2) -> exists pa_p_hjt_h_prefix_product pa_r_hjt_h_prefix_product pa_s_hjt_h_prefix_product. ((((exists pa_h_hjt_h_prefix_product_factor. pa_h_hjt_h_prefix_product_factor + S (pa_p_hjt_h_prefix_product) = S ((S (pa_i_hjt_h_prefix_product)) * pa_c_hjt_h_prefix)) /\ exists pa_q_hjt_h_prefix_product_factor. pa_b_hjt_h_prefix = pa_q_hjt_h_prefix_product_factor * S ((S (pa_i_hjt_h_prefix_product)) * pa_c_hjt_h_prefix) + (pa_p_hjt_h_prefix_product))) /\ ((((exists pa_h_hjt_h_prefix_product_partial. pa_h_hjt_h_prefix_product_partial + S (pa_r_hjt_h_prefix_product) = S ((S (pa_i_hjt_h_prefix_product)) * pa_v_hjt_h_prefix_product)) /\ exists pa_q_hjt_h_prefix_product_partial. pa_u_hjt_h_prefix_product = pa_q_hjt_h_prefix_product_partial * S ((S (pa_i_hjt_h_prefix_product)) * pa_v_hjt_h_prefix_product) + (pa_r_hjt_h_prefix_product))) /\ ((((exists pa_h_hjt_h_prefix_product_successor. pa_h_hjt_h_prefix_product_successor + S (pa_s_hjt_h_prefix_product) = S ((S (S pa_i_hjt_h_prefix_product)) * pa_v_hjt_h_prefix_product)) /\ exists pa_q_hjt_h_prefix_product_successor. pa_u_hjt_h_prefix_product = pa_q_hjt_h_prefix_product_successor * S ((S (S pa_i_hjt_h_prefix_product)) * pa_v_hjt_h_prefix_product) + (pa_s_hjt_h_prefix_product))) /\ pa_s_hjt_h_prefix_product = pa_r_hjt_h_prefix_product * pa_p_hjt_h_prefix_product))))))))
  46. 0046specialize htotal (s + 7)
  47. 0047specialize htotal (2 * s + 2)
  48. 0048exact htotal
  49. 0049cases hprefix_exists
  50. 0050have hdouble_exists : exists hd. (exists pa_b_hjt_h_double pa_c_hjt_h_double. ((forall pa_i_hjt_h_double_repeat. (exists pa_lt_hjt_h_double_repeat_bound. pa_lt_hjt_h_double_repeat_bound + S pa_i_hjt_h_double_repeat = 2 * s + 2) -> (((exists pa_h_hjt_h_double_repeat_decoded. pa_h_hjt_h_double_repeat_decoded + S (2 * (s + 1)) = S ((S (pa_i_hjt_h_double_repeat)) * pa_c_hjt_h_double)) /\ exists pa_q_hjt_h_double_repeat_decoded. pa_b_hjt_h_double = pa_q_hjt_h_double_repeat_decoded * S ((S (pa_i_hjt_h_double_repeat)) * pa_c_hjt_h_double) + (2 * (s + 1))))) /\ (exists pa_u_hjt_h_double_product pa_v_hjt_h_double_product. ((((exists pa_h_hjt_h_double_product_start. pa_h_hjt_h_double_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_double_product)) /\ exists pa_q_hjt_h_double_product_start. pa_u_hjt_h_double_product = pa_q_hjt_h_double_product_start * S ((S (0)) * pa_v_hjt_h_double_product) + (1))) /\ ((((exists pa_h_hjt_h_double_product_terminal. pa_h_hjt_h_double_product_terminal + S (hd) = S ((S (2 * s + 2)) * pa_v_hjt_h_double_product)) /\ exists pa_q_hjt_h_double_product_terminal. pa_u_hjt_h_double_product = pa_q_hjt_h_double_product_terminal * S ((S (2 * s + 2)) * pa_v_hjt_h_double_product) + (hd))) /\ forall pa_i_hjt_h_double_product. (exists pa_lt_hjt_h_double_product_bound. pa_lt_hjt_h_double_product_bound + S pa_i_hjt_h_double_product = 2 * s + 2) -> exists pa_p_hjt_h_double_product pa_r_hjt_h_double_product pa_s_hjt_h_double_product. ((((exists pa_h_hjt_h_double_product_factor. pa_h_hjt_h_double_product_factor + S (pa_p_hjt_h_double_product) = S ((S (pa_i_hjt_h_double_product)) * pa_c_hjt_h_double)) /\ exists pa_q_hjt_h_double_product_factor. pa_b_hjt_h_double = pa_q_hjt_h_double_product_factor * S ((S (pa_i_hjt_h_double_product)) * pa_c_hjt_h_double) + (pa_p_hjt_h_double_product))) /\ ((((exists pa_h_hjt_h_double_product_partial. pa_h_hjt_h_double_product_partial + S (pa_r_hjt_h_double_product) = S ((S (pa_i_hjt_h_double_product)) * pa_v_hjt_h_double_product)) /\ exists pa_q_hjt_h_double_product_partial. pa_u_hjt_h_double_product = pa_q_hjt_h_double_product_partial * S ((S (pa_i_hjt_h_double_product)) * pa_v_hjt_h_double_product) + (pa_r_hjt_h_double_product))) /\ ((((exists pa_h_hjt_h_double_product_successor. pa_h_hjt_h_double_product_successor + S (pa_s_hjt_h_double_product) = S ((S (S pa_i_hjt_h_double_product)) * pa_v_hjt_h_double_product)) /\ exists pa_q_hjt_h_double_product_successor. pa_u_hjt_h_double_product = pa_q_hjt_h_double_product_successor * S ((S (S pa_i_hjt_h_double_product)) * pa_v_hjt_h_double_product) + (pa_s_hjt_h_double_product))) /\ pa_s_hjt_h_double_product = pa_r_hjt_h_double_product * pa_p_hjt_h_double_product))))))))
  51. 0051specialize htotal (2 * (s + 1))
  52. 0052specialize htotal (2 * s + 2)
  53. 0053exact htotal
  54. 0054cases hdouble_exists
  55. 0055have hprefix_double : exists bqb_le_gap_hjt_h_prefix_double. bqb_le_gap_hjt_h_prefix_double + (x1) = (x2)
  56. 0056specialize pow_base_monotone (s + 7)
  57. 0057specialize pow_base_monotone (2 * (s + 1))
  58. 0058specialize pow_base_monotone (2 * s + 2)
  59. 0059specialize pow_base_monotone x1
  60. 0060specialize pow_base_monotone x2
  61. 0061apply pow_base_monotone
  62. 0062exact hbase
  63. 0063exact hprefix_exists_witness
  64. 0064exact hdouble_exists_witness
  65. 0065have htwo_exists : exists ht. (exists pa_b_hjt_h_two_factor pa_c_hjt_h_two_factor. ((forall pa_i_hjt_h_two_factor_repeat. (exists pa_lt_hjt_h_two_factor_repeat_bound. pa_lt_hjt_h_two_factor_repeat_bound + S pa_i_hjt_h_two_factor_repeat = 2 * s + 2) -> (((exists pa_h_hjt_h_two_factor_repeat_decoded. pa_h_hjt_h_two_factor_repeat_decoded + S (2) = S ((S (pa_i_hjt_h_two_factor_repeat)) * pa_c_hjt_h_two_factor)) /\ exists pa_q_hjt_h_two_factor_repeat_decoded. pa_b_hjt_h_two_factor = pa_q_hjt_h_two_factor_repeat_decoded * S ((S (pa_i_hjt_h_two_factor_repeat)) * pa_c_hjt_h_two_factor) + (2)))) /\ (exists pa_u_hjt_h_two_factor_product pa_v_hjt_h_two_factor_product. ((((exists pa_h_hjt_h_two_factor_product_start. pa_h_hjt_h_two_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_two_factor_product)) /\ exists pa_q_hjt_h_two_factor_product_start. pa_u_hjt_h_two_factor_product = pa_q_hjt_h_two_factor_product_start * S ((S (0)) * pa_v_hjt_h_two_factor_product) + (1))) /\ ((((exists pa_h_hjt_h_two_factor_product_terminal. pa_h_hjt_h_two_factor_product_terminal + S (ht) = S ((S (2 * s + 2)) * pa_v_hjt_h_two_factor_product)) /\ exists pa_q_hjt_h_two_factor_product_terminal. pa_u_hjt_h_two_factor_product = pa_q_hjt_h_two_factor_product_terminal * S ((S (2 * s + 2)) * pa_v_hjt_h_two_factor_product) + (ht))) /\ forall pa_i_hjt_h_two_factor_product. (exists pa_lt_hjt_h_two_factor_product_bound. pa_lt_hjt_h_two_factor_product_bound + S pa_i_hjt_h_two_factor_product = 2 * s + 2) -> exists pa_p_hjt_h_two_factor_product pa_r_hjt_h_two_factor_product pa_s_hjt_h_two_factor_product. ((((exists pa_h_hjt_h_two_factor_product_factor. pa_h_hjt_h_two_factor_product_factor + S (pa_p_hjt_h_two_factor_product) = S ((S (pa_i_hjt_h_two_factor_product)) * pa_c_hjt_h_two_factor)) /\ exists pa_q_hjt_h_two_factor_product_factor. pa_b_hjt_h_two_factor = pa_q_hjt_h_two_factor_product_factor * S ((S (pa_i_hjt_h_two_factor_product)) * pa_c_hjt_h_two_factor) + (pa_p_hjt_h_two_factor_product))) /\ ((((exists pa_h_hjt_h_two_factor_product_partial. pa_h_hjt_h_two_factor_product_partial + S (pa_r_hjt_h_two_factor_product) = S ((S (pa_i_hjt_h_two_factor_product)) * pa_v_hjt_h_two_factor_product)) /\ exists pa_q_hjt_h_two_factor_product_partial. pa_u_hjt_h_two_factor_product = pa_q_hjt_h_two_factor_product_partial * S ((S (pa_i_hjt_h_two_factor_product)) * pa_v_hjt_h_two_factor_product) + (pa_r_hjt_h_two_factor_product))) /\ ((((exists pa_h_hjt_h_two_factor_product_successor. pa_h_hjt_h_two_factor_product_successor + S (pa_s_hjt_h_two_factor_product) = S ((S (S pa_i_hjt_h_two_factor_product)) * pa_v_hjt_h_two_factor_product)) /\ exists pa_q_hjt_h_two_factor_product_successor. pa_u_hjt_h_two_factor_product = pa_q_hjt_h_two_factor_product_successor * S ((S (S pa_i_hjt_h_two_factor_product)) * pa_v_hjt_h_two_factor_product) + (pa_s_hjt_h_two_factor_product))) /\ pa_s_hjt_h_two_factor_product = pa_r_hjt_h_two_factor_product * pa_p_hjt_h_two_factor_product))))))))
  66. 0066specialize htotal 2
  67. 0067specialize htotal (2 * s + 2)
  68. 0068exact htotal
  69. 0069cases htwo_exists
  70. 0070have hfour_exists : exists hf. (exists pa_b_hjt_h_four_factor pa_c_hjt_h_four_factor. ((forall pa_i_hjt_h_four_factor_repeat. (exists pa_lt_hjt_h_four_factor_repeat_bound. pa_lt_hjt_h_four_factor_repeat_bound + S pa_i_hjt_h_four_factor_repeat = s + 1) -> (((exists pa_h_hjt_h_four_factor_repeat_decoded. pa_h_hjt_h_four_factor_repeat_decoded + S (4) = S ((S (pa_i_hjt_h_four_factor_repeat)) * pa_c_hjt_h_four_factor)) /\ exists pa_q_hjt_h_four_factor_repeat_decoded. pa_b_hjt_h_four_factor = pa_q_hjt_h_four_factor_repeat_decoded * S ((S (pa_i_hjt_h_four_factor_repeat)) * pa_c_hjt_h_four_factor) + (4)))) /\ (exists pa_u_hjt_h_four_factor_product pa_v_hjt_h_four_factor_product. ((((exists pa_h_hjt_h_four_factor_product_start. pa_h_hjt_h_four_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_four_factor_product)) /\ exists pa_q_hjt_h_four_factor_product_start. pa_u_hjt_h_four_factor_product = pa_q_hjt_h_four_factor_product_start * S ((S (0)) * pa_v_hjt_h_four_factor_product) + (1))) /\ ((((exists pa_h_hjt_h_four_factor_product_terminal. pa_h_hjt_h_four_factor_product_terminal + S (hf) = S ((S (s + 1)) * pa_v_hjt_h_four_factor_product)) /\ exists pa_q_hjt_h_four_factor_product_terminal. pa_u_hjt_h_four_factor_product = pa_q_hjt_h_four_factor_product_terminal * S ((S (s + 1)) * pa_v_hjt_h_four_factor_product) + (hf))) /\ forall pa_i_hjt_h_four_factor_product. (exists pa_lt_hjt_h_four_factor_product_bound. pa_lt_hjt_h_four_factor_product_bound + S pa_i_hjt_h_four_factor_product = s + 1) -> exists pa_p_hjt_h_four_factor_product pa_r_hjt_h_four_factor_product pa_s_hjt_h_four_factor_product. ((((exists pa_h_hjt_h_four_factor_product_factor. pa_h_hjt_h_four_factor_product_factor + S (pa_p_hjt_h_four_factor_product) = S ((S (pa_i_hjt_h_four_factor_product)) * pa_c_hjt_h_four_factor)) /\ exists pa_q_hjt_h_four_factor_product_factor. pa_b_hjt_h_four_factor = pa_q_hjt_h_four_factor_product_factor * S ((S (pa_i_hjt_h_four_factor_product)) * pa_c_hjt_h_four_factor) + (pa_p_hjt_h_four_factor_product))) /\ ((((exists pa_h_hjt_h_four_factor_product_partial. pa_h_hjt_h_four_factor_product_partial + S (pa_r_hjt_h_four_factor_product) = S ((S (pa_i_hjt_h_four_factor_product)) * pa_v_hjt_h_four_factor_product)) /\ exists pa_q_hjt_h_four_factor_product_partial. pa_u_hjt_h_four_factor_product = pa_q_hjt_h_four_factor_product_partial * S ((S (pa_i_hjt_h_four_factor_product)) * pa_v_hjt_h_four_factor_product) + (pa_r_hjt_h_four_factor_product))) /\ ((((exists pa_h_hjt_h_four_factor_product_successor. pa_h_hjt_h_four_factor_product_successor + S (pa_s_hjt_h_four_factor_product) = S ((S (S pa_i_hjt_h_four_factor_product)) * pa_v_hjt_h_four_factor_product)) /\ exists pa_q_hjt_h_four_factor_product_successor. pa_u_hjt_h_four_factor_product = pa_q_hjt_h_four_factor_product_successor * S ((S (S pa_i_hjt_h_four_factor_product)) * pa_v_hjt_h_four_factor_product) + (pa_s_hjt_h_four_factor_product))) /\ pa_s_hjt_h_four_factor_product = pa_r_hjt_h_four_factor_product * pa_p_hjt_h_four_factor_product))))))))
  71. 0071specialize htotal 4
  72. 0072specialize htotal (s + 1)
  73. 0073exact htotal
  74. 0074cases hfour_exists
  75. 0075have hseeds : (exists pa_b_hjt_h_seed_two pa_c_hjt_h_seed_two. ((forall pa_i_hjt_h_seed_two_repeat. (exists pa_lt_hjt_h_seed_two_repeat_bound. pa_lt_hjt_h_seed_two_repeat_bound + S pa_i_hjt_h_seed_two_repeat = 2) -> (((exists pa_h_hjt_h_seed_two_repeat_decoded. pa_h_hjt_h_seed_two_repeat_decoded + S (2) = S ((S (pa_i_hjt_h_seed_two_repeat)) * pa_c_hjt_h_seed_two)) /\ exists pa_q_hjt_h_seed_two_repeat_decoded. pa_b_hjt_h_seed_two = pa_q_hjt_h_seed_two_repeat_decoded * S ((S (pa_i_hjt_h_seed_two_repeat)) * pa_c_hjt_h_seed_two) + (2)))) /\ (exists pa_u_hjt_h_seed_two_product pa_v_hjt_h_seed_two_product. ((((exists pa_h_hjt_h_seed_two_product_start. pa_h_hjt_h_seed_two_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_seed_two_product)) /\ exists pa_q_hjt_h_seed_two_product_start. pa_u_hjt_h_seed_two_product = pa_q_hjt_h_seed_two_product_start * S ((S (0)) * pa_v_hjt_h_seed_two_product) + (1))) /\ ((((exists pa_h_hjt_h_seed_two_product_terminal. pa_h_hjt_h_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_hjt_h_seed_two_product)) /\ exists pa_q_hjt_h_seed_two_product_terminal. pa_u_hjt_h_seed_two_product = pa_q_hjt_h_seed_two_product_terminal * S ((S (2)) * pa_v_hjt_h_seed_two_product) + (4))) /\ forall pa_i_hjt_h_seed_two_product. (exists pa_lt_hjt_h_seed_two_product_bound. pa_lt_hjt_h_seed_two_product_bound + S pa_i_hjt_h_seed_two_product = 2) -> exists pa_p_hjt_h_seed_two_product pa_r_hjt_h_seed_two_product pa_s_hjt_h_seed_two_product. ((((exists pa_h_hjt_h_seed_two_product_factor. pa_h_hjt_h_seed_two_product_factor + S (pa_p_hjt_h_seed_two_product) = S ((S (pa_i_hjt_h_seed_two_product)) * pa_c_hjt_h_seed_two)) /\ exists pa_q_hjt_h_seed_two_product_factor. pa_b_hjt_h_seed_two = pa_q_hjt_h_seed_two_product_factor * S ((S (pa_i_hjt_h_seed_two_product)) * pa_c_hjt_h_seed_two) + (pa_p_hjt_h_seed_two_product))) /\ ((((exists pa_h_hjt_h_seed_two_product_partial. pa_h_hjt_h_seed_two_product_partial + S (pa_r_hjt_h_seed_two_product) = S ((S (pa_i_hjt_h_seed_two_product)) * pa_v_hjt_h_seed_two_product)) /\ exists pa_q_hjt_h_seed_two_product_partial. pa_u_hjt_h_seed_two_product = pa_q_hjt_h_seed_two_product_partial * S ((S (pa_i_hjt_h_seed_two_product)) * pa_v_hjt_h_seed_two_product) + (pa_r_hjt_h_seed_two_product))) /\ ((((exists pa_h_hjt_h_seed_two_product_successor. pa_h_hjt_h_seed_two_product_successor + S (pa_s_hjt_h_seed_two_product) = S ((S (S pa_i_hjt_h_seed_two_product)) * pa_v_hjt_h_seed_two_product)) /\ exists pa_q_hjt_h_seed_two_product_successor. pa_u_hjt_h_seed_two_product = pa_q_hjt_h_seed_two_product_successor * S ((S (S pa_i_hjt_h_seed_two_product)) * pa_v_hjt_h_seed_two_product) + (pa_s_hjt_h_seed_two_product))) /\ pa_s_hjt_h_seed_two_product = pa_r_hjt_h_seed_two_product * pa_p_hjt_h_seed_two_product)))))))) /\ (exists pa_b_hjt_h_seed_seven pa_c_hjt_h_seed_seven. ((forall pa_i_hjt_h_seed_seven_repeat. (exists pa_lt_hjt_h_seed_seven_repeat_bound. pa_lt_hjt_h_seed_seven_repeat_bound + S pa_i_hjt_h_seed_seven_repeat = 7) -> (((exists pa_h_hjt_h_seed_seven_repeat_decoded. pa_h_hjt_h_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_hjt_h_seed_seven_repeat)) * pa_c_hjt_h_seed_seven)) /\ exists pa_q_hjt_h_seed_seven_repeat_decoded. pa_b_hjt_h_seed_seven = pa_q_hjt_h_seed_seven_repeat_decoded * S ((S (pa_i_hjt_h_seed_seven_repeat)) * pa_c_hjt_h_seed_seven) + (2)))) /\ (exists pa_u_hjt_h_seed_seven_product pa_v_hjt_h_seed_seven_product. ((((exists pa_h_hjt_h_seed_seven_product_start. pa_h_hjt_h_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_seed_seven_product)) /\ exists pa_q_hjt_h_seed_seven_product_start. pa_u_hjt_h_seed_seven_product = pa_q_hjt_h_seed_seven_product_start * S ((S (0)) * pa_v_hjt_h_seed_seven_product) + (1))) /\ ((((exists pa_h_hjt_h_seed_seven_product_terminal. pa_h_hjt_h_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hjt_h_seed_seven_product)) /\ exists pa_q_hjt_h_seed_seven_product_terminal. pa_u_hjt_h_seed_seven_product = pa_q_hjt_h_seed_seven_product_terminal * S ((S (7)) * pa_v_hjt_h_seed_seven_product) + (128))) /\ forall pa_i_hjt_h_seed_seven_product. (exists pa_lt_hjt_h_seed_seven_product_bound. pa_lt_hjt_h_seed_seven_product_bound + S pa_i_hjt_h_seed_seven_product = 7) -> exists pa_p_hjt_h_seed_seven_product pa_r_hjt_h_seed_seven_product pa_s_hjt_h_seed_seven_product. ((((exists pa_h_hjt_h_seed_seven_product_factor. pa_h_hjt_h_seed_seven_product_factor + S (pa_p_hjt_h_seed_seven_product) = S ((S (pa_i_hjt_h_seed_seven_product)) * pa_c_hjt_h_seed_seven)) /\ exists pa_q_hjt_h_seed_seven_product_factor. pa_b_hjt_h_seed_seven = pa_q_hjt_h_seed_seven_product_factor * S ((S (pa_i_hjt_h_seed_seven_product)) * pa_c_hjt_h_seed_seven) + (pa_p_hjt_h_seed_seven_product))) /\ ((((exists pa_h_hjt_h_seed_seven_product_partial. pa_h_hjt_h_seed_seven_product_partial + S (pa_r_hjt_h_seed_seven_product) = S ((S (pa_i_hjt_h_seed_seven_product)) * pa_v_hjt_h_seed_seven_product)) /\ exists pa_q_hjt_h_seed_seven_product_partial. pa_u_hjt_h_seed_seven_product = pa_q_hjt_h_seed_seven_product_partial * S ((S (pa_i_hjt_h_seed_seven_product)) * pa_v_hjt_h_seed_seven_product) + (pa_r_hjt_h_seed_seven_product))) /\ ((((exists pa_h_hjt_h_seed_seven_product_successor. pa_h_hjt_h_seed_seven_product_successor + S (pa_s_hjt_h_seed_seven_product) = S ((S (S pa_i_hjt_h_seed_seven_product)) * pa_v_hjt_h_seed_seven_product)) /\ exists pa_q_hjt_h_seed_seven_product_successor. pa_u_hjt_h_seed_seven_product = pa_q_hjt_h_seed_seven_product_successor * S ((S (S pa_i_hjt_h_seed_seven_product)) * pa_v_hjt_h_seed_seven_product) + (pa_s_hjt_h_seed_seven_product))) /\ pa_s_hjt_h_seed_seven_product = pa_r_hjt_h_seed_seven_product * pa_p_hjt_h_seed_seven_product))))))))
  76. 0076apply pow_two_seed_bundle_from_total
  77. 0077exact htotal
  78. 0078cases hseeds
  79. 0079have htwo_four : x3 = x4
  80. 0080specialize pow_mul_exp_from_total 2
  81. 0081specialize pow_mul_exp_from_total 2
  82. 0082specialize pow_mul_exp_from_total (s + 1)
  83. 0083specialize pow_mul_exp_from_total (2 * s + 2)
  84. 0084specialize pow_mul_exp_from_total 4
  85. 0085specialize pow_mul_exp_from_total x4
  86. 0086specialize pow_mul_exp_from_total x3
  87. 0087symm
  88. 0088apply pow_mul_exp_from_total
  89. 0089exact htotal
  90. 0090symm
  91. 0091exact hdouble_exponent
  92. 0092exact hseeds_left
  93. 0093exact hfour_exists_witness
  94. 0094exact htwo_exists_witness
  95. 0095have hdouble_factor : x2 = x3 * h
  96. 0096specialize pow_mul_base 2
  97. 0097specialize pow_mul_base (s + 1)
  98. 0098specialize pow_mul_base (2 * s + 2)
  99. 0099specialize pow_mul_base x3
  100. 0100specialize pow_mul_base h
  101. 0101specialize pow_mul_base x2
  102. 0102apply pow_mul_base
  103. 0103exact htwo_exists_witness
  104. 0104exact hh
  105. 0105exact hdouble_exists_witness
  106. 0106rewrite hdouble_factor at hprefix_double
  107. 0107rewrite htwo_four at hprefix_double
  108. 0108have hhfactor_bound : exists bqb_le_gap_hjt_h_factor_bound. bqb_le_gap_hjt_h_factor_bound + (x4 * h) = (x4 * u)
  109. 0109specialize mul_le_mul x4
  110. 0110specialize mul_le_mul x4
  111. 0111specialize mul_le_mul h
  112. 0112specialize mul_le_mul u
  113. 0113apply mul_le_mul
  114. 0114specialize le_refl x4
  115. 0115exact le_refl
  116. 0116exact hhu
  117. 0117have hprefix_bound : exists bqb_le_gap_hjt_h_prefix_bound. bqb_le_gap_hjt_h_prefix_bound + (x1) = (x4 * u)
  118. 0118specialize le_trans x1
  119. 0119specialize le_trans (x4 * h)
  120. 0120specialize le_trans (x4 * u)
  121. 0121apply le_trans
  122. 0122exact hprefix_double
  123. 0123exact hhfactor_bound
  124. 0124have hnext_sum : 2 * s + 14 = (2 * s + 2) + 12
  125. 0125simp [add_assoc]
  126. 0126have hnext_factor : hn = x1 * j
  127. 0127specialize pow_add (s + 7)
  128. 0128specialize pow_add (2 * s + 2)
  129. 0129specialize pow_add 12
  130. 0130specialize pow_add (2 * s + 14)
  131. 0131specialize pow_add x1
  132. 0132specialize pow_add j
  133. 0133specialize pow_add hn
  134. 0134apply pow_add
  135. 0135exact hnext_sum
  136. 0136exact hprefix_exists_witness
  137. 0137exact hj
  138. 0138exact hhn
  139. 0139have hbound_prefix_exists : exists hb. (exists pa_b_hjt_h_bound_prefix pa_c_hjt_h_bound_prefix. ((forall pa_i_hjt_h_bound_prefix_repeat. (exists pa_lt_hjt_h_bound_prefix_repeat_bound. pa_lt_hjt_h_bound_prefix_repeat_bound + S pa_i_hjt_h_bound_prefix_repeat = (s + 1) + e) -> (((exists pa_h_hjt_h_bound_prefix_repeat_decoded. pa_h_hjt_h_bound_prefix_repeat_decoded + S (4) = S ((S (pa_i_hjt_h_bound_prefix_repeat)) * pa_c_hjt_h_bound_prefix)) /\ exists pa_q_hjt_h_bound_prefix_repeat_decoded. pa_b_hjt_h_bound_prefix = pa_q_hjt_h_bound_prefix_repeat_decoded * S ((S (pa_i_hjt_h_bound_prefix_repeat)) * pa_c_hjt_h_bound_prefix) + (4)))) /\ (exists pa_u_hjt_h_bound_prefix_product pa_v_hjt_h_bound_prefix_product. ((((exists pa_h_hjt_h_bound_prefix_product_start. pa_h_hjt_h_bound_prefix_product_start + S (1) = S ((S (0)) * pa_v_hjt_h_bound_prefix_product)) /\ exists pa_q_hjt_h_bound_prefix_product_start. pa_u_hjt_h_bound_prefix_product = pa_q_hjt_h_bound_prefix_product_start * S ((S (0)) * pa_v_hjt_h_bound_prefix_product) + (1))) /\ ((((exists pa_h_hjt_h_bound_prefix_product_terminal. pa_h_hjt_h_bound_prefix_product_terminal + S (hb) = S ((S ((s + 1) + e)) * pa_v_hjt_h_bound_prefix_product)) /\ exists pa_q_hjt_h_bound_prefix_product_terminal. pa_u_hjt_h_bound_prefix_product = pa_q_hjt_h_bound_prefix_product_terminal * S ((S ((s + 1) + e)) * pa_v_hjt_h_bound_prefix_product) + (hb))) /\ forall pa_i_hjt_h_bound_prefix_product. (exists pa_lt_hjt_h_bound_prefix_product_bound. pa_lt_hjt_h_bound_prefix_product_bound + S pa_i_hjt_h_bound_prefix_product = (s + 1) + e) -> exists pa_p_hjt_h_bound_prefix_product pa_r_hjt_h_bound_prefix_product pa_s_hjt_h_bound_prefix_product. ((((exists pa_h_hjt_h_bound_prefix_product_factor. pa_h_hjt_h_bound_prefix_product_factor + S (pa_p_hjt_h_bound_prefix_product) = S ((S (pa_i_hjt_h_bound_prefix_product)) * pa_c_hjt_h_bound_prefix)) /\ exists pa_q_hjt_h_bound_prefix_product_factor. pa_b_hjt_h_bound_prefix = pa_q_hjt_h_bound_prefix_product_factor * S ((S (pa_i_hjt_h_bound_prefix_product)) * pa_c_hjt_h_bound_prefix) + (pa_p_hjt_h_bound_prefix_product))) /\ ((((exists pa_h_hjt_h_bound_prefix_product_partial. pa_h_hjt_h_bound_prefix_product_partial + S (pa_r_hjt_h_bound_prefix_product) = S ((S (pa_i_hjt_h_bound_prefix_product)) * pa_v_hjt_h_bound_prefix_product)) /\ exists pa_q_hjt_h_bound_prefix_product_partial. pa_u_hjt_h_bound_prefix_product = pa_q_hjt_h_bound_prefix_product_partial * S ((S (pa_i_hjt_h_bound_prefix_product)) * pa_v_hjt_h_bound_prefix_product) + (pa_r_hjt_h_bound_prefix_product))) /\ ((((exists pa_h_hjt_h_bound_prefix_product_successor. pa_h_hjt_h_bound_prefix_product_successor + S (pa_s_hjt_h_bound_prefix_product) = S ((S (S pa_i_hjt_h_bound_prefix_product)) * pa_v_hjt_h_bound_prefix_product)) /\ exists pa_q_hjt_h_bound_prefix_product_successor. pa_u_hjt_h_bound_prefix_product = pa_q_hjt_h_bound_prefix_product_successor * S ((S (S pa_i_hjt_h_bound_prefix_product)) * pa_v_hjt_h_bound_prefix_product) + (pa_s_hjt_h_bound_prefix_product))) /\ pa_s_hjt_h_bound_prefix_product = pa_r_hjt_h_bound_prefix_product * pa_p_hjt_h_bound_prefix_product))))))))
  140. 0140specialize htotal 4
  141. 0141specialize htotal ((s + 1) + e)
  142. 0142exact htotal
  143. 0143cases hbound_prefix_exists
  144. 0144have hbound_prefix_factor : x5 = x4 * u
  145. 0145specialize pow_add 4
  146. 0146specialize pow_add (s + 1)
  147. 0147specialize pow_add e
  148. 0148specialize pow_add ((s + 1) + e)
  149. 0149specialize pow_add x4
  150. 0150specialize pow_add u
  151. 0151specialize pow_add x5
  152. 0152apply pow_add
  153. 0153refl
  154. 0154exact hfour_exists_witness
  155. 0155exact hu
  156. 0156exact hbound_prefix_exists_witness
  157. 0157have hbound_sum : f = ((s + 1) + e) + (s + 5)
  158. 0158rewrite hceilshift
  159. 0159simp [two_mul_eq_add_self, add_assoc, add_comm]
  160. 0160congr
  161. 0161congr
  162. 0162congr
  163. 0163congr
  164. 0164congr
  165. 0165trans S (s + (e + s))
  166. 0166congr
  167. 0167trans (e + s) + s
  168. 0168symm
  169. 0169apply add_assoc
  170. 0170trans (s + e) + s
  171. 0171congr
  172. 0172apply add_comm
  173. 0173refl
  174. 0174apply add_assoc
  175. 0175symm
  176. 0176apply add_succ_left
  177. 0177have hbound_factor : un = x5 * g
  178. 0178specialize pow_add 4
  179. 0179specialize pow_add ((s + 1) + e)
  180. 0180specialize pow_add (s + 5)
  181. 0181specialize pow_add f
  182. 0182specialize pow_add x5
  183. 0183specialize pow_add g
  184. 0184specialize pow_add un
  185. 0185apply pow_add
  186. 0186exact hbound_sum
  187. 0187exact hbound_prefix_exists_witness
  188. 0188exact hg
  189. 0189exact hun
  190. 0190have hproducts : exists bqb_le_gap_hjt_h_products. bqb_le_gap_hjt_h_products + (x1 * j) = ((x4 * u) * g)
  191. 0191specialize mul_le_mul x1
  192. 0192specialize mul_le_mul (x4 * u)
  193. 0193specialize mul_le_mul j
  194. 0194specialize mul_le_mul g
  195. 0195apply mul_le_mul
  196. 0196exact hprefix_bound
  197. 0197exact hjg
  198. 0198rewrite hnext_factor
  199. 0199rewrite hbound_factor
  200. 0200rewrite hbound_prefix_factor
  201. 0201exact hproducts