matrix_rank_signed_selected_square_functional

Exact expanded first-order arithmetic statement

forall pb pc nb nc w rb rc cb cc q ub uc vb vc Ub Uc Vb Vc. (((forall mdr_i_first_selectedpositive. (exists mdr_gap_first_selectedpositivebound. mdr_gap_first_selectedpositivebound + S (mdr_i_first_selectedpositive) = ((q) * (q))) -> exists mdr_a_first_selectedpositive. (((exists mdr_r_first_selectedpositivepoint mdr_s_first_selectedpositivepoint mdr_u_first_selectedpositivepoint mdr_v_first_selectedpositivepoint. ((mdr_i_first_selectedpositive = (q) * mdr_r_first_selectedpositivepoint + mdr_s_first_selectedpositivepoint) /\ ((exists mdr_gap_first_selectedpositivepointcolumn. mdr_gap_first_selectedpositivepointcolumn + S (mdr_s_first_selectedpositivepoint) = (q)) /\ ((((exists ff_h_mdr_first_selectedpositivepointrow_index. ff_h_mdr_first_selectedpositivepointrow_index + S (mdr_u_first_selectedpositivepoint) = S ((S (mdr_r_first_selectedpositivepoint)) * rc)) /\ exists ff_q_mdr_first_selectedpositivepointrow_index. rb = ff_q_mdr_first_selectedpositivepointrow_index * S ((S (mdr_r_first_selectedpositivepoint)) * rc) + (mdr_u_first_selectedpositivepoint))) /\ ((((exists ff_h_mdr_first_selectedpositivepointcolumn_index. ff_h_mdr_first_selectedpositivepointcolumn_index + S (mdr_v_first_selectedpositivepoint) = S ((S (mdr_s_first_selectedpositivepoint)) * cc)) /\ exists ff_q_mdr_first_selectedpositivepointcolumn_index. cb = ff_q_mdr_first_selectedpositivepointcolumn_index * S ((S (mdr_s_first_selectedpositivepoint)) * cc) + (mdr_v_first_selectedpositivepoint))) /\ (((exists ff_h_mdr_first_selectedpositivepointsource. ff_h_mdr_first_selectedpositivepointsource + S (mdr_a_first_selectedpositive) = S ((S ((mdr_u_first_selectedpositivepoint) * (w) + (mdr_v_first_selectedpositivepoint))) * pc)) /\ exists ff_q_mdr_first_selectedpositivepointsource. pb = ff_q_mdr_first_selectedpositivepointsource * S ((S ((mdr_u_first_selectedpositivepoint) * (w) + (mdr_v_first_selectedpositivepoint))) * pc) + (mdr_a_first_selectedpositive)))))))) /\ (((exists ff_h_mdr_first_selectedpositiveoutput. ff_h_mdr_first_selectedpositiveoutput + S (mdr_a_first_selectedpositive) = S ((S (mdr_i_first_selectedpositive)) * uc)) /\ exists ff_q_mdr_first_selectedpositiveoutput. ub = ff_q_mdr_first_selectedpositiveoutput * S ((S (mdr_i_first_selectedpositive)) * uc) + (mdr_a_first_selectedpositive)))))) /\ (forall mdr_i_first_selectednegative. (exists mdr_gap_first_selectednegativebound. mdr_gap_first_selectednegativebound + S (mdr_i_first_selectednegative) = ((q) * (q))) -> exists mdr_a_first_selectednegative. (((exists mdr_r_first_selectednegativepoint mdr_s_first_selectednegativepoint mdr_u_first_selectednegativepoint mdr_v_first_selectednegativepoint. ((mdr_i_first_selectednegative = (q) * mdr_r_first_selectednegativepoint + mdr_s_first_selectednegativepoint) /\ ((exists mdr_gap_first_selectednegativepointcolumn. mdr_gap_first_selectednegativepointcolumn + S (mdr_s_first_selectednegativepoint) = (q)) /\ ((((exists ff_h_mdr_first_selectednegativepointrow_index. ff_h_mdr_first_selectednegativepointrow_index + S (mdr_u_first_selectednegativepoint) = S ((S (mdr_r_first_selectednegativepoint)) * rc)) /\ exists ff_q_mdr_first_selectednegativepointrow_index. rb = ff_q_mdr_first_selectednegativepointrow_index * S ((S (mdr_r_first_selectednegativepoint)) * rc) + (mdr_u_first_selectednegativepoint))) /\ ((((exists ff_h_mdr_first_selectednegativepointcolumn_index. ff_h_mdr_first_selectednegativepointcolumn_index + S (mdr_v_first_selectednegativepoint) = S ((S (mdr_s_first_selectednegativepoint)) * cc)) /\ exists ff_q_mdr_first_selectednegativepointcolumn_index. cb = ff_q_mdr_first_selectednegativepointcolumn_index * S ((S (mdr_s_first_selectednegativepoint)) * cc) + (mdr_v_first_selectednegativepoint))) /\ (((exists ff_h_mdr_first_selectednegativepointsource. ff_h_mdr_first_selectednegativepointsource + S (mdr_a_first_selectednegative) = S ((S ((mdr_u_first_selectednegativepoint) * (w) + (mdr_v_first_selectednegativepoint))) * nc)) /\ exists ff_q_mdr_first_selectednegativepointsource. nb = ff_q_mdr_first_selectednegativepointsource * S ((S ((mdr_u_first_selectednegativepoint) * (w) + (mdr_v_first_selectednegativepoint))) * nc) + (mdr_a_first_selectednegative)))))))) /\ (((exists ff_h_mdr_first_selectednegativeoutput. ff_h_mdr_first_selectednegativeoutput + S (mdr_a_first_selectednegative) = S ((S (mdr_i_first_selectednegative)) * vc)) /\ exists ff_q_mdr_first_selectednegativeoutput. vb = ff_q_mdr_first_selectednegativeoutput * S ((S (mdr_i_first_selectednegative)) * vc) + (mdr_a_first_selectednegative)))))))) -> (((forall mdr_i_second_selectedpositive. (exists mdr_gap_second_selectedpositivebound. mdr_gap_second_selectedpositivebound + S (mdr_i_second_selectedpositive) = ((q) * (q))) -> exists mdr_a_second_selectedpositive. (((exists mdr_r_second_selectedpositivepoint mdr_s_second_selectedpositivepoint mdr_u_second_selectedpositivepoint mdr_v_second_selectedpositivepoint. ((mdr_i_second_selectedpositive = (q) * mdr_r_second_selectedpositivepoint + mdr_s_second_selectedpositivepoint) /\ ((exists mdr_gap_second_selectedpositivepointcolumn. mdr_gap_second_selectedpositivepointcolumn + S (mdr_s_second_selectedpositivepoint) = (q)) /\ ((((exists ff_h_mdr_second_selectedpositivepointrow_index. ff_h_mdr_second_selectedpositivepointrow_index + S (mdr_u_second_selectedpositivepoint) = S ((S (mdr_r_second_selectedpositivepoint)) * rc)) /\ exists ff_q_mdr_second_selectedpositivepointrow_index. rb = ff_q_mdr_second_selectedpositivepointrow_index * S ((S (mdr_r_second_selectedpositivepoint)) * rc) + (mdr_u_second_selectedpositivepoint))) /\ ((((exists ff_h_mdr_second_selectedpositivepointcolumn_index. ff_h_mdr_second_selectedpositivepointcolumn_index + S (mdr_v_second_selectedpositivepoint) = S ((S (mdr_s_second_selectedpositivepoint)) * cc)) /\ exists ff_q_mdr_second_selectedpositivepointcolumn_index. cb = ff_q_mdr_second_selectedpositivepointcolumn_index * S ((S (mdr_s_second_selectedpositivepoint)) * cc) + (mdr_v_second_selectedpositivepoint))) /\ (((exists ff_h_mdr_second_selectedpositivepointsource. ff_h_mdr_second_selectedpositivepointsource + S (mdr_a_second_selectedpositive) = S ((S ((mdr_u_second_selectedpositivepoint) * (w) + (mdr_v_second_selectedpositivepoint))) * pc)) /\ exists ff_q_mdr_second_selectedpositivepointsource. pb = ff_q_mdr_second_selectedpositivepointsource * S ((S ((mdr_u_second_selectedpositivepoint) * (w) + (mdr_v_second_selectedpositivepoint))) * pc) + (mdr_a_second_selectedpositive)))))))) /\ (((exists ff_h_mdr_second_selectedpositiveoutput. ff_h_mdr_second_selectedpositiveoutput + S (mdr_a_second_selectedpositive) = S ((S (mdr_i_second_selectedpositive)) * Uc)) /\ exists ff_q_mdr_second_selectedpositiveoutput. Ub = ff_q_mdr_second_selectedpositiveoutput * S ((S (mdr_i_second_selectedpositive)) * Uc) + (mdr_a_second_selectedpositive)))))) /\ (forall mdr_i_second_selectednegative. (exists mdr_gap_second_selectednegativebound. mdr_gap_second_selectednegativebound + S (mdr_i_second_selectednegative) = ((q) * (q))) -> exists mdr_a_second_selectednegative. (((exists mdr_r_second_selectednegativepoint mdr_s_second_selectednegativepoint mdr_u_second_selectednegativepoint mdr_v_second_selectednegativepoint. ((mdr_i_second_selectednegative = (q) * mdr_r_second_selectednegativepoint + mdr_s_second_selectednegativepoint) /\ ((exists mdr_gap_second_selectednegativepointcolumn. mdr_gap_second_selectednegativepointcolumn + S (mdr_s_second_selectednegativepoint) = (q)) /\ ((((exists ff_h_mdr_second_selectednegativepointrow_index. ff_h_mdr_second_selectednegativepointrow_index + S (mdr_u_second_selectednegativepoint) = S ((S (mdr_r_second_selectednegativepoint)) * rc)) /\ exists ff_q_mdr_second_selectednegativepointrow_index. rb = ff_q_mdr_second_selectednegativepointrow_index * S ((S (mdr_r_second_selectednegativepoint)) * rc) + (mdr_u_second_selectednegativepoint))) /\ ((((exists ff_h_mdr_second_selectednegativepointcolumn_index. ff_h_mdr_second_selectednegativepointcolumn_index + S (mdr_v_second_selectednegativepoint) = S ((S (mdr_s_second_selectednegativepoint)) * cc)) /\ exists ff_q_mdr_second_selectednegativepointcolumn_index. cb = ff_q_mdr_second_selectednegativepointcolumn_index * S ((S (mdr_s_second_selectednegativepoint)) * cc) + (mdr_v_second_selectednegativepoint))) /\ (((exists ff_h_mdr_second_selectednegativepointsource. ff_h_mdr_second_selectednegativepointsource + S (mdr_a_second_selectednegative) = S ((S ((mdr_u_second_selectednegativepoint) * (w) + (mdr_v_second_selectednegativepoint))) * nc)) /\ exists ff_q_mdr_second_selectednegativepointsource. nb = ff_q_mdr_second_selectednegativepointsource * S ((S ((mdr_u_second_selectednegativepoint) * (w) + (mdr_v_second_selectednegativepoint))) * nc) + (mdr_a_second_selectednegative)))))))) /\ (((exists ff_h_mdr_second_selectednegativeoutput. ff_h_mdr_second_selectednegativeoutput + S (mdr_a_second_selectednegative) = S ((S (mdr_i_second_selectednegative)) * Vc)) /\ exists ff_q_mdr_second_selectednegativeoutput. Vb = ff_q_mdr_second_selectednegativeoutput * S ((S (mdr_i_second_selectednegative)) * Vc) + (mdr_a_second_selectednegative)))))))) -> (((forall mdr_i_signed_selected_equalp mdr_a_signed_selected_equalp. (exists mdr_gap_signed_selected_equalpb. mdr_gap_signed_selected_equalpb + S (mdr_i_signed_selected_equalp) = ((q) * (q))) -> (((exists ff_h_mdr_signed_selected_equalpo. ff_h_mdr_signed_selected_equalpo + S (mdr_a_signed_selected_equalp) = S ((S (mdr_i_signed_selected_equalp)) * uc)) /\ exists ff_q_mdr_signed_selected_equalpo. ub = ff_q_mdr_signed_selected_equalpo * S ((S (mdr_i_signed_selected_equalp)) * uc) + (mdr_a_signed_selected_equalp))) -> (((exists ff_h_mdr_signed_selected_equalpn. ff_h_mdr_signed_selected_equalpn + S (mdr_a_signed_selected_equalp) = S ((S (mdr_i_signed_selected_equalp)) * Uc)) /\ exists ff_q_mdr_signed_selected_equalpn. Ub = ff_q_mdr_signed_selected_equalpn * S ((S (mdr_i_signed_selected_equalp)) * Uc) + (mdr_a_signed_selected_equalp)))) /\ (forall mdr_i_signed_selected_equaln mdr_a_signed_selected_equaln. (exists mdr_gap_signed_selected_equalnb. mdr_gap_signed_selected_equalnb + S (mdr_i_signed_selected_equaln) = ((q) * (q))) -> (((exists ff_h_mdr_signed_selected_equalno. ff_h_mdr_signed_selected_equalno + S (mdr_a_signed_selected_equaln) = S ((S (mdr_i_signed_selected_equaln)) * vc)) /\ exists ff_q_mdr_signed_selected_equalno. vb = ff_q_mdr_signed_selected_equalno * S ((S (mdr_i_signed_selected_equaln)) * vc) + (mdr_a_signed_selected_equaln))) -> (((exists ff_h_mdr_signed_selected_equalnn. ff_h_mdr_signed_selected_equalnn + S (mdr_a_signed_selected_equaln) = S ((S (mdr_i_signed_selected_equaln)) * Vc)) /\ exists ff_q_mdr_signed_selected_equalnn. Vb = ff_q_mdr_signed_selected_equalnn * S ((S (mdr_i_signed_selected_equaln)) * Vc) + (mdr_a_signed_selected_equaln))))))