BT00SW

bertrand_h_six_step_transport_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

201 script commands · 51 reading checkpoints · 21 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (12)
ceil div six square six steppow base monotonepow mul basepow two seed bundle from totalpow mul exp from totalpow addmul le mulle reflle transadd assocadd commadd succ left

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro s
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro h
  5. L5
    intro u
  6. L6
    intro j
  7. L7
    intro g
  8. L8
    intro hn
  9. L9
    intro un
  10. L10
    intro htotal
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hlower
  2. L12
    intro hceiling
  3. L13
    intro hnextceiling
  4. L14
    intro hh
  5. L15
    intro hu
  6. L16
    intro hhu
  7. L17
    intro hj
  8. L18
    intro hg
  9. L19
    intro hjg
  10. L20
    intro hhn
03Fix variables and assumptionsL21–21

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro hun
04Establish hceilshiftL22–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ceil div six square six step.

  1. L22
    have hceilshift : f = e + (2 * s + 6)
  2. L23
    specialize ceil_div_six_square_six_step s
  3. L24
    specialize ceil_div_six_square_six_step e
  4. L25
    specialize ceil_div_six_square_six_step f
  5. L26
    apply ceil_div_six_square_six_step
  6. L27
    exact hceiling
  7. L28
    exact hnextceiling
05Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hlower
06Establish hbaseL30–30

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hbase : exists bqb_le_gap_hjt_h_base. bqb_le_gap_hjt_h_base + (s + 7) = (2 * (s + 1))
07Construct an explicit witnessL31–31

Supply the displayed value, then prove that it has the required property.

  1. L31
    exists x
08Calculate and transport equalitiesL32–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite <- hlower_witness
  2. L33
    simp [two_mul_eq_add_self, add_assoc, add_comm]
  3. L34
    rewrite <- hlower_witness
  4. L35
    rewrite <- hlower_witness
  5. L36
    simp [add_assoc, add_comm]
09Establish honeL37–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA4.

  1. L37
    have hone : s + 1 = S s
  2. L38
    trans S (s + 0)
  3. L39
    apply PA4
  4. L40
    congr
  5. L41
    apply PA3
10Establish hdouble_exponentL42–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA6.

  1. L42
    have hdouble_exponent : 2 * (s + 1) = 2 * s + 2
  2. L43
    rewrite hone
  3. L44
    apply PA6
11Establish hprefix_existsL45–48

Establish this local claim before using it. It is not an additional assumption.

  1. L45
    have hprefix_exists : ∃ hp. Pow(s + 7,2 · s + 2,hp)Definitions: Pow
  2. L46
    specialize htotal (s + 7)
  3. L47
    specialize htotal (2 * s + 2)
  4. L48
    exact htotal
12Separate the logical casesL49–49

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L49
    cases hprefix_exists
13Establish hdouble_existsL50–53

Establish this local claim before using it. It is not an additional assumption.

  1. L50
    have hdouble_exists : ∃ hd. Pow(2 · (s + 1),2 · s + 2,hd)Definitions: Pow
  2. L51
    specialize htotal (2 * (s + 1))
  3. L52
    specialize htotal (2 * s + 2)
  4. L53
    exact htotal
14Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hdouble_exists
15Establish hprefix_doubleL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.

  1. L55
    have hprefix_double : exists bqb_le_gap_hjt_h_prefix_double. bqb_le_gap_hjt_h_prefix_double + (x1) = (x2)
  2. L56
    specialize pow_base_monotone (s + 7)
  3. L57
    specialize pow_base_monotone (2 * (s + 1))
  4. L58
    specialize pow_base_monotone (2 * s + 2)
  5. L59
    specialize pow_base_monotone x1
  6. L60
    specialize pow_base_monotone x2
  7. L61
    apply pow_base_monotone
  8. L62
    exact hbase
  9. L63
    exact hprefix_exists_witness
  10. L64
    exact hdouble_exists_witness
16Establish htwo_existsL65–68

Establish this local claim before using it. It is not an additional assumption.

  1. L65
    have htwo_exists : ∃ ht. Pow(2,2 · s + 2,ht)Definitions: Pow
  2. L66
    specialize htotal 2
  3. L67
    specialize htotal (2 * s + 2)
  4. L68
    exact htotal
