eisenstein_rectangle_row_count_prefix_extend

Exact expanded PA statement

forall p q k cb cc l. (forall erc_row_rectangle_count_extend_before. (exists erc_lt_gap_rectangle_count_extend_before_bound. erc_lt_gap_rectangle_count_extend_before_bound + S (erc_row_rectangle_count_extend_before) = l) -> exists erc_count_rectangle_count_extend_before. ((((exists ff_h_erc_rectangle_count_extend_before_decoded. ff_h_erc_rectangle_count_extend_before_decoded + S (erc_count_rectangle_count_extend_before) = S ((S (erc_row_rectangle_count_extend_before)) * cc)) /\ exists ff_q_erc_rectangle_count_extend_before_decoded. cb = ff_q_erc_rectangle_count_extend_before_decoded * S ((S (erc_row_rectangle_count_extend_before)) * cc) + (erc_count_rectangle_count_extend_before))) /\ (exists erc_row_code_rectangle_count_extend_before_witness erc_row_scale_rectangle_count_extend_before_witness. ((forall eri_column_erc_rectangle_count_extend_before_witness_row. (exists eri_gap_erc_rectangle_count_extend_before_witness_row_bound. eri_gap_erc_rectangle_count_extend_before_witness_row_bound + S (eri_column_erc_rectangle_count_extend_before_witness_row) = k) -> exists eri_bit_erc_rectangle_count_extend_before_witness_row. ((((exists ff_h_eri_erc_rectangle_count_extend_before_witness_row_decoded. ff_h_eri_erc_rectangle_count_extend_before_witness_row_decoded + S (eri_bit_erc_rectangle_count_extend_before_witness_row) = S ((S (eri_column_erc_rectangle_count_extend_before_witness_row)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_eri_erc_rectangle_count_extend_before_witness_row_decoded. erc_row_code_rectangle_count_extend_before_witness = ff_q_eri_erc_rectangle_count_extend_before_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_before_witness_row)) * erc_row_scale_rectangle_count_extend_before_witness) + (eri_bit_erc_rectangle_count_extend_before_witness_row))) /\ (((eri_bit_erc_rectangle_count_extend_before_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_before) = p * S eri_column_erc_rectangle_count_extend_before_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_before_witness_row) = q * S erc_row_rectangle_count_extend_before))) \/ (eri_bit_erc_rectangle_count_extend_before_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_before_witness_row) = q * S erc_row_rectangle_count_extend_before) /\ ~(exists eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_before_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_before) = p * S eri_column_erc_rectangle_count_extend_before_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_before_witness_count_sum ff_v_erc_rectangle_count_extend_before_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_start. ff_h_erc_rectangle_count_extend_before_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_start. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_terminal. ff_h_erc_rectangle_count_extend_before_witness_count_sum_terminal + S (erc_count_rectangle_count_extend_before) = S ((S (k)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_terminal. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (erc_count_rectangle_count_extend_before))) /\ forall ff_i_erc_rectangle_count_extend_before_witness_count_sum. (exists ff_lt_erc_rectangle_count_extend_before_witness_count_sum_bound. ff_lt_erc_rectangle_count_extend_before_witness_count_sum_bound + S ff_i_erc_rectangle_count_extend_before_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_before_witness_count_sum ff_r_erc_rectangle_count_extend_before_witness_count_sum ff_s_erc_rectangle_count_extend_before_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_summand. ff_h_erc_rectangle_count_extend_before_witness_count_sum_summand + S (ff_a_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_summand. erc_row_code_rectangle_count_extend_before_witness = ff_q_erc_rectangle_count_extend_before_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * erc_row_scale_rectangle_count_extend_before_witness) + (ff_a_erc_rectangle_count_extend_before_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_partial. ff_h_erc_rectangle_count_extend_before_witness_count_sum_partial + S (ff_r_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_partial. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (ff_r_erc_rectangle_count_extend_before_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_sum_successor. ff_h_erc_rectangle_count_extend_before_witness_count_sum_successor + S (ff_s_erc_rectangle_count_extend_before_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_sum_successor. ff_u_erc_rectangle_count_extend_before_witness_count_sum = ff_q_erc_rectangle_count_extend_before_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_before_witness_count_sum)) * ff_v_erc_rectangle_count_extend_before_witness_count_sum) + (ff_s_erc_rectangle_count_extend_before_witness_count_sum))) /\ ff_s_erc_rectangle_count_extend_before_witness_count_sum = ff_r_erc_rectangle_count_extend_before_witness_count_sum + ff_a_erc_rectangle_count_extend_before_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_before_witness_count_bits. (exists ff_lt_erc_rectangle_count_extend_before_witness_count_bits_bound. ff_lt_erc_rectangle_count_extend_before_witness_count_bits_bound + S ff_i_erc_rectangle_count_extend_before_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_before_witness_count_bits. ((((exists ff_h_erc_rectangle_count_extend_before_witness_count_bits_decoded. ff_h_erc_rectangle_count_extend_before_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_before_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_bits)) * erc_row_scale_rectangle_count_extend_before_witness)) /\ exists ff_q_erc_rectangle_count_extend_before_witness_count_bits_decoded. erc_row_code_rectangle_count_extend_before_witness = ff_q_erc_rectangle_count_extend_before_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_before_witness_count_bits)) * erc_row_scale_rectangle_count_extend_before_witness) + (ff_bit_erc_rectangle_count_extend_before_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_before_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_before_witness_count_bits = 1))))))))) -> (exists n. (exists erc_row_code_rectangle_count_extend_last erc_row_scale_rectangle_count_extend_last. ((forall eri_column_erc_rectangle_count_extend_last_row. (exists eri_gap_erc_rectangle_count_extend_last_row_bound. eri_gap_erc_rectangle_count_extend_last_row_bound + S (eri_column_erc_rectangle_count_extend_last_row) = k) -> exists eri_bit_erc_rectangle_count_extend_last_row. ((((exists ff_h_eri_erc_rectangle_count_extend_last_row_decoded. ff_h_eri_erc_rectangle_count_extend_last_row_decoded + S (eri_bit_erc_rectangle_count_extend_last_row) = S ((S (eri_column_erc_rectangle_count_extend_last_row)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_eri_erc_rectangle_count_extend_last_row_decoded. erc_row_code_rectangle_count_extend_last = ff_q_eri_erc_rectangle_count_extend_last_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_last_row)) * erc_row_scale_rectangle_count_extend_last) + (eri_bit_erc_rectangle_count_extend_last_row))) /\ (((eri_bit_erc_rectangle_count_extend_last_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_last_row_choice_left. eri_gap_erc_rectangle_count_extend_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_extend_last_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_last_row_choice_right. eri_gap_erc_rectangle_count_extend_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_last_row) = q * S l))) \/ (eri_bit_erc_rectangle_count_extend_last_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_last_row_choice_right. eri_gap_erc_rectangle_count_extend_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_last_row) = q * S l) /\ ~(exists eri_gap_erc_rectangle_count_extend_last_row_choice_left. eri_gap_erc_rectangle_count_extend_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_extend_last_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_last_count_sum ff_v_erc_rectangle_count_extend_last_count_sum. ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_start. ff_h_erc_rectangle_count_extend_last_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_start. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_terminal. ff_h_erc_rectangle_count_extend_last_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_terminal. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_extend_last_count_sum. (exists ff_lt_erc_rectangle_count_extend_last_count_sum_bound. ff_lt_erc_rectangle_count_extend_last_count_sum_bound + S ff_i_erc_rectangle_count_extend_last_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_last_count_sum ff_r_erc_rectangle_count_extend_last_count_sum ff_s_erc_rectangle_count_extend_last_count_sum. ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_summand. ff_h_erc_rectangle_count_extend_last_count_sum_summand + S (ff_a_erc_rectangle_count_extend_last_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_summand. erc_row_code_rectangle_count_extend_last = ff_q_erc_rectangle_count_extend_last_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * erc_row_scale_rectangle_count_extend_last) + (ff_a_erc_rectangle_count_extend_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_partial. ff_h_erc_rectangle_count_extend_last_count_sum_partial + S (ff_r_erc_rectangle_count_extend_last_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_partial. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (ff_r_erc_rectangle_count_extend_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_last_count_sum_successor. ff_h_erc_rectangle_count_extend_last_count_sum_successor + S (ff_s_erc_rectangle_count_extend_last_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_last_count_sum_successor. ff_u_erc_rectangle_count_extend_last_count_sum = ff_q_erc_rectangle_count_extend_last_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_last_count_sum)) * ff_v_erc_rectangle_count_extend_last_count_sum) + (ff_s_erc_rectangle_count_extend_last_count_sum))) /\ ff_s_erc_rectangle_count_extend_last_count_sum = ff_r_erc_rectangle_count_extend_last_count_sum + ff_a_erc_rectangle_count_extend_last_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_last_count_bits. (exists ff_lt_erc_rectangle_count_extend_last_count_bits_bound. ff_lt_erc_rectangle_count_extend_last_count_bits_bound + S ff_i_erc_rectangle_count_extend_last_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_last_count_bits. ((((exists ff_h_erc_rectangle_count_extend_last_count_bits_decoded. ff_h_erc_rectangle_count_extend_last_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_last_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_last_count_bits)) * erc_row_scale_rectangle_count_extend_last)) /\ exists ff_q_erc_rectangle_count_extend_last_count_bits_decoded. erc_row_code_rectangle_count_extend_last = ff_q_erc_rectangle_count_extend_last_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_last_count_bits)) * erc_row_scale_rectangle_count_extend_last) + (ff_bit_erc_rectangle_count_extend_last_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_last_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_last_count_bits = 1)))))))) -> exists z d. (forall erc_row_rectangle_count_extend_after. (exists erc_lt_gap_rectangle_count_extend_after_bound. erc_lt_gap_rectangle_count_extend_after_bound + S (erc_row_rectangle_count_extend_after) = S l) -> exists erc_count_rectangle_count_extend_after. ((((exists ff_h_erc_rectangle_count_extend_after_decoded. ff_h_erc_rectangle_count_extend_after_decoded + S (erc_count_rectangle_count_extend_after) = S ((S (erc_row_rectangle_count_extend_after)) * d)) /\ exists ff_q_erc_rectangle_count_extend_after_decoded. z = ff_q_erc_rectangle_count_extend_after_decoded * S ((S (erc_row_rectangle_count_extend_after)) * d) + (erc_count_rectangle_count_extend_after))) /\ (exists erc_row_code_rectangle_count_extend_after_witness erc_row_scale_rectangle_count_extend_after_witness. ((forall eri_column_erc_rectangle_count_extend_after_witness_row. (exists eri_gap_erc_rectangle_count_extend_after_witness_row_bound. eri_gap_erc_rectangle_count_extend_after_witness_row_bound + S (eri_column_erc_rectangle_count_extend_after_witness_row) = k) -> exists eri_bit_erc_rectangle_count_extend_after_witness_row. ((((exists ff_h_eri_erc_rectangle_count_extend_after_witness_row_decoded. ff_h_eri_erc_rectangle_count_extend_after_witness_row_decoded + S (eri_bit_erc_rectangle_count_extend_after_witness_row) = S ((S (eri_column_erc_rectangle_count_extend_after_witness_row)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_eri_erc_rectangle_count_extend_after_witness_row_decoded. erc_row_code_rectangle_count_extend_after_witness = ff_q_eri_erc_rectangle_count_extend_after_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_extend_after_witness_row)) * erc_row_scale_rectangle_count_extend_after_witness) + (eri_bit_erc_rectangle_count_extend_after_witness_row))) /\ (((eri_bit_erc_rectangle_count_extend_after_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_after) = p * S eri_column_erc_rectangle_count_extend_after_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_after_witness_row) = q * S erc_row_rectangle_count_extend_after))) \/ (eri_bit_erc_rectangle_count_extend_after_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_extend_after_witness_row) = q * S erc_row_rectangle_count_extend_after) /\ ~(exists eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left. eri_gap_erc_rectangle_count_extend_after_witness_row_choice_left + S (q * S erc_row_rectangle_count_extend_after) = p * S eri_column_erc_rectangle_count_extend_after_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_extend_after_witness_count_sum ff_v_erc_rectangle_count_extend_after_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_start. ff_h_erc_rectangle_count_extend_after_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_start. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_terminal. ff_h_erc_rectangle_count_extend_after_witness_count_sum_terminal + S (erc_count_rectangle_count_extend_after) = S ((S (k)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_terminal. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (erc_count_rectangle_count_extend_after))) /\ forall ff_i_erc_rectangle_count_extend_after_witness_count_sum. (exists ff_lt_erc_rectangle_count_extend_after_witness_count_sum_bound. ff_lt_erc_rectangle_count_extend_after_witness_count_sum_bound + S ff_i_erc_rectangle_count_extend_after_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_extend_after_witness_count_sum ff_r_erc_rectangle_count_extend_after_witness_count_sum ff_s_erc_rectangle_count_extend_after_witness_count_sum. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_summand. ff_h_erc_rectangle_count_extend_after_witness_count_sum_summand + S (ff_a_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_summand. erc_row_code_rectangle_count_extend_after_witness = ff_q_erc_rectangle_count_extend_after_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * erc_row_scale_rectangle_count_extend_after_witness) + (ff_a_erc_rectangle_count_extend_after_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_partial. ff_h_erc_rectangle_count_extend_after_witness_count_sum_partial + S (ff_r_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_partial. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (ff_r_erc_rectangle_count_extend_after_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_sum_successor. ff_h_erc_rectangle_count_extend_after_witness_count_sum_successor + S (ff_s_erc_rectangle_count_extend_after_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_sum_successor. ff_u_erc_rectangle_count_extend_after_witness_count_sum = ff_q_erc_rectangle_count_extend_after_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_extend_after_witness_count_sum)) * ff_v_erc_rectangle_count_extend_after_witness_count_sum) + (ff_s_erc_rectangle_count_extend_after_witness_count_sum))) /\ ff_s_erc_rectangle_count_extend_after_witness_count_sum = ff_r_erc_rectangle_count_extend_after_witness_count_sum + ff_a_erc_rectangle_count_extend_after_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_extend_after_witness_count_bits. (exists ff_lt_erc_rectangle_count_extend_after_witness_count_bits_bound. ff_lt_erc_rectangle_count_extend_after_witness_count_bits_bound + S ff_i_erc_rectangle_count_extend_after_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_extend_after_witness_count_bits. ((((exists ff_h_erc_rectangle_count_extend_after_witness_count_bits_decoded. ff_h_erc_rectangle_count_extend_after_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_extend_after_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_bits)) * erc_row_scale_rectangle_count_extend_after_witness)) /\ exists ff_q_erc_rectangle_count_extend_after_witness_count_bits_decoded. erc_row_code_rectangle_count_extend_after_witness = ff_q_erc_rectangle_count_extend_after_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_extend_after_witness_count_bits)) * erc_row_scale_rectangle_count_extend_after_witness) + (ff_bit_erc_rectangle_count_extend_after_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_extend_after_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_extend_after_witness_count_bits = 1)))))))))