JordanTupleEnumeration(k,n,B,C,D,E,j)

((forall jt_i_definition_jordan. (exists jt_gap_definition_jordansoundindex. jt_gap_definition_jordansoundindex+S (jt_i_definition_jordan)=(j)) -> exists jt_b_definition_jordan jt_c_definition_jordan. ((((((exists fs_h_jt_definition_jordansoundcode. fs_h_jt_definition_jordansoundcode + S (jt_b_definition_jordan) = S ((S (jt_i_definition_jordan)) * C)) /\ exists fs_q_jt_definition_jordansoundcode. B = fs_q_jt_definition_jordansoundcode * S ((S (jt_i_definition_jordan)) * C) + (jt_b_definition_jordan))) /\ (((exists fs_h_jt_definition_jordansoundscale. fs_h_jt_definition_jordansoundscale + S (jt_c_definition_jordan) = S ((S (jt_i_definition_jordan)) * E)) /\ exists fs_q_jt_definition_jordansoundscale. D = fs_q_jt_definition_jordansoundscale * S ((S (jt_i_definition_jordan)) * E) + (jt_c_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_c_definition_jordan)) /\ exists fs_q_jt_definition_jordanboundat. jt_b_definition_jordan = fs_q_jt_definition_jordanboundat * S ((S (jt_index_definition_jordanbound)) * jt_c_definition_jordan) + (jt_value_definition_jordanbound))) /\ (exists jt_gap_definition_jordanboundvalue. jt_gap_definition_jordanboundvalue+S (jt_value_definition_jordanbound)=(n)))) /\ (forall jt_divisor_definition_jordanprimitive. (exists jt_factor_definition_jordanprimitivemodulus. (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_c_definition_jordan)) /\ exists fs_q_jt_definition_jordanprimitivecoordinatesat. jt_b_definition_jordan = fs_q_jt_definition_jordanprimitivecoordinatesat * S ((S (jt_index_definition_jordanprimitivecoordinates)) * jt_c_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))))) /\ (((forall jt_b_definition_jordan jt_c_definition_jordan. (forall jt_index_definition_jordaninputbound. (exists jt_gap_definition_jordaninputboundindex. jt_gap_definition_jordaninputboundindex+S (jt_index_definition_jordaninputbound)=(k)) -> exists jt_value_definition_jordaninputbound. ((((exists fs_h_jt_definition_jordaninputboundat. fs_h_jt_definition_jordaninputboundat + S (jt_value_definition_jordaninputbound) = S ((S (jt_index_definition_jordaninputbound)) * jt_c_definition_jordan)) /\ exists fs_q_jt_definition_jordaninputboundat. jt_b_definition_jordan = fs_q_jt_definition_jordaninputboundat * S ((S (jt_index_definition_jordaninputbound)) * jt_c_definition_jordan) + (jt_value_definition_jordaninputbound))) /\ (exists jt_gap_definition_jordaninputboundvalue. jt_gap_definition_jordaninputboundvalue+S (jt_value_definition_jordaninputbound)=(n)))) -> (forall jt_divisor_definition_jordaninputprimitive. (exists jt_factor_definition_jordaninputprimitivemodulus. (n)=(jt_divisor_definition_jordaninputprimitive)*jt_factor_definition_jordaninputprimitivemodulus) -> (forall jt_index_definition_jordaninputprimitivecoordinates jt_value_definition_jordaninputprimitivecoordinates. (exists jt_gap_definition_jordaninputprimitivecoordinatesindex. jt_gap_definition_jordaninputprimitivecoordinatesindex+S (jt_index_definition_jordaninputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_definition_jordaninputprimitivecoordinatesat. fs_h_jt_definition_jordaninputprimitivecoordinatesat + S (jt_value_definition_jordaninputprimitivecoordinates) = S ((S (jt_index_definition_jordaninputprimitivecoordinates)) * jt_c_definition_jordan)) /\ exists fs_q_jt_definition_jordaninputprimitivecoordinatesat. jt_b_definition_jordan = fs_q_jt_definition_jordaninputprimitivecoordinatesat * S ((S (jt_index_definition_jordaninputprimitivecoordinates)) * jt_c_definition_jordan) + (jt_value_definition_jordaninputprimitivecoordinates))) -> (exists jt_factor_definition_jordaninputprimitivecoordinatesdivides. (jt_value_definition_jordaninputprimitivecoordinates)=(jt_divisor_definition_jordaninputprimitive)*jt_factor_definition_jordaninputprimitivecoordinatesdivides)) -> jt_divisor_definition_jordaninputprimitive=1) -> exists jt_i_definition_jordan jt_d_definition_jordan jt_e_definition_jordan. ((exists jt_gap_definition_jordancompleteindex. jt_gap_definition_jordancompleteindex+S (jt_i_definition_jordan)=(j)) /\ (((((((exists fs_h_jt_definition_jordancompletecode. fs_h_jt_definition_jordancompletecode + S (jt_d_definition_jordan) = S ((S (jt_i_definition_jordan)) * C)) /\ exists fs_q_jt_definition_jordancompletecode. B = fs_q_jt_definition_jordancompletecode * S ((S (jt_i_definition_jordan)) * C) + (jt_d_definition_jordan))) /\ (((exists fs_h_jt_definition_jordancompletescale. fs_h_jt_definition_jordancompletescale + S (jt_e_definition_jordan) = S ((S (jt_i_definition_jordan)) * E)) /\ exists fs_q_jt_definition_jordancompletescale. D = fs_q_jt_definition_jordancompletescale * S ((S (jt_i_definition_jordan)) * E) + (jt_e_definition_jordan))))) /\ (forall jt_index_definition_jordanrepresented jt_left_definition_jordanrepresented jt_right_definition_jordanrepresented. (exists jt_gap_definition_jordanrepresentedindex. jt_gap_definition_jordanrepresentedindex+S (jt_index_definition_jordanrepresented)=(k)) -> (((exists fs_h_jt_definition_jordanrepresentedleft. fs_h_jt_definition_jordanrepresentedleft + S (jt_left_definition_jordanrepresented) = S ((S (jt_index_definition_jordanrepresented)) * jt_c_definition_jordan)) /\ exists fs_q_jt_definition_jordanrepresentedleft. jt_b_definition_jordan = fs_q_jt_definition_jordanrepresentedleft * S ((S (jt_index_definition_jordanrepresented)) * jt_c_definition_jordan) + (jt_left_definition_jordanrepresented))) -> (((exists fs_h_jt_definition_jordanrepresentedright. fs_h_jt_definition_jordanrepresentedright + S (jt_right_definition_jordanrepresented) = S ((S (jt_index_definition_jordanrepresented)) * jt_e_definition_jordan)) /\ exists fs_q_jt_definition_jordanrepresentedright. jt_d_definition_jordan = fs_q_jt_definition_jordanrepresentedright * S ((S (jt_index_definition_jordanrepresented)) * jt_e_definition_jordan) + (jt_right_definition_jordanrepresented))) -> jt_left_definition_jordanrepresented=jt_right_definition_jordanrepresented))))) /\ (forall jt_i_definition_jordan jt_h_definition_jordan jt_b_definition_jordan jt_c_definition_jordan jt_d_definition_jordan jt_e_definition_jordan. (exists jt_gap_definition_jordanfirstindex. jt_gap_definition_jordanfirstindex+S (jt_i_definition_jordan)=(j)) -> (exists jt_gap_definition_jordansecondindex. jt_gap_definition_jordansecondindex+S (jt_h_definition_jordan)=(j)) -> (((((exists fs_h_jt_definition_jordanfirstcode. fs_h_jt_definition_jordanfirstcode + S (jt_b_definition_jordan) = S ((S (jt_i_definition_jordan)) * C)) /\ exists fs_q_jt_definition_jordanfirstcode. B = fs_q_jt_definition_jordanfirstcode * S ((S (jt_i_definition_jordan)) * C) + (jt_b_definition_jordan))) /\ (((exists fs_h_jt_definition_jordanfirstscale. fs_h_jt_definition_jordanfirstscale + S (jt_c_definition_jordan) = S ((S (jt_i_definition_jordan)) * E)) /\ exists fs_q_jt_definition_jordanfirstscale. D = fs_q_jt_definition_jordanfirstscale * S ((S (jt_i_definition_jordan)) * E) + (jt_c_definition_jordan))))) -> (((((exists fs_h_jt_definition_jordansecondcode. fs_h_jt_definition_jordansecondcode + S (jt_d_definition_jordan) = S ((S (jt_h_definition_jordan)) * C)) /\ exists fs_q_jt_definition_jordansecondcode. B = fs_q_jt_definition_jordansecondcode * S ((S (jt_h_definition_jordan)) * C) + (jt_d_definition_jordan))) /\ (((exists fs_h_jt_definition_jordansecondscale. fs_h_jt_definition_jordansecondscale + S (jt_e_definition_jordan) = S ((S (jt_h_definition_jordan)) * E)) /\ exists fs_q_jt_definition_jordansecondscale. D = fs_q_jt_definition_jordansecondscale * S ((S (jt_h_definition_jordan)) * E) + (jt_e_definition_jordan))))) -> (forall jt_index_definition_jordansame jt_left_definition_jordansame jt_right_definition_jordansame. (exists jt_gap_definition_jordansameindex. jt_gap_definition_jordansameindex+S (jt_index_definition_jordansame)=(k)) -> (((exists fs_h_jt_definition_jordansameleft. fs_h_jt_definition_jordansameleft + S (jt_left_definition_jordansame) = S ((S (jt_index_definition_jordansame)) * jt_c_definition_jordan)) /\ exists fs_q_jt_definition_jordansameleft. jt_b_definition_jordan = fs_q_jt_definition_jordansameleft * S ((S (jt_index_definition_jordansame)) * jt_c_definition_jordan) + (jt_left_definition_jordansame))) -> (((exists fs_h_jt_definition_jordansameright. fs_h_jt_definition_jordansameright + S (jt_right_definition_jordansame) = S ((S (jt_index_definition_jordansame)) * jt_e_definition_jordan)) /\ exists fs_q_jt_definition_jordansameright. jt_d_definition_jordan = fs_q_jt_definition_jordansameright * S ((S (jt_index_definition_jordansame)) * jt_e_definition_jordan) + (jt_right_definition_jordansame))) -> jt_left_definition_jordansame=jt_right_definition_jordansame) -> jt_i_definition_jordan=jt_h_definition_jordan))))

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