SignedSelectedSubmatrix(pb,pc,nb,nc,w,rb,rc,cb,cc,q,ub,uc,vb,vc)

((forall mdr_i_secondwavepositive. (exists mdr_gap_secondwavepositivebound. mdr_gap_secondwavepositivebound + S (mdr_i_secondwavepositive) = ((q) * (q))) -> exists mdr_a_secondwavepositive. (((exists mdr_r_secondwavepositivepoint mdr_s_secondwavepositivepoint mdr_u_secondwavepositivepoint mdr_v_secondwavepositivepoint. ((mdr_i_secondwavepositive = (q) * mdr_r_secondwavepositivepoint + mdr_s_secondwavepositivepoint) /\ ((exists mdr_gap_secondwavepositivepointcolumn. mdr_gap_secondwavepositivepointcolumn + S (mdr_s_secondwavepositivepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavepositivepointrow_index. ff_h_mdr_secondwavepositivepointrow_index + S (mdr_u_secondwavepositivepoint) = S ((S (mdr_r_secondwavepositivepoint)) * rc)) /\ exists ff_q_mdr_secondwavepositivepointrow_index. rb = ff_q_mdr_secondwavepositivepointrow_index * S ((S (mdr_r_secondwavepositivepoint)) * rc) + (mdr_u_secondwavepositivepoint))) /\ ((((exists ff_h_mdr_secondwavepositivepointcolumn_index. ff_h_mdr_secondwavepositivepointcolumn_index + S (mdr_v_secondwavepositivepoint) = S ((S (mdr_s_secondwavepositivepoint)) * cc)) /\ exists ff_q_mdr_secondwavepositivepointcolumn_index. cb = ff_q_mdr_secondwavepositivepointcolumn_index * S ((S (mdr_s_secondwavepositivepoint)) * cc) + (mdr_v_secondwavepositivepoint))) /\ (((exists ff_h_mdr_secondwavepositivepointsource. ff_h_mdr_secondwavepositivepointsource + S (mdr_a_secondwavepositive) = S ((S ((mdr_u_secondwavepositivepoint) * (w) + (mdr_v_secondwavepositivepoint))) * pc)) /\ exists ff_q_mdr_secondwavepositivepointsource. pb = ff_q_mdr_secondwavepositivepointsource * S ((S ((mdr_u_secondwavepositivepoint) * (w) + (mdr_v_secondwavepositivepoint))) * pc) + (mdr_a_secondwavepositive)))))))) /\ (((exists ff_h_mdr_secondwavepositiveoutput. ff_h_mdr_secondwavepositiveoutput + S (mdr_a_secondwavepositive) = S ((S (mdr_i_secondwavepositive)) * uc)) /\ exists ff_q_mdr_secondwavepositiveoutput. ub = ff_q_mdr_secondwavepositiveoutput * S ((S (mdr_i_secondwavepositive)) * uc) + (mdr_a_secondwavepositive)))))) /\ (forall mdr_i_secondwavenegative. (exists mdr_gap_secondwavenegativebound. mdr_gap_secondwavenegativebound + S (mdr_i_secondwavenegative) = ((q) * (q))) -> exists mdr_a_secondwavenegative. (((exists mdr_r_secondwavenegativepoint mdr_s_secondwavenegativepoint mdr_u_secondwavenegativepoint mdr_v_secondwavenegativepoint. ((mdr_i_secondwavenegative = (q) * mdr_r_secondwavenegativepoint + mdr_s_secondwavenegativepoint) /\ ((exists mdr_gap_secondwavenegativepointcolumn. mdr_gap_secondwavenegativepointcolumn + S (mdr_s_secondwavenegativepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavenegativepointrow_index. ff_h_mdr_secondwavenegativepointrow_index + S (mdr_u_secondwavenegativepoint) = S ((S (mdr_r_secondwavenegativepoint)) * rc)) /\ exists ff_q_mdr_secondwavenegativepointrow_index. rb = ff_q_mdr_secondwavenegativepointrow_index * S ((S (mdr_r_secondwavenegativepoint)) * rc) + (mdr_u_secondwavenegativepoint))) /\ ((((exists ff_h_mdr_secondwavenegativepointcolumn_index. ff_h_mdr_secondwavenegativepointcolumn_index + S (mdr_v_secondwavenegativepoint) = S ((S (mdr_s_secondwavenegativepoint)) * cc)) /\ exists ff_q_mdr_secondwavenegativepointcolumn_index. cb = ff_q_mdr_secondwavenegativepointcolumn_index * S ((S (mdr_s_secondwavenegativepoint)) * cc) + (mdr_v_secondwavenegativepoint))) /\ (((exists ff_h_mdr_secondwavenegativepointsource. ff_h_mdr_secondwavenegativepointsource + S (mdr_a_secondwavenegative) = S ((S ((mdr_u_secondwavenegativepoint) * (w) + (mdr_v_secondwavenegativepoint))) * nc)) /\ exists ff_q_mdr_secondwavenegativepointsource. nb = ff_q_mdr_secondwavenegativepointsource * S ((S ((mdr_u_secondwavenegativepoint) * (w) + (mdr_v_secondwavenegativepoint))) * nc) + (mdr_a_secondwavenegative)))))))) /\ (((exists ff_h_mdr_secondwavenegativeoutput. ff_h_mdr_secondwavenegativeoutput + S (mdr_a_secondwavenegative) = S ((S (mdr_i_secondwavenegative)) * vc)) /\ exists ff_q_mdr_secondwavenegativeoutput. vb = ff_q_mdr_secondwavenegativeoutput * S ((S (mdr_i_secondwavenegative)) * vc) + (mdr_a_secondwavenegative)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.