matrix_rank_signed_selected_square_exists

forall pb pc nb nc w rb rc cb cc q. exists ub uc vb vc. (((forall mdr_i_signed_square_existspositive. (exists mdr_gap_signed_square_existspositivebound. mdr_gap_signed_square_existspositivebound + S (mdr_i_signed_square_existspositive) = ((q) * (q))) -> exists mdr_a_signed_square_existspositive. (((exists mdr_r_signed_square_existspositivepoint mdr_s_signed_square_existspositivepoint mdr_u_signed_square_existspositivepoint mdr_v_signed_square_existspositivepoint. ((mdr_i_signed_square_existspositive = (q) * mdr_r_signed_square_existspositivepoint + mdr_s_signed_square_existspositivepoint) /\ ((exists mdr_gap_signed_square_existspositivepointcolumn. mdr_gap_signed_square_existspositivepointcolumn + S (mdr_s_signed_square_existspositivepoint) = (q)) /\ ((((exists ff_h_mdr_signed_square_existspositivepointrow_index. ff_h_mdr_signed_square_existspositivepointrow_index + S (mdr_u_signed_square_existspositivepoint) = S ((S (mdr_r_signed_square_existspositivepoint)) * rc)) /\ exists ff_q_mdr_signed_square_existspositivepointrow_index. rb = ff_q_mdr_signed_square_existspositivepointrow_index * S ((S (mdr_r_signed_square_existspositivepoint)) * rc) + (mdr_u_signed_square_existspositivepoint))) /\ ((((exists ff_h_mdr_signed_square_existspositivepointcolumn_index. ff_h_mdr_signed_square_existspositivepointcolumn_index + S (mdr_v_signed_square_existspositivepoint) = S ((S (mdr_s_signed_square_existspositivepoint)) * cc)) /\ exists ff_q_mdr_signed_square_existspositivepointcolumn_index. cb = ff_q_mdr_signed_square_existspositivepointcolumn_index * S ((S (mdr_s_signed_square_existspositivepoint)) * cc) + (mdr_v_signed_square_existspositivepoint))) /\ (((exists ff_h_mdr_signed_square_existspositivepointsource. ff_h_mdr_signed_square_existspositivepointsource + S (mdr_a_signed_square_existspositive) = S ((S ((mdr_u_signed_square_existspositivepoint) * (w) + (mdr_v_signed_square_existspositivepoint))) * pc)) /\ exists ff_q_mdr_signed_square_existspositivepointsource. pb = ff_q_mdr_signed_square_existspositivepointsource * S ((S ((mdr_u_signed_square_existspositivepoint) * (w) + (mdr_v_signed_square_existspositivepoint))) * pc) + (mdr_a_signed_square_existspositive)))))))) /\ (((exists ff_h_mdr_signed_square_existspositiveoutput. ff_h_mdr_signed_square_existspositiveoutput + S (mdr_a_signed_square_existspositive) = S ((S (mdr_i_signed_square_existspositive)) * uc)) /\ exists ff_q_mdr_signed_square_existspositiveoutput. ub = ff_q_mdr_signed_square_existspositiveoutput * S ((S (mdr_i_signed_square_existspositive)) * uc) + (mdr_a_signed_square_existspositive)))))) /\ (forall mdr_i_signed_square_existsnegative. (exists mdr_gap_signed_square_existsnegativebound. mdr_gap_signed_square_existsnegativebound + S (mdr_i_signed_square_existsnegative) = ((q) * (q))) -> exists mdr_a_signed_square_existsnegative. (((exists mdr_r_signed_square_existsnegativepoint mdr_s_signed_square_existsnegativepoint mdr_u_signed_square_existsnegativepoint mdr_v_signed_square_existsnegativepoint. ((mdr_i_signed_square_existsnegative = (q) * mdr_r_signed_square_existsnegativepoint + mdr_s_signed_square_existsnegativepoint) /\ ((exists mdr_gap_signed_square_existsnegativepointcolumn. mdr_gap_signed_square_existsnegativepointcolumn + S (mdr_s_signed_square_existsnegativepoint) = (q)) /\ ((((exists ff_h_mdr_signed_square_existsnegativepointrow_index. ff_h_mdr_signed_square_existsnegativepointrow_index + S (mdr_u_signed_square_existsnegativepoint) = S ((S (mdr_r_signed_square_existsnegativepoint)) * rc)) /\ exists ff_q_mdr_signed_square_existsnegativepointrow_index. rb = ff_q_mdr_signed_square_existsnegativepointrow_index * S ((S (mdr_r_signed_square_existsnegativepoint)) * rc) + (mdr_u_signed_square_existsnegativepoint))) /\ ((((exists ff_h_mdr_signed_square_existsnegativepointcolumn_index. ff_h_mdr_signed_square_existsnegativepointcolumn_index + S (mdr_v_signed_square_existsnegativepoint) = S ((S (mdr_s_signed_square_existsnegativepoint)) * cc)) /\ exists ff_q_mdr_signed_square_existsnegativepointcolumn_index. cb = ff_q_mdr_signed_square_existsnegativepointcolumn_index * S ((S (mdr_s_signed_square_existsnegativepoint)) * cc) + (mdr_v_signed_square_existsnegativepoint))) /\ (((exists ff_h_mdr_signed_square_existsnegativepointsource. ff_h_mdr_signed_square_existsnegativepointsource + S (mdr_a_signed_square_existsnegative) = S ((S ((mdr_u_signed_square_existsnegativepoint) * (w) + (mdr_v_signed_square_existsnegativepoint))) * nc)) /\ exists ff_q_mdr_signed_square_existsnegativepointsource. nb = ff_q_mdr_signed_square_existsnegativepointsource * S ((S ((mdr_u_signed_square_existsnegativepoint) * (w) + (mdr_v_signed_square_existsnegativepoint))) * nc) + (mdr_a_signed_square_existsnegative)))))))) /\ (((exists ff_h_mdr_signed_square_existsnegativeoutput. ff_h_mdr_signed_square_existsnegativeoutput + S (mdr_a_signed_square_existsnegative) = S ((S (mdr_i_signed_square_existsnegative)) * vc)) /\ exists ff_q_mdr_signed_square_existsnegativeoutput. vb = ff_q_mdr_signed_square_existsnegativeoutput * S ((S (mdr_i_signed_square_existsnegative)) * vc) + (mdr_a_signed_square_existsnegative))))))))