JordanTotient(k,n,j)

((~((k)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_definition_jordan jt_code_scale_definition_jordan jt_scales_definition_jordan jt_scale_scale_definition_jordan. ((forall jt_i_definition_jordanenum. (exists jt_gap_definition_jordanenumsoundindex. jt_gap_definition_jordanenumsoundindex+S (jt_i_definition_jordanenum)=(j)) -> exists jt_b_definition_jordanenum jt_c_definition_jordanenum. ((((((exists fs_h_jt_definition_jordanenumsoundcode. fs_h_jt_definition_jordanenumsoundcode + S (jt_b_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumsoundcode. jt_codes_definition_jordan = fs_q_jt_definition_jordanenumsoundcode * S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan) + (jt_b_definition_jordanenum))) /\ (((exists fs_h_jt_definition_jordanenumsoundscale. fs_h_jt_definition_jordanenumsoundscale + S (jt_c_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumsoundscale. jt_scales_definition_jordan = fs_q_jt_definition_jordanenumsoundscale * S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan) + (jt_c_definition_jordanenum))))) /\ (((forall jt_index_definition_jordanenumbound. (exists jt_gap_definition_jordanenumboundindex. jt_gap_definition_jordanenumboundindex+S (jt_index_definition_jordanenumbound)=(k)) -> exists jt_value_definition_jordanenumbound. ((((exists fs_h_jt_definition_jordanenumboundat. fs_h_jt_definition_jordanenumboundat + S (jt_value_definition_jordanenumbound) = S ((S (jt_index_definition_jordanenumbound)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumboundat. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenumboundat * S ((S (jt_index_definition_jordanenumbound)) * jt_c_definition_jordanenum) + (jt_value_definition_jordanenumbound))) /\ (exists jt_gap_definition_jordanenumboundvalue. jt_gap_definition_jordanenumboundvalue+S (jt_value_definition_jordanenumbound)=(n)))) /\ (forall jt_divisor_definition_jordanenumprimitive. (exists jt_factor_definition_jordanenumprimitivemodulus. (n)=(jt_divisor_definition_jordanenumprimitive)*jt_factor_definition_jordanenumprimitivemodulus) -> (forall jt_index_definition_jordanenumprimitivecoordinates jt_value_definition_jordanenumprimitivecoordinates. (exists jt_gap_definition_jordanenumprimitivecoordinatesindex. jt_gap_definition_jordanenumprimitivecoordinatesindex+S (jt_index_definition_jordanenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_definition_jordanenumprimitivecoordinatesat. fs_h_jt_definition_jordanenumprimitivecoordinatesat + S (jt_value_definition_jordanenumprimitivecoordinates) = S ((S (jt_index_definition_jordanenumprimitivecoordinates)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumprimitivecoordinatesat. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenumprimitivecoordinatesat * S ((S (jt_index_definition_jordanenumprimitivecoordinates)) * jt_c_definition_jordanenum) + (jt_value_definition_jordanenumprimitivecoordinates))) -> (exists jt_factor_definition_jordanenumprimitivecoordinatesdivides. (jt_value_definition_jordanenumprimitivecoordinates)=(jt_divisor_definition_jordanenumprimitive)*jt_factor_definition_jordanenumprimitivecoordinatesdivides)) -> jt_divisor_definition_jordanenumprimitive=1))))) /\ (((forall jt_b_definition_jordanenum jt_c_definition_jordanenum. (forall jt_index_definition_jordanenuminputbound. (exists jt_gap_definition_jordanenuminputboundindex. jt_gap_definition_jordanenuminputboundindex+S (jt_index_definition_jordanenuminputbound)=(k)) -> exists jt_value_definition_jordanenuminputbound. ((((exists fs_h_jt_definition_jordanenuminputboundat. fs_h_jt_definition_jordanenuminputboundat + S (jt_value_definition_jordanenuminputbound) = S ((S (jt_index_definition_jordanenuminputbound)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenuminputboundat. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenuminputboundat * S ((S (jt_index_definition_jordanenuminputbound)) * jt_c_definition_jordanenum) + (jt_value_definition_jordanenuminputbound))) /\ (exists jt_gap_definition_jordanenuminputboundvalue. jt_gap_definition_jordanenuminputboundvalue+S (jt_value_definition_jordanenuminputbound)=(n)))) -> (forall jt_divisor_definition_jordanenuminputprimitive. (exists jt_factor_definition_jordanenuminputprimitivemodulus. (n)=(jt_divisor_definition_jordanenuminputprimitive)*jt_factor_definition_jordanenuminputprimitivemodulus) -> (forall jt_index_definition_jordanenuminputprimitivecoordinates jt_value_definition_jordanenuminputprimitivecoordinates. (exists jt_gap_definition_jordanenuminputprimitivecoordinatesindex. jt_gap_definition_jordanenuminputprimitivecoordinatesindex+S (jt_index_definition_jordanenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_definition_jordanenuminputprimitivecoordinatesat. fs_h_jt_definition_jordanenuminputprimitivecoordinatesat + S (jt_value_definition_jordanenuminputprimitivecoordinates) = S ((S (jt_index_definition_jordanenuminputprimitivecoordinates)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenuminputprimitivecoordinatesat. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenuminputprimitivecoordinatesat * S ((S (jt_index_definition_jordanenuminputprimitivecoordinates)) * jt_c_definition_jordanenum) + (jt_value_definition_jordanenuminputprimitivecoordinates))) -> (exists jt_factor_definition_jordanenuminputprimitivecoordinatesdivides. (jt_value_definition_jordanenuminputprimitivecoordinates)=(jt_divisor_definition_jordanenuminputprimitive)*jt_factor_definition_jordanenuminputprimitivecoordinatesdivides)) -> jt_divisor_definition_jordanenuminputprimitive=1) -> exists jt_i_definition_jordanenum jt_d_definition_jordanenum jt_e_definition_jordanenum. ((exists jt_gap_definition_jordanenumcompleteindex. jt_gap_definition_jordanenumcompleteindex+S (jt_i_definition_jordanenum)=(j)) /\ (((((((exists fs_h_jt_definition_jordanenumcompletecode. fs_h_jt_definition_jordanenumcompletecode + S (jt_d_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumcompletecode. jt_codes_definition_jordan = fs_q_jt_definition_jordanenumcompletecode * S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan) + (jt_d_definition_jordanenum))) /\ (((exists fs_h_jt_definition_jordanenumcompletescale. fs_h_jt_definition_jordanenumcompletescale + S (jt_e_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumcompletescale. jt_scales_definition_jordan = fs_q_jt_definition_jordanenumcompletescale * S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan) + (jt_e_definition_jordanenum))))) /\ (forall jt_index_definition_jordanenumrepresented jt_left_definition_jordanenumrepresented jt_right_definition_jordanenumrepresented. (exists jt_gap_definition_jordanenumrepresentedindex. jt_gap_definition_jordanenumrepresentedindex+S (jt_index_definition_jordanenumrepresented)=(k)) -> (((exists fs_h_jt_definition_jordanenumrepresentedleft. fs_h_jt_definition_jordanenumrepresentedleft + S (jt_left_definition_jordanenumrepresented) = S ((S (jt_index_definition_jordanenumrepresented)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumrepresentedleft. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenumrepresentedleft * S ((S (jt_index_definition_jordanenumrepresented)) * jt_c_definition_jordanenum) + (jt_left_definition_jordanenumrepresented))) -> (((exists fs_h_jt_definition_jordanenumrepresentedright. fs_h_jt_definition_jordanenumrepresentedright + S (jt_right_definition_jordanenumrepresented) = S ((S (jt_index_definition_jordanenumrepresented)) * jt_e_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumrepresentedright. jt_d_definition_jordanenum = fs_q_jt_definition_jordanenumrepresentedright * S ((S (jt_index_definition_jordanenumrepresented)) * jt_e_definition_jordanenum) + (jt_right_definition_jordanenumrepresented))) -> jt_left_definition_jordanenumrepresented=jt_right_definition_jordanenumrepresented))))) /\ (forall jt_i_definition_jordanenum jt_h_definition_jordanenum jt_b_definition_jordanenum jt_c_definition_jordanenum jt_d_definition_jordanenum jt_e_definition_jordanenum. (exists jt_gap_definition_jordanenumfirstindex. jt_gap_definition_jordanenumfirstindex+S (jt_i_definition_jordanenum)=(j)) -> (exists jt_gap_definition_jordanenumsecondindex. jt_gap_definition_jordanenumsecondindex+S (jt_h_definition_jordanenum)=(j)) -> (((((exists fs_h_jt_definition_jordanenumfirstcode. fs_h_jt_definition_jordanenumfirstcode + S (jt_b_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumfirstcode. jt_codes_definition_jordan = fs_q_jt_definition_jordanenumfirstcode * S ((S (jt_i_definition_jordanenum)) * jt_code_scale_definition_jordan) + (jt_b_definition_jordanenum))) /\ (((exists fs_h_jt_definition_jordanenumfirstscale. fs_h_jt_definition_jordanenumfirstscale + S (jt_c_definition_jordanenum) = S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumfirstscale. jt_scales_definition_jordan = fs_q_jt_definition_jordanenumfirstscale * S ((S (jt_i_definition_jordanenum)) * jt_scale_scale_definition_jordan) + (jt_c_definition_jordanenum))))) -> (((((exists fs_h_jt_definition_jordanenumsecondcode. fs_h_jt_definition_jordanenumsecondcode + S (jt_d_definition_jordanenum) = S ((S (jt_h_definition_jordanenum)) * jt_code_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumsecondcode. jt_codes_definition_jordan = fs_q_jt_definition_jordanenumsecondcode * S ((S (jt_h_definition_jordanenum)) * jt_code_scale_definition_jordan) + (jt_d_definition_jordanenum))) /\ (((exists fs_h_jt_definition_jordanenumsecondscale. fs_h_jt_definition_jordanenumsecondscale + S (jt_e_definition_jordanenum) = S ((S (jt_h_definition_jordanenum)) * jt_scale_scale_definition_jordan)) /\ exists fs_q_jt_definition_jordanenumsecondscale. jt_scales_definition_jordan = fs_q_jt_definition_jordanenumsecondscale * S ((S (jt_h_definition_jordanenum)) * jt_scale_scale_definition_jordan) + (jt_e_definition_jordanenum))))) -> (forall jt_index_definition_jordanenumsame jt_left_definition_jordanenumsame jt_right_definition_jordanenumsame. (exists jt_gap_definition_jordanenumsameindex. jt_gap_definition_jordanenumsameindex+S (jt_index_definition_jordanenumsame)=(k)) -> (((exists fs_h_jt_definition_jordanenumsameleft. fs_h_jt_definition_jordanenumsameleft + S (jt_left_definition_jordanenumsame) = S ((S (jt_index_definition_jordanenumsame)) * jt_c_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumsameleft. jt_b_definition_jordanenum = fs_q_jt_definition_jordanenumsameleft * S ((S (jt_index_definition_jordanenumsame)) * jt_c_definition_jordanenum) + (jt_left_definition_jordanenumsame))) -> (((exists fs_h_jt_definition_jordanenumsameright. fs_h_jt_definition_jordanenumsameright + S (jt_right_definition_jordanenumsame) = S ((S (jt_index_definition_jordanenumsame)) * jt_e_definition_jordanenum)) /\ exists fs_q_jt_definition_jordanenumsameright. jt_d_definition_jordanenum = fs_q_jt_definition_jordanenumsameright * S ((S (jt_index_definition_jordanenumsame)) * jt_e_definition_jordanenum) + (jt_right_definition_jordanenumsame))) -> jt_left_definition_jordanenumsame=jt_right_definition_jordanenumsame) -> jt_i_definition_jordanenum=jt_h_definition_jordanenum))))))))

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