distinct_odd_prime_row_bit_count_equals_decoded_quotient

Exact expanded PA statement

forall p q h k i tb tc qb qc ub uc rb rc n d. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_quotient_prime_p frp_prime_right_row_quotient_prime_p. p = frp_prime_left_row_quotient_prime_p * frp_prime_right_row_quotient_prime_p -> frp_prime_left_row_quotient_prime_p = 1 \/ frp_prime_right_row_quotient_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_quotient_prime_q frp_prime_right_row_quotient_prime_q. q = frp_prime_left_row_quotient_prime_q * frp_prime_right_row_quotient_prime_q -> frp_prime_left_row_quotient_prime_q = 1 \/ frp_prime_right_row_quotient_prime_q = 1)) -> ~(p = q) -> (exists edt_lt_gap_row_quotient_row_bound. edt_lt_gap_row_quotient_row_bound + S (i) = h) -> (forall esd_index_row_quotient_scaled esd_value_row_quotient_scaled. (exists esd_gap_row_quotient_scaled. esd_gap_row_quotient_scaled + S esd_index_row_quotient_scaled = h) -> (((exists ff_h_esd_row_quotient_scaled_decoded. ff_h_esd_row_quotient_scaled_decoded + S (esd_value_row_quotient_scaled) = S ((S (esd_index_row_quotient_scaled)) * tc)) /\ exists ff_q_esd_row_quotient_scaled_decoded. tb = ff_q_esd_row_quotient_scaled_decoded * S ((S (esd_index_row_quotient_scaled)) * tc) + (esd_value_row_quotient_scaled))) -> esd_value_row_quotient_scaled = q * (1 + esd_index_row_quotient_scaled)) -> (forall fdp_index_row_quotient_division. (exists gsp_lt_gap_row_quotient_division_index_bound. gsp_lt_gap_row_quotient_division_index_bound + S fdp_index_row_quotient_division = h) -> exists fdp_value_row_quotient_division fdp_quotient_row_quotient_division fdp_remainder_row_quotient_division. (((exists ff_h_fdp_row_quotient_division_source. ff_h_fdp_row_quotient_division_source + S (fdp_value_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * tc)) /\ exists ff_q_fdp_row_quotient_division_source. tb = ff_q_fdp_row_quotient_division_source * S ((S (fdp_index_row_quotient_division)) * tc) + (fdp_value_row_quotient_division))) /\ ((((exists ff_h_fdp_row_quotient_division_quotient_entry. ff_h_fdp_row_quotient_division_quotient_entry + S (fdp_quotient_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * qc)) /\ exists ff_q_fdp_row_quotient_division_quotient_entry. qb = ff_q_fdp_row_quotient_division_quotient_entry * S ((S (fdp_index_row_quotient_division)) * qc) + (fdp_quotient_row_quotient_division))) /\ ((((exists ff_h_fdp_row_quotient_division_remainder_entry. ff_h_fdp_row_quotient_division_remainder_entry + S (fdp_remainder_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * uc)) /\ exists ff_q_fdp_row_quotient_division_remainder_entry. ub = ff_q_fdp_row_quotient_division_remainder_entry * S ((S (fdp_index_row_quotient_division)) * uc) + (fdp_remainder_row_quotient_division))) /\ (fdp_value_row_quotient_division = p * fdp_quotient_row_quotient_division + fdp_remainder_row_quotient_division /\ (exists gsp_lt_gap_row_quotient_division_remainder_bound. gsp_lt_gap_row_quotient_division_remainder_bound + S fdp_remainder_row_quotient_division = p))))) -> (forall eri_column_row_quotient_source. (exists eri_gap_row_quotient_source_bound. eri_gap_row_quotient_source_bound + S (eri_column_row_quotient_source) = k) -> exists eri_bit_row_quotient_source. ((((exists ff_h_eri_row_quotient_source_decoded. ff_h_eri_row_quotient_source_decoded + S (eri_bit_row_quotient_source) = S ((S (eri_column_row_quotient_source)) * rc)) /\ exists ff_q_eri_row_quotient_source_decoded. rb = ff_q_eri_row_quotient_source_decoded * S ((S (eri_column_row_quotient_source)) * rc) + (eri_bit_row_quotient_source))) /\ (((eri_bit_row_quotient_source = 0 /\ ((exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source) /\ ~(exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i))) \/ (eri_bit_row_quotient_source = 1 /\ ((exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i) /\ ~(exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source))))))) -> (((exists ff_u_row_quotient_count_n_sum ff_v_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_start. ff_h_row_quotient_count_n_sum_start + S (0) = S ((S (0)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_start. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_start * S ((S (0)) * ff_v_row_quotient_count_n_sum) + (0))) /\ ((((exists ff_h_row_quotient_count_n_sum_terminal. ff_h_row_quotient_count_n_sum_terminal + S (n) = S ((S (k)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_terminal. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_terminal * S ((S (k)) * ff_v_row_quotient_count_n_sum) + (n))) /\ forall ff_i_row_quotient_count_n_sum. (exists ff_lt_row_quotient_count_n_sum_bound. ff_lt_row_quotient_count_n_sum_bound + S ff_i_row_quotient_count_n_sum = k) -> exists ff_a_row_quotient_count_n_sum ff_r_row_quotient_count_n_sum ff_s_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_summand. ff_h_row_quotient_count_n_sum_summand + S (ff_a_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * rc)) /\ exists ff_q_row_quotient_count_n_sum_summand. rb = ff_q_row_quotient_count_n_sum_summand * S ((S (ff_i_row_quotient_count_n_sum)) * rc) + (ff_a_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_partial. ff_h_row_quotient_count_n_sum_partial + S (ff_r_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_partial. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_partial * S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_r_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_successor. ff_h_row_quotient_count_n_sum_successor + S (ff_s_row_quotient_count_n_sum) = S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_successor. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_successor * S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_s_row_quotient_count_n_sum))) /\ ff_s_row_quotient_count_n_sum = ff_r_row_quotient_count_n_sum + ff_a_row_quotient_count_n_sum)))))) /\ (forall ff_i_row_quotient_count_n_bits. (exists ff_lt_row_quotient_count_n_bits_bound. ff_lt_row_quotient_count_n_bits_bound + S ff_i_row_quotient_count_n_bits = k) -> exists ff_bit_row_quotient_count_n_bits. ((((exists ff_h_row_quotient_count_n_bits_decoded. ff_h_row_quotient_count_n_bits_decoded + S (ff_bit_row_quotient_count_n_bits) = S ((S (ff_i_row_quotient_count_n_bits)) * rc)) /\ exists ff_q_row_quotient_count_n_bits_decoded. rb = ff_q_row_quotient_count_n_bits_decoded * S ((S (ff_i_row_quotient_count_n_bits)) * rc) + (ff_bit_row_quotient_count_n_bits))) /\ (ff_bit_row_quotient_count_n_bits = 0 \/ ff_bit_row_quotient_count_n_bits = 1))))) -> (((exists ff_h_row_quotient_decoded_quotient. ff_h_row_quotient_decoded_quotient + S (d) = S ((S (i)) * qc)) /\ exists ff_q_row_quotient_decoded_quotient. qb = ff_q_row_quotient_decoded_quotient * S ((S (i)) * qc) + (d))) -> n = d