JordanTupleRepresentatives(k,n,c,T)

forall jt_code_definition_jordan jt_scale_definition_jordan. (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)) * jt_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanboundat. jt_code_definition_jordan = fs_q_jt_definition_jordanboundat * S ((S (jt_index_definition_jordanbound)) * jt_scale_definition_jordan) + (jt_value_definition_jordanbound))) /\ (exists jt_gap_definition_jordanboundvalue. jt_gap_definition_jordanboundvalue+S (jt_value_definition_jordanbound)=(n)))) -> exists jt_representative_definition_jordan. ((exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_representative_definition_jordan)=(T)) /\ (forall jt_index_definition_jordanequal jt_left_definition_jordanequal jt_right_definition_jordanequal. (exists jt_gap_definition_jordanequalindex. jt_gap_definition_jordanequalindex+S (jt_index_definition_jordanequal)=(k)) -> (((exists fs_h_jt_definition_jordanequalleft. fs_h_jt_definition_jordanequalleft + S (jt_left_definition_jordanequal) = S ((S (jt_index_definition_jordanequal)) * jt_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanequalleft. jt_code_definition_jordan = fs_q_jt_definition_jordanequalleft * S ((S (jt_index_definition_jordanequal)) * jt_scale_definition_jordan) + (jt_left_definition_jordanequal))) -> (((exists fs_h_jt_definition_jordanequalright. fs_h_jt_definition_jordanequalright + S (jt_right_definition_jordanequal) = S ((S (jt_index_definition_jordanequal)) * c)) /\ exists fs_q_jt_definition_jordanequalright. jt_representative_definition_jordan = fs_q_jt_definition_jordanequalright * S ((S (jt_index_definition_jordanequal)) * c) + (jt_right_definition_jordanequal))) -> jt_left_definition_jordanequal=jt_right_definition_jordanequal))

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