jordan_totient_count_unique

Exact expanded first-order arithmetic statement

forall k n u v. (((~((k)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_unique_jordan_left jt_code_scale_unique_jordan_left jt_scales_unique_jordan_left jt_scale_scale_unique_jordan_left. ((forall jt_i_unique_jordan_leftenum. (exists jt_gap_unique_jordan_leftenumsoundindex. jt_gap_unique_jordan_leftenumsoundindex+S (jt_i_unique_jordan_leftenum)=(u)) -> exists jt_b_unique_jordan_leftenum jt_c_unique_jordan_leftenum. ((((((exists fs_h_jt_unique_jordan_leftenumsoundcode. fs_h_jt_unique_jordan_leftenumsoundcode + S (jt_b_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumsoundcode. jt_codes_unique_jordan_left = fs_q_jt_unique_jordan_leftenumsoundcode * S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left) + (jt_b_unique_jordan_leftenum))) /\ (((exists fs_h_jt_unique_jordan_leftenumsoundscale. fs_h_jt_unique_jordan_leftenumsoundscale + S (jt_c_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumsoundscale. jt_scales_unique_jordan_left = fs_q_jt_unique_jordan_leftenumsoundscale * S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left) + (jt_c_unique_jordan_leftenum))))) /\ (((forall jt_index_unique_jordan_leftenumbound. (exists jt_gap_unique_jordan_leftenumboundindex. jt_gap_unique_jordan_leftenumboundindex+S (jt_index_unique_jordan_leftenumbound)=(k)) -> exists jt_value_unique_jordan_leftenumbound. ((((exists fs_h_jt_unique_jordan_leftenumboundat. fs_h_jt_unique_jordan_leftenumboundat + S (jt_value_unique_jordan_leftenumbound) = S ((S (jt_index_unique_jordan_leftenumbound)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumboundat. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumboundat * S ((S (jt_index_unique_jordan_leftenumbound)) * jt_c_unique_jordan_leftenum) + (jt_value_unique_jordan_leftenumbound))) /\ (exists jt_gap_unique_jordan_leftenumboundvalue. jt_gap_unique_jordan_leftenumboundvalue+S (jt_value_unique_jordan_leftenumbound)=(n)))) /\ (forall jt_divisor_unique_jordan_leftenumprimitive. (exists jt_factor_unique_jordan_leftenumprimitivemodulus. (n)=(jt_divisor_unique_jordan_leftenumprimitive)*jt_factor_unique_jordan_leftenumprimitivemodulus) -> (forall jt_index_unique_jordan_leftenumprimitivecoordinates jt_value_unique_jordan_leftenumprimitivecoordinates. (exists jt_gap_unique_jordan_leftenumprimitivecoordinatesindex. jt_gap_unique_jordan_leftenumprimitivecoordinatesindex+S (jt_index_unique_jordan_leftenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unique_jordan_leftenumprimitivecoordinatesat. fs_h_jt_unique_jordan_leftenumprimitivecoordinatesat + S (jt_value_unique_jordan_leftenumprimitivecoordinates) = S ((S (jt_index_unique_jordan_leftenumprimitivecoordinates)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumprimitivecoordinatesat. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumprimitivecoordinatesat * S ((S (jt_index_unique_jordan_leftenumprimitivecoordinates)) * jt_c_unique_jordan_leftenum) + (jt_value_unique_jordan_leftenumprimitivecoordinates))) -> (exists jt_factor_unique_jordan_leftenumprimitivecoordinatesdivides. (jt_value_unique_jordan_leftenumprimitivecoordinates)=(jt_divisor_unique_jordan_leftenumprimitive)*jt_factor_unique_jordan_leftenumprimitivecoordinatesdivides)) -> jt_divisor_unique_jordan_leftenumprimitive=1))))) /\ (((forall jt_b_unique_jordan_leftenum jt_c_unique_jordan_leftenum. (forall jt_index_unique_jordan_leftenuminputbound. (exists jt_gap_unique_jordan_leftenuminputboundindex. jt_gap_unique_jordan_leftenuminputboundindex+S (jt_index_unique_jordan_leftenuminputbound)=(k)) -> exists jt_value_unique_jordan_leftenuminputbound. ((((exists fs_h_jt_unique_jordan_leftenuminputboundat. fs_h_jt_unique_jordan_leftenuminputboundat + S (jt_value_unique_jordan_leftenuminputbound) = S ((S (jt_index_unique_jordan_leftenuminputbound)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenuminputboundat. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenuminputboundat * S ((S (jt_index_unique_jordan_leftenuminputbound)) * jt_c_unique_jordan_leftenum) + (jt_value_unique_jordan_leftenuminputbound))) /\ (exists jt_gap_unique_jordan_leftenuminputboundvalue. jt_gap_unique_jordan_leftenuminputboundvalue+S (jt_value_unique_jordan_leftenuminputbound)=(n)))) -> (forall jt_divisor_unique_jordan_leftenuminputprimitive. (exists jt_factor_unique_jordan_leftenuminputprimitivemodulus. (n)=(jt_divisor_unique_jordan_leftenuminputprimitive)*jt_factor_unique_jordan_leftenuminputprimitivemodulus) -> (forall jt_index_unique_jordan_leftenuminputprimitivecoordinates jt_value_unique_jordan_leftenuminputprimitivecoordinates. (exists jt_gap_unique_jordan_leftenuminputprimitivecoordinatesindex. jt_gap_unique_jordan_leftenuminputprimitivecoordinatesindex+S (jt_index_unique_jordan_leftenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unique_jordan_leftenuminputprimitivecoordinatesat. fs_h_jt_unique_jordan_leftenuminputprimitivecoordinatesat + S (jt_value_unique_jordan_leftenuminputprimitivecoordinates) = S ((S (jt_index_unique_jordan_leftenuminputprimitivecoordinates)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenuminputprimitivecoordinatesat. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenuminputprimitivecoordinatesat * S ((S (jt_index_unique_jordan_leftenuminputprimitivecoordinates)) * jt_c_unique_jordan_leftenum) + (jt_value_unique_jordan_leftenuminputprimitivecoordinates))) -> (exists jt_factor_unique_jordan_leftenuminputprimitivecoordinatesdivides. (jt_value_unique_jordan_leftenuminputprimitivecoordinates)=(jt_divisor_unique_jordan_leftenuminputprimitive)*jt_factor_unique_jordan_leftenuminputprimitivecoordinatesdivides)) -> jt_divisor_unique_jordan_leftenuminputprimitive=1) -> exists jt_i_unique_jordan_leftenum jt_d_unique_jordan_leftenum jt_e_unique_jordan_leftenum. ((exists jt_gap_unique_jordan_leftenumcompleteindex. jt_gap_unique_jordan_leftenumcompleteindex+S (jt_i_unique_jordan_leftenum)=(u)) /\ (((((((exists fs_h_jt_unique_jordan_leftenumcompletecode. fs_h_jt_unique_jordan_leftenumcompletecode + S (jt_d_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumcompletecode. jt_codes_unique_jordan_left = fs_q_jt_unique_jordan_leftenumcompletecode * S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left) + (jt_d_unique_jordan_leftenum))) /\ (((exists fs_h_jt_unique_jordan_leftenumcompletescale. fs_h_jt_unique_jordan_leftenumcompletescale + S (jt_e_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumcompletescale. jt_scales_unique_jordan_left = fs_q_jt_unique_jordan_leftenumcompletescale * S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left) + (jt_e_unique_jordan_leftenum))))) /\ (forall jt_index_unique_jordan_leftenumrepresented jt_left_unique_jordan_leftenumrepresented jt_right_unique_jordan_leftenumrepresented. (exists jt_gap_unique_jordan_leftenumrepresentedindex. jt_gap_unique_jordan_leftenumrepresentedindex+S (jt_index_unique_jordan_leftenumrepresented)=(k)) -> (((exists fs_h_jt_unique_jordan_leftenumrepresentedleft. fs_h_jt_unique_jordan_leftenumrepresentedleft + S (jt_left_unique_jordan_leftenumrepresented) = S ((S (jt_index_unique_jordan_leftenumrepresented)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumrepresentedleft. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumrepresentedleft * S ((S (jt_index_unique_jordan_leftenumrepresented)) * jt_c_unique_jordan_leftenum) + (jt_left_unique_jordan_leftenumrepresented))) -> (((exists fs_h_jt_unique_jordan_leftenumrepresentedright. fs_h_jt_unique_jordan_leftenumrepresentedright + S (jt_right_unique_jordan_leftenumrepresented) = S ((S (jt_index_unique_jordan_leftenumrepresented)) * jt_e_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumrepresentedright. jt_d_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumrepresentedright * S ((S (jt_index_unique_jordan_leftenumrepresented)) * jt_e_unique_jordan_leftenum) + (jt_right_unique_jordan_leftenumrepresented))) -> jt_left_unique_jordan_leftenumrepresented=jt_right_unique_jordan_leftenumrepresented))))) /\ (forall jt_i_unique_jordan_leftenum jt_h_unique_jordan_leftenum jt_b_unique_jordan_leftenum jt_c_unique_jordan_leftenum jt_d_unique_jordan_leftenum jt_e_unique_jordan_leftenum. (exists jt_gap_unique_jordan_leftenumfirstindex. jt_gap_unique_jordan_leftenumfirstindex+S (jt_i_unique_jordan_leftenum)=(u)) -> (exists jt_gap_unique_jordan_leftenumsecondindex. jt_gap_unique_jordan_leftenumsecondindex+S (jt_h_unique_jordan_leftenum)=(u)) -> (((((exists fs_h_jt_unique_jordan_leftenumfirstcode. fs_h_jt_unique_jordan_leftenumfirstcode + S (jt_b_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumfirstcode. jt_codes_unique_jordan_left = fs_q_jt_unique_jordan_leftenumfirstcode * S ((S (jt_i_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left) + (jt_b_unique_jordan_leftenum))) /\ (((exists fs_h_jt_unique_jordan_leftenumfirstscale. fs_h_jt_unique_jordan_leftenumfirstscale + S (jt_c_unique_jordan_leftenum) = S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumfirstscale. jt_scales_unique_jordan_left = fs_q_jt_unique_jordan_leftenumfirstscale * S ((S (jt_i_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left) + (jt_c_unique_jordan_leftenum))))) -> (((((exists fs_h_jt_unique_jordan_leftenumsecondcode. fs_h_jt_unique_jordan_leftenumsecondcode + S (jt_d_unique_jordan_leftenum) = S ((S (jt_h_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumsecondcode. jt_codes_unique_jordan_left = fs_q_jt_unique_jordan_leftenumsecondcode * S ((S (jt_h_unique_jordan_leftenum)) * jt_code_scale_unique_jordan_left) + (jt_d_unique_jordan_leftenum))) /\ (((exists fs_h_jt_unique_jordan_leftenumsecondscale. fs_h_jt_unique_jordan_leftenumsecondscale + S (jt_e_unique_jordan_leftenum) = S ((S (jt_h_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left)) /\ exists fs_q_jt_unique_jordan_leftenumsecondscale. jt_scales_unique_jordan_left = fs_q_jt_unique_jordan_leftenumsecondscale * S ((S (jt_h_unique_jordan_leftenum)) * jt_scale_scale_unique_jordan_left) + (jt_e_unique_jordan_leftenum))))) -> (forall jt_index_unique_jordan_leftenumsame jt_left_unique_jordan_leftenumsame jt_right_unique_jordan_leftenumsame. (exists jt_gap_unique_jordan_leftenumsameindex. jt_gap_unique_jordan_leftenumsameindex+S (jt_index_unique_jordan_leftenumsame)=(k)) -> (((exists fs_h_jt_unique_jordan_leftenumsameleft. fs_h_jt_unique_jordan_leftenumsameleft + S (jt_left_unique_jordan_leftenumsame) = S ((S (jt_index_unique_jordan_leftenumsame)) * jt_c_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumsameleft. jt_b_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumsameleft * S ((S (jt_index_unique_jordan_leftenumsame)) * jt_c_unique_jordan_leftenum) + (jt_left_unique_jordan_leftenumsame))) -> (((exists fs_h_jt_unique_jordan_leftenumsameright. fs_h_jt_unique_jordan_leftenumsameright + S (jt_right_unique_jordan_leftenumsame) = S ((S (jt_index_unique_jordan_leftenumsame)) * jt_e_unique_jordan_leftenum)) /\ exists fs_q_jt_unique_jordan_leftenumsameright. jt_d_unique_jordan_leftenum = fs_q_jt_unique_jordan_leftenumsameright * S ((S (jt_index_unique_jordan_leftenumsame)) * jt_e_unique_jordan_leftenum) + (jt_right_unique_jordan_leftenumsame))) -> jt_left_unique_jordan_leftenumsame=jt_right_unique_jordan_leftenumsame) -> jt_i_unique_jordan_leftenum=jt_h_unique_jordan_leftenum))))))))) -> (((~((k)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_unique_jordan_right jt_code_scale_unique_jordan_right jt_scales_unique_jordan_right jt_scale_scale_unique_jordan_right. ((forall jt_i_unique_jordan_rightenum. (exists jt_gap_unique_jordan_rightenumsoundindex. jt_gap_unique_jordan_rightenumsoundindex+S (jt_i_unique_jordan_rightenum)=(v)) -> exists jt_b_unique_jordan_rightenum jt_c_unique_jordan_rightenum. ((((((exists fs_h_jt_unique_jordan_rightenumsoundcode. fs_h_jt_unique_jordan_rightenumsoundcode + S (jt_b_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumsoundcode. jt_codes_unique_jordan_right = fs_q_jt_unique_jordan_rightenumsoundcode * S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right) + (jt_b_unique_jordan_rightenum))) /\ (((exists fs_h_jt_unique_jordan_rightenumsoundscale. fs_h_jt_unique_jordan_rightenumsoundscale + S (jt_c_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumsoundscale. jt_scales_unique_jordan_right = fs_q_jt_unique_jordan_rightenumsoundscale * S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right) + (jt_c_unique_jordan_rightenum))))) /\ (((forall jt_index_unique_jordan_rightenumbound. (exists jt_gap_unique_jordan_rightenumboundindex. jt_gap_unique_jordan_rightenumboundindex+S (jt_index_unique_jordan_rightenumbound)=(k)) -> exists jt_value_unique_jordan_rightenumbound. ((((exists fs_h_jt_unique_jordan_rightenumboundat. fs_h_jt_unique_jordan_rightenumboundat + S (jt_value_unique_jordan_rightenumbound) = S ((S (jt_index_unique_jordan_rightenumbound)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumboundat. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumboundat * S ((S (jt_index_unique_jordan_rightenumbound)) * jt_c_unique_jordan_rightenum) + (jt_value_unique_jordan_rightenumbound))) /\ (exists jt_gap_unique_jordan_rightenumboundvalue. jt_gap_unique_jordan_rightenumboundvalue+S (jt_value_unique_jordan_rightenumbound)=(n)))) /\ (forall jt_divisor_unique_jordan_rightenumprimitive. (exists jt_factor_unique_jordan_rightenumprimitivemodulus. (n)=(jt_divisor_unique_jordan_rightenumprimitive)*jt_factor_unique_jordan_rightenumprimitivemodulus) -> (forall jt_index_unique_jordan_rightenumprimitivecoordinates jt_value_unique_jordan_rightenumprimitivecoordinates. (exists jt_gap_unique_jordan_rightenumprimitivecoordinatesindex. jt_gap_unique_jordan_rightenumprimitivecoordinatesindex+S (jt_index_unique_jordan_rightenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unique_jordan_rightenumprimitivecoordinatesat. fs_h_jt_unique_jordan_rightenumprimitivecoordinatesat + S (jt_value_unique_jordan_rightenumprimitivecoordinates) = S ((S (jt_index_unique_jordan_rightenumprimitivecoordinates)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumprimitivecoordinatesat. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumprimitivecoordinatesat * S ((S (jt_index_unique_jordan_rightenumprimitivecoordinates)) * jt_c_unique_jordan_rightenum) + (jt_value_unique_jordan_rightenumprimitivecoordinates))) -> (exists jt_factor_unique_jordan_rightenumprimitivecoordinatesdivides. (jt_value_unique_jordan_rightenumprimitivecoordinates)=(jt_divisor_unique_jordan_rightenumprimitive)*jt_factor_unique_jordan_rightenumprimitivecoordinatesdivides)) -> jt_divisor_unique_jordan_rightenumprimitive=1))))) /\ (((forall jt_b_unique_jordan_rightenum jt_c_unique_jordan_rightenum. (forall jt_index_unique_jordan_rightenuminputbound. (exists jt_gap_unique_jordan_rightenuminputboundindex. jt_gap_unique_jordan_rightenuminputboundindex+S (jt_index_unique_jordan_rightenuminputbound)=(k)) -> exists jt_value_unique_jordan_rightenuminputbound. ((((exists fs_h_jt_unique_jordan_rightenuminputboundat. fs_h_jt_unique_jordan_rightenuminputboundat + S (jt_value_unique_jordan_rightenuminputbound) = S ((S (jt_index_unique_jordan_rightenuminputbound)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenuminputboundat. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenuminputboundat * S ((S (jt_index_unique_jordan_rightenuminputbound)) * jt_c_unique_jordan_rightenum) + (jt_value_unique_jordan_rightenuminputbound))) /\ (exists jt_gap_unique_jordan_rightenuminputboundvalue. jt_gap_unique_jordan_rightenuminputboundvalue+S (jt_value_unique_jordan_rightenuminputbound)=(n)))) -> (forall jt_divisor_unique_jordan_rightenuminputprimitive. (exists jt_factor_unique_jordan_rightenuminputprimitivemodulus. (n)=(jt_divisor_unique_jordan_rightenuminputprimitive)*jt_factor_unique_jordan_rightenuminputprimitivemodulus) -> (forall jt_index_unique_jordan_rightenuminputprimitivecoordinates jt_value_unique_jordan_rightenuminputprimitivecoordinates. (exists jt_gap_unique_jordan_rightenuminputprimitivecoordinatesindex. jt_gap_unique_jordan_rightenuminputprimitivecoordinatesindex+S (jt_index_unique_jordan_rightenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unique_jordan_rightenuminputprimitivecoordinatesat. fs_h_jt_unique_jordan_rightenuminputprimitivecoordinatesat + S (jt_value_unique_jordan_rightenuminputprimitivecoordinates) = S ((S (jt_index_unique_jordan_rightenuminputprimitivecoordinates)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenuminputprimitivecoordinatesat. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenuminputprimitivecoordinatesat * S ((S (jt_index_unique_jordan_rightenuminputprimitivecoordinates)) * jt_c_unique_jordan_rightenum) + (jt_value_unique_jordan_rightenuminputprimitivecoordinates))) -> (exists jt_factor_unique_jordan_rightenuminputprimitivecoordinatesdivides. (jt_value_unique_jordan_rightenuminputprimitivecoordinates)=(jt_divisor_unique_jordan_rightenuminputprimitive)*jt_factor_unique_jordan_rightenuminputprimitivecoordinatesdivides)) -> jt_divisor_unique_jordan_rightenuminputprimitive=1) -> exists jt_i_unique_jordan_rightenum jt_d_unique_jordan_rightenum jt_e_unique_jordan_rightenum. ((exists jt_gap_unique_jordan_rightenumcompleteindex. jt_gap_unique_jordan_rightenumcompleteindex+S (jt_i_unique_jordan_rightenum)=(v)) /\ (((((((exists fs_h_jt_unique_jordan_rightenumcompletecode. fs_h_jt_unique_jordan_rightenumcompletecode + S (jt_d_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumcompletecode. jt_codes_unique_jordan_right = fs_q_jt_unique_jordan_rightenumcompletecode * S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right) + (jt_d_unique_jordan_rightenum))) /\ (((exists fs_h_jt_unique_jordan_rightenumcompletescale. fs_h_jt_unique_jordan_rightenumcompletescale + S (jt_e_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumcompletescale. jt_scales_unique_jordan_right = fs_q_jt_unique_jordan_rightenumcompletescale * S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right) + (jt_e_unique_jordan_rightenum))))) /\ (forall jt_index_unique_jordan_rightenumrepresented jt_left_unique_jordan_rightenumrepresented jt_right_unique_jordan_rightenumrepresented. (exists jt_gap_unique_jordan_rightenumrepresentedindex. jt_gap_unique_jordan_rightenumrepresentedindex+S (jt_index_unique_jordan_rightenumrepresented)=(k)) -> (((exists fs_h_jt_unique_jordan_rightenumrepresentedleft. fs_h_jt_unique_jordan_rightenumrepresentedleft + S (jt_left_unique_jordan_rightenumrepresented) = S ((S (jt_index_unique_jordan_rightenumrepresented)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumrepresentedleft. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumrepresentedleft * S ((S (jt_index_unique_jordan_rightenumrepresented)) * jt_c_unique_jordan_rightenum) + (jt_left_unique_jordan_rightenumrepresented))) -> (((exists fs_h_jt_unique_jordan_rightenumrepresentedright. fs_h_jt_unique_jordan_rightenumrepresentedright + S (jt_right_unique_jordan_rightenumrepresented) = S ((S (jt_index_unique_jordan_rightenumrepresented)) * jt_e_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumrepresentedright. jt_d_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumrepresentedright * S ((S (jt_index_unique_jordan_rightenumrepresented)) * jt_e_unique_jordan_rightenum) + (jt_right_unique_jordan_rightenumrepresented))) -> jt_left_unique_jordan_rightenumrepresented=jt_right_unique_jordan_rightenumrepresented))))) /\ (forall jt_i_unique_jordan_rightenum jt_h_unique_jordan_rightenum jt_b_unique_jordan_rightenum jt_c_unique_jordan_rightenum jt_d_unique_jordan_rightenum jt_e_unique_jordan_rightenum. (exists jt_gap_unique_jordan_rightenumfirstindex. jt_gap_unique_jordan_rightenumfirstindex+S (jt_i_unique_jordan_rightenum)=(v)) -> (exists jt_gap_unique_jordan_rightenumsecondindex. jt_gap_unique_jordan_rightenumsecondindex+S (jt_h_unique_jordan_rightenum)=(v)) -> (((((exists fs_h_jt_unique_jordan_rightenumfirstcode. fs_h_jt_unique_jordan_rightenumfirstcode + S (jt_b_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumfirstcode. jt_codes_unique_jordan_right = fs_q_jt_unique_jordan_rightenumfirstcode * S ((S (jt_i_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right) + (jt_b_unique_jordan_rightenum))) /\ (((exists fs_h_jt_unique_jordan_rightenumfirstscale. fs_h_jt_unique_jordan_rightenumfirstscale + S (jt_c_unique_jordan_rightenum) = S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumfirstscale. jt_scales_unique_jordan_right = fs_q_jt_unique_jordan_rightenumfirstscale * S ((S (jt_i_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right) + (jt_c_unique_jordan_rightenum))))) -> (((((exists fs_h_jt_unique_jordan_rightenumsecondcode. fs_h_jt_unique_jordan_rightenumsecondcode + S (jt_d_unique_jordan_rightenum) = S ((S (jt_h_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumsecondcode. jt_codes_unique_jordan_right = fs_q_jt_unique_jordan_rightenumsecondcode * S ((S (jt_h_unique_jordan_rightenum)) * jt_code_scale_unique_jordan_right) + (jt_d_unique_jordan_rightenum))) /\ (((exists fs_h_jt_unique_jordan_rightenumsecondscale. fs_h_jt_unique_jordan_rightenumsecondscale + S (jt_e_unique_jordan_rightenum) = S ((S (jt_h_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right)) /\ exists fs_q_jt_unique_jordan_rightenumsecondscale. jt_scales_unique_jordan_right = fs_q_jt_unique_jordan_rightenumsecondscale * S ((S (jt_h_unique_jordan_rightenum)) * jt_scale_scale_unique_jordan_right) + (jt_e_unique_jordan_rightenum))))) -> (forall jt_index_unique_jordan_rightenumsame jt_left_unique_jordan_rightenumsame jt_right_unique_jordan_rightenumsame. (exists jt_gap_unique_jordan_rightenumsameindex. jt_gap_unique_jordan_rightenumsameindex+S (jt_index_unique_jordan_rightenumsame)=(k)) -> (((exists fs_h_jt_unique_jordan_rightenumsameleft. fs_h_jt_unique_jordan_rightenumsameleft + S (jt_left_unique_jordan_rightenumsame) = S ((S (jt_index_unique_jordan_rightenumsame)) * jt_c_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumsameleft. jt_b_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumsameleft * S ((S (jt_index_unique_jordan_rightenumsame)) * jt_c_unique_jordan_rightenum) + (jt_left_unique_jordan_rightenumsame))) -> (((exists fs_h_jt_unique_jordan_rightenumsameright. fs_h_jt_unique_jordan_rightenumsameright + S (jt_right_unique_jordan_rightenumsame) = S ((S (jt_index_unique_jordan_rightenumsame)) * jt_e_unique_jordan_rightenum)) /\ exists fs_q_jt_unique_jordan_rightenumsameright. jt_d_unique_jordan_rightenum = fs_q_jt_unique_jordan_rightenumsameright * S ((S (jt_index_unique_jordan_rightenumsame)) * jt_e_unique_jordan_rightenum) + (jt_right_unique_jordan_rightenumsame))) -> jt_left_unique_jordan_rightenumsame=jt_right_unique_jordan_rightenumsame) -> jt_i_unique_jordan_rightenum=jt_h_unique_jordan_rightenum))))))))) -> (u=v)