double_quotient_carry_prefix_entries_zero

Exact expanded PA statement

forall p n b c d e f g l q r R s. (exists bcf_le_gap_bdqcpez_base. bcf_le_gap_bdqcpez_base + (1) = p) -> (exists bpvi_b_bdqcpez_square bpvi_c_bdqcpez_square. ((forall bpvi_i_bdqcpez_square. (exists bpvi_repeat_gap_bdqcpez_square. bpvi_repeat_gap_bdqcpez_square + S bpvi_i_bdqcpez_square = 2) -> (((exists bpvi_h_bdqcpez_square_repeat. bpvi_h_bdqcpez_square_repeat + S (p) = S ((S (bpvi_i_bdqcpez_square)) * bpvi_c_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_repeat. bpvi_b_bdqcpez_square = bpvi_q_bdqcpez_square_repeat * S ((S (bpvi_i_bdqcpez_square)) * bpvi_c_bdqcpez_square) + (p)))) /\ (exists bpvi_u_bdqcpez_square bpvi_v_bdqcpez_square. ((((exists bpvi_h_bdqcpez_square_start. bpvi_h_bdqcpez_square_start + S (1) = S ((S (0)) * bpvi_v_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_start. bpvi_u_bdqcpez_square = bpvi_q_bdqcpez_square_start * S ((S (0)) * bpvi_v_bdqcpez_square) + (1))) /\ ((((exists bpvi_h_bdqcpez_square_terminal. bpvi_h_bdqcpez_square_terminal + S (s) = S ((S (2)) * bpvi_v_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_terminal. bpvi_u_bdqcpez_square = bpvi_q_bdqcpez_square_terminal * S ((S (2)) * bpvi_v_bdqcpez_square) + (s))) /\ forall bpvi_j_bdqcpez_square. (exists bpvi_product_gap_bdqcpez_square. bpvi_product_gap_bdqcpez_square + S bpvi_j_bdqcpez_square = 2) -> exists bpvi_factor_bdqcpez_square bpvi_partial_bdqcpez_square bpvi_successor_bdqcpez_square. ((((exists bpvi_h_bdqcpez_square_factor. bpvi_h_bdqcpez_square_factor + S (bpvi_factor_bdqcpez_square) = S ((S (bpvi_j_bdqcpez_square)) * bpvi_c_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_factor. bpvi_b_bdqcpez_square = bpvi_q_bdqcpez_square_factor * S ((S (bpvi_j_bdqcpez_square)) * bpvi_c_bdqcpez_square) + (bpvi_factor_bdqcpez_square))) /\ ((((exists bpvi_h_bdqcpez_square_partial. bpvi_h_bdqcpez_square_partial + S (bpvi_partial_bdqcpez_square) = S ((S (bpvi_j_bdqcpez_square)) * bpvi_v_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_partial. bpvi_u_bdqcpez_square = bpvi_q_bdqcpez_square_partial * S ((S (bpvi_j_bdqcpez_square)) * bpvi_v_bdqcpez_square) + (bpvi_partial_bdqcpez_square))) /\ ((((exists bpvi_h_bdqcpez_square_successor. bpvi_h_bdqcpez_square_successor + S (bpvi_successor_bdqcpez_square) = S ((S (S bpvi_j_bdqcpez_square)) * bpvi_v_bdqcpez_square)) /\ exists bpvi_q_bdqcpez_square_successor. bpvi_u_bdqcpez_square = bpvi_q_bdqcpez_square_successor * S ((S (S bpvi_j_bdqcpez_square)) * bpvi_v_bdqcpez_square) + (bpvi_successor_bdqcpez_square))) /\ bpvi_successor_bdqcpez_square = bpvi_partial_bdqcpez_square * bpvi_factor_bdqcpez_square)))))))) -> (exists bcf_lt_gap_bdqcpez_strict. bcf_lt_gap_bdqcpez_strict + S (n + n) = s) -> (forall bls_index_bdqcpez_left. (exists bls_gap_bdqcpez_left_bound. bls_gap_bdqcpez_left_bound + S (bls_index_bdqcpez_left) = (l)) -> exists bls_power_bdqcpez_left bls_quotient_bdqcpez_left bls_remainder_bdqcpez_left. ((exists bpvi_b_bls_bdqcpez_left_power bpvi_c_bls_bdqcpez_left_power. ((forall bpvi_i_bls_bdqcpez_left_power. (exists bpvi_repeat_gap_bls_bdqcpez_left_power. bpvi_repeat_gap_bls_bdqcpez_left_power + S bpvi_i_bls_bdqcpez_left_power = S bls_index_bdqcpez_left) -> (((exists bpvi_h_bls_bdqcpez_left_power_repeat. bpvi_h_bls_bdqcpez_left_power_repeat + S (p) = S ((S (bpvi_i_bls_bdqcpez_left_power)) * bpvi_c_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_repeat. bpvi_b_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_repeat * S ((S (bpvi_i_bls_bdqcpez_left_power)) * bpvi_c_bls_bdqcpez_left_power) + (p)))) /\ (exists bpvi_u_bls_bdqcpez_left_power bpvi_v_bls_bdqcpez_left_power. ((((exists bpvi_h_bls_bdqcpez_left_power_start. bpvi_h_bls_bdqcpez_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_start. bpvi_u_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_start * S ((S (0)) * bpvi_v_bls_bdqcpez_left_power) + (1))) /\ ((((exists bpvi_h_bls_bdqcpez_left_power_terminal. bpvi_h_bls_bdqcpez_left_power_terminal + S (bls_power_bdqcpez_left) = S ((S (S bls_index_bdqcpez_left)) * bpvi_v_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_terminal. bpvi_u_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_terminal * S ((S (S bls_index_bdqcpez_left)) * bpvi_v_bls_bdqcpez_left_power) + (bls_power_bdqcpez_left))) /\ forall bpvi_j_bls_bdqcpez_left_power. (exists bpvi_product_gap_bls_bdqcpez_left_power. bpvi_product_gap_bls_bdqcpez_left_power + S bpvi_j_bls_bdqcpez_left_power = S bls_index_bdqcpez_left) -> exists bpvi_factor_bls_bdqcpez_left_power bpvi_partial_bls_bdqcpez_left_power bpvi_successor_bls_bdqcpez_left_power. ((((exists bpvi_h_bls_bdqcpez_left_power_factor. bpvi_h_bls_bdqcpez_left_power_factor + S (bpvi_factor_bls_bdqcpez_left_power) = S ((S (bpvi_j_bls_bdqcpez_left_power)) * bpvi_c_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_factor. bpvi_b_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_factor * S ((S (bpvi_j_bls_bdqcpez_left_power)) * bpvi_c_bls_bdqcpez_left_power) + (bpvi_factor_bls_bdqcpez_left_power))) /\ ((((exists bpvi_h_bls_bdqcpez_left_power_partial. bpvi_h_bls_bdqcpez_left_power_partial + S (bpvi_partial_bls_bdqcpez_left_power) = S ((S (bpvi_j_bls_bdqcpez_left_power)) * bpvi_v_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_partial. bpvi_u_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_partial * S ((S (bpvi_j_bls_bdqcpez_left_power)) * bpvi_v_bls_bdqcpez_left_power) + (bpvi_partial_bls_bdqcpez_left_power))) /\ ((((exists bpvi_h_bls_bdqcpez_left_power_successor. bpvi_h_bls_bdqcpez_left_power_successor + S (bpvi_successor_bls_bdqcpez_left_power) = S ((S (S bpvi_j_bls_bdqcpez_left_power)) * bpvi_v_bls_bdqcpez_left_power)) /\ exists bpvi_q_bls_bdqcpez_left_power_successor. bpvi_u_bls_bdqcpez_left_power = bpvi_q_bls_bdqcpez_left_power_successor * S ((S (S bpvi_j_bls_bdqcpez_left_power)) * bpvi_v_bls_bdqcpez_left_power) + (bpvi_successor_bls_bdqcpez_left_power))) /\ bpvi_successor_bls_bdqcpez_left_power = bpvi_partial_bls_bdqcpez_left_power * bpvi_factor_bls_bdqcpez_left_power)))))))) /\ ((((exists ff_h_bls_bdqcpez_left_quotient_entry. ff_h_bls_bdqcpez_left_quotient_entry + S (bls_quotient_bdqcpez_left) = S ((S (bls_index_bdqcpez_left)) * c)) /\ exists ff_q_bls_bdqcpez_left_quotient_entry. b = ff_q_bls_bdqcpez_left_quotient_entry * S ((S (bls_index_bdqcpez_left)) * c) + (bls_quotient_bdqcpez_left))) /\ ((n = bls_power_bdqcpez_left * bls_quotient_bdqcpez_left + bls_remainder_bdqcpez_left /\ exists bls_remainder_gap_bdqcpez_left_division. bls_remainder_gap_bdqcpez_left_division + S (bls_remainder_bdqcpez_left) = bls_power_bdqcpez_left))))) -> (forall bls_index_bdqcpez_right. (exists bls_gap_bdqcpez_right_bound. bls_gap_bdqcpez_right_bound + S (bls_index_bdqcpez_right) = (l)) -> exists bls_power_bdqcpez_right bls_quotient_bdqcpez_right bls_remainder_bdqcpez_right. ((exists bpvi_b_bls_bdqcpez_right_power bpvi_c_bls_bdqcpez_right_power. ((forall bpvi_i_bls_bdqcpez_right_power. (exists bpvi_repeat_gap_bls_bdqcpez_right_power. bpvi_repeat_gap_bls_bdqcpez_right_power + S bpvi_i_bls_bdqcpez_right_power = S bls_index_bdqcpez_right) -> (((exists bpvi_h_bls_bdqcpez_right_power_repeat. bpvi_h_bls_bdqcpez_right_power_repeat + S (p) = S ((S (bpvi_i_bls_bdqcpez_right_power)) * bpvi_c_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_repeat. bpvi_b_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_repeat * S ((S (bpvi_i_bls_bdqcpez_right_power)) * bpvi_c_bls_bdqcpez_right_power) + (p)))) /\ (exists bpvi_u_bls_bdqcpez_right_power bpvi_v_bls_bdqcpez_right_power. ((((exists bpvi_h_bls_bdqcpez_right_power_start. bpvi_h_bls_bdqcpez_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_start. bpvi_u_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_start * S ((S (0)) * bpvi_v_bls_bdqcpez_right_power) + (1))) /\ ((((exists bpvi_h_bls_bdqcpez_right_power_terminal. bpvi_h_bls_bdqcpez_right_power_terminal + S (bls_power_bdqcpez_right) = S ((S (S bls_index_bdqcpez_right)) * bpvi_v_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_terminal. bpvi_u_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_terminal * S ((S (S bls_index_bdqcpez_right)) * bpvi_v_bls_bdqcpez_right_power) + (bls_power_bdqcpez_right))) /\ forall bpvi_j_bls_bdqcpez_right_power. (exists bpvi_product_gap_bls_bdqcpez_right_power. bpvi_product_gap_bls_bdqcpez_right_power + S bpvi_j_bls_bdqcpez_right_power = S bls_index_bdqcpez_right) -> exists bpvi_factor_bls_bdqcpez_right_power bpvi_partial_bls_bdqcpez_right_power bpvi_successor_bls_bdqcpez_right_power. ((((exists bpvi_h_bls_bdqcpez_right_power_factor. bpvi_h_bls_bdqcpez_right_power_factor + S (bpvi_factor_bls_bdqcpez_right_power) = S ((S (bpvi_j_bls_bdqcpez_right_power)) * bpvi_c_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_factor. bpvi_b_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_factor * S ((S (bpvi_j_bls_bdqcpez_right_power)) * bpvi_c_bls_bdqcpez_right_power) + (bpvi_factor_bls_bdqcpez_right_power))) /\ ((((exists bpvi_h_bls_bdqcpez_right_power_partial. bpvi_h_bls_bdqcpez_right_power_partial + S (bpvi_partial_bls_bdqcpez_right_power) = S ((S (bpvi_j_bls_bdqcpez_right_power)) * bpvi_v_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_partial. bpvi_u_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_partial * S ((S (bpvi_j_bls_bdqcpez_right_power)) * bpvi_v_bls_bdqcpez_right_power) + (bpvi_partial_bls_bdqcpez_right_power))) /\ ((((exists bpvi_h_bls_bdqcpez_right_power_successor. bpvi_h_bls_bdqcpez_right_power_successor + S (bpvi_successor_bls_bdqcpez_right_power) = S ((S (S bpvi_j_bls_bdqcpez_right_power)) * bpvi_v_bls_bdqcpez_right_power)) /\ exists bpvi_q_bls_bdqcpez_right_power_successor. bpvi_u_bls_bdqcpez_right_power = bpvi_q_bls_bdqcpez_right_power_successor * S ((S (S bpvi_j_bls_bdqcpez_right_power)) * bpvi_v_bls_bdqcpez_right_power) + (bpvi_successor_bls_bdqcpez_right_power))) /\ bpvi_successor_bls_bdqcpez_right_power = bpvi_partial_bls_bdqcpez_right_power * bpvi_factor_bls_bdqcpez_right_power)))))))) /\ ((((exists ff_h_bls_bdqcpez_right_quotient_entry. ff_h_bls_bdqcpez_right_quotient_entry + S (bls_quotient_bdqcpez_right) = S ((S (bls_index_bdqcpez_right)) * e)) /\ exists ff_q_bls_bdqcpez_right_quotient_entry. d = ff_q_bls_bdqcpez_right_quotient_entry * S ((S (bls_index_bdqcpez_right)) * e) + (bls_quotient_bdqcpez_right))) /\ ((n + n = bls_power_bdqcpez_right * bls_quotient_bdqcpez_right + bls_remainder_bdqcpez_right /\ exists bls_remainder_gap_bdqcpez_right_division. bls_remainder_gap_bdqcpez_right_division + S (bls_remainder_bdqcpez_right) = bls_power_bdqcpez_right))))) -> (forall b5cc_index_bdqcpez_carry. (exists bcf_lt_gap_bdqcpez_carry_bound. bcf_lt_gap_bdqcpez_carry_bound + S (b5cc_index_bdqcpez_carry) = l) -> exists b5cc_left_bdqcpez_carry b5cc_right_bdqcpez_carry b5cc_bit_bdqcpez_carry. (((exists fs_h_b5cc_bdqcpez_carry_left. fs_h_b5cc_bdqcpez_carry_left + S (b5cc_left_bdqcpez_carry) = S ((S (b5cc_index_bdqcpez_carry)) * c)) /\ exists fs_q_b5cc_bdqcpez_carry_left. b = fs_q_b5cc_bdqcpez_carry_left * S ((S (b5cc_index_bdqcpez_carry)) * c) + (b5cc_left_bdqcpez_carry))) /\ ((((exists fs_h_b5cc_bdqcpez_carry_right. fs_h_b5cc_bdqcpez_carry_right + S (b5cc_right_bdqcpez_carry) = S ((S (b5cc_index_bdqcpez_carry)) * e)) /\ exists fs_q_b5cc_bdqcpez_carry_right. d = fs_q_b5cc_bdqcpez_carry_right * S ((S (b5cc_index_bdqcpez_carry)) * e) + (b5cc_right_bdqcpez_carry))) /\ ((((exists fs_h_b5cc_bdqcpez_carry_bit. fs_h_b5cc_bdqcpez_carry_bit + S (b5cc_bit_bdqcpez_carry) = S ((S (b5cc_index_bdqcpez_carry)) * g)) /\ exists fs_q_b5cc_bdqcpez_carry_bit. f = fs_q_b5cc_bdqcpez_carry_bit * S ((S (b5cc_index_bdqcpez_carry)) * g) + (b5cc_bit_bdqcpez_carry))) /\ (((b5cc_bit_bdqcpez_carry = 0 /\ b5cc_right_bdqcpez_carry = b5cc_left_bdqcpez_carry + b5cc_left_bdqcpez_carry) \/ (b5cc_bit_bdqcpez_carry = 1 /\ b5cc_right_bdqcpez_carry = S (b5cc_left_bdqcpez_carry + b5cc_left_bdqcpez_carry))))))) -> (((n) = (p) * (q) + (r) /\ (exists bcf_lt_gap_bdqcpez_first_bound. bcf_lt_gap_bdqcpez_first_bound + S (r) = p))) -> (((n + n) = (p) * (q + q) + (R) /\ (exists bcf_lt_gap_bdqcpez_double_bound. bcf_lt_gap_bdqcpez_double_bound + S (R) = p))) -> forall i. (exists bcf_lt_gap_bdqcpez_bound. bcf_lt_gap_bdqcpez_bound + S (i) = l) -> (((exists fs_h_bdqcpez_result. fs_h_bdqcpez_result + S (0) = S ((S (i)) * g)) /\ exists fs_q_bdqcpez_result. f = fs_q_bdqcpez_result * S ((S (i)) * g) + (0)))