17Separate the logical casesL69–69

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L69
    cases htwo_exists
18Establish hfour_existsL70–73

Establish this local claim before using it. It is not an additional assumption.

  1. L70
    have hfour_exists : ∃ hf. Pow(4,s + 1,hf)Definitions: Pow
  2. L71
    specialize htotal 4
  3. L72
    specialize htotal (s + 1)
  4. L73
    exact htotal
19Separate the logical casesL74–74

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L74
    cases hfour_exists
20Establish hseedsL75–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two seed bundle from total.

  1. L75
    have hseeds : Pow(2,2,4) ∧ Pow(2,7,128)Definitions: Pow
  2. L76
    apply pow_two_seed_bundle_from_total
  3. L77
    exact htotal
21Separate the logical casesL78–78

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L78
    cases hseeds
22Establish htwo_fourL79–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul exp from total.

  1. L79
    have htwo_four : x3 = x4
  2. L80
    specialize pow_mul_exp_from_total 2
  3. L81
    specialize pow_mul_exp_from_total 2
  4. L82
    specialize pow_mul_exp_from_total (s + 1)
  5. L83
    specialize pow_mul_exp_from_total (2 * s + 2)
  6. L84
    specialize pow_mul_exp_from_total 4
  7. L85
    specialize pow_mul_exp_from_total x4
  8. L86
    specialize pow_mul_exp_from_total x3
  9. L87
    symm
  10. L88
    apply pow_mul_exp_from_total
23Use earlier factsL89–89

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L89
    exact htotal
24Calculate and transport equalitiesL90–90

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L90
    symm
25Use earlier factsL91–94

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L91
    exact hdouble_exponent
  2. L92
    exact hseeds_left
  3. L93
    exact hfour_exists_witness
  4. L94
    exact htwo_exists_witness
26Establish hdouble_factorL95–104

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.

  1. L95
    have hdouble_factor : x2 = x3 * h
  2. L96
    specialize pow_mul_base 2
  3. L97
    specialize pow_mul_base (s + 1)
  4. L98
    specialize pow_mul_base (2 * s + 2)
  5. L99
    specialize pow_mul_base x3
  6. L100
    specialize pow_mul_base h
  7. L101
    specialize pow_mul_base x2
  8. L102
    apply pow_mul_base
  9. L103
    exact htwo_exists_witness
  10. L104
    exact hh
27Use earlier factsL105–105

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L105
    exact hdouble_exists_witness
28Calculate and transport equalitiesL106–107

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L106
    rewrite hdouble_factor at hprefix_double
  2. L107
    rewrite htwo_four at hprefix_double
29Establish hhfactor_boundL108–116

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.

  1. L108
    have hhfactor_bound : exists bqb_le_gap_hjt_h_factor_bound. bqb_le_gap_hjt_h_factor_bound + (x4 * h) = (x4 * u)
  2. L109
    specialize mul_le_mul x4
  3. L110
    specialize mul_le_mul x4
  4. L111
    specialize mul_le_mul h
  5. L112
    specialize mul_le_mul u
  6. L113
    apply mul_le_mul
  7. L114
    specialize le_refl x4
  8. L115
    exact le_refl
  9. L116
    exact hhu
30Establish hprefix_boundL117–123

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L117
    have hprefix_bound : exists bqb_le_gap_hjt_h_prefix_bound. bqb_le_gap_hjt_h_prefix_bound + (x1) = (x4 * u)
  2. L118
    specialize le_trans x1
  3. L119
    specialize le_trans (x4 * h)
  4. L120
    specialize le_trans (x4 * u)
  5. L121
    apply le_trans
  6. L122
    exact hprefix_double
  7. L123
    exact hhfactor_bound
31Establish hnext_sumL124–125

Establish this local claim before using it. It is not an additional assumption.

  1. L124
    have hnext_sum : 2 * s + 14 = (2 * s + 2) + 12
  2. L125
    simp [add_assoc]
