matrix_rank_signed_selected_selector_transport

Exact expanded first-order arithmetic statement

forall pb pc nb nc w rb rc cb cc q Rb Rc Cb Cc ub uc vb vc. (forall mdr_i_signed_rows mdr_a_signed_rows. (exists mdr_gap_signed_rowsb. mdr_gap_signed_rowsb + S (mdr_i_signed_rows) = (q)) -> (((exists ff_h_mdr_signed_rowso. ff_h_mdr_signed_rowso + S (mdr_a_signed_rows) = S ((S (mdr_i_signed_rows)) * rc)) /\ exists ff_q_mdr_signed_rowso. rb = ff_q_mdr_signed_rowso * S ((S (mdr_i_signed_rows)) * rc) + (mdr_a_signed_rows))) -> (((exists ff_h_mdr_signed_rowsn. ff_h_mdr_signed_rowsn + S (mdr_a_signed_rows) = S ((S (mdr_i_signed_rows)) * Rc)) /\ exists ff_q_mdr_signed_rowsn. Rb = ff_q_mdr_signed_rowsn * S ((S (mdr_i_signed_rows)) * Rc) + (mdr_a_signed_rows)))) -> (forall mdr_i_signed_columns mdr_a_signed_columns. (exists mdr_gap_signed_columnsb. mdr_gap_signed_columnsb + S (mdr_i_signed_columns) = (q)) -> (((exists ff_h_mdr_signed_columnso. ff_h_mdr_signed_columnso + S (mdr_a_signed_columns) = S ((S (mdr_i_signed_columns)) * cc)) /\ exists ff_q_mdr_signed_columnso. cb = ff_q_mdr_signed_columnso * S ((S (mdr_i_signed_columns)) * cc) + (mdr_a_signed_columns))) -> (((exists ff_h_mdr_signed_columnsn. ff_h_mdr_signed_columnsn + S (mdr_a_signed_columns) = S ((S (mdr_i_signed_columns)) * Cc)) /\ exists ff_q_mdr_signed_columnsn. Cb = ff_q_mdr_signed_columnsn * S ((S (mdr_i_signed_columns)) * Cc) + (mdr_a_signed_columns)))) -> (((forall mdr_i_signed_selected_sourcepositive. (exists mdr_gap_signed_selected_sourcepositivebound. mdr_gap_signed_selected_sourcepositivebound + S (mdr_i_signed_selected_sourcepositive) = ((q) * (q))) -> exists mdr_a_signed_selected_sourcepositive. (((exists mdr_r_signed_selected_sourcepositivepoint mdr_s_signed_selected_sourcepositivepoint mdr_u_signed_selected_sourcepositivepoint mdr_v_signed_selected_sourcepositivepoint. ((mdr_i_signed_selected_sourcepositive = (q) * mdr_r_signed_selected_sourcepositivepoint + mdr_s_signed_selected_sourcepositivepoint) /\ ((exists mdr_gap_signed_selected_sourcepositivepointcolumn. mdr_gap_signed_selected_sourcepositivepointcolumn + S (mdr_s_signed_selected_sourcepositivepoint) = (q)) /\ ((((exists ff_h_mdr_signed_selected_sourcepositivepointrow_index. ff_h_mdr_signed_selected_sourcepositivepointrow_index + S (mdr_u_signed_selected_sourcepositivepoint) = S ((S (mdr_r_signed_selected_sourcepositivepoint)) * rc)) /\ exists ff_q_mdr_signed_selected_sourcepositivepointrow_index. rb = ff_q_mdr_signed_selected_sourcepositivepointrow_index * S ((S (mdr_r_signed_selected_sourcepositivepoint)) * rc) + (mdr_u_signed_selected_sourcepositivepoint))) /\ ((((exists ff_h_mdr_signed_selected_sourcepositivepointcolumn_index. ff_h_mdr_signed_selected_sourcepositivepointcolumn_index + S (mdr_v_signed_selected_sourcepositivepoint) = S ((S (mdr_s_signed_selected_sourcepositivepoint)) * cc)) /\ exists ff_q_mdr_signed_selected_sourcepositivepointcolumn_index. cb = ff_q_mdr_signed_selected_sourcepositivepointcolumn_index * S ((S (mdr_s_signed_selected_sourcepositivepoint)) * cc) + (mdr_v_signed_selected_sourcepositivepoint))) /\ (((exists ff_h_mdr_signed_selected_sourcepositivepointsource. ff_h_mdr_signed_selected_sourcepositivepointsource + S (mdr_a_signed_selected_sourcepositive) = S ((S ((mdr_u_signed_selected_sourcepositivepoint) * (w) + (mdr_v_signed_selected_sourcepositivepoint))) * pc)) /\ exists ff_q_mdr_signed_selected_sourcepositivepointsource. pb = ff_q_mdr_signed_selected_sourcepositivepointsource * S ((S ((mdr_u_signed_selected_sourcepositivepoint) * (w) + (mdr_v_signed_selected_sourcepositivepoint))) * pc) + (mdr_a_signed_selected_sourcepositive)))))))) /\ (((exists ff_h_mdr_signed_selected_sourcepositiveoutput. ff_h_mdr_signed_selected_sourcepositiveoutput + S (mdr_a_signed_selected_sourcepositive) = S ((S (mdr_i_signed_selected_sourcepositive)) * uc)) /\ exists ff_q_mdr_signed_selected_sourcepositiveoutput. ub = ff_q_mdr_signed_selected_sourcepositiveoutput * S ((S (mdr_i_signed_selected_sourcepositive)) * uc) + (mdr_a_signed_selected_sourcepositive)))))) /\ (forall mdr_i_signed_selected_sourcenegative. (exists mdr_gap_signed_selected_sourcenegativebound. mdr_gap_signed_selected_sourcenegativebound + S (mdr_i_signed_selected_sourcenegative) = ((q) * (q))) -> exists mdr_a_signed_selected_sourcenegative. (((exists mdr_r_signed_selected_sourcenegativepoint mdr_s_signed_selected_sourcenegativepoint mdr_u_signed_selected_sourcenegativepoint mdr_v_signed_selected_sourcenegativepoint. ((mdr_i_signed_selected_sourcenegative = (q) * mdr_r_signed_selected_sourcenegativepoint + mdr_s_signed_selected_sourcenegativepoint) /\ ((exists mdr_gap_signed_selected_sourcenegativepointcolumn. mdr_gap_signed_selected_sourcenegativepointcolumn + S (mdr_s_signed_selected_sourcenegativepoint) = (q)) /\ ((((exists ff_h_mdr_signed_selected_sourcenegativepointrow_index. ff_h_mdr_signed_selected_sourcenegativepointrow_index + S (mdr_u_signed_selected_sourcenegativepoint) = S ((S (mdr_r_signed_selected_sourcenegativepoint)) * rc)) /\ exists ff_q_mdr_signed_selected_sourcenegativepointrow_index. rb = ff_q_mdr_signed_selected_sourcenegativepointrow_index * S ((S (mdr_r_signed_selected_sourcenegativepoint)) * rc) + (mdr_u_signed_selected_sourcenegativepoint))) /\ ((((exists ff_h_mdr_signed_selected_sourcenegativepointcolumn_index. ff_h_mdr_signed_selected_sourcenegativepointcolumn_index + S (mdr_v_signed_selected_sourcenegativepoint) = S ((S (mdr_s_signed_selected_sourcenegativepoint)) * cc)) /\ exists ff_q_mdr_signed_selected_sourcenegativepointcolumn_index. cb = ff_q_mdr_signed_selected_sourcenegativepointcolumn_index * S ((S (mdr_s_signed_selected_sourcenegativepoint)) * cc) + (mdr_v_signed_selected_sourcenegativepoint))) /\ (((exists ff_h_mdr_signed_selected_sourcenegativepointsource. ff_h_mdr_signed_selected_sourcenegativepointsource + S (mdr_a_signed_selected_sourcenegative) = S ((S ((mdr_u_signed_selected_sourcenegativepoint) * (w) + (mdr_v_signed_selected_sourcenegativepoint))) * nc)) /\ exists ff_q_mdr_signed_selected_sourcenegativepointsource. nb = ff_q_mdr_signed_selected_sourcenegativepointsource * S ((S ((mdr_u_signed_selected_sourcenegativepoint) * (w) + (mdr_v_signed_selected_sourcenegativepoint))) * nc) + (mdr_a_signed_selected_sourcenegative)))))))) /\ (((exists ff_h_mdr_signed_selected_sourcenegativeoutput. ff_h_mdr_signed_selected_sourcenegativeoutput + S (mdr_a_signed_selected_sourcenegative) = S ((S (mdr_i_signed_selected_sourcenegative)) * vc)) /\ exists ff_q_mdr_signed_selected_sourcenegativeoutput. vb = ff_q_mdr_signed_selected_sourcenegativeoutput * S ((S (mdr_i_signed_selected_sourcenegative)) * vc) + (mdr_a_signed_selected_sourcenegative)))))))) -> (((forall mdr_i_signed_selected_targetpositive. (exists mdr_gap_signed_selected_targetpositivebound. mdr_gap_signed_selected_targetpositivebound + S (mdr_i_signed_selected_targetpositive) = ((q) * (q))) -> exists mdr_a_signed_selected_targetpositive. (((exists mdr_r_signed_selected_targetpositivepoint mdr_s_signed_selected_targetpositivepoint mdr_u_signed_selected_targetpositivepoint mdr_v_signed_selected_targetpositivepoint. ((mdr_i_signed_selected_targetpositive = (q) * mdr_r_signed_selected_targetpositivepoint + mdr_s_signed_selected_targetpositivepoint) /\ ((exists mdr_gap_signed_selected_targetpositivepointcolumn. mdr_gap_signed_selected_targetpositivepointcolumn + S (mdr_s_signed_selected_targetpositivepoint) = (q)) /\ ((((exists ff_h_mdr_signed_selected_targetpositivepointrow_index. ff_h_mdr_signed_selected_targetpositivepointrow_index + S (mdr_u_signed_selected_targetpositivepoint) = S ((S (mdr_r_signed_selected_targetpositivepoint)) * Rc)) /\ exists ff_q_mdr_signed_selected_targetpositivepointrow_index. Rb = ff_q_mdr_signed_selected_targetpositivepointrow_index * S ((S (mdr_r_signed_selected_targetpositivepoint)) * Rc) + (mdr_u_signed_selected_targetpositivepoint))) /\ ((((exists ff_h_mdr_signed_selected_targetpositivepointcolumn_index. ff_h_mdr_signed_selected_targetpositivepointcolumn_index + S (mdr_v_signed_selected_targetpositivepoint) = S ((S (mdr_s_signed_selected_targetpositivepoint)) * Cc)) /\ exists ff_q_mdr_signed_selected_targetpositivepointcolumn_index. Cb = ff_q_mdr_signed_selected_targetpositivepointcolumn_index * S ((S (mdr_s_signed_selected_targetpositivepoint)) * Cc) + (mdr_v_signed_selected_targetpositivepoint))) /\ (((exists ff_h_mdr_signed_selected_targetpositivepointsource. ff_h_mdr_signed_selected_targetpositivepointsource + S (mdr_a_signed_selected_targetpositive) = S ((S ((mdr_u_signed_selected_targetpositivepoint) * (w) + (mdr_v_signed_selected_targetpositivepoint))) * pc)) /\ exists ff_q_mdr_signed_selected_targetpositivepointsource. pb = ff_q_mdr_signed_selected_targetpositivepointsource * S ((S ((mdr_u_signed_selected_targetpositivepoint) * (w) + (mdr_v_signed_selected_targetpositivepoint))) * pc) + (mdr_a_signed_selected_targetpositive)))))))) /\ (((exists ff_h_mdr_signed_selected_targetpositiveoutput. ff_h_mdr_signed_selected_targetpositiveoutput + S (mdr_a_signed_selected_targetpositive) = S ((S (mdr_i_signed_selected_targetpositive)) * uc)) /\ exists ff_q_mdr_signed_selected_targetpositiveoutput. ub = ff_q_mdr_signed_selected_targetpositiveoutput * S ((S (mdr_i_signed_selected_targetpositive)) * uc) + (mdr_a_signed_selected_targetpositive)))))) /\ (forall mdr_i_signed_selected_targetnegative. (exists mdr_gap_signed_selected_targetnegativebound. mdr_gap_signed_selected_targetnegativebound + S (mdr_i_signed_selected_targetnegative) = ((q) * (q))) -> exists mdr_a_signed_selected_targetnegative. (((exists mdr_r_signed_selected_targetnegativepoint mdr_s_signed_selected_targetnegativepoint mdr_u_signed_selected_targetnegativepoint mdr_v_signed_selected_targetnegativepoint. ((mdr_i_signed_selected_targetnegative = (q) * mdr_r_signed_selected_targetnegativepoint + mdr_s_signed_selected_targetnegativepoint) /\ ((exists mdr_gap_signed_selected_targetnegativepointcolumn. mdr_gap_signed_selected_targetnegativepointcolumn + S (mdr_s_signed_selected_targetnegativepoint) = (q)) /\ ((((exists ff_h_mdr_signed_selected_targetnegativepointrow_index. ff_h_mdr_signed_selected_targetnegativepointrow_index + S (mdr_u_signed_selected_targetnegativepoint) = S ((S (mdr_r_signed_selected_targetnegativepoint)) * Rc)) /\ exists ff_q_mdr_signed_selected_targetnegativepointrow_index. Rb = ff_q_mdr_signed_selected_targetnegativepointrow_index * S ((S (mdr_r_signed_selected_targetnegativepoint)) * Rc) + (mdr_u_signed_selected_targetnegativepoint))) /\ ((((exists ff_h_mdr_signed_selected_targetnegativepointcolumn_index. ff_h_mdr_signed_selected_targetnegativepointcolumn_index + S (mdr_v_signed_selected_targetnegativepoint) = S ((S (mdr_s_signed_selected_targetnegativepoint)) * Cc)) /\ exists ff_q_mdr_signed_selected_targetnegativepointcolumn_index. Cb = ff_q_mdr_signed_selected_targetnegativepointcolumn_index * S ((S (mdr_s_signed_selected_targetnegativepoint)) * Cc) + (mdr_v_signed_selected_targetnegativepoint))) /\ (((exists ff_h_mdr_signed_selected_targetnegativepointsource. ff_h_mdr_signed_selected_targetnegativepointsource + S (mdr_a_signed_selected_targetnegative) = S ((S ((mdr_u_signed_selected_targetnegativepoint) * (w) + (mdr_v_signed_selected_targetnegativepoint))) * nc)) /\ exists ff_q_mdr_signed_selected_targetnegativepointsource. nb = ff_q_mdr_signed_selected_targetnegativepointsource * S ((S ((mdr_u_signed_selected_targetnegativepoint) * (w) + (mdr_v_signed_selected_targetnegativepoint))) * nc) + (mdr_a_signed_selected_targetnegative)))))))) /\ (((exists ff_h_mdr_signed_selected_targetnegativeoutput. ff_h_mdr_signed_selected_targetnegativeoutput + S (mdr_a_signed_selected_targetnegative) = S ((S (mdr_i_signed_selected_targetnegative)) * vc)) /\ exists ff_q_mdr_signed_selected_targetnegativeoutput. vb = ff_q_mdr_signed_selected_targetnegativeoutput * S ((S (mdr_i_signed_selected_targetnegative)) * vc) + (mdr_a_signed_selected_targetnegative))))))))