JordanRectangleCRT(m,n,k,A,B,C,D,u,E,F,G,H,v,P,Q,R,T,q)

forall jt_index_definition_jordan. (exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_index_definition_jordan)=(q)) -> exists jt_row_definition_jordan jt_column_definition_jordan jt_b_definition_jordan jt_c_definition_jordan jt_d_definition_jordan jt_e_definition_jordan jt_f_definition_jordan jt_g_definition_jordan. ((exists jt_gap_definition_jordanrow. jt_gap_definition_jordanrow+S (jt_row_definition_jordan)=(u)) /\ (((exists jt_gap_definition_jordancolumn. jt_gap_definition_jordancolumn+S (jt_column_definition_jordan)=(v)) /\ (((jt_index_definition_jordan=(v)*jt_row_definition_jordan+jt_column_definition_jordan) /\ (((((((exists fs_h_jt_definition_jordanleftcode. fs_h_jt_definition_jordanleftcode + S (jt_b_definition_jordan) = S ((S (jt_row_definition_jordan)) * B)) /\ exists fs_q_jt_definition_jordanleftcode. A = fs_q_jt_definition_jordanleftcode * S ((S (jt_row_definition_jordan)) * B) + (jt_b_definition_jordan))) /\ (((exists fs_h_jt_definition_jordanleftscale. fs_h_jt_definition_jordanleftscale + S (jt_c_definition_jordan) = S ((S (jt_row_definition_jordan)) * D)) /\ exists fs_q_jt_definition_jordanleftscale. C = fs_q_jt_definition_jordanleftscale * S ((S (jt_row_definition_jordan)) * D) + (jt_c_definition_jordan))))) /\ (((((((exists fs_h_jt_definition_jordanrightcode. fs_h_jt_definition_jordanrightcode + S (jt_d_definition_jordan) = S ((S (jt_column_definition_jordan)) * F)) /\ exists fs_q_jt_definition_jordanrightcode. E = fs_q_jt_definition_jordanrightcode * S ((S (jt_column_definition_jordan)) * F) + (jt_d_definition_jordan))) /\ (((exists fs_h_jt_definition_jordanrightscale. fs_h_jt_definition_jordanrightscale + S (jt_e_definition_jordan) = S ((S (jt_column_definition_jordan)) * H)) /\ exists fs_q_jt_definition_jordanrightscale. G = fs_q_jt_definition_jordanrightscale * S ((S (jt_column_definition_jordan)) * H) + (jt_e_definition_jordan))))) /\ (((((((exists fs_h_jt_definition_jordanoutputcode. fs_h_jt_definition_jordanoutputcode + S (jt_f_definition_jordan) = S ((S (jt_index_definition_jordan)) * Q)) /\ exists fs_q_jt_definition_jordanoutputcode. P = fs_q_jt_definition_jordanoutputcode * S ((S (jt_index_definition_jordan)) * Q) + (jt_f_definition_jordan))) /\ (((exists fs_h_jt_definition_jordanoutputscale. fs_h_jt_definition_jordanoutputscale + S (jt_g_definition_jordan) = S ((S (jt_index_definition_jordan)) * T)) /\ exists fs_q_jt_definition_jordanoutputscale. R = fs_q_jt_definition_jordanoutputscale * S ((S (jt_index_definition_jordan)) * T) + (jt_g_definition_jordan))))) /\ (((((forall jt_index_definition_jordancrtbound. (exists jt_gap_definition_jordancrtboundindex. jt_gap_definition_jordancrtboundindex+S (jt_index_definition_jordancrtbound)=(k)) -> exists jt_value_definition_jordancrtbound. ((((exists fs_h_jt_definition_jordancrtboundat. fs_h_jt_definition_jordancrtboundat + S (jt_value_definition_jordancrtbound) = S ((S (jt_index_definition_jordancrtbound)) * jt_g_definition_jordan)) /\ exists fs_q_jt_definition_jordancrtboundat. jt_f_definition_jordan = fs_q_jt_definition_jordancrtboundat * S ((S (jt_index_definition_jordancrtbound)) * jt_g_definition_jordan) + (jt_value_definition_jordancrtbound))) /\ (exists jt_gap_definition_jordancrtboundvalue. jt_gap_definition_jordancrtboundvalue+S (jt_value_definition_jordancrtbound)=(m*n)))) /\ (((forall jt_index_definition_jordancrtleft jt_left_definition_jordancrtleft jt_right_definition_jordancrtleft. (exists jt_gap_definition_jordancrtleftindex. jt_gap_definition_jordancrtleftindex+S (jt_index_definition_jordancrtleft)=(k)) -> (((exists fs_h_jt_definition_jordancrtleftleft. fs_h_jt_definition_jordancrtleftleft + S (jt_left_definition_jordancrtleft) = S ((S (jt_index_definition_jordancrtleft)) * jt_g_definition_jordan)) /\ exists fs_q_jt_definition_jordancrtleftleft. jt_f_definition_jordan = fs_q_jt_definition_jordancrtleftleft * S ((S (jt_index_definition_jordancrtleft)) * jt_g_definition_jordan) + (jt_left_definition_jordancrtleft))) -> (((exists fs_h_jt_definition_jordancrtleftright. fs_h_jt_definition_jordancrtleftright + S (jt_right_definition_jordancrtleft) = S ((S (jt_index_definition_jordancrtleft)) * jt_c_definition_jordan)) /\ exists fs_q_jt_definition_jordancrtleftright. jt_b_definition_jordan = fs_q_jt_definition_jordancrtleftright * S ((S (jt_index_definition_jordancrtleft)) * jt_c_definition_jordan) + (jt_right_definition_jordancrtleft))) -> (exists jt_left_definition_jordancrtleftmod jt_right_definition_jordancrtleftmod. (jt_left_definition_jordancrtleft)+(m)*jt_left_definition_jordancrtleftmod=(jt_right_definition_jordancrtleft)+(m)*jt_right_definition_jordancrtleftmod)) /\ (forall jt_index_definition_jordancrtright jt_left_definition_jordancrtright jt_right_definition_jordancrtright. (exists jt_gap_definition_jordancrtrightindex. jt_gap_definition_jordancrtrightindex+S (jt_index_definition_jordancrtright)=(k)) -> (((exists fs_h_jt_definition_jordancrtrightleft. fs_h_jt_definition_jordancrtrightleft + S (jt_left_definition_jordancrtright) = S ((S (jt_index_definition_jordancrtright)) * jt_g_definition_jordan)) /\ exists fs_q_jt_definition_jordancrtrightleft. jt_f_definition_jordan = fs_q_jt_definition_jordancrtrightleft * S ((S (jt_index_definition_jordancrtright)) * jt_g_definition_jordan) + (jt_left_definition_jordancrtright))) -> (((exists fs_h_jt_definition_jordancrtrightright. fs_h_jt_definition_jordancrtrightright + S (jt_right_definition_jordancrtright) = S ((S (jt_index_definition_jordancrtright)) * jt_e_definition_jordan)) /\ exists fs_q_jt_definition_jordancrtrightright. jt_d_definition_jordan = fs_q_jt_definition_jordancrtrightright * S ((S (jt_index_definition_jordancrtright)) * jt_e_definition_jordan) + (jt_right_definition_jordancrtright))) -> (exists jt_left_definition_jordancrtrightmod jt_right_definition_jordancrtrightmod. (jt_left_definition_jordancrtright)+(n)*jt_left_definition_jordancrtrightmod=(jt_right_definition_jordancrtright)+(n)*jt_right_definition_jordancrtrightmod)))))) /\ (forall jt_divisor_definition_jordanprimitive. (exists jt_factor_definition_jordanprimitivemodulus. (m*n)=(jt_divisor_definition_jordanprimitive)*jt_factor_definition_jordanprimitivemodulus) -> (forall jt_index_definition_jordanprimitivecoordinates jt_value_definition_jordanprimitivecoordinates. (exists jt_gap_definition_jordanprimitivecoordinatesindex. jt_gap_definition_jordanprimitivecoordinatesindex+S (jt_index_definition_jordanprimitivecoordinates)=(k)) -> (((exists fs_h_jt_definition_jordanprimitivecoordinatesat. fs_h_jt_definition_jordanprimitivecoordinatesat + S (jt_value_definition_jordanprimitivecoordinates) = S ((S (jt_index_definition_jordanprimitivecoordinates)) * jt_g_definition_jordan)) /\ exists fs_q_jt_definition_jordanprimitivecoordinatesat. jt_f_definition_jordan = fs_q_jt_definition_jordanprimitivecoordinatesat * S ((S (jt_index_definition_jordanprimitivecoordinates)) * jt_g_definition_jordan) + (jt_value_definition_jordanprimitivecoordinates))) -> (exists jt_factor_definition_jordanprimitivecoordinatesdivides. (jt_value_definition_jordanprimitivecoordinates)=(jt_divisor_definition_jordanprimitive)*jt_factor_definition_jordanprimitivecoordinatesdivides)) -> jt_divisor_definition_jordanprimitive=1))))))))))))))

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