JordanTupleCRT(m,n,b,c,d,e,f,g,k)

forall jt_index_definition_jordan. (exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_index_definition_jordan)=(k)) -> exists jt_left_definition_jordan jt_right_definition_jordan jt_output_definition_jordan. ((((exists fs_h_jt_definition_jordanleft. fs_h_jt_definition_jordanleft + S (jt_left_definition_jordan) = S ((S (jt_index_definition_jordan)) * c)) /\ exists fs_q_jt_definition_jordanleft. b = fs_q_jt_definition_jordanleft * S ((S (jt_index_definition_jordan)) * c) + (jt_left_definition_jordan))) /\ (((((exists fs_h_jt_definition_jordanright. fs_h_jt_definition_jordanright + S (jt_right_definition_jordan) = S ((S (jt_index_definition_jordan)) * e)) /\ exists fs_q_jt_definition_jordanright. d = fs_q_jt_definition_jordanright * S ((S (jt_index_definition_jordan)) * e) + (jt_right_definition_jordan))) /\ (((((exists fs_h_jt_definition_jordanoutput. fs_h_jt_definition_jordanoutput + S (jt_output_definition_jordan) = S ((S (jt_index_definition_jordan)) * g)) /\ exists fs_q_jt_definition_jordanoutput. f = fs_q_jt_definition_jordanoutput * S ((S (jt_index_definition_jordan)) * g) + (jt_output_definition_jordan))) /\ (((exists jt_left_definition_jordanmodleft jt_right_definition_jordanmodleft. (jt_output_definition_jordan)+(m)*jt_left_definition_jordanmodleft=(jt_left_definition_jordan)+(m)*jt_right_definition_jordanmodleft) /\ (exists jt_left_definition_jordanmodright jt_right_definition_jordanmodright. (jt_output_definition_jordan)+(n)*jt_left_definition_jordanmodright=(jt_right_definition_jordan)+(n)*jt_right_definition_jordanmodright))))))))

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