BT00WG

pow_six_four_le_pow_four_six_from_total

Alpha body-checked · checked-use disabled

The capacity-safe residual block 6^4 <= 4^6.

Exact expanded PA statement

forall x y. (forall bpt_a_hj32_residual_four bpt_e_hj32_residual_four. exists bpt_x_hj32_residual_four. (exists ff_b_bpt_value_hj32_residual_four ff_c_bpt_value_hj32_residual_four. ((forall ff_i_bpt_value_hj32_residual_four_repeat. (exists ff_lt_bpt_value_hj32_residual_four_repeat_bound. ff_lt_bpt_value_hj32_residual_four_repeat_bound + S ff_i_bpt_value_hj32_residual_four_repeat = bpt_e_hj32_residual_four) -> (((exists ff_h_bpt_value_hj32_residual_four_repeat_decoded. ff_h_bpt_value_hj32_residual_four_repeat_decoded + S (bpt_a_hj32_residual_four) = S ((S (ff_i_bpt_value_hj32_residual_four_repeat)) * ff_c_bpt_value_hj32_residual_four)) /\ exists ff_q_bpt_value_hj32_residual_four_repeat_decoded. ff_b_bpt_value_hj32_residual_four = ff_q_bpt_value_hj32_residual_four_repeat_decoded * S ((S (ff_i_bpt_value_hj32_residual_four_repeat)) * ff_c_bpt_value_hj32_residual_four) + (bpt_a_hj32_residual_four)))) /\ (exists ff_u_bpt_value_hj32_residual_four_product ff_v_bpt_value_hj32_residual_four_product. ((((exists ff_h_bpt_value_hj32_residual_four_product_start. ff_h_bpt_value_hj32_residual_four_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_start. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_start * S ((S (0)) * ff_v_bpt_value_hj32_residual_four_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_terminal. ff_h_bpt_value_hj32_residual_four_product_terminal + S (bpt_x_hj32_residual_four) = S ((S (bpt_e_hj32_residual_four)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_terminal. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_terminal * S ((S (bpt_e_hj32_residual_four)) * ff_v_bpt_value_hj32_residual_four_product) + (bpt_x_hj32_residual_four))) /\ forall ff_i_bpt_value_hj32_residual_four_product. (exists ff_lt_bpt_value_hj32_residual_four_product_bound. ff_lt_bpt_value_hj32_residual_four_product_bound + S ff_i_bpt_value_hj32_residual_four_product = bpt_e_hj32_residual_four) -> exists ff_p_bpt_value_hj32_residual_four_product ff_r_bpt_value_hj32_residual_four_product ff_s_bpt_value_hj32_residual_four_product. ((((exists ff_h_bpt_value_hj32_residual_four_product_factor. ff_h_bpt_value_hj32_residual_four_product_factor + S (ff_p_bpt_value_hj32_residual_four_product) = S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_c_bpt_value_hj32_residual_four)) /\ exists ff_q_bpt_value_hj32_residual_four_product_factor. ff_b_bpt_value_hj32_residual_four = ff_q_bpt_value_hj32_residual_four_product_factor * S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_c_bpt_value_hj32_residual_four) + (ff_p_bpt_value_hj32_residual_four_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_partial. ff_h_bpt_value_hj32_residual_four_product_partial + S (ff_r_bpt_value_hj32_residual_four_product) = S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_partial. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_partial * S ((S (ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product) + (ff_r_bpt_value_hj32_residual_four_product))) /\ ((((exists ff_h_bpt_value_hj32_residual_four_product_successor. ff_h_bpt_value_hj32_residual_four_product_successor + S (ff_s_bpt_value_hj32_residual_four_product) = S ((S (S ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product)) /\ exists ff_q_bpt_value_hj32_residual_four_product_successor. ff_u_bpt_value_hj32_residual_four_product = ff_q_bpt_value_hj32_residual_four_product_successor * S ((S (S ff_i_bpt_value_hj32_residual_four_product)) * ff_v_bpt_value_hj32_residual_four_product) + (ff_s_bpt_value_hj32_residual_four_product))) /\ ff_s_bpt_value_hj32_residual_four_product = ff_r_bpt_value_hj32_residual_four_product * ff_p_bpt_value_hj32_residual_four_product))))))))) -> (exists pa_b_hj32_residual_four_left pa_c_hj32_residual_four_left. ((forall pa_i_hj32_residual_four_left_repeat. (exists pa_lt_hj32_residual_four_left_repeat_bound. pa_lt_hj32_residual_four_left_repeat_bound + S pa_i_hj32_residual_four_left_repeat = 4) -> (((exists pa_h_hj32_residual_four_left_repeat_decoded. pa_h_hj32_residual_four_left_repeat_decoded + S (6) = S ((S (pa_i_hj32_residual_four_left_repeat)) * pa_c_hj32_residual_four_left)) /\ exists pa_q_hj32_residual_four_left_repeat_decoded. pa_b_hj32_residual_four_left = pa_q_hj32_residual_four_left_repeat_decoded * S ((S (pa_i_hj32_residual_four_left_repeat)) * pa_c_hj32_residual_four_left) + (6)))) /\ (exists pa_u_hj32_residual_four_left_product pa_v_hj32_residual_four_left_product. ((((exists pa_h_hj32_residual_four_left_product_start. pa_h_hj32_residual_four_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_start. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_start * S ((S (0)) * pa_v_hj32_residual_four_left_product) + (1))) /\ ((((exists pa_h_hj32_residual_four_left_product_terminal. pa_h_hj32_residual_four_left_product_terminal + S (x) = S ((S (4)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_terminal. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_terminal * S ((S (4)) * pa_v_hj32_residual_four_left_product) + (x))) /\ forall pa_i_hj32_residual_four_left_product. (exists pa_lt_hj32_residual_four_left_product_bound. pa_lt_hj32_residual_four_left_product_bound + S pa_i_hj32_residual_four_left_product = 4) -> exists pa_p_hj32_residual_four_left_product pa_r_hj32_residual_four_left_product pa_s_hj32_residual_four_left_product. ((((exists pa_h_hj32_residual_four_left_product_factor. pa_h_hj32_residual_four_left_product_factor + S (pa_p_hj32_residual_four_left_product) = S ((S (pa_i_hj32_residual_four_left_product)) * pa_c_hj32_residual_four_left)) /\ exists pa_q_hj32_residual_four_left_product_factor. pa_b_hj32_residual_four_left = pa_q_hj32_residual_four_left_product_factor * S ((S (pa_i_hj32_residual_four_left_product)) * pa_c_hj32_residual_four_left) + (pa_p_hj32_residual_four_left_product))) /\ ((((exists pa_h_hj32_residual_four_left_product_partial. pa_h_hj32_residual_four_left_product_partial + S (pa_r_hj32_residual_four_left_product) = S ((S (pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_partial. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_partial * S ((S (pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product) + (pa_r_hj32_residual_four_left_product))) /\ ((((exists pa_h_hj32_residual_four_left_product_successor. pa_h_hj32_residual_four_left_product_successor + S (pa_s_hj32_residual_four_left_product) = S ((S (S pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product)) /\ exists pa_q_hj32_residual_four_left_product_successor. pa_u_hj32_residual_four_left_product = pa_q_hj32_residual_four_left_product_successor * S ((S (S pa_i_hj32_residual_four_left_product)) * pa_v_hj32_residual_four_left_product) + (pa_s_hj32_residual_four_left_product))) /\ pa_s_hj32_residual_four_left_product = pa_r_hj32_residual_four_left_product * pa_p_hj32_residual_four_left_product)))))))) -> (exists pa_b_hj32_residual_four_right pa_c_hj32_residual_four_right. ((forall pa_i_hj32_residual_four_right_repeat. (exists pa_lt_hj32_residual_four_right_repeat_bound. pa_lt_hj32_residual_four_right_repeat_bound + S pa_i_hj32_residual_four_right_repeat = 6) -> (((exists pa_h_hj32_residual_four_right_repeat_decoded. pa_h_hj32_residual_four_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_residual_four_right_repeat)) * pa_c_hj32_residual_four_right)) /\ exists pa_q_hj32_residual_four_right_repeat_decoded. pa_b_hj32_residual_four_right = pa_q_hj32_residual_four_right_repeat_decoded * S ((S (pa_i_hj32_residual_four_right_repeat)) * pa_c_hj32_residual_four_right) + (4)))) /\ (exists pa_u_hj32_residual_four_right_product pa_v_hj32_residual_four_right_product. ((((exists pa_h_hj32_residual_four_right_product_start. pa_h_hj32_residual_four_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_start. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_start * S ((S (0)) * pa_v_hj32_residual_four_right_product) + (1))) /\ ((((exists pa_h_hj32_residual_four_right_product_terminal. pa_h_hj32_residual_four_right_product_terminal + S (y) = S ((S (6)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_terminal. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_terminal * S ((S (6)) * pa_v_hj32_residual_four_right_product) + (y))) /\ forall pa_i_hj32_residual_four_right_product. (exists pa_lt_hj32_residual_four_right_product_bound. pa_lt_hj32_residual_four_right_product_bound + S pa_i_hj32_residual_four_right_product = 6) -> exists pa_p_hj32_residual_four_right_product pa_r_hj32_residual_four_right_product pa_s_hj32_residual_four_right_product. ((((exists pa_h_hj32_residual_four_right_product_factor. pa_h_hj32_residual_four_right_product_factor + S (pa_p_hj32_residual_four_right_product) = S ((S (pa_i_hj32_residual_four_right_product)) * pa_c_hj32_residual_four_right)) /\ exists pa_q_hj32_residual_four_right_product_factor. pa_b_hj32_residual_four_right = pa_q_hj32_residual_four_right_product_factor * S ((S (pa_i_hj32_residual_four_right_product)) * pa_c_hj32_residual_four_right) + (pa_p_hj32_residual_four_right_product))) /\ ((((exists pa_h_hj32_residual_four_right_product_partial. pa_h_hj32_residual_four_right_product_partial + S (pa_r_hj32_residual_four_right_product) = S ((S (pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_partial. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_partial * S ((S (pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product) + (pa_r_hj32_residual_four_right_product))) /\ ((((exists pa_h_hj32_residual_four_right_product_successor. pa_h_hj32_residual_four_right_product_successor + S (pa_s_hj32_residual_four_right_product) = S ((S (S pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product)) /\ exists pa_q_hj32_residual_four_right_product_successor. pa_u_hj32_residual_four_right_product = pa_q_hj32_residual_four_right_product_successor * S ((S (S pa_i_hj32_residual_four_right_product)) * pa_v_hj32_residual_four_right_product) + (pa_s_hj32_residual_four_right_product))) /\ pa_s_hj32_residual_four_right_product = pa_r_hj32_residual_four_right_product * pa_p_hj32_residual_four_right_product)))))))) -> (exists bqb_le_gap_hj32_residual_four_result. bqb_le_gap_hj32_residual_four_result + (x) = (y))

Structural proof guide

The capacity-safe residual block 6^4 <= 4^6.

Direct prerequisites: pow_two_seed_bundle_from_total, pow_mul_exp_from_total, pow_mul_base, pow_add, pow_base_monotone, mul_le_mul, le_refl. The authored body proceeds by case analysis (5), intermediate claims (14), equality transport (5), closed numeral normalization (4).

Proof neighborhood

Direct dependencies

BT00SO pow_two_seed_bundle_from_total BT00SM pow_mul_exp_from_total BT00QV pow_mul_base BT009X pow_add BT00PY pow_base_monotone BT00PV mul_le_mul BT000E le_refl

Direct dependents

BT00WS bertrand_h_root_35_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 x
  2. 0002intro y
  3. 0003intro htotal
  4. 0004intro hx
  5. 0005intro hy
  6. 0006have rf_seeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product))))))))
  7. 0007apply pow_two_seed_bundle_from_total
  8. 0008exact htotal
  9. 0009cases rf_seeds
  10. 0010have rf_p2_four : exists hj32_local_value_rf_p2_four. (exists pa_b_hj32_local_total_rf_p2_four pa_c_hj32_local_total_rf_p2_four. ((forall pa_i_hj32_local_total_rf_p2_four_repeat. (exists pa_lt_hj32_local_total_rf_p2_four_repeat_bound. pa_lt_hj32_local_total_rf_p2_four_repeat_bound + S pa_i_hj32_local_total_rf_p2_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p2_four_repeat_decoded. pa_h_hj32_local_total_rf_p2_four_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_rf_p2_four_repeat)) * pa_c_hj32_local_total_rf_p2_four)) /\ exists pa_q_hj32_local_total_rf_p2_four_repeat_decoded. pa_b_hj32_local_total_rf_p2_four = pa_q_hj32_local_total_rf_p2_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p2_four_repeat)) * pa_c_hj32_local_total_rf_p2_four) + (2)))) /\ (exists pa_u_hj32_local_total_rf_p2_four_product pa_v_hj32_local_total_rf_p2_four_product. ((((exists pa_h_hj32_local_total_rf_p2_four_product_start. pa_h_hj32_local_total_rf_p2_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_start. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p2_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_terminal. pa_h_hj32_local_total_rf_p2_four_product_terminal + S (hj32_local_value_rf_p2_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_terminal. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p2_four_product) + (hj32_local_value_rf_p2_four))) /\ forall pa_i_hj32_local_total_rf_p2_four_product. (exists pa_lt_hj32_local_total_rf_p2_four_product_bound. pa_lt_hj32_local_total_rf_p2_four_product_bound + S pa_i_hj32_local_total_rf_p2_four_product = 4) -> exists pa_p_hj32_local_total_rf_p2_four_product pa_r_hj32_local_total_rf_p2_four_product pa_s_hj32_local_total_rf_p2_four_product. ((((exists pa_h_hj32_local_total_rf_p2_four_product_factor. pa_h_hj32_local_total_rf_p2_four_product_factor + S (pa_p_hj32_local_total_rf_p2_four_product) = S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_c_hj32_local_total_rf_p2_four)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_factor. pa_b_hj32_local_total_rf_p2_four = pa_q_hj32_local_total_rf_p2_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_c_hj32_local_total_rf_p2_four) + (pa_p_hj32_local_total_rf_p2_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_partial. pa_h_hj32_local_total_rf_p2_four_product_partial + S (pa_r_hj32_local_total_rf_p2_four_product) = S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_partial. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product) + (pa_r_hj32_local_total_rf_p2_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p2_four_product_successor. pa_h_hj32_local_total_rf_p2_four_product_successor + S (pa_s_hj32_local_total_rf_p2_four_product) = S ((S (S pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product)) /\ exists pa_q_hj32_local_total_rf_p2_four_product_successor. pa_u_hj32_local_total_rf_p2_four_product = pa_q_hj32_local_total_rf_p2_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p2_four_product)) * pa_v_hj32_local_total_rf_p2_four_product) + (pa_s_hj32_local_total_rf_p2_four_product))) /\ pa_s_hj32_local_total_rf_p2_four_product = pa_r_hj32_local_total_rf_p2_four_product * pa_p_hj32_local_total_rf_p2_four_product))))))))
  11. 0011specialize htotal 2
  12. 0012specialize htotal 4
  13. 0013exact htotal
  14. 0014cases rf_p2_four
  15. 0015have rf_p4_two : exists hj32_local_value_rf_p4_two. (exists pa_b_hj32_local_total_rf_p4_two pa_c_hj32_local_total_rf_p4_two. ((forall pa_i_hj32_local_total_rf_p4_two_repeat. (exists pa_lt_hj32_local_total_rf_p4_two_repeat_bound. pa_lt_hj32_local_total_rf_p4_two_repeat_bound + S pa_i_hj32_local_total_rf_p4_two_repeat = 2) -> (((exists pa_h_hj32_local_total_rf_p4_two_repeat_decoded. pa_h_hj32_local_total_rf_p4_two_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rf_p4_two_repeat)) * pa_c_hj32_local_total_rf_p4_two)) /\ exists pa_q_hj32_local_total_rf_p4_two_repeat_decoded. pa_b_hj32_local_total_rf_p4_two = pa_q_hj32_local_total_rf_p4_two_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p4_two_repeat)) * pa_c_hj32_local_total_rf_p4_two) + (4)))) /\ (exists pa_u_hj32_local_total_rf_p4_two_product pa_v_hj32_local_total_rf_p4_two_product. ((((exists pa_h_hj32_local_total_rf_p4_two_product_start. pa_h_hj32_local_total_rf_p4_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_start. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p4_two_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_terminal. pa_h_hj32_local_total_rf_p4_two_product_terminal + S (hj32_local_value_rf_p4_two) = S ((S (2)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_terminal. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_terminal * S ((S (2)) * pa_v_hj32_local_total_rf_p4_two_product) + (hj32_local_value_rf_p4_two))) /\ forall pa_i_hj32_local_total_rf_p4_two_product. (exists pa_lt_hj32_local_total_rf_p4_two_product_bound. pa_lt_hj32_local_total_rf_p4_two_product_bound + S pa_i_hj32_local_total_rf_p4_two_product = 2) -> exists pa_p_hj32_local_total_rf_p4_two_product pa_r_hj32_local_total_rf_p4_two_product pa_s_hj32_local_total_rf_p4_two_product. ((((exists pa_h_hj32_local_total_rf_p4_two_product_factor. pa_h_hj32_local_total_rf_p4_two_product_factor + S (pa_p_hj32_local_total_rf_p4_two_product) = S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_c_hj32_local_total_rf_p4_two)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_factor. pa_b_hj32_local_total_rf_p4_two = pa_q_hj32_local_total_rf_p4_two_product_factor * S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_c_hj32_local_total_rf_p4_two) + (pa_p_hj32_local_total_rf_p4_two_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_partial. pa_h_hj32_local_total_rf_p4_two_product_partial + S (pa_r_hj32_local_total_rf_p4_two_product) = S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_partial. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_partial * S ((S (pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product) + (pa_r_hj32_local_total_rf_p4_two_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_two_product_successor. pa_h_hj32_local_total_rf_p4_two_product_successor + S (pa_s_hj32_local_total_rf_p4_two_product) = S ((S (S pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product)) /\ exists pa_q_hj32_local_total_rf_p4_two_product_successor. pa_u_hj32_local_total_rf_p4_two_product = pa_q_hj32_local_total_rf_p4_two_product_successor * S ((S (S pa_i_hj32_local_total_rf_p4_two_product)) * pa_v_hj32_local_total_rf_p4_two_product) + (pa_s_hj32_local_total_rf_p4_two_product))) /\ pa_s_hj32_local_total_rf_p4_two_product = pa_r_hj32_local_total_rf_p4_two_product * pa_p_hj32_local_total_rf_p4_two_product))))))))
  16. 0016specialize htotal 4
  17. 0017specialize htotal 2
  18. 0018exact htotal
  19. 0019cases rf_p4_two
  20. 0020have rf_two_bridge : x2 = x1
  21. 0021specialize pow_mul_exp_from_total 2
  22. 0022specialize pow_mul_exp_from_total 2
  23. 0023specialize pow_mul_exp_from_total 2
  24. 0024specialize pow_mul_exp_from_total 4
  25. 0025specialize pow_mul_exp_from_total 4
  26. 0026specialize pow_mul_exp_from_total x2
  27. 0027specialize pow_mul_exp_from_total x1
  28. 0028apply pow_mul_exp_from_total
  29. 0029exact htotal
  30. 0030norm_num
  31. 0031exact rf_seeds_left
  32. 0032exact rf_p4_two_witness
  33. 0033exact rf_p2_four_witness
  34. 0034have rf_two_bound : exists bqb_le_gap_hj32_rf_two_bound. bqb_le_gap_hj32_rf_two_bound + (x1) = (x2)
  35. 0035rewrite rf_two_bridge
  36. 0036specialize le_refl x1
  37. 0037exact le_refl
  38. 0038have rf_p3_four : exists hj32_local_value_rf_p3_four. (exists pa_b_hj32_local_total_rf_p3_four pa_c_hj32_local_total_rf_p3_four. ((forall pa_i_hj32_local_total_rf_p3_four_repeat. (exists pa_lt_hj32_local_total_rf_p3_four_repeat_bound. pa_lt_hj32_local_total_rf_p3_four_repeat_bound + S pa_i_hj32_local_total_rf_p3_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p3_four_repeat_decoded. pa_h_hj32_local_total_rf_p3_four_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_rf_p3_four_repeat)) * pa_c_hj32_local_total_rf_p3_four)) /\ exists pa_q_hj32_local_total_rf_p3_four_repeat_decoded. pa_b_hj32_local_total_rf_p3_four = pa_q_hj32_local_total_rf_p3_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p3_four_repeat)) * pa_c_hj32_local_total_rf_p3_four) + (3)))) /\ (exists pa_u_hj32_local_total_rf_p3_four_product pa_v_hj32_local_total_rf_p3_four_product. ((((exists pa_h_hj32_local_total_rf_p3_four_product_start. pa_h_hj32_local_total_rf_p3_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_start. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p3_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_terminal. pa_h_hj32_local_total_rf_p3_four_product_terminal + S (hj32_local_value_rf_p3_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_terminal. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p3_four_product) + (hj32_local_value_rf_p3_four))) /\ forall pa_i_hj32_local_total_rf_p3_four_product. (exists pa_lt_hj32_local_total_rf_p3_four_product_bound. pa_lt_hj32_local_total_rf_p3_four_product_bound + S pa_i_hj32_local_total_rf_p3_four_product = 4) -> exists pa_p_hj32_local_total_rf_p3_four_product pa_r_hj32_local_total_rf_p3_four_product pa_s_hj32_local_total_rf_p3_four_product. ((((exists pa_h_hj32_local_total_rf_p3_four_product_factor. pa_h_hj32_local_total_rf_p3_four_product_factor + S (pa_p_hj32_local_total_rf_p3_four_product) = S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_c_hj32_local_total_rf_p3_four)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_factor. pa_b_hj32_local_total_rf_p3_four = pa_q_hj32_local_total_rf_p3_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_c_hj32_local_total_rf_p3_four) + (pa_p_hj32_local_total_rf_p3_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_partial. pa_h_hj32_local_total_rf_p3_four_product_partial + S (pa_r_hj32_local_total_rf_p3_four_product) = S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_partial. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product) + (pa_r_hj32_local_total_rf_p3_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p3_four_product_successor. pa_h_hj32_local_total_rf_p3_four_product_successor + S (pa_s_hj32_local_total_rf_p3_four_product) = S ((S (S pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product)) /\ exists pa_q_hj32_local_total_rf_p3_four_product_successor. pa_u_hj32_local_total_rf_p3_four_product = pa_q_hj32_local_total_rf_p3_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p3_four_product)) * pa_v_hj32_local_total_rf_p3_four_product) + (pa_s_hj32_local_total_rf_p3_four_product))) /\ pa_s_hj32_local_total_rf_p3_four_product = pa_r_hj32_local_total_rf_p3_four_product * pa_p_hj32_local_total_rf_p3_four_product))))))))
  39. 0039specialize htotal 3
  40. 0040specialize htotal 4
  41. 0041exact htotal
  42. 0042cases rf_p3_four
  43. 0043have rf_p4_four : exists hj32_local_value_rf_p4_four. (exists pa_b_hj32_local_total_rf_p4_four pa_c_hj32_local_total_rf_p4_four. ((forall pa_i_hj32_local_total_rf_p4_four_repeat. (exists pa_lt_hj32_local_total_rf_p4_four_repeat_bound. pa_lt_hj32_local_total_rf_p4_four_repeat_bound + S pa_i_hj32_local_total_rf_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_rf_p4_four_repeat_decoded. pa_h_hj32_local_total_rf_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_rf_p4_four_repeat)) * pa_c_hj32_local_total_rf_p4_four)) /\ exists pa_q_hj32_local_total_rf_p4_four_repeat_decoded. pa_b_hj32_local_total_rf_p4_four = pa_q_hj32_local_total_rf_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_rf_p4_four_repeat)) * pa_c_hj32_local_total_rf_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_rf_p4_four_product pa_v_hj32_local_total_rf_p4_four_product. ((((exists pa_h_hj32_local_total_rf_p4_four_product_start. pa_h_hj32_local_total_rf_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_start. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_rf_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_terminal. pa_h_hj32_local_total_rf_p4_four_product_terminal + S (hj32_local_value_rf_p4_four) = S ((S (4)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_terminal. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_rf_p4_four_product) + (hj32_local_value_rf_p4_four))) /\ forall pa_i_hj32_local_total_rf_p4_four_product. (exists pa_lt_hj32_local_total_rf_p4_four_product_bound. pa_lt_hj32_local_total_rf_p4_four_product_bound + S pa_i_hj32_local_total_rf_p4_four_product = 4) -> exists pa_p_hj32_local_total_rf_p4_four_product pa_r_hj32_local_total_rf_p4_four_product pa_s_hj32_local_total_rf_p4_four_product. ((((exists pa_h_hj32_local_total_rf_p4_four_product_factor. pa_h_hj32_local_total_rf_p4_four_product_factor + S (pa_p_hj32_local_total_rf_p4_four_product) = S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_c_hj32_local_total_rf_p4_four)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_factor. pa_b_hj32_local_total_rf_p4_four = pa_q_hj32_local_total_rf_p4_four_product_factor * S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_c_hj32_local_total_rf_p4_four) + (pa_p_hj32_local_total_rf_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_partial. pa_h_hj32_local_total_rf_p4_four_product_partial + S (pa_r_hj32_local_total_rf_p4_four_product) = S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_partial. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_partial * S ((S (pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product) + (pa_r_hj32_local_total_rf_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_rf_p4_four_product_successor. pa_h_hj32_local_total_rf_p4_four_product_successor + S (pa_s_hj32_local_total_rf_p4_four_product) = S ((S (S pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product)) /\ exists pa_q_hj32_local_total_rf_p4_four_product_successor. pa_u_hj32_local_total_rf_p4_four_product = pa_q_hj32_local_total_rf_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_rf_p4_four_product)) * pa_v_hj32_local_total_rf_p4_four_product) + (pa_s_hj32_local_total_rf_p4_four_product))) /\ pa_s_hj32_local_total_rf_p4_four_product = pa_r_hj32_local_total_rf_p4_four_product * pa_p_hj32_local_total_rf_p4_four_product))))))))
  44. 0044specialize htotal 4
  45. 0045specialize htotal 4
  46. 0046exact htotal
  47. 0047cases rf_p4_four
  48. 0048have rf_base : exists bqb_le_gap_hj32_rf_base. bqb_le_gap_hj32_rf_base + (3) = (4)
  49. 0049exists 1
  50. 0050norm_num
  51. 0051have rf_three_bound : exists bqb_le_gap_hj32_local_base_bound_rf_three_bound. bqb_le_gap_hj32_local_base_bound_rf_three_bound + (x3) = (x4)
  52. 0052specialize pow_base_monotone 3
  53. 0053specialize pow_base_monotone 4
  54. 0054specialize pow_base_monotone 4
  55. 0055specialize pow_base_monotone x3
  56. 0056specialize pow_base_monotone x4
  57. 0057apply pow_base_monotone
  58. 0058exact rf_base
  59. 0059exact rf_p3_four_witness
  60. 0060exact rf_p4_four_witness
  61. 0061have rf_six_product_graph : exists pa_b_hj32_local_product_rf_six_product pa_c_hj32_local_product_rf_six_product. ((forall pa_i_hj32_local_product_rf_six_product_repeat. (exists pa_lt_hj32_local_product_rf_six_product_repeat_bound. pa_lt_hj32_local_product_rf_six_product_repeat_bound + S pa_i_hj32_local_product_rf_six_product_repeat = 4) -> (((exists pa_h_hj32_local_product_rf_six_product_repeat_decoded. pa_h_hj32_local_product_rf_six_product_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_local_product_rf_six_product_repeat)) * pa_c_hj32_local_product_rf_six_product)) /\ exists pa_q_hj32_local_product_rf_six_product_repeat_decoded. pa_b_hj32_local_product_rf_six_product = pa_q_hj32_local_product_rf_six_product_repeat_decoded * S ((S (pa_i_hj32_local_product_rf_six_product_repeat)) * pa_c_hj32_local_product_rf_six_product) + (2 * 3)))) /\ (exists pa_u_hj32_local_product_rf_six_product_product pa_v_hj32_local_product_rf_six_product_product. ((((exists pa_h_hj32_local_product_rf_six_product_product_start. pa_h_hj32_local_product_rf_six_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_start. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_start * S ((S (0)) * pa_v_hj32_local_product_rf_six_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_terminal. pa_h_hj32_local_product_rf_six_product_product_terminal + S (x) = S ((S (4)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_terminal. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_terminal * S ((S (4)) * pa_v_hj32_local_product_rf_six_product_product) + (x))) /\ forall pa_i_hj32_local_product_rf_six_product_product. (exists pa_lt_hj32_local_product_rf_six_product_product_bound. pa_lt_hj32_local_product_rf_six_product_product_bound + S pa_i_hj32_local_product_rf_six_product_product = 4) -> exists pa_p_hj32_local_product_rf_six_product_product pa_r_hj32_local_product_rf_six_product_product pa_s_hj32_local_product_rf_six_product_product. ((((exists pa_h_hj32_local_product_rf_six_product_product_factor. pa_h_hj32_local_product_rf_six_product_product_factor + S (pa_p_hj32_local_product_rf_six_product_product) = S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_c_hj32_local_product_rf_six_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_factor. pa_b_hj32_local_product_rf_six_product = pa_q_hj32_local_product_rf_six_product_product_factor * S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_c_hj32_local_product_rf_six_product) + (pa_p_hj32_local_product_rf_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_partial. pa_h_hj32_local_product_rf_six_product_product_partial + S (pa_r_hj32_local_product_rf_six_product_product) = S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_partial. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_partial * S ((S (pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product) + (pa_r_hj32_local_product_rf_six_product_product))) /\ ((((exists pa_h_hj32_local_product_rf_six_product_product_successor. pa_h_hj32_local_product_rf_six_product_product_successor + S (pa_s_hj32_local_product_rf_six_product_product) = S ((S (S pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product)) /\ exists pa_q_hj32_local_product_rf_six_product_product_successor. pa_u_hj32_local_product_rf_six_product_product = pa_q_hj32_local_product_rf_six_product_product_successor * S ((S (S pa_i_hj32_local_product_rf_six_product_product)) * pa_v_hj32_local_product_rf_six_product_product) + (pa_s_hj32_local_product_rf_six_product_product))) /\ pa_s_hj32_local_product_rf_six_product_product = pa_r_hj32_local_product_rf_six_product_product * pa_p_hj32_local_product_rf_six_product_product)))))))
  62. 0062have rf_six_product_base : 2 * 3 = 6
  63. 0063norm_num
  64. 0064rewrite rf_six_product_base
  65. 0065rewrite rf_six_product_base
  66. 0066exact hx
  67. 0067have rf_six_product : x = x1 * x3
  68. 0068specialize pow_mul_base 2
  69. 0069specialize pow_mul_base 3
  70. 0070specialize pow_mul_base 4
  71. 0071specialize pow_mul_base x1
  72. 0072specialize pow_mul_base x3
  73. 0073specialize pow_mul_base x
  74. 0074apply pow_mul_base
  75. 0075exact rf_p2_four_witness
  76. 0076exact rf_p3_four_witness
  77. 0077exact rf_six_product_graph
  78. 0078have rf_six_power : y = x2 * x4
  79. 0079specialize pow_add 4
  80. 0080specialize pow_add 2
  81. 0081specialize pow_add 4
  82. 0082specialize pow_add 6
  83. 0083specialize pow_add x2
  84. 0084specialize pow_add x4
  85. 0085specialize pow_add y
  86. 0086apply pow_add
  87. 0087norm_num
  88. 0088exact rf_p4_two_witness
  89. 0089exact rf_p4_four_witness
  90. 0090exact hy
  91. 0091have rf_result : exists bqb_le_gap_hj32_local_product_bound_rf_result. bqb_le_gap_hj32_local_product_bound_rf_result + (x1 * x3) = (x2 * x4)
  92. 0092specialize mul_le_mul x1
  93. 0093specialize mul_le_mul x2
  94. 0094specialize mul_le_mul x3
  95. 0095specialize mul_le_mul x4
  96. 0096apply mul_le_mul
  97. 0097exact rf_two_bound
  98. 0098exact rf_three_bound
  99. 0099rewrite <- rf_six_product at rf_result
  100. 0100rewrite <- rf_six_power at rf_result
  101. 0101exact rf_result