BT00UD — primorial_succ

Exact expanded PA statement

forall m z. (exists bpr_code_bp_succ_source bpr_scale_bp_succ_source. ((forall bpr_index_bp_succ_source_mask. (exists bpr_gap_bp_succ_source_mask_bound. bpr_gap_bp_succ_source_mask_bound + S (bpr_index_bp_succ_source_mask) = S m) -> exists bpr_value_bp_succ_source_mask. ((((exists bpr_height_bp_succ_source_mask_decoded. bpr_height_bp_succ_source_mask_decoded + S (bpr_value_bp_succ_source_mask) = S ((S (bpr_index_bp_succ_source_mask)) * bpr_scale_bp_succ_source)) /\ exists bpr_quotient_bp_succ_source_mask_decoded. bpr_code_bp_succ_source = bpr_quotient_bp_succ_source_mask_decoded * S ((S (bpr_index_bp_succ_source_mask)) * bpr_scale_bp_succ_source) + (bpr_value_bp_succ_source_mask))) /\ (((((~(S (bpr_index_bp_succ_source_mask) = 1) /\ forall bpr_left_bp_succ_source_mask_choice_prime bpr_right_bp_succ_source_mask_choice_prime. S (bpr_index_bp_succ_source_mask) = bpr_left_bp_succ_source_mask_choice_prime * bpr_right_bp_succ_source_mask_choice_prime -> bpr_left_bp_succ_source_mask_choice_prime = 1 \/ bpr_right_bp_succ_source_mask_choice_prime = 1)) /\ bpr_value_bp_succ_source_mask = S (bpr_index_bp_succ_source_mask)) \/ (~((~(S (bpr_index_bp_succ_source_mask) = 1) /\ forall bpr_left_bp_succ_source_mask_choice_prime bpr_right_bp_succ_source_mask_choice_prime. S (bpr_index_bp_succ_source_mask) = bpr_left_bp_succ_source_mask_choice_prime * bpr_right_bp_succ_source_mask_choice_prime -> bpr_left_bp_succ_source_mask_choice_prime = 1 \/ bpr_right_bp_succ_source_mask_choice_prime = 1)) /\ bpr_value_bp_succ_source_mask = 1))))) /\ (exists ff_u_bp_succ_source_product ff_v_bp_succ_source_product. ((((exists ff_h_bp_succ_source_product_start. ff_h_bp_succ_source_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_start. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_start * S ((S (0)) * ff_v_bp_succ_source_product) + (1))) /\ ((((exists ff_h_bp_succ_source_product_terminal. ff_h_bp_succ_source_product_terminal + S (z) = S ((S (S m)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_terminal. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_terminal * S ((S (S m)) * ff_v_bp_succ_source_product) + (z))) /\ forall ff_i_bp_succ_source_product. (exists ff_lt_bp_succ_source_product_bound. ff_lt_bp_succ_source_product_bound + S ff_i_bp_succ_source_product = S m) -> exists ff_p_bp_succ_source_product ff_r_bp_succ_source_product ff_s_bp_succ_source_product. ((((exists ff_h_bp_succ_source_product_factor. ff_h_bp_succ_source_product_factor + S (ff_p_bp_succ_source_product) = S ((S (ff_i_bp_succ_source_product)) * bpr_scale_bp_succ_source)) /\ exists ff_q_bp_succ_source_product_factor. bpr_code_bp_succ_source = ff_q_bp_succ_source_product_factor * S ((S (ff_i_bp_succ_source_product)) * bpr_scale_bp_succ_source) + (ff_p_bp_succ_source_product))) /\ ((((exists ff_h_bp_succ_source_product_partial. ff_h_bp_succ_source_product_partial + S (ff_r_bp_succ_source_product) = S ((S (ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_partial. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_partial * S ((S (ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product) + (ff_r_bp_succ_source_product))) /\ ((((exists ff_h_bp_succ_source_product_successor. ff_h_bp_succ_source_product_successor + S (ff_s_bp_succ_source_product) = S ((S (S ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_successor. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_successor * S ((S (S ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product) + (ff_s_bp_succ_source_product))) /\ ff_s_bp_succ_source_product = ff_r_bp_succ_source_product * ff_p_bp_succ_source_product)))))))) -> (exists p r. (((((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = 1))) /\ ((exists bpr_code_bp_succ_predecessor bpr_scale_bp_succ_predecessor. ((forall bpr_index_bp_succ_predecessor_mask. (exists bpr_gap_bp_succ_predecessor_mask_bound. bpr_gap_bp_succ_predecessor_mask_bound + S (bpr_index_bp_succ_predecessor_mask) = m) -> exists bpr_value_bp_succ_predecessor_mask. ((((exists bpr_height_bp_succ_predecessor_mask_decoded. bpr_height_bp_succ_predecessor_mask_decoded + S (bpr_value_bp_succ_predecessor_mask) = S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor)) /\ exists bpr_quotient_bp_succ_predecessor_mask_decoded. bpr_code_bp_succ_predecessor = bpr_quotient_bp_succ_predecessor_mask_decoded * S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor) + (bpr_value_bp_succ_predecessor_mask))) /\ (((((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = S (bpr_index_bp_succ_predecessor_mask)) \/ (~((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = 1))))) /\ (exists ff_u_bp_succ_predecessor_product ff_v_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_start. ff_h_bp_succ_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_start. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_start * S ((S (0)) * ff_v_bp_succ_predecessor_product) + (1))) /\ ((((exists ff_h_bp_succ_predecessor_product_terminal. ff_h_bp_succ_predecessor_product_terminal + S (r) = S ((S (m)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_terminal. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_terminal * S ((S (m)) * ff_v_bp_succ_predecessor_product) + (r))) /\ forall ff_i_bp_succ_predecessor_product. (exists ff_lt_bp_succ_predecessor_product_bound. ff_lt_bp_succ_predecessor_product_bound + S ff_i_bp_succ_predecessor_product = m) -> exists ff_p_bp_succ_predecessor_product ff_r_bp_succ_predecessor_product ff_s_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_factor. ff_h_bp_succ_predecessor_product_factor + S (ff_p_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor)) /\ exists ff_q_bp_succ_predecessor_product_factor. bpr_code_bp_succ_predecessor = ff_q_bp_succ_predecessor_product_factor * S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor) + (ff_p_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_partial. ff_h_bp_succ_predecessor_product_partial + S (ff_r_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_partial. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_partial * S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_r_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_successor. ff_h_bp_succ_predecessor_product_successor + S (ff_s_bp_succ_predecessor_product) = S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_successor. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_successor * S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_s_bp_succ_predecessor_product))) /\ ff_s_bp_succ_predecessor_product = ff_r_bp_succ_predecessor_product * ff_p_bp_succ_predecessor_product)))))))) /\ z = r * p))

Structural proof guide

A successor primorial splits into its previous value and selector.

Direct prerequisites: beta_product_succ_decompose, beta_at_unique, le_refl, le_succ. The authored body proceeds by case analysis (9), intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT005J beta_product_succ_decompose BT0042 beta_at_unique BT000E le_refl BT0018 le_succ

Direct dependents

BT00UE primorial_positive BT00VQ primorial_one

Formal native tactic body

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

0001intro m
0002intro z
0003intro hprimorial
0004cases hprimorial
0005cases hprimorial_witness
0006cases hprimorial_witness_witness
0007have hdecomposition : exists p r. (((exists bpr_height_bp_succ_last_factor. bpr_height_bp_succ_last_factor + S (p) = S ((S (m)) * x1)) /\ exists bpr_quotient_bp_succ_last_factor. x = bpr_quotient_bp_succ_last_factor * S ((S (m)) * x1) + (p))) /\ ((exists ff_u_bp_succ_prefix_product ff_v_bp_succ_prefix_product. ((((exists ff_h_bp_succ_prefix_product_start. ff_h_bp_succ_prefix_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_start. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_start * S ((S (0)) * ff_v_bp_succ_prefix_product) + (1))) /\ ((((exists ff_h_bp_succ_prefix_product_terminal. ff_h_bp_succ_prefix_product_terminal + S (r) = S ((S (m)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_terminal. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_terminal * S ((S (m)) * ff_v_bp_succ_prefix_product) + (r))) /\ forall ff_i_bp_succ_prefix_product. (exists ff_lt_bp_succ_prefix_product_bound. ff_lt_bp_succ_prefix_product_bound + S ff_i_bp_succ_prefix_product = m) -> exists ff_p_bp_succ_prefix_product ff_r_bp_succ_prefix_product ff_s_bp_succ_prefix_product. ((((exists ff_h_bp_succ_prefix_product_factor. ff_h_bp_succ_prefix_product_factor + S (ff_p_bp_succ_prefix_product) = S ((S (ff_i_bp_succ_prefix_product)) * x1)) /\ exists ff_q_bp_succ_prefix_product_factor. x = ff_q_bp_succ_prefix_product_factor * S ((S (ff_i_bp_succ_prefix_product)) * x1) + (ff_p_bp_succ_prefix_product))) /\ ((((exists ff_h_bp_succ_prefix_product_partial. ff_h_bp_succ_prefix_product_partial + S (ff_r_bp_succ_prefix_product) = S ((S (ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_partial. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_partial * S ((S (ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product) + (ff_r_bp_succ_prefix_product))) /\ ((((exists ff_h_bp_succ_prefix_product_successor. ff_h_bp_succ_prefix_product_successor + S (ff_s_bp_succ_prefix_product) = S ((S (S ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_successor. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_successor * S ((S (S ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product) + (ff_s_bp_succ_prefix_product))) /\ ff_s_bp_succ_prefix_product = ff_r_bp_succ_prefix_product * ff_p_bp_succ_prefix_product)))))) /\ z = r * p)
0008apply beta_product_succ_decompose
0009exact hprimorial_witness_witness_right
0010cases hdecomposition
0011cases hdecomposition_witness
0012cases hdecomposition_witness_witness
0013cases hdecomposition_witness_witness_right
0014have hterminal : exists a. ((((exists bpr_height_bp_succ_mask_terminal. bpr_height_bp_succ_mask_terminal + S (a) = S ((S (m)) * x1)) /\ exists bpr_quotient_bp_succ_mask_terminal. x = bpr_quotient_bp_succ_mask_terminal * S ((S (m)) * x1) + (a))) /\ (((((~(S (m) = 1) /\ forall bpr_left_bp_succ_mask_choice_prime bpr_right_bp_succ_mask_choice_prime. S (m) = bpr_left_bp_succ_mask_choice_prime * bpr_right_bp_succ_mask_choice_prime -> bpr_left_bp_succ_mask_choice_prime = 1 \/ bpr_right_bp_succ_mask_choice_prime = 1)) /\ a = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bp_succ_mask_choice_prime bpr_right_bp_succ_mask_choice_prime. S (m) = bpr_left_bp_succ_mask_choice_prime * bpr_right_bp_succ_mask_choice_prime -> bpr_left_bp_succ_mask_choice_prime = 1 \/ bpr_right_bp_succ_mask_choice_prime = 1)) /\ a = 1))))
0015apply hprimorial_witness_witness_left
0016apply le_refl
0017cases hterminal
0018cases hterminal_witness
0019have hfactor : x2 = x4
0020apply beta_at_unique
0021exact hdecomposition_witness_witness_left
0022exact hterminal_witness_left
0023exists x4
0024exists x3
0025split
0026exact hterminal_witness_right
0027split
0028exists x
0029exists x1
0030split
0031intro i
0032intro hi
0033apply hprimorial_witness_witness_left
0034apply le_succ
0035exact hi
0036exact hdecomposition_witness_witness_right_left
0037trans x3 * x2
0038exact hdecomposition_witness_witness_right_right
0039rewrite hfactor
0040refl