distinct_odd_prime_eisenstein_quotient_sum_identity

Exact expanded PA statement

forall p q h k tb tc qb qc ub uc sb sc vb vc wb wc ab ac bb bc Q U. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_quotient_sum_identity_prime_p frp_prime_right_quotient_sum_identity_prime_p. p = frp_prime_left_quotient_sum_identity_prime_p * frp_prime_right_quotient_sum_identity_prime_p -> frp_prime_left_quotient_sum_identity_prime_p = 1 \/ frp_prime_right_quotient_sum_identity_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_quotient_sum_identity_prime_q frp_prime_right_quotient_sum_identity_prime_q. q = frp_prime_left_quotient_sum_identity_prime_q * frp_prime_right_quotient_sum_identity_prime_q -> frp_prime_left_quotient_sum_identity_prime_q = 1 \/ frp_prime_right_quotient_sum_identity_prime_q = 1)) -> ~(p = q) -> (forall esd_index_quotient_sum_identity_first_scaled esd_value_quotient_sum_identity_first_scaled. (exists esd_gap_quotient_sum_identity_first_scaled. esd_gap_quotient_sum_identity_first_scaled + S esd_index_quotient_sum_identity_first_scaled = h) -> (((exists ff_h_esd_quotient_sum_identity_first_scaled_decoded. ff_h_esd_quotient_sum_identity_first_scaled_decoded + S (esd_value_quotient_sum_identity_first_scaled) = S ((S (esd_index_quotient_sum_identity_first_scaled)) * tc)) /\ exists ff_q_esd_quotient_sum_identity_first_scaled_decoded. tb = ff_q_esd_quotient_sum_identity_first_scaled_decoded * S ((S (esd_index_quotient_sum_identity_first_scaled)) * tc) + (esd_value_quotient_sum_identity_first_scaled))) -> esd_value_quotient_sum_identity_first_scaled = q * (1 + esd_index_quotient_sum_identity_first_scaled)) -> (forall fdp_index_quotient_sum_identity_first_divisions. (exists gsp_lt_gap_quotient_sum_identity_first_divisions_index_bound. gsp_lt_gap_quotient_sum_identity_first_divisions_index_bound + S fdp_index_quotient_sum_identity_first_divisions = h) -> exists fdp_value_quotient_sum_identity_first_divisions fdp_quotient_quotient_sum_identity_first_divisions fdp_remainder_quotient_sum_identity_first_divisions. (((exists ff_h_fdp_quotient_sum_identity_first_divisions_source. ff_h_fdp_quotient_sum_identity_first_divisions_source + S (fdp_value_quotient_sum_identity_first_divisions) = S ((S (fdp_index_quotient_sum_identity_first_divisions)) * tc)) /\ exists ff_q_fdp_quotient_sum_identity_first_divisions_source. tb = ff_q_fdp_quotient_sum_identity_first_divisions_source * S ((S (fdp_index_quotient_sum_identity_first_divisions)) * tc) + (fdp_value_quotient_sum_identity_first_divisions))) /\ ((((exists ff_h_fdp_quotient_sum_identity_first_divisions_quotient_entry. ff_h_fdp_quotient_sum_identity_first_divisions_quotient_entry + S (fdp_quotient_quotient_sum_identity_first_divisions) = S ((S (fdp_index_quotient_sum_identity_first_divisions)) * qc)) /\ exists ff_q_fdp_quotient_sum_identity_first_divisions_quotient_entry. qb = ff_q_fdp_quotient_sum_identity_first_divisions_quotient_entry * S ((S (fdp_index_quotient_sum_identity_first_divisions)) * qc) + (fdp_quotient_quotient_sum_identity_first_divisions))) /\ ((((exists ff_h_fdp_quotient_sum_identity_first_divisions_remainder_entry. ff_h_fdp_quotient_sum_identity_first_divisions_remainder_entry + S (fdp_remainder_quotient_sum_identity_first_divisions) = S ((S (fdp_index_quotient_sum_identity_first_divisions)) * uc)) /\ exists ff_q_fdp_quotient_sum_identity_first_divisions_remainder_entry. ub = ff_q_fdp_quotient_sum_identity_first_divisions_remainder_entry * S ((S (fdp_index_quotient_sum_identity_first_divisions)) * uc) + (fdp_remainder_quotient_sum_identity_first_divisions))) /\ (fdp_value_quotient_sum_identity_first_divisions = p * fdp_quotient_quotient_sum_identity_first_divisions + fdp_remainder_quotient_sum_identity_first_divisions /\ (exists gsp_lt_gap_quotient_sum_identity_first_divisions_remainder_bound. gsp_lt_gap_quotient_sum_identity_first_divisions_remainder_bound + S fdp_remainder_quotient_sum_identity_first_divisions = p))))) -> (forall esd_index_quotient_sum_identity_second_scaled esd_value_quotient_sum_identity_second_scaled. (exists esd_gap_quotient_sum_identity_second_scaled. esd_gap_quotient_sum_identity_second_scaled + S esd_index_quotient_sum_identity_second_scaled = k) -> (((exists ff_h_esd_quotient_sum_identity_second_scaled_decoded. ff_h_esd_quotient_sum_identity_second_scaled_decoded + S (esd_value_quotient_sum_identity_second_scaled) = S ((S (esd_index_quotient_sum_identity_second_scaled)) * sc)) /\ exists ff_q_esd_quotient_sum_identity_second_scaled_decoded. sb = ff_q_esd_quotient_sum_identity_second_scaled_decoded * S ((S (esd_index_quotient_sum_identity_second_scaled)) * sc) + (esd_value_quotient_sum_identity_second_scaled))) -> esd_value_quotient_sum_identity_second_scaled = p * (1 + esd_index_quotient_sum_identity_second_scaled)) -> (forall fdp_index_quotient_sum_identity_second_divisions. (exists gsp_lt_gap_quotient_sum_identity_second_divisions_index_bound. gsp_lt_gap_quotient_sum_identity_second_divisions_index_bound + S fdp_index_quotient_sum_identity_second_divisions = k) -> exists fdp_value_quotient_sum_identity_second_divisions fdp_quotient_quotient_sum_identity_second_divisions fdp_remainder_quotient_sum_identity_second_divisions. (((exists ff_h_fdp_quotient_sum_identity_second_divisions_source. ff_h_fdp_quotient_sum_identity_second_divisions_source + S (fdp_value_quotient_sum_identity_second_divisions) = S ((S (fdp_index_quotient_sum_identity_second_divisions)) * sc)) /\ exists ff_q_fdp_quotient_sum_identity_second_divisions_source. sb = ff_q_fdp_quotient_sum_identity_second_divisions_source * S ((S (fdp_index_quotient_sum_identity_second_divisions)) * sc) + (fdp_value_quotient_sum_identity_second_divisions))) /\ ((((exists ff_h_fdp_quotient_sum_identity_second_divisions_quotient_entry. ff_h_fdp_quotient_sum_identity_second_divisions_quotient_entry + S (fdp_quotient_quotient_sum_identity_second_divisions) = S ((S (fdp_index_quotient_sum_identity_second_divisions)) * vc)) /\ exists ff_q_fdp_quotient_sum_identity_second_divisions_quotient_entry. vb = ff_q_fdp_quotient_sum_identity_second_divisions_quotient_entry * S ((S (fdp_index_quotient_sum_identity_second_divisions)) * vc) + (fdp_quotient_quotient_sum_identity_second_divisions))) /\ ((((exists ff_h_fdp_quotient_sum_identity_second_divisions_remainder_entry. ff_h_fdp_quotient_sum_identity_second_divisions_remainder_entry + S (fdp_remainder_quotient_sum_identity_second_divisions) = S ((S (fdp_index_quotient_sum_identity_second_divisions)) * wc)) /\ exists ff_q_fdp_quotient_sum_identity_second_divisions_remainder_entry. wb = ff_q_fdp_quotient_sum_identity_second_divisions_remainder_entry * S ((S (fdp_index_quotient_sum_identity_second_divisions)) * wc) + (fdp_remainder_quotient_sum_identity_second_divisions))) /\ (fdp_value_quotient_sum_identity_second_divisions = q * fdp_quotient_quotient_sum_identity_second_divisions + fdp_remainder_quotient_sum_identity_second_divisions /\ (exists gsp_lt_gap_quotient_sum_identity_second_divisions_remainder_bound. gsp_lt_gap_quotient_sum_identity_second_divisions_remainder_bound + S fdp_remainder_quotient_sum_identity_second_divisions = q))))) -> (forall erc_row_quotient_sum_identity_first_outer. (exists erc_lt_gap_quotient_sum_identity_first_outer_bound. erc_lt_gap_quotient_sum_identity_first_outer_bound + S (erc_row_quotient_sum_identity_first_outer) = h) -> exists erc_count_quotient_sum_identity_first_outer. ((((exists ff_h_erc_quotient_sum_identity_first_outer_decoded. ff_h_erc_quotient_sum_identity_first_outer_decoded + S (erc_count_quotient_sum_identity_first_outer) = S ((S (erc_row_quotient_sum_identity_first_outer)) * ac)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_decoded. ab = ff_q_erc_quotient_sum_identity_first_outer_decoded * S ((S (erc_row_quotient_sum_identity_first_outer)) * ac) + (erc_count_quotient_sum_identity_first_outer))) /\ (exists erc_row_code_quotient_sum_identity_first_outer_witness erc_row_scale_quotient_sum_identity_first_outer_witness. ((forall eri_column_erc_quotient_sum_identity_first_outer_witness_row. (exists eri_gap_erc_quotient_sum_identity_first_outer_witness_row_bound. eri_gap_erc_quotient_sum_identity_first_outer_witness_row_bound + S (eri_column_erc_quotient_sum_identity_first_outer_witness_row) = k) -> exists eri_bit_erc_quotient_sum_identity_first_outer_witness_row. ((((exists ff_h_eri_erc_quotient_sum_identity_first_outer_witness_row_decoded. ff_h_eri_erc_quotient_sum_identity_first_outer_witness_row_decoded + S (eri_bit_erc_quotient_sum_identity_first_outer_witness_row) = S ((S (eri_column_erc_quotient_sum_identity_first_outer_witness_row)) * erc_row_scale_quotient_sum_identity_first_outer_witness)) /\ exists ff_q_eri_erc_quotient_sum_identity_first_outer_witness_row_decoded. erc_row_code_quotient_sum_identity_first_outer_witness = ff_q_eri_erc_quotient_sum_identity_first_outer_witness_row_decoded * S ((S (eri_column_erc_quotient_sum_identity_first_outer_witness_row)) * erc_row_scale_quotient_sum_identity_first_outer_witness) + (eri_bit_erc_quotient_sum_identity_first_outer_witness_row))) /\ (((eri_bit_erc_quotient_sum_identity_first_outer_witness_row = 0 /\ ((exists eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_left. eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_left + S (q * S erc_row_quotient_sum_identity_first_outer) = p * S eri_column_erc_quotient_sum_identity_first_outer_witness_row) /\ ~(exists eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_right. eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_quotient_sum_identity_first_outer_witness_row) = q * S erc_row_quotient_sum_identity_first_outer))) \/ (eri_bit_erc_quotient_sum_identity_first_outer_witness_row = 1 /\ ((exists eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_right. eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_quotient_sum_identity_first_outer_witness_row) = q * S erc_row_quotient_sum_identity_first_outer) /\ ~(exists eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_left. eri_gap_erc_quotient_sum_identity_first_outer_witness_row_choice_left + S (q * S erc_row_quotient_sum_identity_first_outer) = p * S eri_column_erc_quotient_sum_identity_first_outer_witness_row))))))) /\ (((exists ff_u_erc_quotient_sum_identity_first_outer_witness_count_sum ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_start. ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_start. ff_u_erc_quotient_sum_identity_first_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_terminal. ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_terminal + S (erc_count_quotient_sum_identity_first_outer) = S ((S (k)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_terminal. ff_u_erc_quotient_sum_identity_first_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum) + (erc_count_quotient_sum_identity_first_outer))) /\ forall ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum. (exists ff_lt_erc_quotient_sum_identity_first_outer_witness_count_sum_bound. ff_lt_erc_quotient_sum_identity_first_outer_witness_count_sum_bound + S ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum = k) -> exists ff_a_erc_quotient_sum_identity_first_outer_witness_count_sum ff_r_erc_quotient_sum_identity_first_outer_witness_count_sum ff_s_erc_quotient_sum_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_summand. ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_summand + S (ff_a_erc_quotient_sum_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * erc_row_scale_quotient_sum_identity_first_outer_witness)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_summand. erc_row_code_quotient_sum_identity_first_outer_witness = ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_summand * S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * erc_row_scale_quotient_sum_identity_first_outer_witness) + (ff_a_erc_quotient_sum_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_partial. ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_partial + S (ff_r_erc_quotient_sum_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_partial. ff_u_erc_quotient_sum_identity_first_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_partial * S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum) + (ff_r_erc_quotient_sum_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_successor. ff_h_erc_quotient_sum_identity_first_outer_witness_count_sum_successor + S (ff_s_erc_quotient_sum_identity_first_outer_witness_count_sum) = S ((S (S ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_successor. ff_u_erc_quotient_sum_identity_first_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_first_outer_witness_count_sum_successor * S ((S (S ff_i_erc_quotient_sum_identity_first_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_first_outer_witness_count_sum) + (ff_s_erc_quotient_sum_identity_first_outer_witness_count_sum))) /\ ff_s_erc_quotient_sum_identity_first_outer_witness_count_sum = ff_r_erc_quotient_sum_identity_first_outer_witness_count_sum + ff_a_erc_quotient_sum_identity_first_outer_witness_count_sum)))))) /\ (forall ff_i_erc_quotient_sum_identity_first_outer_witness_count_bits. (exists ff_lt_erc_quotient_sum_identity_first_outer_witness_count_bits_bound. ff_lt_erc_quotient_sum_identity_first_outer_witness_count_bits_bound + S ff_i_erc_quotient_sum_identity_first_outer_witness_count_bits = k) -> exists ff_bit_erc_quotient_sum_identity_first_outer_witness_count_bits. ((((exists ff_h_erc_quotient_sum_identity_first_outer_witness_count_bits_decoded. ff_h_erc_quotient_sum_identity_first_outer_witness_count_bits_decoded + S (ff_bit_erc_quotient_sum_identity_first_outer_witness_count_bits) = S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_bits)) * erc_row_scale_quotient_sum_identity_first_outer_witness)) /\ exists ff_q_erc_quotient_sum_identity_first_outer_witness_count_bits_decoded. erc_row_code_quotient_sum_identity_first_outer_witness = ff_q_erc_quotient_sum_identity_first_outer_witness_count_bits_decoded * S ((S (ff_i_erc_quotient_sum_identity_first_outer_witness_count_bits)) * erc_row_scale_quotient_sum_identity_first_outer_witness) + (ff_bit_erc_quotient_sum_identity_first_outer_witness_count_bits))) /\ (ff_bit_erc_quotient_sum_identity_first_outer_witness_count_bits = 0 \/ ff_bit_erc_quotient_sum_identity_first_outer_witness_count_bits = 1))))))))) -> (forall erc_row_quotient_sum_identity_second_outer. (exists erc_lt_gap_quotient_sum_identity_second_outer_bound. erc_lt_gap_quotient_sum_identity_second_outer_bound + S (erc_row_quotient_sum_identity_second_outer) = k) -> exists erc_count_quotient_sum_identity_second_outer. ((((exists ff_h_erc_quotient_sum_identity_second_outer_decoded. ff_h_erc_quotient_sum_identity_second_outer_decoded + S (erc_count_quotient_sum_identity_second_outer) = S ((S (erc_row_quotient_sum_identity_second_outer)) * bc)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_decoded. bb = ff_q_erc_quotient_sum_identity_second_outer_decoded * S ((S (erc_row_quotient_sum_identity_second_outer)) * bc) + (erc_count_quotient_sum_identity_second_outer))) /\ (exists erc_row_code_quotient_sum_identity_second_outer_witness erc_row_scale_quotient_sum_identity_second_outer_witness. ((forall eri_column_erc_quotient_sum_identity_second_outer_witness_row. (exists eri_gap_erc_quotient_sum_identity_second_outer_witness_row_bound. eri_gap_erc_quotient_sum_identity_second_outer_witness_row_bound + S (eri_column_erc_quotient_sum_identity_second_outer_witness_row) = h) -> exists eri_bit_erc_quotient_sum_identity_second_outer_witness_row. ((((exists ff_h_eri_erc_quotient_sum_identity_second_outer_witness_row_decoded. ff_h_eri_erc_quotient_sum_identity_second_outer_witness_row_decoded + S (eri_bit_erc_quotient_sum_identity_second_outer_witness_row) = S ((S (eri_column_erc_quotient_sum_identity_second_outer_witness_row)) * erc_row_scale_quotient_sum_identity_second_outer_witness)) /\ exists ff_q_eri_erc_quotient_sum_identity_second_outer_witness_row_decoded. erc_row_code_quotient_sum_identity_second_outer_witness = ff_q_eri_erc_quotient_sum_identity_second_outer_witness_row_decoded * S ((S (eri_column_erc_quotient_sum_identity_second_outer_witness_row)) * erc_row_scale_quotient_sum_identity_second_outer_witness) + (eri_bit_erc_quotient_sum_identity_second_outer_witness_row))) /\ (((eri_bit_erc_quotient_sum_identity_second_outer_witness_row = 0 /\ ((exists eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_left. eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_left + S (p * S erc_row_quotient_sum_identity_second_outer) = q * S eri_column_erc_quotient_sum_identity_second_outer_witness_row) /\ ~(exists eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_right. eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_quotient_sum_identity_second_outer_witness_row) = p * S erc_row_quotient_sum_identity_second_outer))) \/ (eri_bit_erc_quotient_sum_identity_second_outer_witness_row = 1 /\ ((exists eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_right. eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_quotient_sum_identity_second_outer_witness_row) = p * S erc_row_quotient_sum_identity_second_outer) /\ ~(exists eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_left. eri_gap_erc_quotient_sum_identity_second_outer_witness_row_choice_left + S (p * S erc_row_quotient_sum_identity_second_outer) = q * S eri_column_erc_quotient_sum_identity_second_outer_witness_row))))))) /\ (((exists ff_u_erc_quotient_sum_identity_second_outer_witness_count_sum ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_start. ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_start. ff_u_erc_quotient_sum_identity_second_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_terminal. ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_terminal + S (erc_count_quotient_sum_identity_second_outer) = S ((S (h)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_terminal. ff_u_erc_quotient_sum_identity_second_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum) + (erc_count_quotient_sum_identity_second_outer))) /\ forall ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum. (exists ff_lt_erc_quotient_sum_identity_second_outer_witness_count_sum_bound. ff_lt_erc_quotient_sum_identity_second_outer_witness_count_sum_bound + S ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum = h) -> exists ff_a_erc_quotient_sum_identity_second_outer_witness_count_sum ff_r_erc_quotient_sum_identity_second_outer_witness_count_sum ff_s_erc_quotient_sum_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_summand. ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_summand + S (ff_a_erc_quotient_sum_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * erc_row_scale_quotient_sum_identity_second_outer_witness)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_summand. erc_row_code_quotient_sum_identity_second_outer_witness = ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_summand * S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * erc_row_scale_quotient_sum_identity_second_outer_witness) + (ff_a_erc_quotient_sum_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_partial. ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_partial + S (ff_r_erc_quotient_sum_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_partial. ff_u_erc_quotient_sum_identity_second_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_partial * S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum) + (ff_r_erc_quotient_sum_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_successor. ff_h_erc_quotient_sum_identity_second_outer_witness_count_sum_successor + S (ff_s_erc_quotient_sum_identity_second_outer_witness_count_sum) = S ((S (S ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_successor. ff_u_erc_quotient_sum_identity_second_outer_witness_count_sum = ff_q_erc_quotient_sum_identity_second_outer_witness_count_sum_successor * S ((S (S ff_i_erc_quotient_sum_identity_second_outer_witness_count_sum)) * ff_v_erc_quotient_sum_identity_second_outer_witness_count_sum) + (ff_s_erc_quotient_sum_identity_second_outer_witness_count_sum))) /\ ff_s_erc_quotient_sum_identity_second_outer_witness_count_sum = ff_r_erc_quotient_sum_identity_second_outer_witness_count_sum + ff_a_erc_quotient_sum_identity_second_outer_witness_count_sum)))))) /\ (forall ff_i_erc_quotient_sum_identity_second_outer_witness_count_bits. (exists ff_lt_erc_quotient_sum_identity_second_outer_witness_count_bits_bound. ff_lt_erc_quotient_sum_identity_second_outer_witness_count_bits_bound + S ff_i_erc_quotient_sum_identity_second_outer_witness_count_bits = h) -> exists ff_bit_erc_quotient_sum_identity_second_outer_witness_count_bits. ((((exists ff_h_erc_quotient_sum_identity_second_outer_witness_count_bits_decoded. ff_h_erc_quotient_sum_identity_second_outer_witness_count_bits_decoded + S (ff_bit_erc_quotient_sum_identity_second_outer_witness_count_bits) = S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_bits)) * erc_row_scale_quotient_sum_identity_second_outer_witness)) /\ exists ff_q_erc_quotient_sum_identity_second_outer_witness_count_bits_decoded. erc_row_code_quotient_sum_identity_second_outer_witness = ff_q_erc_quotient_sum_identity_second_outer_witness_count_bits_decoded * S ((S (ff_i_erc_quotient_sum_identity_second_outer_witness_count_bits)) * erc_row_scale_quotient_sum_identity_second_outer_witness) + (ff_bit_erc_quotient_sum_identity_second_outer_witness_count_bits))) /\ (ff_bit_erc_quotient_sum_identity_second_outer_witness_count_bits = 0 \/ ff_bit_erc_quotient_sum_identity_second_outer_witness_count_bits = 1))))))))) -> (exists ff_u_quotient_sum_identity_first_sum ff_v_quotient_sum_identity_first_sum. ((((exists ff_h_quotient_sum_identity_first_sum_start. ff_h_quotient_sum_identity_first_sum_start + S (0) = S ((S (0)) * ff_v_quotient_sum_identity_first_sum)) /\ exists ff_q_quotient_sum_identity_first_sum_start. ff_u_quotient_sum_identity_first_sum = ff_q_quotient_sum_identity_first_sum_start * S ((S (0)) * ff_v_quotient_sum_identity_first_sum) + (0))) /\ ((((exists ff_h_quotient_sum_identity_first_sum_terminal. ff_h_quotient_sum_identity_first_sum_terminal + S (Q) = S ((S (h)) * ff_v_quotient_sum_identity_first_sum)) /\ exists ff_q_quotient_sum_identity_first_sum_terminal. ff_u_quotient_sum_identity_first_sum = ff_q_quotient_sum_identity_first_sum_terminal * S ((S (h)) * ff_v_quotient_sum_identity_first_sum) + (Q))) /\ forall ff_i_quotient_sum_identity_first_sum. (exists ff_lt_quotient_sum_identity_first_sum_bound. ff_lt_quotient_sum_identity_first_sum_bound + S ff_i_quotient_sum_identity_first_sum = h) -> exists ff_a_quotient_sum_identity_first_sum ff_r_quotient_sum_identity_first_sum ff_s_quotient_sum_identity_first_sum. ((((exists ff_h_quotient_sum_identity_first_sum_summand. ff_h_quotient_sum_identity_first_sum_summand + S (ff_a_quotient_sum_identity_first_sum) = S ((S (ff_i_quotient_sum_identity_first_sum)) * qc)) /\ exists ff_q_quotient_sum_identity_first_sum_summand. qb = ff_q_quotient_sum_identity_first_sum_summand * S ((S (ff_i_quotient_sum_identity_first_sum)) * qc) + (ff_a_quotient_sum_identity_first_sum))) /\ ((((exists ff_h_quotient_sum_identity_first_sum_partial. ff_h_quotient_sum_identity_first_sum_partial + S (ff_r_quotient_sum_identity_first_sum) = S ((S (ff_i_quotient_sum_identity_first_sum)) * ff_v_quotient_sum_identity_first_sum)) /\ exists ff_q_quotient_sum_identity_first_sum_partial. ff_u_quotient_sum_identity_first_sum = ff_q_quotient_sum_identity_first_sum_partial * S ((S (ff_i_quotient_sum_identity_first_sum)) * ff_v_quotient_sum_identity_first_sum) + (ff_r_quotient_sum_identity_first_sum))) /\ ((((exists ff_h_quotient_sum_identity_first_sum_successor. ff_h_quotient_sum_identity_first_sum_successor + S (ff_s_quotient_sum_identity_first_sum) = S ((S (S ff_i_quotient_sum_identity_first_sum)) * ff_v_quotient_sum_identity_first_sum)) /\ exists ff_q_quotient_sum_identity_first_sum_successor. ff_u_quotient_sum_identity_first_sum = ff_q_quotient_sum_identity_first_sum_successor * S ((S (S ff_i_quotient_sum_identity_first_sum)) * ff_v_quotient_sum_identity_first_sum) + (ff_s_quotient_sum_identity_first_sum))) /\ ff_s_quotient_sum_identity_first_sum = ff_r_quotient_sum_identity_first_sum + ff_a_quotient_sum_identity_first_sum)))))) -> (exists ff_u_quotient_sum_identity_second_sum ff_v_quotient_sum_identity_second_sum. ((((exists ff_h_quotient_sum_identity_second_sum_start. ff_h_quotient_sum_identity_second_sum_start + S (0) = S ((S (0)) * ff_v_quotient_sum_identity_second_sum)) /\ exists ff_q_quotient_sum_identity_second_sum_start. ff_u_quotient_sum_identity_second_sum = ff_q_quotient_sum_identity_second_sum_start * S ((S (0)) * ff_v_quotient_sum_identity_second_sum) + (0))) /\ ((((exists ff_h_quotient_sum_identity_second_sum_terminal. ff_h_quotient_sum_identity_second_sum_terminal + S (U) = S ((S (k)) * ff_v_quotient_sum_identity_second_sum)) /\ exists ff_q_quotient_sum_identity_second_sum_terminal. ff_u_quotient_sum_identity_second_sum = ff_q_quotient_sum_identity_second_sum_terminal * S ((S (k)) * ff_v_quotient_sum_identity_second_sum) + (U))) /\ forall ff_i_quotient_sum_identity_second_sum. (exists ff_lt_quotient_sum_identity_second_sum_bound. ff_lt_quotient_sum_identity_second_sum_bound + S ff_i_quotient_sum_identity_second_sum = k) -> exists ff_a_quotient_sum_identity_second_sum ff_r_quotient_sum_identity_second_sum ff_s_quotient_sum_identity_second_sum. ((((exists ff_h_quotient_sum_identity_second_sum_summand. ff_h_quotient_sum_identity_second_sum_summand + S (ff_a_quotient_sum_identity_second_sum) = S ((S (ff_i_quotient_sum_identity_second_sum)) * vc)) /\ exists ff_q_quotient_sum_identity_second_sum_summand. vb = ff_q_quotient_sum_identity_second_sum_summand * S ((S (ff_i_quotient_sum_identity_second_sum)) * vc) + (ff_a_quotient_sum_identity_second_sum))) /\ ((((exists ff_h_quotient_sum_identity_second_sum_partial. ff_h_quotient_sum_identity_second_sum_partial + S (ff_r_quotient_sum_identity_second_sum) = S ((S (ff_i_quotient_sum_identity_second_sum)) * ff_v_quotient_sum_identity_second_sum)) /\ exists ff_q_quotient_sum_identity_second_sum_partial. ff_u_quotient_sum_identity_second_sum = ff_q_quotient_sum_identity_second_sum_partial * S ((S (ff_i_quotient_sum_identity_second_sum)) * ff_v_quotient_sum_identity_second_sum) + (ff_r_quotient_sum_identity_second_sum))) /\ ((((exists ff_h_quotient_sum_identity_second_sum_successor. ff_h_quotient_sum_identity_second_sum_successor + S (ff_s_quotient_sum_identity_second_sum) = S ((S (S ff_i_quotient_sum_identity_second_sum)) * ff_v_quotient_sum_identity_second_sum)) /\ exists ff_q_quotient_sum_identity_second_sum_successor. ff_u_quotient_sum_identity_second_sum = ff_q_quotient_sum_identity_second_sum_successor * S ((S (S ff_i_quotient_sum_identity_second_sum)) * ff_v_quotient_sum_identity_second_sum) + (ff_s_quotient_sum_identity_second_sum))) /\ ff_s_quotient_sum_identity_second_sum = ff_r_quotient_sum_identity_second_sum + ff_a_quotient_sum_identity_second_sum)))))) -> Q + U = h * k