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

((forall jt_index_definition_jordanbound. (exists jt_gap_definition_jordanboundindex. jt_gap_definition_jordanboundindex+S (jt_index_definition_jordanbound)=(k)) -> exists jt_value_definition_jordanbound. ((((exists fs_h_jt_definition_jordanboundat. fs_h_jt_definition_jordanboundat + S (jt_value_definition_jordanbound) = S ((S (jt_index_definition_jordanbound)) * g)) /\ exists fs_q_jt_definition_jordanboundat. f = fs_q_jt_definition_jordanboundat * S ((S (jt_index_definition_jordanbound)) * g) + (jt_value_definition_jordanbound))) /\ (exists jt_gap_definition_jordanboundvalue. jt_gap_definition_jordanboundvalue+S (jt_value_definition_jordanbound)=(m*n)))) /\ (((forall jt_index_definition_jordanleft jt_left_definition_jordanleft jt_right_definition_jordanleft. (exists jt_gap_definition_jordanleftindex. jt_gap_definition_jordanleftindex+S (jt_index_definition_jordanleft)=(k)) -> (((exists fs_h_jt_definition_jordanleftleft. fs_h_jt_definition_jordanleftleft + S (jt_left_definition_jordanleft) = S ((S (jt_index_definition_jordanleft)) * g)) /\ exists fs_q_jt_definition_jordanleftleft. f = fs_q_jt_definition_jordanleftleft * S ((S (jt_index_definition_jordanleft)) * g) + (jt_left_definition_jordanleft))) -> (((exists fs_h_jt_definition_jordanleftright. fs_h_jt_definition_jordanleftright + S (jt_right_definition_jordanleft) = S ((S (jt_index_definition_jordanleft)) * c)) /\ exists fs_q_jt_definition_jordanleftright. b = fs_q_jt_definition_jordanleftright * S ((S (jt_index_definition_jordanleft)) * c) + (jt_right_definition_jordanleft))) -> (exists jt_left_definition_jordanleftmod jt_right_definition_jordanleftmod. (jt_left_definition_jordanleft)+(m)*jt_left_definition_jordanleftmod=(jt_right_definition_jordanleft)+(m)*jt_right_definition_jordanleftmod)) /\ (forall jt_index_definition_jordanright jt_left_definition_jordanright jt_right_definition_jordanright. (exists jt_gap_definition_jordanrightindex. jt_gap_definition_jordanrightindex+S (jt_index_definition_jordanright)=(k)) -> (((exists fs_h_jt_definition_jordanrightleft. fs_h_jt_definition_jordanrightleft + S (jt_left_definition_jordanright) = S ((S (jt_index_definition_jordanright)) * g)) /\ exists fs_q_jt_definition_jordanrightleft. f = fs_q_jt_definition_jordanrightleft * S ((S (jt_index_definition_jordanright)) * g) + (jt_left_definition_jordanright))) -> (((exists fs_h_jt_definition_jordanrightright. fs_h_jt_definition_jordanrightright + S (jt_right_definition_jordanright) = S ((S (jt_index_definition_jordanright)) * e)) /\ exists fs_q_jt_definition_jordanrightright. d = fs_q_jt_definition_jordanrightright * S ((S (jt_index_definition_jordanright)) * e) + (jt_right_definition_jordanright))) -> (exists jt_left_definition_jordanrightmod jt_right_definition_jordanrightmod. (jt_left_definition_jordanright)+(n)*jt_left_definition_jordanrightmod=(jt_right_definition_jordanright)+(n)*jt_right_definition_jordanrightmod)))))

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