matrix_integer_signed_selected_balance

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc r w q rb rc cb cc ub uc vb vc Ub Uc Vb Vc. (forall ics_index_selected_matrix_parents ics_value0_selected_matrix_parents ics_value1_selected_matrix_parents ics_value2_selected_matrix_parents ics_value3_selected_matrix_parents. (exists ics_gap_selected_matrix_parents_bound. ics_gap_selected_matrix_parents_bound + S (ics_index_selected_matrix_parents) = ((r) * (w))) -> (((exists fs_h_ics_selected_matrix_parents_at0. fs_h_ics_selected_matrix_parents_at0 + S (ics_value0_selected_matrix_parents) = S ((S (ics_index_selected_matrix_parents)) * ac)) /\ exists fs_q_ics_selected_matrix_parents_at0. ab = fs_q_ics_selected_matrix_parents_at0 * S ((S (ics_index_selected_matrix_parents)) * ac) + (ics_value0_selected_matrix_parents))) -> (((exists fs_h_ics_selected_matrix_parents_at1. fs_h_ics_selected_matrix_parents_at1 + S (ics_value1_selected_matrix_parents) = S ((S (ics_index_selected_matrix_parents)) * bc)) /\ exists fs_q_ics_selected_matrix_parents_at1. bb = fs_q_ics_selected_matrix_parents_at1 * S ((S (ics_index_selected_matrix_parents)) * bc) + (ics_value1_selected_matrix_parents))) -> (((exists fs_h_ics_selected_matrix_parents_at2. fs_h_ics_selected_matrix_parents_at2 + S (ics_value2_selected_matrix_parents) = S ((S (ics_index_selected_matrix_parents)) * ec)) /\ exists fs_q_ics_selected_matrix_parents_at2. eb = fs_q_ics_selected_matrix_parents_at2 * S ((S (ics_index_selected_matrix_parents)) * ec) + (ics_value2_selected_matrix_parents))) -> (((exists fs_h_ics_selected_matrix_parents_at3. fs_h_ics_selected_matrix_parents_at3 + S (ics_value3_selected_matrix_parents) = S ((S (ics_index_selected_matrix_parents)) * fc)) /\ exists fs_q_ics_selected_matrix_parents_at3. fb = fs_q_ics_selected_matrix_parents_at3 * S ((S (ics_index_selected_matrix_parents)) * fc) + (ics_value3_selected_matrix_parents))) -> ics_value0_selected_matrix_parents + ics_value3_selected_matrix_parents = ics_value2_selected_matrix_parents + ics_value1_selected_matrix_parents) -> (((forall fom_index_mrf_selected_matrix_rowsbound. (exists fom_gap_mrf_selected_matrix_rowsbound_index_bound. fom_gap_mrf_selected_matrix_rowsbound_index_bound + S (fom_index_mrf_selected_matrix_rowsbound) = q) -> exists fom_value_mrf_selected_matrix_rowsbound. ((((exists fom_beta_height_mrf_selected_matrix_rowsbound_entry. fom_beta_height_mrf_selected_matrix_rowsbound_entry + S (fom_value_mrf_selected_matrix_rowsbound) = S ((S (fom_index_mrf_selected_matrix_rowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_selected_matrix_rowsbound_entry. rb = fom_beta_quotient_mrf_selected_matrix_rowsbound_entry * S ((S (fom_index_mrf_selected_matrix_rowsbound)) * rc) + (fom_value_mrf_selected_matrix_rowsbound))) /\ (exists fom_gap_mrf_selected_matrix_rowsbound_value_bound. fom_gap_mrf_selected_matrix_rowsbound_value_bound + S (fom_value_mrf_selected_matrix_rowsbound) = r))) /\ (forall mdr_i_selected_matrix_rowsdistinct mdr_j_selected_matrix_rowsdistinct mdr_a_selected_matrix_rowsdistinct. (exists mdr_gap_selected_matrix_rowsdistincti. mdr_gap_selected_matrix_rowsdistincti + S (mdr_i_selected_matrix_rowsdistinct) = (q)) -> (exists mdr_gap_selected_matrix_rowsdistinctj. mdr_gap_selected_matrix_rowsdistinctj + S (mdr_j_selected_matrix_rowsdistinct) = (q)) -> (((exists ff_h_mdr_selected_matrix_rowsdistinctfirst. ff_h_mdr_selected_matrix_rowsdistinctfirst + S (mdr_a_selected_matrix_rowsdistinct) = S ((S (mdr_i_selected_matrix_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_matrix_rowsdistinctfirst. rb = ff_q_mdr_selected_matrix_rowsdistinctfirst * S ((S (mdr_i_selected_matrix_rowsdistinct)) * rc) + (mdr_a_selected_matrix_rowsdistinct))) -> (((exists ff_h_mdr_selected_matrix_rowsdistinctsecond. ff_h_mdr_selected_matrix_rowsdistinctsecond + S (mdr_a_selected_matrix_rowsdistinct) = S ((S (mdr_j_selected_matrix_rowsdistinct)) * rc)) /\ exists ff_q_mdr_selected_matrix_rowsdistinctsecond. rb = ff_q_mdr_selected_matrix_rowsdistinctsecond * S ((S (mdr_j_selected_matrix_rowsdistinct)) * rc) + (mdr_a_selected_matrix_rowsdistinct))) -> mdr_i_selected_matrix_rowsdistinct = mdr_j_selected_matrix_rowsdistinct))) -> (((forall fom_index_mrf_selected_matrix_columnsbound. (exists fom_gap_mrf_selected_matrix_columnsbound_index_bound. fom_gap_mrf_selected_matrix_columnsbound_index_bound + S (fom_index_mrf_selected_matrix_columnsbound) = q) -> exists fom_value_mrf_selected_matrix_columnsbound. ((((exists fom_beta_height_mrf_selected_matrix_columnsbound_entry. fom_beta_height_mrf_selected_matrix_columnsbound_entry + S (fom_value_mrf_selected_matrix_columnsbound) = S ((S (fom_index_mrf_selected_matrix_columnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_selected_matrix_columnsbound_entry. cb = fom_beta_quotient_mrf_selected_matrix_columnsbound_entry * S ((S (fom_index_mrf_selected_matrix_columnsbound)) * cc) + (fom_value_mrf_selected_matrix_columnsbound))) /\ (exists fom_gap_mrf_selected_matrix_columnsbound_value_bound. fom_gap_mrf_selected_matrix_columnsbound_value_bound + S (fom_value_mrf_selected_matrix_columnsbound) = w))) /\ (forall mdr_i_selected_matrix_columnsdistinct mdr_j_selected_matrix_columnsdistinct mdr_a_selected_matrix_columnsdistinct. (exists mdr_gap_selected_matrix_columnsdistincti. mdr_gap_selected_matrix_columnsdistincti + S (mdr_i_selected_matrix_columnsdistinct) = (q)) -> (exists mdr_gap_selected_matrix_columnsdistinctj. mdr_gap_selected_matrix_columnsdistinctj + S (mdr_j_selected_matrix_columnsdistinct) = (q)) -> (((exists ff_h_mdr_selected_matrix_columnsdistinctfirst. ff_h_mdr_selected_matrix_columnsdistinctfirst + S (mdr_a_selected_matrix_columnsdistinct) = S ((S (mdr_i_selected_matrix_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_matrix_columnsdistinctfirst. cb = ff_q_mdr_selected_matrix_columnsdistinctfirst * S ((S (mdr_i_selected_matrix_columnsdistinct)) * cc) + (mdr_a_selected_matrix_columnsdistinct))) -> (((exists ff_h_mdr_selected_matrix_columnsdistinctsecond. ff_h_mdr_selected_matrix_columnsdistinctsecond + S (mdr_a_selected_matrix_columnsdistinct) = S ((S (mdr_j_selected_matrix_columnsdistinct)) * cc)) /\ exists ff_q_mdr_selected_matrix_columnsdistinctsecond. cb = ff_q_mdr_selected_matrix_columnsdistinctsecond * S ((S (mdr_j_selected_matrix_columnsdistinct)) * cc) + (mdr_a_selected_matrix_columnsdistinct))) -> mdr_i_selected_matrix_columnsdistinct = mdr_j_selected_matrix_columnsdistinct))) -> (((forall mdr_i_first_selected_matrixpositive. (exists mdr_gap_first_selected_matrixpositivebound. mdr_gap_first_selected_matrixpositivebound + S (mdr_i_first_selected_matrixpositive) = ((q) * (q))) -> exists mdr_a_first_selected_matrixpositive. (((exists mdr_r_first_selected_matrixpositivepoint mdr_s_first_selected_matrixpositivepoint mdr_u_first_selected_matrixpositivepoint mdr_v_first_selected_matrixpositivepoint. ((mdr_i_first_selected_matrixpositive = (q) * mdr_r_first_selected_matrixpositivepoint + mdr_s_first_selected_matrixpositivepoint) /\ ((exists mdr_gap_first_selected_matrixpositivepointcolumn. mdr_gap_first_selected_matrixpositivepointcolumn + S (mdr_s_first_selected_matrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_first_selected_matrixpositivepointrow_index. ff_h_mdr_first_selected_matrixpositivepointrow_index + S (mdr_u_first_selected_matrixpositivepoint) = S ((S (mdr_r_first_selected_matrixpositivepoint)) * rc)) /\ exists ff_q_mdr_first_selected_matrixpositivepointrow_index. rb = ff_q_mdr_first_selected_matrixpositivepointrow_index * S ((S (mdr_r_first_selected_matrixpositivepoint)) * rc) + (mdr_u_first_selected_matrixpositivepoint))) /\ ((((exists ff_h_mdr_first_selected_matrixpositivepointcolumn_index. ff_h_mdr_first_selected_matrixpositivepointcolumn_index + S (mdr_v_first_selected_matrixpositivepoint) = S ((S (mdr_s_first_selected_matrixpositivepoint)) * cc)) /\ exists ff_q_mdr_first_selected_matrixpositivepointcolumn_index. cb = ff_q_mdr_first_selected_matrixpositivepointcolumn_index * S ((S (mdr_s_first_selected_matrixpositivepoint)) * cc) + (mdr_v_first_selected_matrixpositivepoint))) /\ (((exists ff_h_mdr_first_selected_matrixpositivepointsource. ff_h_mdr_first_selected_matrixpositivepointsource + S (mdr_a_first_selected_matrixpositive) = S ((S ((mdr_u_first_selected_matrixpositivepoint) * (w) + (mdr_v_first_selected_matrixpositivepoint))) * ac)) /\ exists ff_q_mdr_first_selected_matrixpositivepointsource. ab = ff_q_mdr_first_selected_matrixpositivepointsource * S ((S ((mdr_u_first_selected_matrixpositivepoint) * (w) + (mdr_v_first_selected_matrixpositivepoint))) * ac) + (mdr_a_first_selected_matrixpositive)))))))) /\ (((exists ff_h_mdr_first_selected_matrixpositiveoutput. ff_h_mdr_first_selected_matrixpositiveoutput + S (mdr_a_first_selected_matrixpositive) = S ((S (mdr_i_first_selected_matrixpositive)) * uc)) /\ exists ff_q_mdr_first_selected_matrixpositiveoutput. ub = ff_q_mdr_first_selected_matrixpositiveoutput * S ((S (mdr_i_first_selected_matrixpositive)) * uc) + (mdr_a_first_selected_matrixpositive)))))) /\ (forall mdr_i_first_selected_matrixnegative. (exists mdr_gap_first_selected_matrixnegativebound. mdr_gap_first_selected_matrixnegativebound + S (mdr_i_first_selected_matrixnegative) = ((q) * (q))) -> exists mdr_a_first_selected_matrixnegative. (((exists mdr_r_first_selected_matrixnegativepoint mdr_s_first_selected_matrixnegativepoint mdr_u_first_selected_matrixnegativepoint mdr_v_first_selected_matrixnegativepoint. ((mdr_i_first_selected_matrixnegative = (q) * mdr_r_first_selected_matrixnegativepoint + mdr_s_first_selected_matrixnegativepoint) /\ ((exists mdr_gap_first_selected_matrixnegativepointcolumn. mdr_gap_first_selected_matrixnegativepointcolumn + S (mdr_s_first_selected_matrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_first_selected_matrixnegativepointrow_index. ff_h_mdr_first_selected_matrixnegativepointrow_index + S (mdr_u_first_selected_matrixnegativepoint) = S ((S (mdr_r_first_selected_matrixnegativepoint)) * rc)) /\ exists ff_q_mdr_first_selected_matrixnegativepointrow_index. rb = ff_q_mdr_first_selected_matrixnegativepointrow_index * S ((S (mdr_r_first_selected_matrixnegativepoint)) * rc) + (mdr_u_first_selected_matrixnegativepoint))) /\ ((((exists ff_h_mdr_first_selected_matrixnegativepointcolumn_index. ff_h_mdr_first_selected_matrixnegativepointcolumn_index + S (mdr_v_first_selected_matrixnegativepoint) = S ((S (mdr_s_first_selected_matrixnegativepoint)) * cc)) /\ exists ff_q_mdr_first_selected_matrixnegativepointcolumn_index. cb = ff_q_mdr_first_selected_matrixnegativepointcolumn_index * S ((S (mdr_s_first_selected_matrixnegativepoint)) * cc) + (mdr_v_first_selected_matrixnegativepoint))) /\ (((exists ff_h_mdr_first_selected_matrixnegativepointsource. ff_h_mdr_first_selected_matrixnegativepointsource + S (mdr_a_first_selected_matrixnegative) = S ((S ((mdr_u_first_selected_matrixnegativepoint) * (w) + (mdr_v_first_selected_matrixnegativepoint))) * bc)) /\ exists ff_q_mdr_first_selected_matrixnegativepointsource. bb = ff_q_mdr_first_selected_matrixnegativepointsource * S ((S ((mdr_u_first_selected_matrixnegativepoint) * (w) + (mdr_v_first_selected_matrixnegativepoint))) * bc) + (mdr_a_first_selected_matrixnegative)))))))) /\ (((exists ff_h_mdr_first_selected_matrixnegativeoutput. ff_h_mdr_first_selected_matrixnegativeoutput + S (mdr_a_first_selected_matrixnegative) = S ((S (mdr_i_first_selected_matrixnegative)) * vc)) /\ exists ff_q_mdr_first_selected_matrixnegativeoutput. vb = ff_q_mdr_first_selected_matrixnegativeoutput * S ((S (mdr_i_first_selected_matrixnegative)) * vc) + (mdr_a_first_selected_matrixnegative)))))))) -> (((forall mdr_i_second_selected_matrixpositive. (exists mdr_gap_second_selected_matrixpositivebound. mdr_gap_second_selected_matrixpositivebound + S (mdr_i_second_selected_matrixpositive) = ((q) * (q))) -> exists mdr_a_second_selected_matrixpositive. (((exists mdr_r_second_selected_matrixpositivepoint mdr_s_second_selected_matrixpositivepoint mdr_u_second_selected_matrixpositivepoint mdr_v_second_selected_matrixpositivepoint. ((mdr_i_second_selected_matrixpositive = (q) * mdr_r_second_selected_matrixpositivepoint + mdr_s_second_selected_matrixpositivepoint) /\ ((exists mdr_gap_second_selected_matrixpositivepointcolumn. mdr_gap_second_selected_matrixpositivepointcolumn + S (mdr_s_second_selected_matrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_second_selected_matrixpositivepointrow_index. ff_h_mdr_second_selected_matrixpositivepointrow_index + S (mdr_u_second_selected_matrixpositivepoint) = S ((S (mdr_r_second_selected_matrixpositivepoint)) * rc)) /\ exists ff_q_mdr_second_selected_matrixpositivepointrow_index. rb = ff_q_mdr_second_selected_matrixpositivepointrow_index * S ((S (mdr_r_second_selected_matrixpositivepoint)) * rc) + (mdr_u_second_selected_matrixpositivepoint))) /\ ((((exists ff_h_mdr_second_selected_matrixpositivepointcolumn_index. ff_h_mdr_second_selected_matrixpositivepointcolumn_index + S (mdr_v_second_selected_matrixpositivepoint) = S ((S (mdr_s_second_selected_matrixpositivepoint)) * cc)) /\ exists ff_q_mdr_second_selected_matrixpositivepointcolumn_index. cb = ff_q_mdr_second_selected_matrixpositivepointcolumn_index * S ((S (mdr_s_second_selected_matrixpositivepoint)) * cc) + (mdr_v_second_selected_matrixpositivepoint))) /\ (((exists ff_h_mdr_second_selected_matrixpositivepointsource. ff_h_mdr_second_selected_matrixpositivepointsource + S (mdr_a_second_selected_matrixpositive) = S ((S ((mdr_u_second_selected_matrixpositivepoint) * (w) + (mdr_v_second_selected_matrixpositivepoint))) * ec)) /\ exists ff_q_mdr_second_selected_matrixpositivepointsource. eb = ff_q_mdr_second_selected_matrixpositivepointsource * S ((S ((mdr_u_second_selected_matrixpositivepoint) * (w) + (mdr_v_second_selected_matrixpositivepoint))) * ec) + (mdr_a_second_selected_matrixpositive)))))))) /\ (((exists ff_h_mdr_second_selected_matrixpositiveoutput. ff_h_mdr_second_selected_matrixpositiveoutput + S (mdr_a_second_selected_matrixpositive) = S ((S (mdr_i_second_selected_matrixpositive)) * Uc)) /\ exists ff_q_mdr_second_selected_matrixpositiveoutput. Ub = ff_q_mdr_second_selected_matrixpositiveoutput * S ((S (mdr_i_second_selected_matrixpositive)) * Uc) + (mdr_a_second_selected_matrixpositive)))))) /\ (forall mdr_i_second_selected_matrixnegative. (exists mdr_gap_second_selected_matrixnegativebound. mdr_gap_second_selected_matrixnegativebound + S (mdr_i_second_selected_matrixnegative) = ((q) * (q))) -> exists mdr_a_second_selected_matrixnegative. (((exists mdr_r_second_selected_matrixnegativepoint mdr_s_second_selected_matrixnegativepoint mdr_u_second_selected_matrixnegativepoint mdr_v_second_selected_matrixnegativepoint. ((mdr_i_second_selected_matrixnegative = (q) * mdr_r_second_selected_matrixnegativepoint + mdr_s_second_selected_matrixnegativepoint) /\ ((exists mdr_gap_second_selected_matrixnegativepointcolumn. mdr_gap_second_selected_matrixnegativepointcolumn + S (mdr_s_second_selected_matrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_second_selected_matrixnegativepointrow_index. ff_h_mdr_second_selected_matrixnegativepointrow_index + S (mdr_u_second_selected_matrixnegativepoint) = S ((S (mdr_r_second_selected_matrixnegativepoint)) * rc)) /\ exists ff_q_mdr_second_selected_matrixnegativepointrow_index. rb = ff_q_mdr_second_selected_matrixnegativepointrow_index * S ((S (mdr_r_second_selected_matrixnegativepoint)) * rc) + (mdr_u_second_selected_matrixnegativepoint))) /\ ((((exists ff_h_mdr_second_selected_matrixnegativepointcolumn_index. ff_h_mdr_second_selected_matrixnegativepointcolumn_index + S (mdr_v_second_selected_matrixnegativepoint) = S ((S (mdr_s_second_selected_matrixnegativepoint)) * cc)) /\ exists ff_q_mdr_second_selected_matrixnegativepointcolumn_index. cb = ff_q_mdr_second_selected_matrixnegativepointcolumn_index * S ((S (mdr_s_second_selected_matrixnegativepoint)) * cc) + (mdr_v_second_selected_matrixnegativepoint))) /\ (((exists ff_h_mdr_second_selected_matrixnegativepointsource. ff_h_mdr_second_selected_matrixnegativepointsource + S (mdr_a_second_selected_matrixnegative) = S ((S ((mdr_u_second_selected_matrixnegativepoint) * (w) + (mdr_v_second_selected_matrixnegativepoint))) * fc)) /\ exists ff_q_mdr_second_selected_matrixnegativepointsource. fb = ff_q_mdr_second_selected_matrixnegativepointsource * S ((S ((mdr_u_second_selected_matrixnegativepoint) * (w) + (mdr_v_second_selected_matrixnegativepoint))) * fc) + (mdr_a_second_selected_matrixnegative)))))))) /\ (((exists ff_h_mdr_second_selected_matrixnegativeoutput. ff_h_mdr_second_selected_matrixnegativeoutput + S (mdr_a_second_selected_matrixnegative) = S ((S (mdr_i_second_selected_matrixnegative)) * Vc)) /\ exists ff_q_mdr_second_selected_matrixnegativeoutput. Vb = ff_q_mdr_second_selected_matrixnegativeoutput * S ((S (mdr_i_second_selected_matrixnegative)) * Vc) + (mdr_a_second_selected_matrixnegative)))))))) -> (forall ics_index_selected_matrices_equal ics_value0_selected_matrices_equal ics_value1_selected_matrices_equal ics_value2_selected_matrices_equal ics_value3_selected_matrices_equal. (exists ics_gap_selected_matrices_equal_bound. ics_gap_selected_matrices_equal_bound + S (ics_index_selected_matrices_equal) = ((q) * (q))) -> (((exists fs_h_ics_selected_matrices_equal_at0. fs_h_ics_selected_matrices_equal_at0 + S (ics_value0_selected_matrices_equal) = S ((S (ics_index_selected_matrices_equal)) * uc)) /\ exists fs_q_ics_selected_matrices_equal_at0. ub = fs_q_ics_selected_matrices_equal_at0 * S ((S (ics_index_selected_matrices_equal)) * uc) + (ics_value0_selected_matrices_equal))) -> (((exists fs_h_ics_selected_matrices_equal_at1. fs_h_ics_selected_matrices_equal_at1 + S (ics_value1_selected_matrices_equal) = S ((S (ics_index_selected_matrices_equal)) * vc)) /\ exists fs_q_ics_selected_matrices_equal_at1. vb = fs_q_ics_selected_matrices_equal_at1 * S ((S (ics_index_selected_matrices_equal)) * vc) + (ics_value1_selected_matrices_equal))) -> (((exists fs_h_ics_selected_matrices_equal_at2. fs_h_ics_selected_matrices_equal_at2 + S (ics_value2_selected_matrices_equal) = S ((S (ics_index_selected_matrices_equal)) * Uc)) /\ exists fs_q_ics_selected_matrices_equal_at2. Ub = fs_q_ics_selected_matrices_equal_at2 * S ((S (ics_index_selected_matrices_equal)) * Uc) + (ics_value2_selected_matrices_equal))) -> (((exists fs_h_ics_selected_matrices_equal_at3. fs_h_ics_selected_matrices_equal_at3 + S (ics_value3_selected_matrices_equal) = S ((S (ics_index_selected_matrices_equal)) * Vc)) /\ exists fs_q_ics_selected_matrices_equal_at3. Vb = fs_q_ics_selected_matrices_equal_at3 * S ((S (ics_index_selected_matrices_equal)) * Vc) + (ics_value3_selected_matrices_equal))) -> ics_value0_selected_matrices_equal + ics_value3_selected_matrices_equal = ics_value2_selected_matrices_equal + ics_value1_selected_matrices_equal)