32Establish hnext_factorL126–135

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.

  1. L126
    have hnext_factor : hn = x1 * j
  2. L127
    specialize pow_add (s + 7)
  3. L128
    specialize pow_add (2 * s + 2)
  4. L129
    specialize pow_add 12
  5. L130
    specialize pow_add (2 * s + 14)
  6. L131
    specialize pow_add x1
  7. L132
    specialize pow_add j
  8. L133
    specialize pow_add hn
  9. L134
    apply pow_add
  10. L135
    exact hnext_sum
33Use earlier factsL136–138

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L136
    exact hprefix_exists_witness
  2. L137
    exact hj
  3. L138
    exact hhn
34Establish hbound_prefix_existsL139–142

Establish this local claim before using it. It is not an additional assumption.

  1. L139
    have hbound_prefix_exists : ∃ hb. Pow(4,s + 1 + e,hb)Definitions: Pow
  2. L140
    specialize htotal 4
  3. L141
    specialize htotal ((s + 1) + e)
  4. L142
    exact htotal
35Separate the logical casesL143–143

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L143
    cases hbound_prefix_exists
36Establish hbound_prefix_factorL144–153

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.

  1. L144
    have hbound_prefix_factor : x5 = x4 * u
  2. L145
    specialize pow_add 4
  3. L146
    specialize pow_add (s + 1)
  4. L147
    specialize pow_add e
  5. L148
    specialize pow_add ((s + 1) + e)
  6. L149
    specialize pow_add x4
  7. L150
    specialize pow_add u
  8. L151
    specialize pow_add x5
  9. L152
    apply pow_add
  10. L153
    refl
37Use earlier factsL154–156

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L154
    exact hfour_exists_witness
  2. L155
    exact hu
  3. L156
    exact hbound_prefix_exists_witness
38Establish hbound_sumL157–166

Establish this local claim before using it. It is not an additional assumption.

  1. L157
    have hbound_sum : f = ((s + 1) + e) + (s + 5)
  2. L158
    rewrite hceilshift
  3. L159
    simp [two_mul_eq_add_self, add_assoc, add_comm]
  4. L160
    congr
  5. L161
    congr
  6. L162
    congr
  7. L163
    congr
  8. L164
    congr
  9. L165
    trans S (s + (e + s))
  10. L166
    congr
39Calculate and transport equalitiesL167–168

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L167
    trans (e + s) + s
  2. L168
    symm
40Use earlier factsL169–169

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L169
    apply add_assoc
41Calculate and transport equalitiesL170–171

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L170
    trans (s + e) + s
  2. L171
    congr
42Use earlier factsL172–172

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L172
    apply add_comm
43Calculate and transport equalitiesL173–173

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L173
    refl
44Use earlier factsL174–174

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L174
    apply add_assoc
45Calculate and transport equalitiesL175–175

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L175
    symm
46Use earlier factsL176–176

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L176
    apply add_succ_left
47Establish hbound_factorL177–186

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.

  1. L177
    have hbound_factor : un = x5 * g
  2. L178
    specialize pow_add 4
  3. L179
    specialize pow_add ((s + 1) + e)
  4. L180
    specialize pow_add (s + 5)
  5. L181
    specialize pow_add f
  6. L182
    specialize pow_add x5
  7. L183
    specialize pow_add g
  8. L184
    specialize pow_add un
  9. L185
    apply pow_add
  10. L186
    exact hbound_sum
48Use earlier factsL187–189

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L187
    exact hbound_prefix_exists_witness
  2. L188
    exact hg
  3. L189
    exact hun
49Establish hproductsL190–199

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.

  1. L190
    have hproducts : exists bqb_le_gap_hjt_h_products. bqb_le_gap_hjt_h_products + (x1 * j) = ((x4 * u) * g)
  2. L191
    specialize mul_le_mul x1
  3. L192
    specialize mul_le_mul (x4 * u)
  4. L193
    specialize mul_le_mul j
  5. L194
    specialize mul_le_mul g
  6. L195
    apply mul_le_mul
  7. L196
    exact hprefix_bound
  8. L197
    exact hjg
  9. L198
    rewrite hnext_factor
  10. L199
    rewrite hbound_factor
50Calculate and transport equalitiesL200–200

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L200
    rewrite hbound_prefix_factor
51Use earlier factsL201–201

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L201
    exact hproducts

Library-wide reading audit

Original exact command ledger · 201 lines
  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