BT00SX

bertrand_j_six_step_transport_from_total

Alpha body-checked · checked-use disabled

J(s) implies J(s+6) through the shared 2^12 = 4^6 factor.

Exact expanded PA statement

forall s j g jn gn. (forall bpt_a_hjt_j bpt_e_hjt_j. exists bpt_x_hjt_j. (exists ff_b_bpt_value_hjt_j ff_c_bpt_value_hjt_j. ((forall ff_i_bpt_value_hjt_j_repeat. (exists ff_lt_bpt_value_hjt_j_repeat_bound. ff_lt_bpt_value_hjt_j_repeat_bound + S ff_i_bpt_value_hjt_j_repeat = bpt_e_hjt_j) -> (((exists ff_h_bpt_value_hjt_j_repeat_decoded. ff_h_bpt_value_hjt_j_repeat_decoded + S (bpt_a_hjt_j) = S ((S (ff_i_bpt_value_hjt_j_repeat)) * ff_c_bpt_value_hjt_j)) /\ exists ff_q_bpt_value_hjt_j_repeat_decoded. ff_b_bpt_value_hjt_j = ff_q_bpt_value_hjt_j_repeat_decoded * S ((S (ff_i_bpt_value_hjt_j_repeat)) * ff_c_bpt_value_hjt_j) + (bpt_a_hjt_j)))) /\ (exists ff_u_bpt_value_hjt_j_product ff_v_bpt_value_hjt_j_product. ((((exists ff_h_bpt_value_hjt_j_product_start. ff_h_bpt_value_hjt_j_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_start. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_start * S ((S (0)) * ff_v_bpt_value_hjt_j_product) + (1))) /\ ((((exists ff_h_bpt_value_hjt_j_product_terminal. ff_h_bpt_value_hjt_j_product_terminal + S (bpt_x_hjt_j) = S ((S (bpt_e_hjt_j)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_terminal. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_terminal * S ((S (bpt_e_hjt_j)) * ff_v_bpt_value_hjt_j_product) + (bpt_x_hjt_j))) /\ forall ff_i_bpt_value_hjt_j_product. (exists ff_lt_bpt_value_hjt_j_product_bound. ff_lt_bpt_value_hjt_j_product_bound + S ff_i_bpt_value_hjt_j_product = bpt_e_hjt_j) -> exists ff_p_bpt_value_hjt_j_product ff_r_bpt_value_hjt_j_product ff_s_bpt_value_hjt_j_product. ((((exists ff_h_bpt_value_hjt_j_product_factor. ff_h_bpt_value_hjt_j_product_factor + S (ff_p_bpt_value_hjt_j_product) = S ((S (ff_i_bpt_value_hjt_j_product)) * ff_c_bpt_value_hjt_j)) /\ exists ff_q_bpt_value_hjt_j_product_factor. ff_b_bpt_value_hjt_j = ff_q_bpt_value_hjt_j_product_factor * S ((S (ff_i_bpt_value_hjt_j_product)) * ff_c_bpt_value_hjt_j) + (ff_p_bpt_value_hjt_j_product))) /\ ((((exists ff_h_bpt_value_hjt_j_product_partial. ff_h_bpt_value_hjt_j_product_partial + S (ff_r_bpt_value_hjt_j_product) = S ((S (ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_partial. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_partial * S ((S (ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product) + (ff_r_bpt_value_hjt_j_product))) /\ ((((exists ff_h_bpt_value_hjt_j_product_successor. ff_h_bpt_value_hjt_j_product_successor + S (ff_s_bpt_value_hjt_j_product) = S ((S (S ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_successor. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_successor * S ((S (S ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product) + (ff_s_bpt_value_hjt_j_product))) /\ ff_s_bpt_value_hjt_j_product = ff_r_bpt_value_hjt_j_product * ff_p_bpt_value_hjt_j_product))))))))) -> (exists pa_b_hjt_j_now pa_c_hjt_j_now. ((forall pa_i_hjt_j_now_repeat. (exists pa_lt_hjt_j_now_repeat_bound. pa_lt_hjt_j_now_repeat_bound + S pa_i_hjt_j_now_repeat = 12) -> (((exists pa_h_hjt_j_now_repeat_decoded. pa_h_hjt_j_now_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_j_now_repeat)) * pa_c_hjt_j_now)) /\ exists pa_q_hjt_j_now_repeat_decoded. pa_b_hjt_j_now = pa_q_hjt_j_now_repeat_decoded * S ((S (pa_i_hjt_j_now_repeat)) * pa_c_hjt_j_now) + (s + 7)))) /\ (exists pa_u_hjt_j_now_product pa_v_hjt_j_now_product. ((((exists pa_h_hjt_j_now_product_start. pa_h_hjt_j_now_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_start. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_start * S ((S (0)) * pa_v_hjt_j_now_product) + (1))) /\ ((((exists pa_h_hjt_j_now_product_terminal. pa_h_hjt_j_now_product_terminal + S (j) = S ((S (12)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_terminal. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_terminal * S ((S (12)) * pa_v_hjt_j_now_product) + (j))) /\ forall pa_i_hjt_j_now_product. (exists pa_lt_hjt_j_now_product_bound. pa_lt_hjt_j_now_product_bound + S pa_i_hjt_j_now_product = 12) -> exists pa_p_hjt_j_now_product pa_r_hjt_j_now_product pa_s_hjt_j_now_product. ((((exists pa_h_hjt_j_now_product_factor. pa_h_hjt_j_now_product_factor + S (pa_p_hjt_j_now_product) = S ((S (pa_i_hjt_j_now_product)) * pa_c_hjt_j_now)) /\ exists pa_q_hjt_j_now_product_factor. pa_b_hjt_j_now = pa_q_hjt_j_now_product_factor * S ((S (pa_i_hjt_j_now_product)) * pa_c_hjt_j_now) + (pa_p_hjt_j_now_product))) /\ ((((exists pa_h_hjt_j_now_product_partial. pa_h_hjt_j_now_product_partial + S (pa_r_hjt_j_now_product) = S ((S (pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_partial. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_partial * S ((S (pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product) + (pa_r_hjt_j_now_product))) /\ ((((exists pa_h_hjt_j_now_product_successor. pa_h_hjt_j_now_product_successor + S (pa_s_hjt_j_now_product) = S ((S (S pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_successor. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_successor * S ((S (S pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product) + (pa_s_hjt_j_now_product))) /\ pa_s_hjt_j_now_product = pa_r_hjt_j_now_product * pa_p_hjt_j_now_product)))))))) -> (exists pa_b_hjt_j_now_bound pa_c_hjt_j_now_bound. ((forall pa_i_hjt_j_now_bound_repeat. (exists pa_lt_hjt_j_now_bound_repeat_bound. pa_lt_hjt_j_now_bound_repeat_bound + S pa_i_hjt_j_now_bound_repeat = s + 5) -> (((exists pa_h_hjt_j_now_bound_repeat_decoded. pa_h_hjt_j_now_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_now_bound_repeat)) * pa_c_hjt_j_now_bound)) /\ exists pa_q_hjt_j_now_bound_repeat_decoded. pa_b_hjt_j_now_bound = pa_q_hjt_j_now_bound_repeat_decoded * S ((S (pa_i_hjt_j_now_bound_repeat)) * pa_c_hjt_j_now_bound) + (4)))) /\ (exists pa_u_hjt_j_now_bound_product pa_v_hjt_j_now_bound_product. ((((exists pa_h_hjt_j_now_bound_product_start. pa_h_hjt_j_now_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_start. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_start * S ((S (0)) * pa_v_hjt_j_now_bound_product) + (1))) /\ ((((exists pa_h_hjt_j_now_bound_product_terminal. pa_h_hjt_j_now_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_terminal. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_terminal * S ((S (s + 5)) * pa_v_hjt_j_now_bound_product) + (g))) /\ forall pa_i_hjt_j_now_bound_product. (exists pa_lt_hjt_j_now_bound_product_bound. pa_lt_hjt_j_now_bound_product_bound + S pa_i_hjt_j_now_bound_product = s + 5) -> exists pa_p_hjt_j_now_bound_product pa_r_hjt_j_now_bound_product pa_s_hjt_j_now_bound_product. ((((exists pa_h_hjt_j_now_bound_product_factor. pa_h_hjt_j_now_bound_product_factor + S (pa_p_hjt_j_now_bound_product) = S ((S (pa_i_hjt_j_now_bound_product)) * pa_c_hjt_j_now_bound)) /\ exists pa_q_hjt_j_now_bound_product_factor. pa_b_hjt_j_now_bound = pa_q_hjt_j_now_bound_product_factor * S ((S (pa_i_hjt_j_now_bound_product)) * pa_c_hjt_j_now_bound) + (pa_p_hjt_j_now_bound_product))) /\ ((((exists pa_h_hjt_j_now_bound_product_partial. pa_h_hjt_j_now_bound_product_partial + S (pa_r_hjt_j_now_bound_product) = S ((S (pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_partial. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_partial * S ((S (pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product) + (pa_r_hjt_j_now_bound_product))) /\ ((((exists pa_h_hjt_j_now_bound_product_successor. pa_h_hjt_j_now_bound_product_successor + S (pa_s_hjt_j_now_bound_product) = S ((S (S pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_successor. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_successor * S ((S (S pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product) + (pa_s_hjt_j_now_bound_product))) /\ pa_s_hjt_j_now_bound_product = pa_r_hjt_j_now_bound_product * pa_p_hjt_j_now_bound_product)))))))) -> (exists bqb_le_gap_hjt_j_now_result. bqb_le_gap_hjt_j_now_result + (j) = (g)) -> (exists pa_b_hjt_j_next pa_c_hjt_j_next. ((forall pa_i_hjt_j_next_repeat. (exists pa_lt_hjt_j_next_repeat_bound. pa_lt_hjt_j_next_repeat_bound + S pa_i_hjt_j_next_repeat = 12) -> (((exists pa_h_hjt_j_next_repeat_decoded. pa_h_hjt_j_next_repeat_decoded + S (s + 13) = S ((S (pa_i_hjt_j_next_repeat)) * pa_c_hjt_j_next)) /\ exists pa_q_hjt_j_next_repeat_decoded. pa_b_hjt_j_next = pa_q_hjt_j_next_repeat_decoded * S ((S (pa_i_hjt_j_next_repeat)) * pa_c_hjt_j_next) + (s + 13)))) /\ (exists pa_u_hjt_j_next_product pa_v_hjt_j_next_product. ((((exists pa_h_hjt_j_next_product_start. pa_h_hjt_j_next_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_start. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_start * S ((S (0)) * pa_v_hjt_j_next_product) + (1))) /\ ((((exists pa_h_hjt_j_next_product_terminal. pa_h_hjt_j_next_product_terminal + S (jn) = S ((S (12)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_terminal. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_terminal * S ((S (12)) * pa_v_hjt_j_next_product) + (jn))) /\ forall pa_i_hjt_j_next_product. (exists pa_lt_hjt_j_next_product_bound. pa_lt_hjt_j_next_product_bound + S pa_i_hjt_j_next_product = 12) -> exists pa_p_hjt_j_next_product pa_r_hjt_j_next_product pa_s_hjt_j_next_product. ((((exists pa_h_hjt_j_next_product_factor. pa_h_hjt_j_next_product_factor + S (pa_p_hjt_j_next_product) = S ((S (pa_i_hjt_j_next_product)) * pa_c_hjt_j_next)) /\ exists pa_q_hjt_j_next_product_factor. pa_b_hjt_j_next = pa_q_hjt_j_next_product_factor * S ((S (pa_i_hjt_j_next_product)) * pa_c_hjt_j_next) + (pa_p_hjt_j_next_product))) /\ ((((exists pa_h_hjt_j_next_product_partial. pa_h_hjt_j_next_product_partial + S (pa_r_hjt_j_next_product) = S ((S (pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_partial. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_partial * S ((S (pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product) + (pa_r_hjt_j_next_product))) /\ ((((exists pa_h_hjt_j_next_product_successor. pa_h_hjt_j_next_product_successor + S (pa_s_hjt_j_next_product) = S ((S (S pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_successor. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_successor * S ((S (S pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product) + (pa_s_hjt_j_next_product))) /\ pa_s_hjt_j_next_product = pa_r_hjt_j_next_product * pa_p_hjt_j_next_product)))))))) -> (exists pa_b_hjt_j_next_bound pa_c_hjt_j_next_bound. ((forall pa_i_hjt_j_next_bound_repeat. (exists pa_lt_hjt_j_next_bound_repeat_bound. pa_lt_hjt_j_next_bound_repeat_bound + S pa_i_hjt_j_next_bound_repeat = s + 11) -> (((exists pa_h_hjt_j_next_bound_repeat_decoded. pa_h_hjt_j_next_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_next_bound_repeat)) * pa_c_hjt_j_next_bound)) /\ exists pa_q_hjt_j_next_bound_repeat_decoded. pa_b_hjt_j_next_bound = pa_q_hjt_j_next_bound_repeat_decoded * S ((S (pa_i_hjt_j_next_bound_repeat)) * pa_c_hjt_j_next_bound) + (4)))) /\ (exists pa_u_hjt_j_next_bound_product pa_v_hjt_j_next_bound_product. ((((exists pa_h_hjt_j_next_bound_product_start. pa_h_hjt_j_next_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_start. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_start * S ((S (0)) * pa_v_hjt_j_next_bound_product) + (1))) /\ ((((exists pa_h_hjt_j_next_bound_product_terminal. pa_h_hjt_j_next_bound_product_terminal + S (gn) = S ((S (s + 11)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_terminal. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_terminal * S ((S (s + 11)) * pa_v_hjt_j_next_bound_product) + (gn))) /\ forall pa_i_hjt_j_next_bound_product. (exists pa_lt_hjt_j_next_bound_product_bound. pa_lt_hjt_j_next_bound_product_bound + S pa_i_hjt_j_next_bound_product = s + 11) -> exists pa_p_hjt_j_next_bound_product pa_r_hjt_j_next_bound_product pa_s_hjt_j_next_bound_product. ((((exists pa_h_hjt_j_next_bound_product_factor. pa_h_hjt_j_next_bound_product_factor + S (pa_p_hjt_j_next_bound_product) = S ((S (pa_i_hjt_j_next_bound_product)) * pa_c_hjt_j_next_bound)) /\ exists pa_q_hjt_j_next_bound_product_factor. pa_b_hjt_j_next_bound = pa_q_hjt_j_next_bound_product_factor * S ((S (pa_i_hjt_j_next_bound_product)) * pa_c_hjt_j_next_bound) + (pa_p_hjt_j_next_bound_product))) /\ ((((exists pa_h_hjt_j_next_bound_product_partial. pa_h_hjt_j_next_bound_product_partial + S (pa_r_hjt_j_next_bound_product) = S ((S (pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_partial. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_partial * S ((S (pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product) + (pa_r_hjt_j_next_bound_product))) /\ ((((exists pa_h_hjt_j_next_bound_product_successor. pa_h_hjt_j_next_bound_product_successor + S (pa_s_hjt_j_next_bound_product) = S ((S (S pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_successor. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_successor * S ((S (S pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product) + (pa_s_hjt_j_next_bound_product))) /\ pa_s_hjt_j_next_bound_product = pa_r_hjt_j_next_bound_product * pa_p_hjt_j_next_bound_product)))))))) -> (exists bqb_le_gap_hjt_j_next_result. bqb_le_gap_hjt_j_next_result + (jn) = (gn))

Structural proof guide

J(s) implies J(s+6) through the shared 2^12 = 4^6 factor.

Direct prerequisites: 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. The authored body proceeds by case analysis (4), intermediate claims (11), equality transport (3), closed numeral normalization (2).

Proof neighborhood

Direct dependencies

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

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 j
  3. 0003intro g
  4. 0004intro jn
  5. 0005intro gn
  6. 0006intro htotal
  7. 0007intro hj
  8. 0008intro hg
  9. 0009intro hjg
  10. 0010intro hjn
  11. 0011intro hgn
  12. 0012have hbase : exists bqb_le_gap_hjt_j_base. bqb_le_gap_hjt_j_base + (s + 13) = (2 * (s + 7))
  13. 0013exists S s
  14. 0014simp [two_mul_eq_add_self, add_assoc, add_comm]
  15. 0015have hdouble : exists jd. (exists pa_b_hjt_j_double pa_c_hjt_j_double. ((forall pa_i_hjt_j_double_repeat. (exists pa_lt_hjt_j_double_repeat_bound. pa_lt_hjt_j_double_repeat_bound + S pa_i_hjt_j_double_repeat = 12) -> (((exists pa_h_hjt_j_double_repeat_decoded. pa_h_hjt_j_double_repeat_decoded + S (2 * (s + 7)) = S ((S (pa_i_hjt_j_double_repeat)) * pa_c_hjt_j_double)) /\ exists pa_q_hjt_j_double_repeat_decoded. pa_b_hjt_j_double = pa_q_hjt_j_double_repeat_decoded * S ((S (pa_i_hjt_j_double_repeat)) * pa_c_hjt_j_double) + (2 * (s + 7))))) /\ (exists pa_u_hjt_j_double_product pa_v_hjt_j_double_product. ((((exists pa_h_hjt_j_double_product_start. pa_h_hjt_j_double_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_start. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_start * S ((S (0)) * pa_v_hjt_j_double_product) + (1))) /\ ((((exists pa_h_hjt_j_double_product_terminal. pa_h_hjt_j_double_product_terminal + S (jd) = S ((S (12)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_terminal. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_terminal * S ((S (12)) * pa_v_hjt_j_double_product) + (jd))) /\ forall pa_i_hjt_j_double_product. (exists pa_lt_hjt_j_double_product_bound. pa_lt_hjt_j_double_product_bound + S pa_i_hjt_j_double_product = 12) -> exists pa_p_hjt_j_double_product pa_r_hjt_j_double_product pa_s_hjt_j_double_product. ((((exists pa_h_hjt_j_double_product_factor. pa_h_hjt_j_double_product_factor + S (pa_p_hjt_j_double_product) = S ((S (pa_i_hjt_j_double_product)) * pa_c_hjt_j_double)) /\ exists pa_q_hjt_j_double_product_factor. pa_b_hjt_j_double = pa_q_hjt_j_double_product_factor * S ((S (pa_i_hjt_j_double_product)) * pa_c_hjt_j_double) + (pa_p_hjt_j_double_product))) /\ ((((exists pa_h_hjt_j_double_product_partial. pa_h_hjt_j_double_product_partial + S (pa_r_hjt_j_double_product) = S ((S (pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_partial. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_partial * S ((S (pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product) + (pa_r_hjt_j_double_product))) /\ ((((exists pa_h_hjt_j_double_product_successor. pa_h_hjt_j_double_product_successor + S (pa_s_hjt_j_double_product) = S ((S (S pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_successor. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_successor * S ((S (S pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product) + (pa_s_hjt_j_double_product))) /\ pa_s_hjt_j_double_product = pa_r_hjt_j_double_product * pa_p_hjt_j_double_product))))))))
  16. 0016specialize htotal (2 * (s + 7))
  17. 0017specialize htotal 12
  18. 0018exact htotal
  19. 0019cases hdouble
  20. 0020have hjdouble : exists bqb_le_gap_hjt_j_next_double. bqb_le_gap_hjt_j_next_double + (jn) = (x)
  21. 0021specialize pow_base_monotone (s + 13)
  22. 0022specialize pow_base_monotone (2 * (s + 7))
  23. 0023specialize pow_base_monotone 12
  24. 0024specialize pow_base_monotone jn
  25. 0025specialize pow_base_monotone x
  26. 0026apply pow_base_monotone
  27. 0027exact hbase
  28. 0028exact hjn
  29. 0029exact hdouble_witness
  30. 0030have htwo : exists jt. (exists pa_b_hjt_j_two_factor pa_c_hjt_j_two_factor. ((forall pa_i_hjt_j_two_factor_repeat. (exists pa_lt_hjt_j_two_factor_repeat_bound. pa_lt_hjt_j_two_factor_repeat_bound + S pa_i_hjt_j_two_factor_repeat = 12) -> (((exists pa_h_hjt_j_two_factor_repeat_decoded. pa_h_hjt_j_two_factor_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_two_factor_repeat)) * pa_c_hjt_j_two_factor)) /\ exists pa_q_hjt_j_two_factor_repeat_decoded. pa_b_hjt_j_two_factor = pa_q_hjt_j_two_factor_repeat_decoded * S ((S (pa_i_hjt_j_two_factor_repeat)) * pa_c_hjt_j_two_factor) + (2)))) /\ (exists pa_u_hjt_j_two_factor_product pa_v_hjt_j_two_factor_product. ((((exists pa_h_hjt_j_two_factor_product_start. pa_h_hjt_j_two_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_start. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_start * S ((S (0)) * pa_v_hjt_j_two_factor_product) + (1))) /\ ((((exists pa_h_hjt_j_two_factor_product_terminal. pa_h_hjt_j_two_factor_product_terminal + S (jt) = S ((S (12)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_terminal. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_terminal * S ((S (12)) * pa_v_hjt_j_two_factor_product) + (jt))) /\ forall pa_i_hjt_j_two_factor_product. (exists pa_lt_hjt_j_two_factor_product_bound. pa_lt_hjt_j_two_factor_product_bound + S pa_i_hjt_j_two_factor_product = 12) -> exists pa_p_hjt_j_two_factor_product pa_r_hjt_j_two_factor_product pa_s_hjt_j_two_factor_product. ((((exists pa_h_hjt_j_two_factor_product_factor. pa_h_hjt_j_two_factor_product_factor + S (pa_p_hjt_j_two_factor_product) = S ((S (pa_i_hjt_j_two_factor_product)) * pa_c_hjt_j_two_factor)) /\ exists pa_q_hjt_j_two_factor_product_factor. pa_b_hjt_j_two_factor = pa_q_hjt_j_two_factor_product_factor * S ((S (pa_i_hjt_j_two_factor_product)) * pa_c_hjt_j_two_factor) + (pa_p_hjt_j_two_factor_product))) /\ ((((exists pa_h_hjt_j_two_factor_product_partial. pa_h_hjt_j_two_factor_product_partial + S (pa_r_hjt_j_two_factor_product) = S ((S (pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_partial. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_partial * S ((S (pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product) + (pa_r_hjt_j_two_factor_product))) /\ ((((exists pa_h_hjt_j_two_factor_product_successor. pa_h_hjt_j_two_factor_product_successor + S (pa_s_hjt_j_two_factor_product) = S ((S (S pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_successor. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_successor * S ((S (S pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product) + (pa_s_hjt_j_two_factor_product))) /\ pa_s_hjt_j_two_factor_product = pa_r_hjt_j_two_factor_product * pa_p_hjt_j_two_factor_product))))))))
  31. 0031specialize htotal 2
  32. 0032specialize htotal 12
  33. 0033exact htotal
  34. 0034cases htwo
  35. 0035have hfour : exists jf. (exists pa_b_hjt_j_four_factor pa_c_hjt_j_four_factor. ((forall pa_i_hjt_j_four_factor_repeat. (exists pa_lt_hjt_j_four_factor_repeat_bound. pa_lt_hjt_j_four_factor_repeat_bound + S pa_i_hjt_j_four_factor_repeat = 6) -> (((exists pa_h_hjt_j_four_factor_repeat_decoded. pa_h_hjt_j_four_factor_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_four_factor_repeat)) * pa_c_hjt_j_four_factor)) /\ exists pa_q_hjt_j_four_factor_repeat_decoded. pa_b_hjt_j_four_factor = pa_q_hjt_j_four_factor_repeat_decoded * S ((S (pa_i_hjt_j_four_factor_repeat)) * pa_c_hjt_j_four_factor) + (4)))) /\ (exists pa_u_hjt_j_four_factor_product pa_v_hjt_j_four_factor_product. ((((exists pa_h_hjt_j_four_factor_product_start. pa_h_hjt_j_four_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_start. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_start * S ((S (0)) * pa_v_hjt_j_four_factor_product) + (1))) /\ ((((exists pa_h_hjt_j_four_factor_product_terminal. pa_h_hjt_j_four_factor_product_terminal + S (jf) = S ((S (6)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_terminal. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_terminal * S ((S (6)) * pa_v_hjt_j_four_factor_product) + (jf))) /\ forall pa_i_hjt_j_four_factor_product. (exists pa_lt_hjt_j_four_factor_product_bound. pa_lt_hjt_j_four_factor_product_bound + S pa_i_hjt_j_four_factor_product = 6) -> exists pa_p_hjt_j_four_factor_product pa_r_hjt_j_four_factor_product pa_s_hjt_j_four_factor_product. ((((exists pa_h_hjt_j_four_factor_product_factor. pa_h_hjt_j_four_factor_product_factor + S (pa_p_hjt_j_four_factor_product) = S ((S (pa_i_hjt_j_four_factor_product)) * pa_c_hjt_j_four_factor)) /\ exists pa_q_hjt_j_four_factor_product_factor. pa_b_hjt_j_four_factor = pa_q_hjt_j_four_factor_product_factor * S ((S (pa_i_hjt_j_four_factor_product)) * pa_c_hjt_j_four_factor) + (pa_p_hjt_j_four_factor_product))) /\ ((((exists pa_h_hjt_j_four_factor_product_partial. pa_h_hjt_j_four_factor_product_partial + S (pa_r_hjt_j_four_factor_product) = S ((S (pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_partial. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_partial * S ((S (pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product) + (pa_r_hjt_j_four_factor_product))) /\ ((((exists pa_h_hjt_j_four_factor_product_successor. pa_h_hjt_j_four_factor_product_successor + S (pa_s_hjt_j_four_factor_product) = S ((S (S pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_successor. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_successor * S ((S (S pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product) + (pa_s_hjt_j_four_factor_product))) /\ pa_s_hjt_j_four_factor_product = pa_r_hjt_j_four_factor_product * pa_p_hjt_j_four_factor_product))))))))
  36. 0036specialize htotal 4
  37. 0037specialize htotal 6
  38. 0038exact htotal
  39. 0039cases hfour
  40. 0040have hseeds : (exists pa_b_hjt_j_seed_two pa_c_hjt_j_seed_two. ((forall pa_i_hjt_j_seed_two_repeat. (exists pa_lt_hjt_j_seed_two_repeat_bound. pa_lt_hjt_j_seed_two_repeat_bound + S pa_i_hjt_j_seed_two_repeat = 2) -> (((exists pa_h_hjt_j_seed_two_repeat_decoded. pa_h_hjt_j_seed_two_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_seed_two_repeat)) * pa_c_hjt_j_seed_two)) /\ exists pa_q_hjt_j_seed_two_repeat_decoded. pa_b_hjt_j_seed_two = pa_q_hjt_j_seed_two_repeat_decoded * S ((S (pa_i_hjt_j_seed_two_repeat)) * pa_c_hjt_j_seed_two) + (2)))) /\ (exists pa_u_hjt_j_seed_two_product pa_v_hjt_j_seed_two_product. ((((exists pa_h_hjt_j_seed_two_product_start. pa_h_hjt_j_seed_two_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_start. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_start * S ((S (0)) * pa_v_hjt_j_seed_two_product) + (1))) /\ ((((exists pa_h_hjt_j_seed_two_product_terminal. pa_h_hjt_j_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_terminal. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_terminal * S ((S (2)) * pa_v_hjt_j_seed_two_product) + (4))) /\ forall pa_i_hjt_j_seed_two_product. (exists pa_lt_hjt_j_seed_two_product_bound. pa_lt_hjt_j_seed_two_product_bound + S pa_i_hjt_j_seed_two_product = 2) -> exists pa_p_hjt_j_seed_two_product pa_r_hjt_j_seed_two_product pa_s_hjt_j_seed_two_product. ((((exists pa_h_hjt_j_seed_two_product_factor. pa_h_hjt_j_seed_two_product_factor + S (pa_p_hjt_j_seed_two_product) = S ((S (pa_i_hjt_j_seed_two_product)) * pa_c_hjt_j_seed_two)) /\ exists pa_q_hjt_j_seed_two_product_factor. pa_b_hjt_j_seed_two = pa_q_hjt_j_seed_two_product_factor * S ((S (pa_i_hjt_j_seed_two_product)) * pa_c_hjt_j_seed_two) + (pa_p_hjt_j_seed_two_product))) /\ ((((exists pa_h_hjt_j_seed_two_product_partial. pa_h_hjt_j_seed_two_product_partial + S (pa_r_hjt_j_seed_two_product) = S ((S (pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_partial. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_partial * S ((S (pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product) + (pa_r_hjt_j_seed_two_product))) /\ ((((exists pa_h_hjt_j_seed_two_product_successor. pa_h_hjt_j_seed_two_product_successor + S (pa_s_hjt_j_seed_two_product) = S ((S (S pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_successor. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_successor * S ((S (S pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product) + (pa_s_hjt_j_seed_two_product))) /\ pa_s_hjt_j_seed_two_product = pa_r_hjt_j_seed_two_product * pa_p_hjt_j_seed_two_product)))))))) /\ (exists pa_b_hjt_j_seed_seven pa_c_hjt_j_seed_seven. ((forall pa_i_hjt_j_seed_seven_repeat. (exists pa_lt_hjt_j_seed_seven_repeat_bound. pa_lt_hjt_j_seed_seven_repeat_bound + S pa_i_hjt_j_seed_seven_repeat = 7) -> (((exists pa_h_hjt_j_seed_seven_repeat_decoded. pa_h_hjt_j_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_seed_seven_repeat)) * pa_c_hjt_j_seed_seven)) /\ exists pa_q_hjt_j_seed_seven_repeat_decoded. pa_b_hjt_j_seed_seven = pa_q_hjt_j_seed_seven_repeat_decoded * S ((S (pa_i_hjt_j_seed_seven_repeat)) * pa_c_hjt_j_seed_seven) + (2)))) /\ (exists pa_u_hjt_j_seed_seven_product pa_v_hjt_j_seed_seven_product. ((((exists pa_h_hjt_j_seed_seven_product_start. pa_h_hjt_j_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_start. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_start * S ((S (0)) * pa_v_hjt_j_seed_seven_product) + (1))) /\ ((((exists pa_h_hjt_j_seed_seven_product_terminal. pa_h_hjt_j_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_terminal. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_terminal * S ((S (7)) * pa_v_hjt_j_seed_seven_product) + (128))) /\ forall pa_i_hjt_j_seed_seven_product. (exists pa_lt_hjt_j_seed_seven_product_bound. pa_lt_hjt_j_seed_seven_product_bound + S pa_i_hjt_j_seed_seven_product = 7) -> exists pa_p_hjt_j_seed_seven_product pa_r_hjt_j_seed_seven_product pa_s_hjt_j_seed_seven_product. ((((exists pa_h_hjt_j_seed_seven_product_factor. pa_h_hjt_j_seed_seven_product_factor + S (pa_p_hjt_j_seed_seven_product) = S ((S (pa_i_hjt_j_seed_seven_product)) * pa_c_hjt_j_seed_seven)) /\ exists pa_q_hjt_j_seed_seven_product_factor. pa_b_hjt_j_seed_seven = pa_q_hjt_j_seed_seven_product_factor * S ((S (pa_i_hjt_j_seed_seven_product)) * pa_c_hjt_j_seed_seven) + (pa_p_hjt_j_seed_seven_product))) /\ ((((exists pa_h_hjt_j_seed_seven_product_partial. pa_h_hjt_j_seed_seven_product_partial + S (pa_r_hjt_j_seed_seven_product) = S ((S (pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_partial. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_partial * S ((S (pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product) + (pa_r_hjt_j_seed_seven_product))) /\ ((((exists pa_h_hjt_j_seed_seven_product_successor. pa_h_hjt_j_seed_seven_product_successor + S (pa_s_hjt_j_seed_seven_product) = S ((S (S pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_successor. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_successor * S ((S (S pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product) + (pa_s_hjt_j_seed_seven_product))) /\ pa_s_hjt_j_seed_seven_product = pa_r_hjt_j_seed_seven_product * pa_p_hjt_j_seed_seven_product))))))))
  41. 0041apply pow_two_seed_bundle_from_total
  42. 0042exact htotal
  43. 0043cases hseeds
  44. 0044have htwo_four : x1 = x2
  45. 0045specialize pow_mul_exp_from_total 2
  46. 0046specialize pow_mul_exp_from_total 2
  47. 0047specialize pow_mul_exp_from_total 6
  48. 0048specialize pow_mul_exp_from_total 12
  49. 0049specialize pow_mul_exp_from_total 4
  50. 0050specialize pow_mul_exp_from_total x2
  51. 0051specialize pow_mul_exp_from_total x1
  52. 0052symm
  53. 0053apply pow_mul_exp_from_total
  54. 0054exact htotal
  55. 0055norm_num
  56. 0056exact hseeds_left
  57. 0057exact hfour_witness
  58. 0058exact htwo_witness
  59. 0059have hdouble_factor : x = x1 * j
  60. 0060specialize pow_mul_base 2
  61. 0061specialize pow_mul_base (s + 7)
  62. 0062specialize pow_mul_base 12
  63. 0063specialize pow_mul_base x1
  64. 0064specialize pow_mul_base j
  65. 0065specialize pow_mul_base x
  66. 0066apply pow_mul_base
  67. 0067exact htwo_witness
  68. 0068exact hj
  69. 0069exact hdouble_witness
  70. 0070have hsum : s + 11 = 6 + (s + 5)
  71. 0071trans s + (6 + 5)
  72. 0072congr
  73. 0073refl
  74. 0074norm_num
  75. 0075trans (s + 6) + 5
  76. 0076symm
  77. 0077apply add_assoc
  78. 0078trans (6 + s) + 5
  79. 0079congr
  80. 0080apply add_comm
  81. 0081refl
  82. 0082apply add_assoc
  83. 0083have hbound_factor : gn = x2 * g
  84. 0084specialize pow_add 4
  85. 0085specialize pow_add 6
  86. 0086specialize pow_add (s + 5)
  87. 0087specialize pow_add (s + 11)
  88. 0088specialize pow_add x2
  89. 0089specialize pow_add g
  90. 0090specialize pow_add gn
  91. 0091apply pow_add
  92. 0092exact hsum
  93. 0093exact hfour_witness
  94. 0094exact hg
  95. 0095exact hgn
  96. 0096have hproducts : exists bqb_le_gap_hjt_j_products. bqb_le_gap_hjt_j_products + (x1 * j) = (x2 * g)
  97. 0097rewrite htwo_four
  98. 0098specialize mul_le_mul x2
  99. 0099specialize mul_le_mul x2
  100. 0100specialize mul_le_mul j
  101. 0101specialize mul_le_mul g
  102. 0102apply mul_le_mul
  103. 0103specialize le_refl x2
  104. 0104exact le_refl
  105. 0105exact hjg
  106. 0106specialize le_trans jn
  107. 0107specialize le_trans x
  108. 0108specialize le_trans gn
  109. 0109apply le_trans
  110. 0110exact hjdouble
  111. 0111rewrite hdouble_factor
  112. 0112rewrite hbound_factor
  113. 0113exact hproducts