JordanTupleListed(b,c,k,B,C,D,E,j)

exists jt_index_definition_jordan jt_code_definition_jordan jt_scale_definition_jordan. ((exists jt_gap_definition_jordanindex. jt_gap_definition_jordanindex+S (jt_index_definition_jordan)=(j)) /\ (((((((exists fs_h_jt_definition_jordancode. fs_h_jt_definition_jordancode + S (jt_code_definition_jordan) = S ((S (jt_index_definition_jordan)) * C)) /\ exists fs_q_jt_definition_jordancode. B = fs_q_jt_definition_jordancode * S ((S (jt_index_definition_jordan)) * C) + (jt_code_definition_jordan))) /\ (((exists fs_h_jt_definition_jordanscale. fs_h_jt_definition_jordanscale + S (jt_scale_definition_jordan) = S ((S (jt_index_definition_jordan)) * E)) /\ exists fs_q_jt_definition_jordanscale. D = fs_q_jt_definition_jordanscale * S ((S (jt_index_definition_jordan)) * E) + (jt_scale_definition_jordan))))) /\ (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)) * c)) /\ exists fs_q_jt_definition_jordanequalleft. b = fs_q_jt_definition_jordanequalleft * S ((S (jt_index_definition_jordanequal)) * c) + (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)) * jt_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanequalright. jt_code_definition_jordan = fs_q_jt_definition_jordanequalright * S ((S (jt_index_definition_jordanequal)) * jt_scale_definition_jordan) + (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.