JordanTupleScan(k,n,c,limit,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_e_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_e_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_e_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_e_definition_jordan)) /\ exists fs_q_jt_definition_jordanboundat. jt_b_definition_jordan = fs_q_jt_definition_jordanboundat * S ((S (jt_index_definition_jordanbound)) * jt_e_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_e_definition_jordan)) /\ exists fs_q_jt_definition_jordanprimitivecoordinatesat. jt_b_definition_jordan = fs_q_jt_definition_jordanprimitivecoordinatesat * S ((S (jt_index_definition_jordanprimitivecoordinates)) * jt_e_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_i_definition_jordan jt_h_definition_jordan jt_b_definition_jordan jt_e_definition_jordan jt_d_definition_jordan jt_f_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_e_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_e_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_f_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_f_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_e_definition_jordan)) /\ exists fs_q_jt_definition_jordansameleft. jt_b_definition_jordan = fs_q_jt_definition_jordansameleft * S ((S (jt_index_definition_jordansame)) * jt_e_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_f_definition_jordan)) /\ exists fs_q_jt_definition_jordansameright. jt_d_definition_jordan = fs_q_jt_definition_jordansameright * S ((S (jt_index_definition_jordansame)) * jt_f_definition_jordan) + (jt_right_definition_jordansame))) -> jt_left_definition_jordansame=jt_right_definition_jordansame) -> jt_i_definition_jordan=jt_h_definition_jordan) /\ (forall jt_z_definition_jordan. (exists jt_gap_definition_jordancodeindex. jt_gap_definition_jordancodeindex+S (jt_z_definition_jordan)=(limit)) -> (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)) * c)) /\ exists fs_q_jt_definition_jordaninputboundat. jt_z_definition_jordan = fs_q_jt_definition_jordaninputboundat * S ((S (jt_index_definition_jordaninputbound)) * c) + (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)) * c)) /\ exists fs_q_jt_definition_jordaninputprimitivecoordinatesat. jt_z_definition_jordan = fs_q_jt_definition_jordaninputprimitivecoordinatesat * S ((S (jt_index_definition_jordaninputprimitivecoordinates)) * c) + (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_index_definition_jordanlisted jt_code_definition_jordanlisted jt_scale_definition_jordanlisted. ((exists jt_gap_definition_jordanlistedindex. jt_gap_definition_jordanlistedindex+S (jt_index_definition_jordanlisted)=(j)) /\ (((((((exists fs_h_jt_definition_jordanlistedcode. fs_h_jt_definition_jordanlistedcode + S (jt_code_definition_jordanlisted) = S ((S (jt_index_definition_jordanlisted)) * C)) /\ exists fs_q_jt_definition_jordanlistedcode. B = fs_q_jt_definition_jordanlistedcode * S ((S (jt_index_definition_jordanlisted)) * C) + (jt_code_definition_jordanlisted))) /\ (((exists fs_h_jt_definition_jordanlistedscale. fs_h_jt_definition_jordanlistedscale + S (jt_scale_definition_jordanlisted) = S ((S (jt_index_definition_jordanlisted)) * E)) /\ exists fs_q_jt_definition_jordanlistedscale. D = fs_q_jt_definition_jordanlistedscale * S ((S (jt_index_definition_jordanlisted)) * E) + (jt_scale_definition_jordanlisted))))) /\ (forall jt_index_definition_jordanlistedequal jt_left_definition_jordanlistedequal jt_right_definition_jordanlistedequal. (exists jt_gap_definition_jordanlistedequalindex. jt_gap_definition_jordanlistedequalindex+S (jt_index_definition_jordanlistedequal)=(k)) -> (((exists fs_h_jt_definition_jordanlistedequalleft. fs_h_jt_definition_jordanlistedequalleft + S (jt_left_definition_jordanlistedequal) = S ((S (jt_index_definition_jordanlistedequal)) * c)) /\ exists fs_q_jt_definition_jordanlistedequalleft. jt_z_definition_jordan = fs_q_jt_definition_jordanlistedequalleft * S ((S (jt_index_definition_jordanlistedequal)) * c) + (jt_left_definition_jordanlistedequal))) -> (((exists fs_h_jt_definition_jordanlistedequalright. fs_h_jt_definition_jordanlistedequalright + S (jt_right_definition_jordanlistedequal) = S ((S (jt_index_definition_jordanlistedequal)) * jt_scale_definition_jordanlisted)) /\ exists fs_q_jt_definition_jordanlistedequalright. jt_code_definition_jordanlisted = fs_q_jt_definition_jordanlistedequalright * S ((S (jt_index_definition_jordanlistedequal)) * jt_scale_definition_jordanlisted) + (jt_right_definition_jordanlistedequal))) -> jt_left_definition_jordanlistedequal=jt_right_definition_jordanlistedequal)))))))))

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