eisenstein_successor_terminal_sum_matches_last_column

Exact expanded PA statement

forall p q h sh bb bc db dc tb tc cb cc l D M. sh = S h -> (forall efrd_row_index_fubini_terminal_column_split_prefix. (exists efrd_lt_gap_fubini_terminal_column_split_prefix_bound. efrd_lt_gap_fubini_terminal_column_split_prefix_bound + S (efrd_row_index_fubini_terminal_column_split_prefix) = l) -> exists efrd_count_fubini_terminal_column_split_prefix efrd_reduced_count_fubini_terminal_column_split_prefix efrd_terminal_bit_fubini_terminal_column_split_prefix. (((((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_outer_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_outer_entry + S (efrd_count_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * bc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_terminal_column_split_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * bc) + (efrd_count_fubini_terminal_column_split_prefix))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * dc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_terminal_column_split_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * dc) + (efrd_reduced_count_fubini_terminal_column_split_prefix)))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_terminal_column_split_prefix) = S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * tc)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_terminal_column_split_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_terminal_column_split_prefix)) * tc) + (efrd_terminal_bit_fubini_terminal_column_split_prefix)))) /\ (exists efrd_row_code_fubini_terminal_column_split_prefix_entry_split efrd_row_scale_fubini_terminal_column_split_prefix_entry_split. (((((forall eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix))) \/ (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_terminal_column_split_prefix) = S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_terminal_column_split_prefix))) /\ forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_eri_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix))) \/ (eri_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_terminal_column_split_prefix) /\ ~(exists eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_terminal_column_split_prefix) = q * S eri_column_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_terminal_column_split_prefix) = S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (efrd_terminal_bit_fubini_terminal_column_split_prefix))))) /\ (((((exists ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_terminal_column_split_prefix) = S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_terminal_column_split_prefix))) /\ forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split)) /\ exists ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_terminal_column_split_prefix_entry_split = ff_q_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_terminal_column_split_prefix_entry_split) + (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_terminal_column_split_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_terminal_column_split_prefix = 0 \/ efrd_terminal_bit_fubini_terminal_column_split_prefix = 1)) /\ efrd_count_fubini_terminal_column_split_prefix = efrd_reduced_count_fubini_terminal_column_split_prefix + efrd_terminal_bit_fubini_terminal_column_split_prefix))))))) -> (forall etc_row_index_fubini_terminal_column_prefix. (exists edt_lt_gap_fubini_terminal_column_prefix_bound. edt_lt_gap_fubini_terminal_column_prefix_bound + S (etc_row_index_fubini_terminal_column_prefix) = l) -> exists etc_bit_fubini_terminal_column_prefix. ((((exists ff_h_etc_fubini_terminal_column_prefix_decoded. ff_h_etc_fubini_terminal_column_prefix_decoded + S (etc_bit_fubini_terminal_column_prefix) = S ((S (etc_row_index_fubini_terminal_column_prefix)) * cc)) /\ exists ff_q_etc_fubini_terminal_column_prefix_decoded. cb = ff_q_etc_fubini_terminal_column_prefix_decoded * S ((S (etc_row_index_fubini_terminal_column_prefix)) * cc) + (etc_bit_fubini_terminal_column_prefix))) /\ (exists etc_count_fubini_terminal_column_prefix_witness etc_row_code_fubini_terminal_column_prefix_witness etc_row_scale_fubini_terminal_column_prefix_witness. ((((((exists ff_h_etc_fubini_terminal_column_prefix_witness_outer_entry. ff_h_etc_fubini_terminal_column_prefix_witness_outer_entry + S (etc_count_fubini_terminal_column_prefix_witness) = S ((S (etc_row_index_fubini_terminal_column_prefix)) * bc)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_outer_entry. bb = ff_q_etc_fubini_terminal_column_prefix_witness_outer_entry * S ((S (etc_row_index_fubini_terminal_column_prefix)) * bc) + (etc_count_fubini_terminal_column_prefix_witness))) /\ (forall eri_column_etc_fubini_terminal_column_prefix_witness_row. (exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_bound. eri_gap_etc_fubini_terminal_column_prefix_witness_row_bound + S (eri_column_etc_fubini_terminal_column_prefix_witness_row) = sh) -> exists eri_bit_etc_fubini_terminal_column_prefix_witness_row. ((((exists ff_h_eri_etc_fubini_terminal_column_prefix_witness_row_decoded. ff_h_eri_etc_fubini_terminal_column_prefix_witness_row_decoded + S (eri_bit_etc_fubini_terminal_column_prefix_witness_row) = S ((S (eri_column_etc_fubini_terminal_column_prefix_witness_row)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_eri_etc_fubini_terminal_column_prefix_witness_row_decoded. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_eri_etc_fubini_terminal_column_prefix_witness_row_decoded * S ((S (eri_column_etc_fubini_terminal_column_prefix_witness_row)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (eri_bit_etc_fubini_terminal_column_prefix_witness_row))) /\ (((eri_bit_etc_fubini_terminal_column_prefix_witness_row = 0 /\ ((exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left + S (p * S etc_row_index_fubini_terminal_column_prefix) = q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) /\ ~(exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) = p * S etc_row_index_fubini_terminal_column_prefix))) \/ (eri_bit_etc_fubini_terminal_column_prefix_witness_row = 1 /\ ((exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_right + S (q * S eri_column_etc_fubini_terminal_column_prefix_witness_row) = p * S etc_row_index_fubini_terminal_column_prefix) /\ ~(exists eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left. eri_gap_etc_fubini_terminal_column_prefix_witness_row_choice_left + S (p * S etc_row_index_fubini_terminal_column_prefix) = q * S eri_column_etc_fubini_terminal_column_prefix_witness_row)))))))) /\ (((exists ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal + S (etc_count_fubini_terminal_column_prefix_witness) = S ((S (sh)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_terminal * S ((S (sh)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (etc_count_fubini_terminal_column_prefix_witness))) /\ forall ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum. (exists ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_sum_bound. ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_sum_bound + S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum = sh) -> exists ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand + S (ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_summand * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial + S (ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_partial * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor + S (ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum) = S ((S (S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor. ff_u_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_sum_successor * S ((S (S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_sum)) * ff_v_etc_fubini_terminal_column_prefix_witness_count_relation_sum) + (ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum))) /\ ff_s_etc_fubini_terminal_column_prefix_witness_count_relation_sum = ff_r_etc_fubini_terminal_column_prefix_witness_count_relation_sum + ff_a_etc_fubini_terminal_column_prefix_witness_count_relation_sum)))))) /\ (forall ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits. (exists ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_bits_bound. ff_lt_etc_fubini_terminal_column_prefix_witness_count_relation_bits_bound + S ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits = sh) -> exists ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits. ((((exists ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded. ff_h_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded + S (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits) = S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_count_relation_bits_decoded * S ((S (ff_i_etc_fubini_terminal_column_prefix_witness_count_relation_bits)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits))) /\ (ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits = 0 \/ ff_bit_etc_fubini_terminal_column_prefix_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_fubini_terminal_column_prefix_witness_inner_entry. ff_h_etc_fubini_terminal_column_prefix_witness_inner_entry + S (etc_bit_fubini_terminal_column_prefix) = S ((S (h)) * etc_row_scale_fubini_terminal_column_prefix_witness)) /\ exists ff_q_etc_fubini_terminal_column_prefix_witness_inner_entry. etc_row_code_fubini_terminal_column_prefix_witness = ff_q_etc_fubini_terminal_column_prefix_witness_inner_entry * S ((S (h)) * etc_row_scale_fubini_terminal_column_prefix_witness) + (etc_bit_fubini_terminal_column_prefix))))))) -> (exists ff_u_fubini_row_split_terminal_sum ff_v_fubini_row_split_terminal_sum. ((((exists ff_h_fubini_row_split_terminal_sum_start. ff_h_fubini_row_split_terminal_sum_start + S (0) = S ((S (0)) * ff_v_fubini_row_split_terminal_sum)) /\ exists ff_q_fubini_row_split_terminal_sum_start. ff_u_fubini_row_split_terminal_sum = ff_q_fubini_row_split_terminal_sum_start * S ((S (0)) * ff_v_fubini_row_split_terminal_sum) + (0))) /\ ((((exists ff_h_fubini_row_split_terminal_sum_terminal. ff_h_fubini_row_split_terminal_sum_terminal + S (D) = S ((S (l)) * ff_v_fubini_row_split_terminal_sum)) /\ exists ff_q_fubini_row_split_terminal_sum_terminal. ff_u_fubini_row_split_terminal_sum = ff_q_fubini_row_split_terminal_sum_terminal * S ((S (l)) * ff_v_fubini_row_split_terminal_sum) + (D))) /\ forall ff_i_fubini_row_split_terminal_sum. (exists ff_lt_fubini_row_split_terminal_sum_bound. ff_lt_fubini_row_split_terminal_sum_bound + S ff_i_fubini_row_split_terminal_sum = l) -> exists ff_a_fubini_row_split_terminal_sum ff_r_fubini_row_split_terminal_sum ff_s_fubini_row_split_terminal_sum. ((((exists ff_h_fubini_row_split_terminal_sum_summand. ff_h_fubini_row_split_terminal_sum_summand + S (ff_a_fubini_row_split_terminal_sum) = S ((S (ff_i_fubini_row_split_terminal_sum)) * tc)) /\ exists ff_q_fubini_row_split_terminal_sum_summand. tb = ff_q_fubini_row_split_terminal_sum_summand * S ((S (ff_i_fubini_row_split_terminal_sum)) * tc) + (ff_a_fubini_row_split_terminal_sum))) /\ ((((exists ff_h_fubini_row_split_terminal_sum_partial. ff_h_fubini_row_split_terminal_sum_partial + S (ff_r_fubini_row_split_terminal_sum) = S ((S (ff_i_fubini_row_split_terminal_sum)) * ff_v_fubini_row_split_terminal_sum)) /\ exists ff_q_fubini_row_split_terminal_sum_partial. ff_u_fubini_row_split_terminal_sum = ff_q_fubini_row_split_terminal_sum_partial * S ((S (ff_i_fubini_row_split_terminal_sum)) * ff_v_fubini_row_split_terminal_sum) + (ff_r_fubini_row_split_terminal_sum))) /\ ((((exists ff_h_fubini_row_split_terminal_sum_successor. ff_h_fubini_row_split_terminal_sum_successor + S (ff_s_fubini_row_split_terminal_sum) = S ((S (S ff_i_fubini_row_split_terminal_sum)) * ff_v_fubini_row_split_terminal_sum)) /\ exists ff_q_fubini_row_split_terminal_sum_successor. ff_u_fubini_row_split_terminal_sum = ff_q_fubini_row_split_terminal_sum_successor * S ((S (S ff_i_fubini_row_split_terminal_sum)) * ff_v_fubini_row_split_terminal_sum) + (ff_s_fubini_row_split_terminal_sum))) /\ ff_s_fubini_row_split_terminal_sum = ff_r_fubini_row_split_terminal_sum + ff_a_fubini_row_split_terminal_sum)))))) -> (exists ff_u_fubini_terminal_column_sum ff_v_fubini_terminal_column_sum. ((((exists ff_h_fubini_terminal_column_sum_start. ff_h_fubini_terminal_column_sum_start + S (0) = S ((S (0)) * ff_v_fubini_terminal_column_sum)) /\ exists ff_q_fubini_terminal_column_sum_start. ff_u_fubini_terminal_column_sum = ff_q_fubini_terminal_column_sum_start * S ((S (0)) * ff_v_fubini_terminal_column_sum) + (0))) /\ ((((exists ff_h_fubini_terminal_column_sum_terminal. ff_h_fubini_terminal_column_sum_terminal + S (M) = S ((S (l)) * ff_v_fubini_terminal_column_sum)) /\ exists ff_q_fubini_terminal_column_sum_terminal. ff_u_fubini_terminal_column_sum = ff_q_fubini_terminal_column_sum_terminal * S ((S (l)) * ff_v_fubini_terminal_column_sum) + (M))) /\ forall ff_i_fubini_terminal_column_sum. (exists ff_lt_fubini_terminal_column_sum_bound. ff_lt_fubini_terminal_column_sum_bound + S ff_i_fubini_terminal_column_sum = l) -> exists ff_a_fubini_terminal_column_sum ff_r_fubini_terminal_column_sum ff_s_fubini_terminal_column_sum. ((((exists ff_h_fubini_terminal_column_sum_summand. ff_h_fubini_terminal_column_sum_summand + S (ff_a_fubini_terminal_column_sum) = S ((S (ff_i_fubini_terminal_column_sum)) * cc)) /\ exists ff_q_fubini_terminal_column_sum_summand. cb = ff_q_fubini_terminal_column_sum_summand * S ((S (ff_i_fubini_terminal_column_sum)) * cc) + (ff_a_fubini_terminal_column_sum))) /\ ((((exists ff_h_fubini_terminal_column_sum_partial. ff_h_fubini_terminal_column_sum_partial + S (ff_r_fubini_terminal_column_sum) = S ((S (ff_i_fubini_terminal_column_sum)) * ff_v_fubini_terminal_column_sum)) /\ exists ff_q_fubini_terminal_column_sum_partial. ff_u_fubini_terminal_column_sum = ff_q_fubini_terminal_column_sum_partial * S ((S (ff_i_fubini_terminal_column_sum)) * ff_v_fubini_terminal_column_sum) + (ff_r_fubini_terminal_column_sum))) /\ ((((exists ff_h_fubini_terminal_column_sum_successor. ff_h_fubini_terminal_column_sum_successor + S (ff_s_fubini_terminal_column_sum) = S ((S (S ff_i_fubini_terminal_column_sum)) * ff_v_fubini_terminal_column_sum)) /\ exists ff_q_fubini_terminal_column_sum_successor. ff_u_fubini_terminal_column_sum = ff_q_fubini_terminal_column_sum_successor * S ((S (S ff_i_fubini_terminal_column_sum)) * ff_v_fubini_terminal_column_sum) + (ff_s_fubini_terminal_column_sum))) /\ ff_s_fubini_terminal_column_sum = ff_r_fubini_terminal_column_sum + ff_a_fubini_terminal_column_sum)))))) -> D = M