BT00UY

primorial_prefix_interval_split

Alpha body-checked · checked-use disabled

Split Primorial(a+l) into its prefix and offset interval product.

Exact expanded PA statement

forall a l z. (exists bpr_code_bppis_source bpr_scale_bppis_source. ((forall bpr_index_bppis_source_mask. (exists bpr_gap_bppis_source_mask_bound. bpr_gap_bppis_source_mask_bound + S (bpr_index_bppis_source_mask) = a + l) -> exists bpr_value_bppis_source_mask. ((((exists bpr_height_bppis_source_mask_decoded. bpr_height_bppis_source_mask_decoded + S (bpr_value_bppis_source_mask) = S ((S (bpr_index_bppis_source_mask)) * bpr_scale_bppis_source)) /\ exists bpr_quotient_bppis_source_mask_decoded. bpr_code_bppis_source = bpr_quotient_bppis_source_mask_decoded * S ((S (bpr_index_bppis_source_mask)) * bpr_scale_bppis_source) + (bpr_value_bppis_source_mask))) /\ (((((~(S (bpr_index_bppis_source_mask) = 1) /\ forall bpr_left_bppis_source_mask_choice_prime bpr_right_bppis_source_mask_choice_prime. S (bpr_index_bppis_source_mask) = bpr_left_bppis_source_mask_choice_prime * bpr_right_bppis_source_mask_choice_prime -> bpr_left_bppis_source_mask_choice_prime = 1 \/ bpr_right_bppis_source_mask_choice_prime = 1)) /\ bpr_value_bppis_source_mask = S (bpr_index_bppis_source_mask)) \/ (~((~(S (bpr_index_bppis_source_mask) = 1) /\ forall bpr_left_bppis_source_mask_choice_prime bpr_right_bppis_source_mask_choice_prime. S (bpr_index_bppis_source_mask) = bpr_left_bppis_source_mask_choice_prime * bpr_right_bppis_source_mask_choice_prime -> bpr_left_bppis_source_mask_choice_prime = 1 \/ bpr_right_bppis_source_mask_choice_prime = 1)) /\ bpr_value_bppis_source_mask = 1))))) /\ (exists ff_u_bppis_source_product ff_v_bppis_source_product. ((((exists ff_h_bppis_source_product_start. ff_h_bppis_source_product_start + S (1) = S ((S (0)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_start. ff_u_bppis_source_product = ff_q_bppis_source_product_start * S ((S (0)) * ff_v_bppis_source_product) + (1))) /\ ((((exists ff_h_bppis_source_product_terminal. ff_h_bppis_source_product_terminal + S (z) = S ((S (a + l)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_terminal. ff_u_bppis_source_product = ff_q_bppis_source_product_terminal * S ((S (a + l)) * ff_v_bppis_source_product) + (z))) /\ forall ff_i_bppis_source_product. (exists ff_lt_bppis_source_product_bound. ff_lt_bppis_source_product_bound + S ff_i_bppis_source_product = a + l) -> exists ff_p_bppis_source_product ff_r_bppis_source_product ff_s_bppis_source_product. ((((exists ff_h_bppis_source_product_factor. ff_h_bppis_source_product_factor + S (ff_p_bppis_source_product) = S ((S (ff_i_bppis_source_product)) * bpr_scale_bppis_source)) /\ exists ff_q_bppis_source_product_factor. bpr_code_bppis_source = ff_q_bppis_source_product_factor * S ((S (ff_i_bppis_source_product)) * bpr_scale_bppis_source) + (ff_p_bppis_source_product))) /\ ((((exists ff_h_bppis_source_product_partial. ff_h_bppis_source_product_partial + S (ff_r_bppis_source_product) = S ((S (ff_i_bppis_source_product)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_partial. ff_u_bppis_source_product = ff_q_bppis_source_product_partial * S ((S (ff_i_bppis_source_product)) * ff_v_bppis_source_product) + (ff_r_bppis_source_product))) /\ ((((exists ff_h_bppis_source_product_successor. ff_h_bppis_source_product_successor + S (ff_s_bppis_source_product) = S ((S (S ff_i_bppis_source_product)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_successor. ff_u_bppis_source_product = ff_q_bppis_source_product_successor * S ((S (S ff_i_bppis_source_product)) * ff_v_bppis_source_product) + (ff_s_bppis_source_product))) /\ ff_s_bppis_source_product = ff_r_bppis_source_product * ff_p_bppis_source_product)))))))) -> (exists x y. (exists bpr_code_bppis_prefix bpr_scale_bppis_prefix. ((forall bpr_index_bppis_prefix_mask. (exists bpr_gap_bppis_prefix_mask_bound. bpr_gap_bppis_prefix_mask_bound + S (bpr_index_bppis_prefix_mask) = a) -> exists bpr_value_bppis_prefix_mask. ((((exists bpr_height_bppis_prefix_mask_decoded. bpr_height_bppis_prefix_mask_decoded + S (bpr_value_bppis_prefix_mask) = S ((S (bpr_index_bppis_prefix_mask)) * bpr_scale_bppis_prefix)) /\ exists bpr_quotient_bppis_prefix_mask_decoded. bpr_code_bppis_prefix = bpr_quotient_bppis_prefix_mask_decoded * S ((S (bpr_index_bppis_prefix_mask)) * bpr_scale_bppis_prefix) + (bpr_value_bppis_prefix_mask))) /\ (((((~(S (bpr_index_bppis_prefix_mask) = 1) /\ forall bpr_left_bppis_prefix_mask_choice_prime bpr_right_bppis_prefix_mask_choice_prime. S (bpr_index_bppis_prefix_mask) = bpr_left_bppis_prefix_mask_choice_prime * bpr_right_bppis_prefix_mask_choice_prime -> bpr_left_bppis_prefix_mask_choice_prime = 1 \/ bpr_right_bppis_prefix_mask_choice_prime = 1)) /\ bpr_value_bppis_prefix_mask = S (bpr_index_bppis_prefix_mask)) \/ (~((~(S (bpr_index_bppis_prefix_mask) = 1) /\ forall bpr_left_bppis_prefix_mask_choice_prime bpr_right_bppis_prefix_mask_choice_prime. S (bpr_index_bppis_prefix_mask) = bpr_left_bppis_prefix_mask_choice_prime * bpr_right_bppis_prefix_mask_choice_prime -> bpr_left_bppis_prefix_mask_choice_prime = 1 \/ bpr_right_bppis_prefix_mask_choice_prime = 1)) /\ bpr_value_bppis_prefix_mask = 1))))) /\ (exists ff_u_bppis_prefix_product ff_v_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_start. ff_h_bppis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_start. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_start * S ((S (0)) * ff_v_bppis_prefix_product) + (1))) /\ ((((exists ff_h_bppis_prefix_product_terminal. ff_h_bppis_prefix_product_terminal + S (x) = S ((S (a)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_terminal. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_terminal * S ((S (a)) * ff_v_bppis_prefix_product) + (x))) /\ forall ff_i_bppis_prefix_product. (exists ff_lt_bppis_prefix_product_bound. ff_lt_bppis_prefix_product_bound + S ff_i_bppis_prefix_product = a) -> exists ff_p_bppis_prefix_product ff_r_bppis_prefix_product ff_s_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_factor. ff_h_bppis_prefix_product_factor + S (ff_p_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * bpr_scale_bppis_prefix)) /\ exists ff_q_bppis_prefix_product_factor. bpr_code_bppis_prefix = ff_q_bppis_prefix_product_factor * S ((S (ff_i_bppis_prefix_product)) * bpr_scale_bppis_prefix) + (ff_p_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_partial. ff_h_bppis_prefix_product_partial + S (ff_r_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_partial. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_partial * S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_r_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_successor. ff_h_bppis_prefix_product_successor + S (ff_s_bppis_prefix_product) = S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_successor. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_successor * S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_s_bppis_prefix_product))) /\ ff_s_bppis_prefix_product = ff_r_bppis_prefix_product * ff_p_bppis_prefix_product)))))))) /\ ((exists bpr_code_bppis_interval bpr_scale_bppis_interval. ((forall bpr_index_bppis_interval_mask. (exists bpr_gap_bppis_interval_mask_bound. bpr_gap_bppis_interval_mask_bound + S (bpr_index_bppis_interval_mask) = l) -> exists bpr_value_bppis_interval_mask. ((((exists bpr_height_bppis_interval_mask_decoded. bpr_height_bppis_interval_mask_decoded + S (bpr_value_bppis_interval_mask) = S ((S (bpr_index_bppis_interval_mask)) * bpr_scale_bppis_interval)) /\ exists bpr_quotient_bppis_interval_mask_decoded. bpr_code_bppis_interval = bpr_quotient_bppis_interval_mask_decoded * S ((S (bpr_index_bppis_interval_mask)) * bpr_scale_bppis_interval) + (bpr_value_bppis_interval_mask))) /\ (((((~(S (a + bpr_index_bppis_interval_mask) = 1) /\ forall bpr_left_bppis_interval_mask_choice_prime bpr_right_bppis_interval_mask_choice_prime. S (a + bpr_index_bppis_interval_mask) = bpr_left_bppis_interval_mask_choice_prime * bpr_right_bppis_interval_mask_choice_prime -> bpr_left_bppis_interval_mask_choice_prime = 1 \/ bpr_right_bppis_interval_mask_choice_prime = 1)) /\ bpr_value_bppis_interval_mask = S (a + bpr_index_bppis_interval_mask)) \/ (~((~(S (a + bpr_index_bppis_interval_mask) = 1) /\ forall bpr_left_bppis_interval_mask_choice_prime bpr_right_bppis_interval_mask_choice_prime. S (a + bpr_index_bppis_interval_mask) = bpr_left_bppis_interval_mask_choice_prime * bpr_right_bppis_interval_mask_choice_prime -> bpr_left_bppis_interval_mask_choice_prime = 1 \/ bpr_right_bppis_interval_mask_choice_prime = 1)) /\ bpr_value_bppis_interval_mask = 1))))) /\ (exists ff_u_bppis_interval_product ff_v_bppis_interval_product. ((((exists ff_h_bppis_interval_product_start. ff_h_bppis_interval_product_start + S (1) = S ((S (0)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_start. ff_u_bppis_interval_product = ff_q_bppis_interval_product_start * S ((S (0)) * ff_v_bppis_interval_product) + (1))) /\ ((((exists ff_h_bppis_interval_product_terminal. ff_h_bppis_interval_product_terminal + S (y) = S ((S (l)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_terminal. ff_u_bppis_interval_product = ff_q_bppis_interval_product_terminal * S ((S (l)) * ff_v_bppis_interval_product) + (y))) /\ forall ff_i_bppis_interval_product. (exists ff_lt_bppis_interval_product_bound. ff_lt_bppis_interval_product_bound + S ff_i_bppis_interval_product = l) -> exists ff_p_bppis_interval_product ff_r_bppis_interval_product ff_s_bppis_interval_product. ((((exists ff_h_bppis_interval_product_factor. ff_h_bppis_interval_product_factor + S (ff_p_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * bpr_scale_bppis_interval)) /\ exists ff_q_bppis_interval_product_factor. bpr_code_bppis_interval = ff_q_bppis_interval_product_factor * S ((S (ff_i_bppis_interval_product)) * bpr_scale_bppis_interval) + (ff_p_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_partial. ff_h_bppis_interval_product_partial + S (ff_r_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_partial. ff_u_bppis_interval_product = ff_q_bppis_interval_product_partial * S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_r_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_successor. ff_h_bppis_interval_product_successor + S (ff_s_bppis_interval_product) = S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_successor. ff_u_bppis_interval_product = ff_q_bppis_interval_product_successor * S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_s_bppis_interval_product))) /\ ff_s_bppis_interval_product = ff_r_bppis_interval_product * ff_p_bppis_interval_product)))))))) /\ z = x * y))

Structural proof guide

Split Primorial(a+l) into its prefix and offset interval product.

Direct prerequisites: beta_product_prefix_suffix_split, primorial_interval_factor_prefix_exists, primorial_interval_factor_prefix_shift, primorial_factor_prefix_restrict_add. The authored body proceeds by case analysis (9), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT00UQ beta_product_prefix_suffix_split BT00US primorial_interval_factor_prefix_exists BT00UW primorial_interval_factor_prefix_shift BT00UX primorial_factor_prefix_restrict_add

Direct dependents

BT00VU primorial_four_power_support_package BT0111 no_bertrand_middle_contribution_interval_le_four_pow

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro l
  3. 0003intro z
  4. 0004intro hprimorial
  5. 0005cases hprimorial
  6. 0006cases hprimorial_witness
  7. 0007cases hprimorial_witness_witness
  8. 0008have hrestricted : forall bpr_index_bppis_restricted. (exists bpr_gap_bppis_restricted_bound. bpr_gap_bppis_restricted_bound + S (bpr_index_bppis_restricted) = a) -> exists bpr_value_bppis_restricted. ((((exists bpr_height_bppis_restricted_decoded. bpr_height_bppis_restricted_decoded + S (bpr_value_bppis_restricted) = S ((S (bpr_index_bppis_restricted)) * x1)) /\ exists bpr_quotient_bppis_restricted_decoded. x = bpr_quotient_bppis_restricted_decoded * S ((S (bpr_index_bppis_restricted)) * x1) + (bpr_value_bppis_restricted))) /\ (((((~(S (bpr_index_bppis_restricted) = 1) /\ forall bpr_left_bppis_restricted_choice_prime bpr_right_bppis_restricted_choice_prime. S (bpr_index_bppis_restricted) = bpr_left_bppis_restricted_choice_prime * bpr_right_bppis_restricted_choice_prime -> bpr_left_bppis_restricted_choice_prime = 1 \/ bpr_right_bppis_restricted_choice_prime = 1)) /\ bpr_value_bppis_restricted = S (bpr_index_bppis_restricted)) \/ (~((~(S (bpr_index_bppis_restricted) = 1) /\ forall bpr_left_bppis_restricted_choice_prime bpr_right_bppis_restricted_choice_prime. S (bpr_index_bppis_restricted) = bpr_left_bppis_restricted_choice_prime * bpr_right_bppis_restricted_choice_prime -> bpr_left_bppis_restricted_choice_prime = 1 \/ bpr_right_bppis_restricted_choice_prime = 1)) /\ bpr_value_bppis_restricted = 1))))
  9. 0009apply primorial_factor_prefix_restrict_add
  10. 0010exact hprimorial_witness_witness_left
  11. 0011have hinterval : exists d e. (forall bpr_index_bppis_interval_prefix. (exists bpr_gap_bppis_interval_prefix_bound. bpr_gap_bppis_interval_prefix_bound + S (bpr_index_bppis_interval_prefix) = l) -> exists bpr_value_bppis_interval_prefix. ((((exists bpr_height_bppis_interval_prefix_decoded. bpr_height_bppis_interval_prefix_decoded + S (bpr_value_bppis_interval_prefix) = S ((S (bpr_index_bppis_interval_prefix)) * e)) /\ exists bpr_quotient_bppis_interval_prefix_decoded. d = bpr_quotient_bppis_interval_prefix_decoded * S ((S (bpr_index_bppis_interval_prefix)) * e) + (bpr_value_bppis_interval_prefix))) /\ (((((~(S (a + bpr_index_bppis_interval_prefix) = 1) /\ forall bpr_left_bppis_interval_prefix_choice_prime bpr_right_bppis_interval_prefix_choice_prime. S (a + bpr_index_bppis_interval_prefix) = bpr_left_bppis_interval_prefix_choice_prime * bpr_right_bppis_interval_prefix_choice_prime -> bpr_left_bppis_interval_prefix_choice_prime = 1 \/ bpr_right_bppis_interval_prefix_choice_prime = 1)) /\ bpr_value_bppis_interval_prefix = S (a + bpr_index_bppis_interval_prefix)) \/ (~((~(S (a + bpr_index_bppis_interval_prefix) = 1) /\ forall bpr_left_bppis_interval_prefix_choice_prime bpr_right_bppis_interval_prefix_choice_prime. S (a + bpr_index_bppis_interval_prefix) = bpr_left_bppis_interval_prefix_choice_prime * bpr_right_bppis_interval_prefix_choice_prime -> bpr_left_bppis_interval_prefix_choice_prime = 1 \/ bpr_right_bppis_interval_prefix_choice_prime = 1)) /\ bpr_value_bppis_interval_prefix = 1)))))
  12. 0012apply primorial_interval_factor_prefix_exists
  13. 0013cases hinterval
  14. 0014cases hinterval_witness
  15. 0015have hshift : forall i p. (exists bpr_gap_bppis_shift_bound. bpr_gap_bppis_shift_bound + S (i) = l) -> (((exists bpr_height_bppis_shift_source. bpr_height_bppis_shift_source + S (p) = S ((S (a + i)) * x1)) /\ exists bpr_quotient_bppis_shift_source. x = bpr_quotient_bppis_shift_source * S ((S (a + i)) * x1) + (p))) -> (((exists bpr_height_bppis_shift_target. bpr_height_bppis_shift_target + S (p) = S ((S (i)) * x3)) /\ exists bpr_quotient_bppis_shift_target. x2 = bpr_quotient_bppis_shift_target * S ((S (i)) * x3) + (p)))
  16. 0016specialize primorial_interval_factor_prefix_shift a
  17. 0017specialize primorial_interval_factor_prefix_shift x
  18. 0018specialize primorial_interval_factor_prefix_shift x1
  19. 0019specialize primorial_interval_factor_prefix_shift x2
  20. 0020specialize primorial_interval_factor_prefix_shift x3
  21. 0021specialize primorial_interval_factor_prefix_shift l
  22. 0022apply primorial_interval_factor_prefix_shift
  23. 0023exact hprimorial_witness_witness_left
  24. 0024exact hinterval_witness_witness
  25. 0025have hsplit : exists p q. (exists ff_u_bppis_prefix_product ff_v_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_start. ff_h_bppis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_start. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_start * S ((S (0)) * ff_v_bppis_prefix_product) + (1))) /\ ((((exists ff_h_bppis_prefix_product_terminal. ff_h_bppis_prefix_product_terminal + S (p) = S ((S (a)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_terminal. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_terminal * S ((S (a)) * ff_v_bppis_prefix_product) + (p))) /\ forall ff_i_bppis_prefix_product. (exists ff_lt_bppis_prefix_product_bound. ff_lt_bppis_prefix_product_bound + S ff_i_bppis_prefix_product = a) -> exists ff_p_bppis_prefix_product ff_r_bppis_prefix_product ff_s_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_factor. ff_h_bppis_prefix_product_factor + S (ff_p_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * x1)) /\ exists ff_q_bppis_prefix_product_factor. x = ff_q_bppis_prefix_product_factor * S ((S (ff_i_bppis_prefix_product)) * x1) + (ff_p_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_partial. ff_h_bppis_prefix_product_partial + S (ff_r_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_partial. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_partial * S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_r_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_successor. ff_h_bppis_prefix_product_successor + S (ff_s_bppis_prefix_product) = S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_successor. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_successor * S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_s_bppis_prefix_product))) /\ ff_s_bppis_prefix_product = ff_r_bppis_prefix_product * ff_p_bppis_prefix_product)))))) /\ ((exists ff_u_bppis_interval_product ff_v_bppis_interval_product. ((((exists ff_h_bppis_interval_product_start. ff_h_bppis_interval_product_start + S (1) = S ((S (0)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_start. ff_u_bppis_interval_product = ff_q_bppis_interval_product_start * S ((S (0)) * ff_v_bppis_interval_product) + (1))) /\ ((((exists ff_h_bppis_interval_product_terminal. ff_h_bppis_interval_product_terminal + S (q) = S ((S (l)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_terminal. ff_u_bppis_interval_product = ff_q_bppis_interval_product_terminal * S ((S (l)) * ff_v_bppis_interval_product) + (q))) /\ forall ff_i_bppis_interval_product. (exists ff_lt_bppis_interval_product_bound. ff_lt_bppis_interval_product_bound + S ff_i_bppis_interval_product = l) -> exists ff_p_bppis_interval_product ff_r_bppis_interval_product ff_s_bppis_interval_product. ((((exists ff_h_bppis_interval_product_factor. ff_h_bppis_interval_product_factor + S (ff_p_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * x3)) /\ exists ff_q_bppis_interval_product_factor. x2 = ff_q_bppis_interval_product_factor * S ((S (ff_i_bppis_interval_product)) * x3) + (ff_p_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_partial. ff_h_bppis_interval_product_partial + S (ff_r_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_partial. ff_u_bppis_interval_product = ff_q_bppis_interval_product_partial * S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_r_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_successor. ff_h_bppis_interval_product_successor + S (ff_s_bppis_interval_product) = S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_successor. ff_u_bppis_interval_product = ff_q_bppis_interval_product_successor * S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_s_bppis_interval_product))) /\ ff_s_bppis_interval_product = ff_r_bppis_interval_product * ff_p_bppis_interval_product)))))) /\ z = p * q)
  26. 0026specialize beta_product_prefix_suffix_split x
  27. 0027specialize beta_product_prefix_suffix_split x1
  28. 0028specialize beta_product_prefix_suffix_split x2
  29. 0029specialize beta_product_prefix_suffix_split x3
  30. 0030specialize beta_product_prefix_suffix_split a
  31. 0031specialize beta_product_prefix_suffix_split l
  32. 0032specialize beta_product_prefix_suffix_split z
  33. 0033apply beta_product_prefix_suffix_split
  34. 0034exact hshift
  35. 0035exact hprimorial_witness_witness_right
  36. 0036cases hsplit
  37. 0037cases hsplit_witness
  38. 0038cases hsplit_witness_witness
  39. 0039cases hsplit_witness_witness_right
  40. 0040exists x4
  41. 0041exists x5
  42. 0042split
  43. 0043exists x
  44. 0044exists x1
  45. 0045split
  46. 0046exact hrestricted
  47. 0047exact hsplit_witness_witness_left
  48. 0048split
  49. 0049exists x2
  50. 0050exists x3
  51. 0051split
  52. 0052exact hinterval_witness_witness
  53. 0053exact hsplit_witness_witness_right_left
  54. 0054exact hsplit_witness_witness_right_right